Remaining Lean work after L1–L6 axioms
What is left after accepting L6 opaque symbols. No fake proof claims.
Deferred / blocked
| Item | Why blocked |
|---|---|
L7 bridge HCALCStep ≃ FoundryStep |
Requires Spec discharge of G-SHAPE / Gap-ShapeMap; additive ≠ nested |
| Unique Banach fixed point (L5 full) | Narrative PROPERTIES 41; needs discharged q < 1-ε + complete metric structure |
| ℝ-valued Λm / spectral radius theorems | No Mathlib in first cut; Nat proxies only |
| Matrix Gershgorin proof of A2 | Needs Jacobian carrier + Mathlib analysis |
| PMAT conservation (A5) in Lean | Optional Foundry surface; not HCALC-core |
| Guardian (A6) in Lean | Prop 55; Core verb may be absent |
Open research (Spec must define before Lean can prove)
- Explicit scalar Λm and stabilizing range (G-Lm).
- Formal Ξ(t,·) operator laws (Gap-Ξ).
- Tensor / Banach / F_p carrier for X_t (Gap-Carrier).
- Convergence conditions for nested form (Gap-Converge).
- In-step contraction algorithm realizing C (G-C, Gap-ContractAlg).
- Optimization objective J (Gap-OptObj).
- Construction of T_p from P64 / PrimeMask / PMAT (G-Tp).
- Shape-map morphism nested ↔ additive (G-SHAPE).
Safe next Lean increments (no invention)
- Port A5/A6 as optional gated modules once Spec marks them in-scope.
- Replace Nat proxies with Mathlib ℝ after Spec freezes types.
- Prove list properties of
P64List(pairwise distinct, true primality) as data lemmas. - Strengthen
iterateNestedinduction lemmas under explicit measure hypotheses (when Gap-ContractAlg closes).