File size: 4,249 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 74 75 76 77 78 79 80 81 82 | <!--
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 |
|