| <!-- |
| Copyright (C) 2026 HCALC contributors |
| SPDX-License-Identifier: AGPL-3.0-only |
| --> |
|
|
| # HANDOFF — Production close (copy-paste for Alloy / Lean / Verify / Core) |
|
|
| **Authority:** [`PRODUCTION.md`](PRODUCTION.md) @ commit with InstanceBridge + Pass-2 provenance. |
| **Do not invent** beyond PRODUCTION / AXIOMS. Spec does not edit `.als` / `.lean` bodies. |
|
|
| --- |
|
|
| ## Alloy |
|
|
| 1. Replace A7 GapRecord status `Undefined` → `SpecDefined` for Λm, Ξ, C, Tp; point comments at PRODUCTION.md. |
| 2. Encode production preds: Carrier ℝ^n / abstract n; diag Tp α; C scale-or-id; Λm scalar min formula; Ξ = ξ·y+g (Uniform). |
| 3. Add `bridgeMode ∈ {NestedFaithful, FoundryAdditive}` + `InstanceBridge` param table. |
| 4. **Forbid** NestedFaithful = Foundry prop-**39** / `rfl` / silent symbol identity. |
| 5. Keep A1–A6; rewire A3 to Spec q / in-step C (**spec-adapt** ≠ Foundry **43** schedule soft_project). |
| 6. OptObj = residual \(\ell_\infty\); ContractAlg = Gershgorin→power-iter→scale-or-id. |
| 7. Re-run `alloy/run.sh`; expect green with SpecDefined A7. |
|
|
| ## Lean |
|
|
| 1. Replace L6 axioms with **defs**: `Carrier`, `Tp`, `C`, `LambdaM`, `Xi`, `J`. |
| 2. Unblock L7: `structure InstanceBridge` holding param table; dual-mode theorems — **never** `FoundryStep = hcalcStep` / **never** `rfl`. |
| 3. L5: theorem under PRODUCTION Hyp (0 sorry). |
| 4. Keep infra Gap-Real-* / Gap-Foundry-* stubs labeled infra-not-production-gap. |
| 5. Tag α as **spec-def**; C as **spec-adapt**. |
| 6. `lake build` exit 0. |
|
|
| ## Verify |
|
|
| 1. Flip SKIP→PASS where hyps hold (PROPERTY_MAP H-A7, H-SHAPE, H-NEST, H-OPT, H-L5). |
| 2. H-SHAPE PASS **only** for InstanceBridge witness — never identity PASS. |
| 3. Note Spec residual \(\ell_\infty\) ≠ Foundry **46** \(\ell_2\). |
| 4. FAIL-open still if Lean sorry / Alloy unsat / Undefined A7. |
| 5. Update `verify/PROPERTY_MAP.md` to match `spec/PROPERTIES.md`. |
|
|
| ## Core (`/workspace/hcalc/j/`) |
|
|
| 1. Implement Option B verbs: `tp_from_p64`, `c_wrap`, `lam_m_from_bound`, `hcalc_xi_apply`, `hcalc_step`, `hcalc_run`. |
| 2. Cite Foundry hooks (`P64`, `spectral_analyze`, `soft_project`, `q_estimate`, `synth_weights`) — do **not** equate `hcalc_step` with `rec_step`. |
| 3. Expose `toFoundryStep` only as FoundryAdditive diagnostic. |
| 4. Leave Foundry additive API unchanged. |
|
|
| ## Push gate |
|
|
| Do **not** push until Alloy + Lean + Verify are green. |
|
|
