| <!-- |
| Copyright (C) 2026 HCALC contributors |
| SPDX-License-Identifier: AGPL-3.0-only |
| --> |
|
|
| # HCALC Interfaces — Alloy vs Lean |
|
|
| **Owner:** HCALC Spec agent |
| **Definitions live in:** [`PRODUCTION.md`](PRODUCTION.md), [`COHERENCE.md`](COHERENCE.md), [`AXIOMS.md`](AXIOMS.md), [`FOUNDRY_J_CROSSLINKS.md`](FOUNDRY_J_CROSSLINKS.md). |
| **Status:** Production definitions landed; Alloy must replace A7 Undefined→SpecDefined; Lean defs not axioms; Verify flip SKIP→PASS where hyps hold. |
| **Spec does not write** `.als` or `.lean` bodies (see [`HANDOFF_PRODUCTION.md`](HANDOFF_PRODUCTION.md)). |
|
|
| --- |
|
|
| ## Shared vocabulary (symbol table) |
|
|
| | Symbol | Meaning | Gap / ID | Status | |
| |--------|---------|----------|--------| |
| | \(X_t\) | State | Gap-Carrier | **CLOSED** — `HCALC.Carrier` | |
| | \(T_p\) | Diagonal prime-indexed transform | Gap-Tp-from-P64, A7, L6 | **CLOSED** (**spec-def** α) | |
| | \(C\) | In-step scale-or-id | Gap-C-wrapper, A7, L6 | **CLOSED** (**spec-adapt** ≠ **43**) | |
| | \(\Lambda_m\) | Stabilizing **scalar** | Gap-Λm-scalar, A7, L6 | **CLOSED** | |
| | \(\Xi(t,\cdot)\) | HCALC evolution operator | Gap-Ξ, A7, L6 | **CLOSED** | |
| | Foundry step | \(x'=\Xi x+\Lambda T(x)+g\) | A4, L3 | FoundryAdditive diagnostic | |
| | HCALC step | \(X_{t+1}=\Xi(t,\Lambda_m\cdot C(T_p(X_t)))\) | NestedFaithful | production Core verb | |
| | InstanceBridge | Param table \(T:=C\circ T_p\), \(\Lambda:=\Lambda_m\mathbf{1}\), \(\Xi:=\xi_t\) | Gap-ShapeMap, L7 | **CLOSED** — NOT `rfl` | |
| | `P_64` | First-64 primes index set | A1, L1 | source-claim **23** | |
|
|
| Provenance on every Alloy assert / Lean axiom: `source-claim` | `axiom-gap` | `derived` | `SpecDefined` | `spec-def` | `spec-adapt`. |
|
|
| --- |
|
|
| ## What HCALC Alloy must assert |
|
|
| - **A1–A6** when the model claims Foundry-backed surfaces (finite predicates / traces). |
| - **A7** with **SpecDefined** records pointing at PRODUCTION.md (replace prior `Undefined`). |
| - **Inv-StepForm … Inv-OpaqueGaps** (COHERENCE invariant inventory). |
| - Dual `bridgeMode ∈ {NestedFaithful, FoundryAdditive}` + InstanceBridge table; **forbid** NestedFaithful = prop-**39** / `rfl`. |
| - Forbidden: PASS when guardian (**A6**) would reject. |
| - May leave as **parameters:** ε tier, instance tag, carrier dimension, whether PMAT is enabled. |
| - OptObj = Spec \(\ell_\infty\) residual; ContractAlg = Gershgorin→power-iter→scale-or-id. |
| |
| Provenance tags should reference GapIds / A* / L* from COHERENCE/AXIOMS/PRODUCTION. |
| |
| --- |
| |
| ## What HCALC Lean may axiomize vs must prove |
| |
| | May keep as infra axiom (toolchain only) | Must define or prove | |
| |------------------------------------------|----------------------| |
| | Gap-Real-arith / Gap-Foundry-* stubs | L1 P64 data as def | |
| | | L2 gershgorin/contractiveG | |
| | | L3 FoundryStep def (**≠** hcalcStep) | |
| | | L4 qEstimate/softProject (Foundry) | |
| | | L5 theorem under Hyp (0 sorry) | |
| | | L6: Λm, Ξ, C, Tp as **defs** (replace axioms) | |
| | | L7: `structure InstanceBridge` + dual-mode thms — **NOT** `rfl` / **NOT** `FoundryStep = hcalcStep` | |
| |
| Zero `sorry` in production leaves. Domain gaps are CLOSED — no new L6 axioms. |
| |
| --- |
| |
| ## Foundry J Core / Verify |
| |
| - Cross-links: `FOUNDRY_J_CROSSLINKS.md`; Foundry mirror `/workspace/foundry-j/spec/HCALC_CROSSLINKS.md`. |
| - Core implement path (authoritative): **`/workspace/hcalc/j/`** — verbs `tp_from_p64`, `c_wrap`, `lam_m_from_bound`, `hcalc_xi_apply`, `hcalc_step`, `hcalc_run`. |
| - Core hooks are **cite-only** — do not equate `hcalc_step` with `rec_step`. |
| - Verify outline: [`PROPERTIES.md`](PROPERTIES.md); harness [`../verify/README.md`](../verify/README.md). |
| - H-SHAPE PASS only for InstanceBridge witness, never identity. |
|
|
| --- |
|
|
| ## Hand-off |
|
|
| | Agent | Owns | Does not own | |
| |-------|------|--------------| |
| | **Spec** | PRODUCTION, COHERENCE, AXIOMS, PROPERTIES outline, INTERFACES, crosslinks | `.als`, `.lean`, J verb bodies | |
| | **Alloy** | `alloy/**/*.als`, Alloy README beyond stub | Changing GapId meanings / inventing `rfl` bridge | |
| | **Lean** | `lean/**/*.lean` | Re-axiomatizing CLOSED L6; `FoundryStep = hcalcStep` | |
| | **Verify** | `verify/` harness per PROPERTIES | Closing ShapeMap without Spec | |
| | **Core** | `/workspace/hcalc/j/` production verbs | Equating FoundryAdditive with NestedFaithful | |
|
|
