spec/PRODUCTION.md

<!--
  Copyright (C) 2026 HCALC contributors
  SPDX-License-Identifier: AGPL-3.0-only
-->

# HCALC Production Definitions

**Owner:** HCALC Spec  
**License:** AGPL-3.0-only  
**Status:** PRODUCTION — all domain Gap-* CLOSED by definition (not opaque axioms).  
**Consumers:** Alloy, Lean, Foundry J Core/Verify/Spec.  
**Related:** [`AXIOMS.md`](AXIOMS.md), [`COHERENCE.md`](COHERENCE.md), [`FOUNDRY_J_CROSSLINKS.md`](FOUNDRY_J_CROSSLINKS.md).

Nested recurrence (canonical):

\[
X_{t+1} = \Xi\bigl(t,\; \Lambda_m \cdot C(T_p(X_t))\bigr).
\]

---

## Parameters (fixed for production)

| Symbol | Meaning | Default |
|--------|---------|---------|
| \(n\) | Carrier dimension | parameter \(\ge 1\) (Lean: free `n : ℕ`) |
| \(\varepsilon\) | Contraction margin | tier schedule Foundry **25**: T1→0.10, T2→0.05, T3→0.02, T4→0.01; **default T2 = 0.05** |
| \(\delta\) | Guard for Λm denominator | \(10^{-12}\) (positive) |
| \(\mathrm{tol}\) | Residual stop | \(10^{-6}\) |
| `xi_schedule` | \(\xi_t\) law | **Uniform**: \(\xi_t = 1\) for all \(t\) |
| `g_t` | Affine kick | default \(0\) (zero vector) unless instance supplies otherwise |

Foundry cites used below: PROPERTIES **23**, **25**, **33–43**, **39**, **41**, **46**.

---

## Closed definitions

### 1. Gap-Carrier → `HCALC.Carrier` — CLOSED

\[
\texttt{HCALC.Carrier} \;\equiv\; X \;:=\; \mathbb{R}^n \;=\; (\mathrm{Fin}\, n \to \mathbb{R})
\]

with \(\ell_\infty\) norm \(\|x\|_\infty = \max_{j} |x_j|\).  
Optional later instance: Goldilocks \(\mathbb{F}_p\) (Foundry **1–17**) — **not** required for production ℝ path.

### 2. Gap-Tp-from-P64 → `Tp` — CLOSED

Let \(P_{64} = (p_0,\ldots,p_{63})\) be the first-64 primes (Lean **L1** / Foundry prop **23**).  
For dimension \(n\), use primes \(p_{j \bmod 64}\).

**Exact formula (diagonal PrimeMask weights):**

\[
\alpha_j \;=\; \frac{1}{1 + \log p_{j\bmod 64}}, \qquad
(T_p\, x)_j \;=\; \alpha_j \cdot x_j.
\]

So \(\varphi\) is the **identity on coordinates** (diagonal action).
Equivalent view: \(T_p = \mathrm{diag}(\alpha)\).
**Provenance:** \(\alpha\) law is **`spec-def`** (HCALC Spec) — **not** a Foundry source-claim. \(P_{64}\) list alone is Foundry **23** / Lean L1.
**Not** Sedona/PIRTM tooling; **not** full PMAT recursion.

**Provenance (§2):** `P64` list = Foundry **source-claim** (prop **23**). The weight law $\alpha_j=1/(1+\log p_{j\bmod 64})$ is **`spec-def`** — **not** a Foundry PROPERTY / not `source-claim` from foundry-j.

### 3. Gap-C-wrapper → `C` — CLOSED

Let \(D(T_p)\) be the Jacobian of \(T_p\) (here \(D(T_p)=\mathrm{diag}(\alpha)\)).  
Let \(q\) be the operator-norm estimate via Gershgorin, with power-iteration fallback (Foundry **33–37**):

\[
q \;:=\; \|D(T_p)\|_{\mathrm{est}}.
\]

**In-step governor** — Spec-defined **state scale-or-id** (not post-hoc `ace_certify`):

\[
C(x) \;=\;
\begin{cases}
\dfrac{1-\varepsilon}{q}\, x & \text{if } q > 1-\varepsilon, \\[6pt]
x & \text{otherwise.}
\end{cases}
\]

I.e. \(C = s\cdot\mathrm{id}\) on **state**, with \(s=(1-\varepsilon)/q\) when over margin.

**Provenance (Foundry pass 2):** \(C\) is **`spec-adapt`** of the scale-factor *idea* \((1-\varepsilon)/q\).
**REJECT** identity with Foundry `soft_project` **43** (which scales schedule vectors \(\Xi,\Lambda\), not state).
Foundry **43** remains the coded schedule soft_project on the **FoundryAdditive** path. Production \(q=\|D(T_p)\|_{\mathrm{est}}\) is Spec \(q\), not Foundry **42** schedule \(q\).

**Provenance (§3):** Production `C` is **`spec-adapt`**: it reuses the *scale-or-id* idea \((1-\varepsilon)/q\) as an **algorithmic cousin** of Foundry `soft_project` (prop **43**), but it is **not** symbol-identical to **43**. Foundry **43** scales schedule weights \(\Xi,\Lambda\) under Foundry \(q\) (prop **42**); production `C` scales the **state** under Spec \(q:=\|D(T_p)\|_{\mathrm{est}}\). Do **not** tag `C` as Foundry `source-claim` for **43**. Shared helper name `softProjectScale` OK; **Foundry `soft_project` API stays schedule-scaling** (prop **43**). Production `C` remains Spec-wiring / **spec-adapt** (state scale).

### 4. Gap-Λm-scalar → `Λm` — CLOSED

\(\Lambda_m \in \mathbb{R}_{\ge 0}\) is a **scalar** (not Foundry `lambda_schedule` vector):

\[
\Lambda_m \;=\; \min\Bigl(1,\; \frac{1-\varepsilon}{\|C\circ T_p\|_{\mathrm{op}} + \delta}\Bigr),
\]

ensuring \(\|\Lambda_m\cdot(C\circ T_p)\|_{\mathrm{op}} \le 1-\varepsilon\).

### 5. Gap-Ξ → `Ξ` — CLOSED

With \(\xi_t\) from `xi_schedule(t)` (default **Uniform**: \(\xi_t=1\)) and kick \(g_t\):

\[
\Xi(t,y) \;:=\; \xi_t\cdot y + g_t.
\]

Therefore

\[
X_{t+1} = \xi_t\cdot\bigl(\Lambda_m\cdot C(T_p(X_t))\bigr) + g_t.
\]

### 6. Gap-ShapeMap / L7 — CLOSED via **InstanceBridge** (NOT `rfl`)

**REJECTED (Foundry J Spec review):** identity `Foundry39 ≡ nested`; silent `Λ_t↔Λm`, `T↔T_p`, `Ξ_t↔Ξ(t,·)`, Gershgorin/`soft_project` measures ↔ in-step `C` as Foundry-native law.

**ACCEPTED:** Gap-ShapeMap is a **non-identity** morphism. soft_project remains **Foundry-coded** (props **42–43**) and is *used by* HCALC `C` under this Spec — that is Spec wiring, not a Foundry identity claim.

#### Dual `bridgeMode` (keep both; never silent equate)

| `bridgeMode` | Meaning | Prop-**39**? |
|--------------|---------|--------------|
| **NestedFaithful** | production verb = `hcalcStep` (nested) | **no** — Spec nested; ≠ classical **39** |
| **FoundryAdditive** | diagnostic `toFoundryStep` via InstanceBridge param table | **yes-shaped** morphism toward **39**; still ≠ nested |

`InstanceBridge` is the **parameter table** \(T:=C\circ T_p\), \(\Lambda_{\mathrm{vec}}:=\Lambda_m\cdot\mathbf{1}\), \(\Xi_{\mathrm{vec}}:=\xi_t\), \(g:=g_t\) — a **non-identity** morphism, never `rfl`.

#### Explicit morphism `InstanceBridge` (feeds FoundryAdditive mode)

Let HCALC state \(x\in\texttt{HCALC.Carrier}\). Define a **labeled instance map** (Lean: `InstanceBridge`, Alloy: `bridgeMode = InstanceBridge`):

\[
\texttt{toFoundryStep}(t,x)
\;:=\;
\texttt{FoundryStep}\bigl(
  \Xi_{\mathrm{vec}}:=\xi_t,\;
  \Lambda_{\mathrm{vec}}:=\Lambda_m\cdot\mathbf{1},\;
  T := C\circ T_p,\;
  g := g_t,\;
  x
\bigr)
\;=\;
\xi_t\cdot x + \Lambda_m\cdot(C\circ T_p)(x) + g_t.
\]

The **HCALC nested step** is separately:

\[
\texttt{hcalcStep}(t,x)
\;:=\;
\Xi\bigl(t,\, \Lambda_m\cdot C(T_p(x))\bigr)
\;=\;
\xi_t\cdot\bigl(\Lambda_m\cdot C(T_p(x))\bigr) + g_t.
\]

These are **different** morphisms in general (\(\xi_t\cdot x\) term present only on the Foundry side).  
**L7 theorem (production):** there exists an explicit Spec-named witness relating them — *not* `rfl`:

- **Option A (recommended default):** `bridgeWitness = Projective` — equality after applying the HCALC projection that discards the free \(\xi_t\cdot x\) drift, or equivalently require \(\xi_t=0\) on the identity channel (not used).  
- **Option B (operational default for Core):** implement **only** `hcalcStep` as the production verb; expose `toFoundryStep` as a **cite-only diagnostic** that uses Foundry `rec_step` shape with the parameter table above, **without claiming** `hcalcStep = toFoundryStep`.  
- **Option C:** when \(\xi_t = 1\) and one rewrites nested as additive on an extended state, document the embedding \(\iota\) and prove `toFoundryStep(t,ι(x)) = ι(hcalcStep(t,x))` — still a morphism, **never** symbol identity.

**Production bridgeMode (dual — Foundry J Spec ACCEPT):**

| bridgeMode | Meaning | vs Foundry **39** |
|------------|---------|-------------------|
| **FoundryAdditive** | `toFoundryStep` = classical **39**-shaped morphism with InstanceBridge params `T:=C∘Tp`, `Λ:=Λm·1`, `Ξ:=ξ_t` | **ACCEPT** morphism into additive shape — **not** nested |
| **NestedFaithful** / nested `hcalcStep` | `ξ·(Λm·(C∘Tp)(x))+g` | Spec definitional nested — **REJECT** as prop-**39** `rfl` / identity |

**InstanceBridge** = the explicit parameter table (morphism data), not an equality proof. Hilbert morphism \(T:=C\circ T_p\), \(\Lambda:=\Lambda_m\mathbf{1}\), \(\Xi:=\xi\) maps to **FoundryAdditive** shape only.

**Production choice for Core:** implement **`hcalc_step`** = nested (NestedFaithful semantics); expose `toFoundryStep` only as FoundryAdditive diagnostic. **L7 UNBLOCKED** as `structure InstanceBridge` + dual-mode theorems — **never** `FoundryStep = hcalcStep`.

| Foundry symbol (instance params) | HCALC production value | Identity? |
|----------------------------------|------------------------|-----------|
| \(T\) | \(C\circ T_p\) | **no** — assignment under InstanceBridge |
| \(\Lambda_{\mathrm{vec}}\) | \(\Lambda_m\cdot\mathbf{1}\) | **no** — scalar broadcast ≠ Foundry schedule vector law |
| \(\Xi_{\mathrm{vec}}\) | \(\xi_t\) from HCALC `xi_schedule` | **no** — not Foundry \(\Xi_t\) vector schedule identity |
| \(g\) | \(g_t\) | instance param |

### 7. Gap-ContractAlg — CLOSED

Algorithm:

1. Estimate Spec \(q=\|D(T_p)\|_{\mathrm{est}}\) by Gershgorin; power-iteration fallback (Foundry measures **33–37**, Spec-wired).
2. Apply **state** scale-or-id \(C\) as in §3 (`spec-adapt`; ≠ schedule soft_project **43**).
3. Form \(\Lambda_m\) as in §4.
4. On FoundryAdditive path only: Foundry schedule soft_project **43** may still apply to \(\Xi,\Lambda\) schedules as coded.

### 8. Gap-Converge — CLOSED (L5 dischargeable)

**Hyp** (for iteration of **`hcalcStep`** — Option B / nested production path):

\[
|\xi_t|\cdot\|\Lambda_m\cdot(C\circ T_p)\|_{\mathrm{op}} < 1-\varepsilon.
\]

Under Uniform \(\xi_t=1\) this is \(\|\Lambda_m\cdot(C\circ T_p)\|_{\mathrm{op}} < 1-\varepsilon\).

Do **not** state Hyp on `toFoundryStep` / classical additive shape without an extra account of the free \(\xi_t\cdot x\) term (that diagnostic has a different operator).

Then: Banach unique fixed point (Foundry narrative **41**, spirit) and residual \(\to 0\) along **`hcalcStep`** iteration (stop spirit of **46**; metric is Spec \(\ell_\infty\)).  
**L5:** theorem under Hyp (prove in Lean; not unfinished axiom).

### 9. Gap-OptObj — CLOSED

\[
J(X) \;=\; \bigl\| X - \Xi\bigl(t,\, \Lambda_m\cdot C(T_p(X))\bigr) \bigr\|_\infty
\]

(residual). **Optimize** = iterate the nested map until \(J(X)<\mathrm{tol}\).

**Provenance (residual):** PRODUCTION \(J\) uses \(\ell_\infty\). Foundry prop **46** residual is \(\ell_2\). **ACCEPT Spec \(\ell_\infty\) choice**; do not claim metric identity with **46** — only stop-spirit / tolerance pattern.

---

## Infra gaps (not domain blockers)

| GapId | Disposition |
|-------|-------------|
| Gap-Real-arith | Infra stub OK (RealStub / future Mathlib). Must not leave unfinished *production* theorems depending on sorry. |
| Gap-Foundry-StateOps / FinMax / Norm / Div / SoftScale | Infra for Foundry mirrors; production HCALC path uses Carrier ℝ^n defs above. Replace with Mathlib when ready. |

---

## Gap disposition table

| GapId | Was | Now | Alloy action | Lean action | Verify action |
|-------|-----|-----|--------------|-------------|---------------|
| Gap-Carrier | axiom-gap | **CLOSED** `HCALC.Carrier = Fin n → ℝ`, ℓ∞ | Instance param → ℝ^n model / abstract n | `def Carrier` | Check A carrier |
| Gap-Tp-from-P64 | axiom-gap | **CLOSED** diag \(\alpha\) (**spec-def**); P64 list **source-claim** **23** | Retire Undefined; encode diag Tp | `def Tp` from L1 P64 | Prime carrier + Tp law |
| Gap-C-wrapper | axiom-gap | **CLOSED** scale-or-id on Spec \(q\) (**spec-adapt**; cousin of **43**, ≠ **43**) | C = scale-or-id | `def C` | Contraction spectral/q |
| Gap-Λm-scalar | axiom-gap | **CLOSED** scalar min formula | Λm scalar bound assert | `def LambdaM` | Stabilizing range |
| Gap-Ξ | axiom-gap | **CLOSED** \(\xi_t y + g_t\), Uniform default | Ξ affine | `def Xi` | Evolution step shape |
| Gap-ShapeMap / L7 | blocked | **CLOSED** dual `bridgeMode` NestedFaithful|FoundryAdditive + InstanceBridge table (NOT rfl; NestedFaithful ≠ prop39) | Encode InstanceBridge table; forbid symbol identity | **L7** `structure InstanceBridge` + Option B/C thms | H-SHAPE → PASS only for InstanceBridge witness, never identity |
| Gap-ContractAlg | axiom-gap | **CLOSED** Gershgorin→power-iter→soft_project | A2/A3 production wiring | defs + thms | Checks B |
| Gap-Converge | axiom-gap | **CLOSED** Hyp ⇒ Banach + residual→0 | Guardian + residual | **L5** under Hyp | Residual discharge |
| Gap-OptObj | axiom-gap | **CLOSED** \(J=\) residual; iterate to tol | OptObj residual | `def J` + loop spec | Optimize/converge props |
| A7 | Undefined stubs | **SpecDefined** records pointing here | Replace Undefined→Defined | — | A7 gate PASS |
| L6 | uninterpreted axioms | **defs** | — | Replace axioms with defs | Seal Lean↔Alloy |
| Gap-Real-arith / Gap-Foundry-* | infra | infra OK | ignore | keep stubs or Mathlib | no false PASS |

---

## Alloy checklist

1. Retire all `Undefined` on Λm, Ξ, C, Tp → `SpecDefined` / production preds.  
2. Keep A1–A6; rewire A2/A3/A4 to production C/Λm/`InstanceBridge`.  
3. Encode **`bridgeMode`**: nested **`hcalcStep`** vs diagnostic **`toFoundryStep`** (InstanceBridge param table). Do **not** assert Foundry39≡nested; do **not** use a bare `FoundryAdditive` equate without InstanceBridge params.  
4. OptObj = residual (\(\ell_\infty\)); ContractAlg = Gershgorin→power-iter→Spec scale-or-id.  
5. Report check log green.


## Lean checklist

1. `Carrier`, `Tp`, `C`, `LambdaM`, `Xi`, `J` as **defs**.  
2. Unblock **L7** InstanceBridge (`def` / theorem).  
3. **L5** theorem under Hyp (0 sorry).  
4. Infra RealStub only if no production sorry.  
5. `lake build` exit 0.

## Verify checklist

1. Flip SKIP→PASS where hyps hold (A–E).  
2. H-SHAPE PASS under InstanceBridge.  
3. FAIL-open still if Lean sorry / Alloy unsat.  
4. Update `PROPERTY_MAP.md`.

## Core checklist (Foundry J)

Implement verbs: `Tp` from P64 α, in-step `C` state scale-or-id (`spec-adapt`), scalar `Λm`, `Xi` from `xi_schedule`, InstanceBridge step. Cite `P64`, `spectral_analyze`, `soft_project`, `q_estimate`, `synth_weights`, `rec_step`.

---


## Core implement path (AUTHORITATIVE)

**Path:** `/workspace/hcalc/j/` (HCALC research-center repo; AGPL-3.0-only).  
Foundry J Core implements production verbs **here**, calling Foundry cite hooks from `foundry-j` (`P64`, `spectral_analyze`, `soft_project`, `q_estimate`, `synth_weights`) without equating `hcalc_step` to `rec_step`.

| Verb | Formula source in this file |
|------|-----------------------------|
| `tp_from_p64` | §2 Gap-Tp-from-P64 |
| `c_wrap` | §3 Gap-C-wrapper (state scale-or-id; ≠ soft_project **43**) |
| `lam_m_from_bound` | §4 Gap-Λm-scalar |
| `hcalc_xi_apply` | §5 Gap-Ξ |
| `hcalc_step` | nested §5; **not** `rec_step` |
| `hcalc_run` | iterate `hcalc_step` until §9 residual < tol |

Draft names from `foundry-j/j/HCALC_API_DRAFT.md` are **accepted**. Leave Foundry additive API unchanged.

---
## Changelog

- 2026-10-07: Initial PRODUCTION close-all-gaps (USER mandate via Hilbert).
- 2026-10-07: ShapeMap → explicit **InstanceBridge** (Foundry J Spec review); Core path `/workspace/hcalc/j/`.
- 2026-10-07: Pass-3 nits — §3 schedule-scaling note; Alloy checklist InstanceBridge; §8 Hyp on hcalcStep.
- 2026-10-07: Pass-2 absorb — `C`/`q` **spec-adapt** (≠ Foundry **43**/**42**); \(\alpha\) **spec-def**; dual NestedFaithful|FoundryAdditive; residual \(\ell_\infty\neq\ell_2\) note.
- 2026-10-07: Fold Foundry pass 2 — C ≠ soft_project#43; α `spec-def`; NestedFaithful ≠ prop39; dual bridgeMode kept.