spec/PRODUCTION.md

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, COHERENCE.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
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.