From c0abb388137e62a3c00f044fd3d1eb4daa230d5a Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 29 Jun 2026 14:35:18 -0500 Subject: [PATCH] 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 | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index 9c611014..90e0d67b 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/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