spec/HANDOFF_PRODUCTION.md

HANDOFF — Production close (copy-paste for Alloy / Lean / Verify / Core)

Authority: 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.