docs(lean): document ncDerived architecture decisions

- Added Negative Control Witness Architecture section
- Documented Float violation awaiting SilverSight migration
- Recorded motivational CRT link status

0-Core-Formalism/lean/Semantics/AGENTS.md

@@ -145,6 +145,26 @@ Only the following roots are blessed for downstream import and receipt emission:
 | `Semantics.TransportQUBOBridge` | Finsler-Randers geodesic → QUBO discretization bridge (2 axioms, 0 sorries) |
 | `Semantics.MultiSurfacePacker` | Delta-Phi-Gamma-K-Lambda multi-surface packing Lagrangian with coherence gate and GCCL swap gate |
 
+## Negative Control Witness Architecture (2026-06-29)
+
+### Design Decisions
+
+1. **Separation of Concerns Achieved**
+   - CSV contains axioms: `ncObserved`, `residualRisk`, `scaleBandDeclared`, `weakAxesNames`
+   - Lean computes derived witness: `ncDerived = residualRisk × scaleBandDeclared`
+   - Theorem `ncDerived_mul` simplifies to definition; `ncDerived_independence_justification`
+     links to CRT product principle (InteractionGraphSidon)
+
+2. **Float Violation (Pending SilverSight Migration)**
+   - Manifold coordinates use `Float` instead of `Q16_16`
+   - Justification: Research Stack is READ-ONLY archive; full Q16_16 migration belongs in SilverSight
+   - Target: Convert JSON decimals to `Q16_16.ofRatio` in SilverSight
+
+3. **Independence Justification Status**
+   - Current: Motivational link to CRT product principle (InteractionGraphSidon.lean:75-76)
+   - Manifold coordinates are Float in [0,1] without explicit modulus structure
+   - Formal proof requires Q16_16 lattice discretization — future SilverSight task
+
 Build the narrow surface with:
 
 ```bash