meshGeometricDeficit_eq_starDeficit
plain-language theorem explainer
For every real deformation parameter, the mesh geometric deficit equals the star-local Regge hinge deficit built from squared-edge dihedral geometry. Gravity and QG residual workers cite this when discharging the Wave B R1 identification that the recognition mesh deficit is free of ratio fields. The proof is pure definitional equality (rfl).
Claim. For every real $h$, the mesh geometric deficit at $h$ equals the star-local Regge deficit $2\pi - 4\,\theta(h)$, where $\theta(h)$ is the common dihedral angle of the four congruent tetrahedra in the deformed star.
background
The module attacks Wave B residual R1: identify the recognition-mesh geometric deficit without xRatio or log-ratio fields. The honest carrier is a real deformation parameter, not a full HingeCarrier type (which Lean does not yet expose on the Freudenthal mesh).
Upstream, starDeficit h is the star-local Regge deficit at hinge AB: $2\pi$ minus four equal dihedral angles computed by dihedralAngle3Sq on the squared-edge star data starSq (starP h). It is odd, flat-vanishing, and sign-certified. The mesh-side name meshGeometricDeficit is defined by abbreviation as that same map, so the geometric content is squared-edge / dihedral only.
Local setting ties the mesh context to ExactJEqualsTrueReggeHessian on the canonical recognition mesh and to the banked Freudenthal seed flatness star_flat_angle_sum_two_pi. The open remainder is a later lift onto an encoded triangulation deficit angle; that join is not expressible yet.
proof idea
One-line term proof by rfl. Because meshGeometricDeficit is defined as starDeficit, the two functions agree definitionally at every real argument; no algebraic rewriting or external lemma is required.
why it matters
Records the R1 binding that the mesh geometric deficit is exactly the banked signed Regge-convention star deficit, free of ratio coordinates. That is the geometry-first closed form the Wave B DAG asked for under the honest carrier ℝ, and it underwrites sibling facts (arcsin closed form, Regge convention, oddness, flat vanishing, sign) and the typed-residual identification theorems in the same module.
In the Recognition gravity stack this keeps the deficit on pure dihedral geometry rather than CPT ratio fields, consistent with the module's refusal to flip gap1_bridge_derived, inhabit constitutive coupling, or claim recognition_ratio_derived. The remaining open path is lifting starDeficit onto ReggeActionConcrete.deficitAngle for an encoded Freudenthal triangulation; that is flagged only by encodedFreudenthalLiftOpen, not by this equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.