recognitionMeshGeometricDeficit4DStatus_flags
plain-language theorem explainer
Records the Wave B residual-R1 ledger for the 4D recognition-mesh geometric deficit: R1 is closed, the encoded Freudenthal lift remains open, and the gap-1 bridge is not derived. Gravity and QG auditors cite it as the machine-checked status snapshot after identifying mesh geometricDeficit with the signed Regge star deficit. The proof is a one-line decidability check on the status record.
Claim. The 4D recognition-mesh geometric-deficit status record satisfies: residual R1 is closed ($\mathrm{r1Closed}=\mathrm{true}$), the encoded Freudenthal lift is still open ($\mathrm{encodedFreudenthalLiftOpen}=\mathrm{true}$), and the gap-1 bridge is not derived ($\mathrm{gap1BridgeDerived}=\mathrm{false}$).
background
Wave B of the QG full-completion session targets residual R1: identify the mesh geometric deficit with a signed Regge-convention hinge deficit free of $x$-ratio or $\log x$-ratio scaffolding. The honest Lean binding uses deformation carrier $\mathbb{R}$ with starDeficit from four-tetrahedron signed deficit (odd, flat-vanishing, sign-certified), mesh context via exact $J$ equals true Regge Hessian on the canonical recognition mesh, and Freudenthal seed flatness (star angle sum $2\pi$).
The status record is a three-flag ledger for that residual. Closing R1 does not yet lift starDeficit onto a concrete Regge deficit angle on an encoded triangulation of the recognition Freudenthal mesh; that join is unexpressible until the mesh exposes a triangulation field. The ledger therefore keeps the encoded Freudenthal lift open and refuses to claim that the gap-1 bridge is derived.
proof idea
One-line decidability proof. The status definition hard-codes the three Boolean fields; decide discharges the conjunction of equalities against those literals. No algebraic lemmas are invoked.
why it matters
Pins the honest completion boundary of residual R1 in the Recognition mesh geometric-deficit analysis: mesh geometric deficit is identified with the signed Regge star deficit (no $x$-ratio), while the Freudenthal-encoded triangulation lift and the gap-1 constitutive bridge remain explicitly open. Downstream work that would claim full gap-1 residual discharge or inhabit deficit-source constitutive coupling must confront these flags. In the broader RS gravity stack this sits under the Regge/hinge 4D analysis that feeds curvature and action matching; it does not itself advance T0–T8 forcing, RCL, or the $\phi$-ladder mass formula. With no current used-by edges, it functions as an audit checkpoint rather than a lemma in a longer proof chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.