File size: 3,242 Bytes
d7b24f0 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 | # HCALC Lean 4 formalization (PRODUCTION)
**License:** AGPL-3.0-only (see [`LICENSE`](LICENSE))
**Copyright (C) 2026 HCALC contributors**
Production formalization of the HCALC nested recurrence
\[
X_{t+1} = \Xi\bigl(t,\; \Lambda_m \cdot C(T_p(X_t))\bigr)
\]
frozen to Spec [`../spec/PRODUCTION.md`](../spec/PRODUCTION.md) (overrides provisional L6 axioms in COHERENCE/AXIOMS).
## Provenance
| Part | Source |
|------|--------|
| Carrier, Tp α-diag, C softScale-or-id, Λm min-formula, Ξ=ξy+g, J=residual, L5 Hyp, L7 InstanceBridge | **Spec-file** `PRODUCTION.md` |
| Option B InstanceBridge (not NestedFaithful / not rfl) | **Spec-file** PRODUCTION.md §6 (f5a08da) |
| Mathlib `ℝ` (thin bridge in `RealStub`) | Mathlib4 `v4.34.1` |
| Foundry L1–L4 (P64, Gershgorin, FoundryStep additive, softProject schedules) | Spec + Foundry PROPERTIES (FoundryAdditive **distinct**) |
## Mathlib
- **Toolchain:** `leanprover/lean4:v4.34.1` (matches Mathlib tag `v4.34.1` lean-toolchain — no bump needed).
- **Dependency:** `leanprover-community/mathlib` @ `v4.34.1`.
- **Imports used (minimal):**
1. `Mathlib.Basic.Real.Basic` — `ℝ`, field/order/`abs`/`min`/`max`
2. `Mathlib.Analysis.SpecialFunctions.Log.Basic` — `Real.log` (pulls Exp; Topology transitive only)
- `finMax` uses core `Fin.foldl` only (no Finset / `Mathlib.Data.Fin`)
- No Topology / MeasureTheory / aesop / grind / large simp sets.
- Proofs are freehand `calc` / `rw` / `intro` / `apply` / elementary single-lemma `exact`.
### finMax / ℓ∞
`finMax` = `Fin.foldl` of `max` with init `0` (smallest surface; not `Finset.univ.sup'` / `iSup`).
Production sites pass nonnegative args (`|·|`, Gershgorin disks); `n = 0` yields `0`.
## Layout
| File | Role |
|------|------|
| `Hcalc/RealStub.lean` | Thin Mathlib `ℝ` re-exports + freehand Real lemmas (`finMax`, softScale, guards) |
| `Hcalc/Carrier.lean` | **Gap-Carrier CLOSED**: `Carrier n := Fin n → ℝ`, ℓ∞ |
| `Hcalc/Foundry.lean` | L1–L4 defs; FoundryAdditive `FoundryStep` (≠ nested); Gap-Foundry-* may remain |
| `Hcalc/Axioms.lean` | L6 **defs** Tp/C/Λm/Ξ/J/ContractAlg + **L7** `InstanceBridge` |
| `Hcalc/Pipeline.lean` | Nested `hcalcStep` / `step` / `J` / `optimize` |
| `Hcalc/Convergence.lean` | **L5** unique FP + residual under `HypContractive` |
| `Hcalc/Invariants.lean` | Structural invariants |
| `Hcalc/Production.lean` | Stable re-exports for Verify/docs |
## Rules
- Zero `sorry` / `admit`.
- Production Gap-* are **defs/theorems**, not opaque axioms.
- Gap-Real-arith for `Real` itself is **closed** (Mathlib `ℝ`). Gap-Foundry-* stubs OK if Foundry.State stays opaque.
- L7 = `InstanceBridge` Option B (parameter table + `toFoundryStep` diagnostic). **Not** `FoundryStep = hcalcStep`.
- C is state softScale-or-id; does **not** equal Foundry `softProject` on (Ξ,Λ) schedules.
- α (Tp weights) is Spec-only.
- No unconditional convergence — L5 under `HypContractive` only.
## Build
```bash
source ~/.elan/env
cd /workspace/hcalc/lean
lake update # first time / after mathlib pin change
lake exe cache get # download Mathlib oleans (recommended)
lake build 2>&1 | tee build.log
```
Toolchain: `leanprover/lean4:v4.34.1` + Mathlib `v4.34.1`.
|