meshGeometricDeficit
plain-language theorem explainer
Names the mesh geometric deficit as the signed Regge-convention star deficit of four congruent tetrahedra, a real function of a single deformation parameter. Gravity and QG residual work cite it as the xRatio-free geometric channel in dual-entry constitutive couplings. The body is a one-line alias of the banked star deficit from squared-edge dihedral geometry.
Claim. Define the mesh geometric deficit $\delta:\mathbb{R}\to\mathbb{R}$ by $\delta(h)=2\pi-4\,\theta_3^{\mathrm{sq}}(\mathrm{starSq}(\mathrm{starP}(h)),0)$, i.e. twice $\pi$ minus four equal dihedral angles of the congruent incident tetrahedra at the hinge, computed from squared-edge star data. No edge-length ratio or logarithm enters the definition.
background
Wave B residual R1 in the QG completion session identifies a mesh geometric deficit free of edge-length ratios and logarithms. The DAG draft asked for a signed Regge-convention hinge deficit on a recognition Freudenthal mesh carrier; Lean has no HingeCarrier type and the mesh does not yet expose a per-hinge deformation family, so the honest binding uses a real deformation parameter with the banked four-tetrahedron star construction.
Upstream, the star-local Regge deficit is $2\pi$ minus the sum of four equal dihedral angles of congruent incident tetrahedra, each from dihedralAngle3Sq on squared-edge star data. That object is odd, vanishes when flat, and carries a sign certificate. Mesh context is supplied separately by the exact-$J$/true-Regge Hessian bridge on the canonical recognition mesh and by Freudenthal seed flatness (star angle sum $2\pi$).
This module records that identification only. It does not flip the gap-1 bridge flag, inhabit a full deficit-source constitutive coupling, or claim a derived recognition ratio.
proof idea
One-line definitional alias: the mesh geometric deficit is definitionally equal to the upstream star deficit. No tactics, no rewriting, no new geometry. Downstream lemmas then inherit oddness, flat vanishing, the arcsin closed form, and the Regge convention note from that identification.
why it matters
Closes Wave B residual R1: a named, xRatio-free geometric deficit channel for the recognition mesh. Downstream dual-entry coupling (R4) installs it as the geometricDeficit field of a DeficitSourceConstitutiveCoupling, with source equal to $\kappa\cdot\delta$ and magnitude $|\delta|$ on a single mesh channel. Adversarial decoy theorems use its oddness to rule out magnitude-only and even-function substitutes on a punctured interval.
In the broader RS gravity stack this is the geometric half of the constitutive product that feeds typed residual closure for deficit-source coupling. It sits under the Regge hinge / exact-$J$ bridge rather than under the T0–T8 forcing chain directly. Open remainder (explicitly flagged): lift the star deficit onto a concrete triangulation deficitAngle of the recognition Freudenthal mesh; that join is not yet expressible and is recorded only by an open-lift flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.