recognitionMeshGeometricDeficit4DStatus
plain-language theorem explainer
Status package for Wave B residual R1 on the 4D recognition mesh: residual R1 is marked closed, the encoded Freudenthal lift stays open, and the gap-1 bridge is not derived. Gravity auditors cite it to freeze the honest completion boundary after identifying mesh geometric deficit with the signed Regge star deficit. It is a pure structure instance with three boolean field assignments.
Claim. The 4D recognition-mesh geometric-deficit status record sets residual R1 closed ($\mathrm{true}$), the encoded Freudenthal lift open ($\mathrm{true}$), and the gap-1 bridge derived flag to $\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 and $\log x$-ratio. The DAG draft asked for an existential $\delta$ on a hinge carrier; Lean has no HingeCarrier, so the honest binding uses real deformation parameter $h$ with the four-tetrahedra signed star 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 structure packages three booleans: whether R1 is closed, whether the encoded Freudenthal lift remains open, and whether the gap-1 bridge has been derived. The open remainder is the lift of star deficit onto a concrete Regge deficit angle on an encoded triangulation of the recognition Freudenthal mesh; that join is not yet expressible because the mesh type has no triangulation field.
proof idea
Definitional structure instance: three field assignments only. No tactics, no lemmas. The values encode the module's honest boundary after the geometric-deficit identification lemmas (equality with star deficit and arcsin form, Regge convention, oddness, flat vanishing, sign) and the adversarial decoy separations.
why it matters
Freezes the completion boundary for residual R1 so downstream flag checks cannot silently overclaim. The sole consumer is the flags theorem, which asserts exactly these three values: R1 closed, encoded Freudenthal lift open, gap-1 bridge not derived. That matches the module contract: R1 does not flip the gap-1 bridge, does not inhabit constitutive deficit-source coupling, and does not claim recognition-ratio derivation. In the broader Recognition gravity stack this sits under the exact-$J$/true-Regge Hessian bridge and the Regge hinge 4D star kernel, keeping the geometric deficit on the phi-ladder side honest while the Freudenthal triangulation lift stays explicitly open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.