RecognitionMeshGeometricDeficit4DStatus
plain-language theorem explainer
Status record for the 4D recognition-mesh geometric-deficit residual (Wave B R1). Three booleans track whether the mesh deficit is identified with the signed star deficit, whether the encoded Freudenthal triangulation lift remains open, and whether the gap-1 bridge is derived. Downstream code instantiates it with R1 closed, lift open, and gap-1 not derived. Pure data package; no proof content.
Claim. A status triple of booleans $(r_1^{\mathrm{closed}},\ \ell_{\mathrm{Freudenthal}}^{\mathrm{open}},\ g_1^{\mathrm{derived}})$ recording completion of the mesh geometric-deficit identification, openness of the encoded Freudenthal triangulation lift of the signed star deficit, and whether the gap-1 constitutive bridge has been derived.
background
Wave B of the QG completion session attacks the residual that the mesh geometric deficit equals the signed Regge-convention hinge deficit, free of $x$-ratio or $\log x$-ratio scaffolding. The honest binding uses a real deformation carrier with the four-tetrahedra signed star deficit (odd, flat-vanishing, sign-certified), mesh context via exact $J$ equal to the true Regge Hessian on the canonical recognition mesh, and Freudenthal seed flatness (star angle sum $2\pi$).
The module deliberately does not flip the gap-1 bridge flag, does not inhabit a deficit-source constitutive coupling, and does not claim that the recognition ratio is derived. After R1 closes, the remaining open join is lifting the abstract star deficit onto a concrete Regge deficit angle on an encoded triangulation of the recognition Freudenthal mesh; that triangulation field is not yet exposed.
proof idea
No proof: this is a structure declaration with three Bool fields. It is inhabited downstream by a single definition that hard-codes the current Wave B status (r1Closed := true, encodedFreudenthalLiftOpen := true, gap1BridgeDerived := false).
why it matters
Gives a ledger-safe, non-Prop status object for the geometric-deficit residual so completion state can be read without touching gap-1 or constitutive-coupling flags. The sole consumer is the module-local status value that freezes R1 as closed while keeping the encoded Freudenthal lift open and gap-1 underived. That split matches the module contract: R1 is the identification of mesh geometric deficit with star deficit under the Regge convention; the triangulation lift and gap-1 bridge remain separate open work. In the broader Recognition gravity stack this sits under the exact-$J$/true-Regge-Hessian bridge and the four-tet signed-deficit kernel, not under the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.