typedResidual_mesh_geometricDeficit_identified_closed
plain-language theorem explainer
Closes residual R1 of the QG Wave B gap list: the mesh geometric deficit is identified with the signed Regge star deficit on a real deformation parameter, free of any x-ratio. Gravity analysts working the recognition-mesh bridge cite it to discharge that DAG residual. The proof is a direct existential package of the star deficit with its oddness, flat-vanishing, sign certificate, exact-J/Regge Hessian identity, and Freudenthal seed flatness at 2π.
Claim. There exists $\delta:\mathbb{R}\to\mathbb{R}$ equal to the star-local Regge deficit such that $\delta$ is odd, $\delta(0)=0$, $\operatorname{sign}(\delta(h))=\operatorname{sign}(h)$ for $h\neq 0$, the exact-$J$ amplitude Hessian equals the mesh true-Regge Hessian on the canonical recognition mesh, and the Freudenthal seed star angle sum equals $2\pi$.
background
Wave B residual R1 asks that the recognition-mesh geometric deficit be identified without any $x$-ratio or $\log x$-ratio. The module records an honest carrier reshape: Lean has no HingeCarrier, so the deformation parameter is plain $\mathbb{R}$, and the deficit is the star-local Regge quantity from four-tet squared-edge geometry.
That quantity, $\mathrm{starDeficit}(h)=2\pi-4,\theta_{\mathrm{dih}}(\mathrm{starSq}(\mathrm{starP},h))$, is the signed Regge-convention hinge deficit (four equal dihedrals of congruent incident tetrahedra). Upstream lemmas already give oddness, vanishing at the flat value $h=0$, and the sign certificate (sign of deficit equals sign of the rational hinge cosine $h$).
Mesh context is supplied by the exact-$J$ equals true-Regge Hessian identity on the canonical recognition mesh, plus the banked Freudenthal seed fact that the flat star angle sum is $2\pi$. The residual Prop packages exactly those six conjuncts as an existential over $\delta$.
proof idea
Term-mode existential package via refine. Witness is starDeficit with definitional equality rfl. Oddness and flat-vanishing are the upstream theorems starDeficit_odd and starDeficit_flat. The sign goal is discharged by intro h; exact fourTet_deficit_sign h. The last two conjuncts are the already-proved bridge exactJEqualsTrueReggeHessian_holds and the seed lemma star_flat_angle_sum_two_pi. No further algebra.
why it matters
Discharges DAG residual R1 ("mesh geometricDeficit identified, no xRatio") from the QG Wave B gap plan. Downstream, the PascalCase alias of the same name is a one-line re-export matching the residual title for DAG bookkeeping.
In the Recognition gravity stack this pins the geometric side of the exact-$J$/Regge star bridge: deficit is the classical Regge $2\pi-\sum\theta$ object on the four-tet star, not a ratio-log decoy. It does not yet flip gap1_bridge_derived, inhabit constitutive coupling, or claim recognition-ratio derivation.
Open remainder (explicitly not a Prop shell): lift starDeficit onto ReggeActionConcrete.deficitAngle on an encoded triangulation of the recognition Freudenthal mesh. That join is currently inexpressible; the module only records encodedFreudenthalLiftOpen := true.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.