# 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) 1. Explicit scalar Λm and stabilizing range (**G-Lm**). 2. Formal Ξ(t,·) operator laws (**Gap-Ξ**). 3. Tensor / Banach / F_p carrier for X_t (**Gap-Carrier**). 4. Convergence conditions for **nested** form (**Gap-Converge**). 5. In-step contraction algorithm realizing C (**G-C**, **Gap-ContractAlg**). 6. Optimization objective J (**Gap-OptObj**). 7. Construction of T_p from P64 / PrimeMask / PMAT (**G-Tp**). 8. 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 `iterateNested` induction lemmas under explicit measure hypotheses (when Gap-ContractAlg closes).