# Harness: Lean Formalism

## Context
This harness defines the constraints for all Lean-based formalization within the SilverSight/BioSight project. Use these rules to minimize LLM drift during proof construction.

## Core Quirks & Constraints
1. **Fixed-Point Arithmetic:** 
   - NEVER use `Float` in core compute paths.
   - Always use `Q16_16` (mixed) or `Q0_16` (pure fraction).
   - Exception: External boundary inputs/outputs (JSON parsing, sensor data).

2. **The Closure Constraint (Rule 7):**
   - Every formal claim must be "closed" under the operation defined by its DNA Signature.
   - If a theorem is incomplete, it's not just a `sorry`; it must have a `TODO(lean-port)` describing why it's open.

3. **DNA Mapping Alignment:**
   - The Lean proof structure must mirror the BioSight $\tau$ (topology) and $\delta$ (depth) values.
   - Example: A high $\delta$ value implies nested definitions or recursive structures in Lean.

4. **Verification Protocol:**
   - Every change requires a `lake build`.
   - No "bare" sorries are allowed unless they represent a specific, identified gap in the logic.
   - Use `#eval` to provide witnesses for every major theorem.

## Reference Anchors
- **Base Type**: `Semantics.FixedPoint.Q16_16`
- **Core Module**: `0-Core-Formalism/lean/Semantics/`