correctedTrack1BStatus
plain-language theorem explainer
Status record for corrected Track 1.B: the axis-stencil local correspondence is formulated, its algebra, rigidity, legacy exclusivity, D2 residual hook, and N=5 stationarity are marked proved, and the explicit-fiber gate is closed. Gravity and compiler-trust audits cite it as the single boolean snapshot of that scope. The body is a structure literal assigning those flags.
Claim. The corrected Track 1.B scope record sets: corrected endpoint formulated; axis-stencil algebra proved; rigidity proved; exclusivity versus the legacy edge stencil proved; D2 residual hook proved; stationarity at $N=5$ proved; and the $N=5$ coefficient gate closed ($\mathrm{gate\_open}=\mathrm{false}$).
background
Track 1.B aims at a local Regge/J-cost correspondence on a cubic complex. Session 202 showed the old mixed-hinge quadratic was wrong-weighted at the $N=5$ single-vertex bump (mixed value $12$ versus seven-class edge stencil $6+6\sqrt{2}+2\sqrt{3}$). The corrected endpoint identifies the local Taylor quadratic with the canonical periodic mixed axis stencil rather than the legacy edge stencil.
The structure CorrectedTrack1BStatus packages six proved-scope flags plus gate_open. Sibling results in this module supply the substance: the general local correspondence for an arbitrary quadratic $Q$, the axis-stencil instance, nonnegativity and $a^2$-homogeneity, uniqueness of homogeneous quadratics satisfying the correspondence, and the parametric D2 residual bound used by damped-schedule closure.
Module status: zero sorry and zero RS-internal axioms for everything stated; the corrected gate is named closed at $N=5$, while the all-cardinality generalization stays open.
proof idea
Not a proof. One structure instance of CorrectedTrack1BStatus with six true flags and gate_open := false, matching the module doc that the $N=5$ explicit-fiber coefficient gate is closed (via the separate correctedTrack1BGateAtN5_closed decision) and only the all-cardinality lift remains.
why it matters
This is the boolean dashboard for corrected Track 1.B after the Session 202 reweighting. Downstream, track1BCompilerTrustStatus records that the closed $N=5$ gate was discharged by native_decide (extending the kernel with Lean.ofReduceBool and Lean.trustCompiler). The anchoring theorem track1BCompilerTrustStatus_anchors_closed_gate ties that trust record to this definition by proving gate_open = false here and uses_native_decide = true there.
In the gravity stack it certifies that the axis-stencil endpoint, rigidity (at most one homogeneous quadratic can match the local Taylor data), exclusivity against the legacy stencil, and the D2 hook needed for damped-schedule closure are all in place. It does not itself advance the forcing chain (T0–T8) or the RCL; it is bookkeeping for the discrete gravity correspondence layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.