CorrectedTrack1BStatus
plain-language theorem explainer
Status record for the corrected Track 1.B local quadratic program: seven booleans for endpoint formulation, axis-stencil algebra, rigidity, exclusivity versus the legacy stencil, the D2 residual hook, N=5 stationarity, and whether the coefficient gate is still open. Gravity auditors cite the concrete witness built from it. Pure structure definition; no proof content.
Claim. A status bundle of seven boolean flags recording: (i) whether the corrected local correspondence endpoint is formulated, (ii) whether axis-stencil quadratic algebra is proved, (iii) whether quadratic rigidity is proved, (iv) whether exclusivity against the legacy edge stencil is proved, (v) whether the D2 residual hook is proved, (vi) whether stationarity at $N=5$ is proved, and (vii) whether the explicit-fiber coefficient gate remains open.
background
Track 1.B aims at a local cubic-Taylor correspondence between Regge hinge data and a J-cost quadratic on the recognition ledger. Session 202's finite audit showed the old mixed hinge-deficit identification is wrong-weighted: at the $N=5$ single-vertex bump the mixed quadratic evaluates to $12$, while the seven-class square-root edge stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$, and those scalars are proved unequal.
The corrected endpoint replaces the legacy edge stencil by the rational axis stencil (canonicalPeriodicMixedAxisStencilAction). This module supplies the generalized correspondence predicate for an arbitrary candidate quadratic $Q$, the axis-stencil instance, nonnegativity and $a^2$-homogeneity, rigidity (two homogeneous quadratics satisfying the correspondence are pointwise equal), exclusivity with the legacy stencil, and the parametric D2 residual bound used by damped-schedule closure.
The structure is only a checklist type for that corrected scope. The module header states theorem status (0 sorry, 0 RS-internal axiom) for everything stated, while the corrected gate itself is named open rather than asserted as a universal claim.
proof idea
No proof: a structure declaration with seven Bool fields. Downstream, a single definition fills the fields from the module's theorems and sets the gate flag from the $N=5$ closure lemma.
why it matters
Gives a machine-readable scope certificate for the corrected Track 1.B quadratic route after the Session 202 mismatch forced the axis-stencil endpoint. The sole direct consumer is correctedTrack1BStatus, which sets every formulation/proof flag true and gate_open := false via correctedTrack1BGateAtN5_closed, leaving only the all-cardinality generalization open.
In the broader gravity stack this sits under the local Regge/J-cost correspondence that feeds damped-schedule and residual bounds (D2 hook). Rigidity plus the audit mismatch selects the axis stencil as the unique homogeneous quadratic Taylor coefficient among the two candidates. It does not itself touch T5–T8 forcing, RCL, or the mass ladder; it is ledger-geometry bookkeeping for the corrected quadratic identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.