# HCALC Axiom Inventory **Owner:** HCALC Spec agent **Consumers:** HCALC Lean (defs / theorems), HCALC Alloy (Provenance tags), Foundry J Verify (cite-only). **Rule:** Domain Gap-* are **CLOSED by definition** in [`PRODUCTION.md`](PRODUCTION.md). Prefer production defs over opaque axioms. **Source absorbed:** [`FOUNDRY_J_CROSSLINKS.md`](FOUNDRY_J_CROSSLINKS.md). **Production authority:** [`PRODUCTION.md`](PRODUCTION.md). Provenance tags: `source-claim` | `axiom-gap` | `derived` | `SpecDefined`. --- ## Alloy A1–A7 | ID | Statement sketch | Kind | Lean link | Core / doc cite | Provenance | |----|------------------|------|-----------|-----------------|------------| | A1 | `#P_64=64`; elements = first-64 primes | assert | L1 | PROPERTIES **23**; Core `P64` | source-claim | | A2 | `contractive(J,ε) ↔ gershgorin(J)<1-ε` (+ opt. power-iter 37) | assert | L2 | **33–37**; `spectral_analyze`, `gershgorin_*`, `power_iteration*` | source-claim | | A3 | Foundry schedule soft_project when `q>1-ε` (**43** as coded) — **distinct from** production in-step `C` (state scale-or-id, **spec-adapt**) | assert | L4 | **43**/`soft_project`/`q_estimate` = **source-claim** (schedules only); production `C` → PRODUCTION.md / **spec-adapt** | source-claim (Foundry **43** only) | | A4 | affine Foundry recurrence **only if** `instance=Foundry` / FoundryAdditive diagnostic | assert | L3 | **39**; `rec_step`, `rec_run` | source-claim | | A5 | PMAT conservation on insert-set | assert | (PMAT defs) | **29**; `pmat_compose` | source-claim | | A6 | guardian rejects spectral_radius≥1 or non-finite | assert | — | **55** | source-claim | | A7 | definition-records for Λm, Ξ, C, Tp present and **SpecDefined** | gate | L6 defs | [`PRODUCTION.md`](PRODUCTION.md) | **SpecDefined** (CLOSED) | **A7 action:** Alloy must replace `Undefined` → `SpecDefined` on all four GapRecords, pointing at PRODUCTION.md formulas (not leave unconstrained). --- ## Lean L1–L7 | ID | Statement sketch | Kind | Why / status | Depends / dependents | Provenance | |----|------------------|------|--------------|----------------------|------------| | L1 | `P64 : Fin 64 → ℕ` = PROPERTIES 23 list | **def** | Data; no axiom if listed | Used by Tp indexing | source-claim | | L2 | `gershgorinBound`, `contractiveG` | **def+thm** | From 33–34 | Contraction lemmas; A2 | source-claim | | L3 | `FoundryStep Ξ Λ T g x` = prop 39 | **def** | Exact Foundry additive | A4; **≠** `hcalcStep` | source-claim | | L4 | `qEstimate` / `softProject` | **def** | 42–43 as coded | A3; production C | source-claim | | L5 | Unique FP when Hyp holds | **thm** (dischargeable) | Under PRODUCTION Hyp; Banach **41** + residual **46** | Convergence claims | derived | | L6 | `Λm`, `HCALC.Ξ`, `C`, `Tp` | **defs** (not axioms) | PRODUCTION §§2–5 | Nested-form theorems | **SpecDefined** | | L7 | `structure InstanceBridge` + Option B/C thms | **UNBLOCKED** | **NOT** `rfl`; **NOT** `FoundryStep = hcalcStep` | Instance proofs | **SpecDefined** | --- ## Named Gap-* (HCALC-native) — CLOSED All domain gaps CLOSED — see [`PRODUCTION.md`](PRODUCTION.md) disposition table. Summary: | GapId | Status | Definition pointer | |-------|--------|-------------------| | Gap-Carrier | **CLOSED — see PRODUCTION.md** | `HCALC.Carrier := Fin n → ℝ`, ℓ∞ | | Gap-Tp-from-P64 | **CLOSED — see PRODUCTION.md** | `(Tp x)_j = α_j · x_j`, `α_j = 1/(1+log p_{j mod 64})` | | Gap-C-wrapper | **CLOSED — see PRODUCTION.md** | soft_project-or-id on `q = ‖D(Tp)‖_est` (Spec wiring of Foundry-coded soft_project) | | Gap-Λm-scalar | **CLOSED — see PRODUCTION.md** | `Λm = min(1, (1-ε)/(‖C∘Tp‖_op+δ))` | | Gap-Ξ | **CLOSED — see PRODUCTION.md** | `Ξ(t,y) := ξ_t·y + g_t`; Uniform `ξ_t=1` | | Gap-ShapeMap | **CLOSED — see PRODUCTION.md** | **`InstanceBridge` morphism** (NOT `rfl` / NOT Foundry39≡nested); L7 UNBLOCKED | | Gap-ContractAlg | **CLOSED — see PRODUCTION.md** | Gershgorin → power-iter → soft_project (**33–43**) | | Gap-Converge | **CLOSED — see PRODUCTION.md** | Hyp ⇒ Banach unique FP + residual→0; L5 dischargeable | | Gap-OptObj | **CLOSED — see PRODUCTION.md** | `J(X)=‖X−Ξ(t,Λm·C(Tp(X)))‖_∞`; iterate to tol | Provenance for all rows above: **SpecDefined** (not axiom-gap). **ShapeMap / L7 rule (Foundry J Spec review):** REJECT identity `Foundry39 ≡ nested` and silent symbol swaps. ACCEPTED: non-identity `InstanceBridge` parameter table (`T := C∘Tp`, `Λ_vec := Λm·1`, `Ξ_vec := ξ_t`, `g := g_t`). Production Core implements **only** `hcalcStep` (Option B); `toFoundryStep` is cite-only diagnostic. Option C embedding optional later — still a morphism, never symbol identity. --- ## Theorems that may depend on production defs (Lean guidance) | After closing | Dependent results (sketches) | |---------------|------------------------------| | L1 + Tp def | Well-definedness of prime-indexed diagonal layers | | L2 + C def | Lip / non-expansive bound for nested step | | Λm def + L2 | Stabilizing-range lemmas | | Ξ def + InstanceBridge | Parameter-table theorems; **not** `hcalcStep = FoundryStep` | | L7 InstanceBridge | Option B Core path; optional Option C embedding morphism | | L5 under Hyp | Convergence monitors; uniqueness | ### Provenance (production close — Foundry J Spec pass-2) **A3 provenance split:** Alloy may keep a Foundry-instance assert for schedule soft_project (**43**, `source-claim`). Production in-step `C` is **SpecDefined** / **spec-adapt** per PRODUCTION.md — do not merge the two under one `source-claim` tag for **43**. - **Gap-Tp-from-P64** \(\alpha\) law: `spec-def` (P64 list alone is Foundry **source-claim** **23**). - **Gap-C-wrapper**: `spec-adapt` — algorithmic cousin of Foundry soft_project **43**, **not** symbol identity (43 scales schedules; production C scales state under Spec \(q=\|D(T_p)\|\)). - **Gap-ShapeMap / L7**: dual `bridgeMode` **NestedFaithful** | **FoundryAdditive**; InstanceBridge param table; morphism → FoundryAdditive only — never NestedFaithful = prop-**39** rfl. - Residual \(J\): Spec \(\ell_\infty\); Foundry **46** is \(\ell_2\). **FAIL-open:** `sorry` / Alloy `unsat` failure / missing SpecDefined A7 record ⇒ SKIP or FAIL — never PASS. --- ## Infrastructure Gap-* (Lean toolchain stubs) — ACCEPTED (not production blockers) Provisional IDs from HCALC Lean first cut (`lake build` exit 0, Mathlib deferred). Spec **accepts these names as canonical**; do not rename without Spec update. They are **infrastructure only** — not HCALC domain axioms and **not production blockers** when nested defs use explicit Carrier ℝ^n. Closing path: replace with Mathlib `Real` / proven Foundry defs when ready; until then FAIL-open on infra (axioms OK, never silent PASS). | GapId | Role | Lean surface | Status | Provenance | |-------|------|--------------|--------|------------| | Gap-Real-arith | Opaque `Real` + basic arith/order facts absent Mathlib | `Hcalc/RealStub.lean` | infra stub (Mathlib deferred) | infra-not-production-gap | | Gap-Foundry-StateOps | Foundry recurrence carrier + add/smul/zero (≠ HCALC `State`) | `Hcalc/Foundry.lean` | infra stub | infra-not-production-gap | | Gap-Foundry-FinMax | `finMax` for Gershgorin-style bounds | `Hcalc/Foundry.lean` | infra stub | infra-not-production-gap | | Gap-Foundry-Norm | Opaque weight / nonlinear norms for coded q-estimate | `Hcalc/Foundry.lean` | infra stub | infra-not-production-gap | | Gap-Foundry-Div | Real division for soft-project scale | `Hcalc/Foundry.lean` | infra stub | infra-not-production-gap | | Gap-Foundry-SoftScale | Opaque soft-project scale + branch laws | `Hcalc/Foundry.lean` | infra stub | infra-not-production-gap | **Rule:** Infra stubs must not leave unfinished *production* theorems depending on `sorry`. Production Carrier/Tp/C/Λm/Ξ/J path uses explicit ℝ^n defs in PRODUCTION.md. Do **not** use infra stubs to invent an `rfl` ShapeMap. --- ## Steering aliases (G-*) Stable short aliases. Prefer these in tags; Spec GapIds remain canonical. **All CLOSED.** | Alias | Canonical GapId | Statement | Status | |-------|-----------------|-----------|--------| | **G-SHAPE** | Gap-ShapeMap | `InstanceBridge` morphism (NOT `rfl`; NOT Foundry39≡nested) | **CLOSED** — PRODUCTION §6 | | **G-Lm** | Gap-Λm-scalar | Scalar Λm formula (≠ vector schedule) | **CLOSED** — PRODUCTION §4 | | **G-C** | Gap-C-wrapper | In-step soft_project-or-id as C (Spec wiring) | **CLOSED** — PRODUCTION §3 | | **G-Tp** | Gap-Tp-from-P64 | Diagonal Tp from P64 α weights | **CLOSED** — PRODUCTION §2 | Core cite-only (hooks, not alternate defs): `P64`, `pmat_compose`, `spectral_analyze`, `soft_project`, `q_estimate`, `synth_weights`, `rec_step`, `rec_run`, `ace_certify` — see foundry-j `spec/J_API.md`, `j/BOXING.md`, `spec/GAP_DECISIONS.md`.