starDeficit_flat
plain-language theorem explainer
The star-local Regge deficit on the abstract four-tetrahedron hinge vanishes at the flat deformation parameter h=0 (equatorial length p=3/2). Anyone identifying mesh geometric deficit with this star family, or closing the R1 residual package, cites this base point. Proof is a short rewrite through the closed arcsin form plus arcsin(0)=0.
Claim. The star-local Regge deficit of the four-tetrahedron hinge equals zero at vanishing deformation: $\delta_\star(0)=0$. Equivalently, when the equatorial squared edge is the flat value $p=3/2$, the four equal dihedral angles at the hinge sum exactly to $2\pi$.
background
This module builds signed Regge-convention deficit angles on an abstract four-tet star: four congruent tetrahedra sharing hinge AB, given as squared-edge data and certified nondegenerate by Cayley-Menger ($\mathrm{cm}_3>0$). It is not a full Triangulation3D embedding. On the kernel-checked slice $\ell=m=1$, the common dihedral cosine is $q(p)=(3-2p)/3$; the flat equatorial length is $p_0=3/2$ (so $q=0$ and each dihedral is $\pi/2$).
The one-parameter family $p(h)=(3/2)(1-h)$ forces $q=h$. The star deficit is $2\pi$ minus four times the common dihedral at AB (the same $2\pi-\sum\theta$ convention as the hinge deficit elsewhere in the geometry stack). Upstream, that quantity equals $4\arcsin h$ identically, so the sign of the deficit is the sign of the rational parameter $h$ with no interval arithmetic.
proof idea
One short tactic proof. Rewrite the goal by the closed-form identity $\delta_\star(h)=4\arcsin h$, apply $\arcsin 0=0$, and finish with ring. No case splits and no appeal to dihedral bounds beyond that identity.
why it matters
Base point of the signed four-tet deficit family: flat geometry has zero hinge deficit. Downstream, the 4D recognition-mesh geometric deficit is identified with this star deficit, so its flat vanishing is exactly this theorem (one-line alias). The same fact is packaged into the R1 closure that records oddness, flat vanishing, sign control, the exact $J$-equals-true-Regge Hessian, and the flat angle sum $2\pi$.
In the broader gravity analysis stack this anchors the weak-field story that the mesh geometric residual is a genuine signed Regge deficit (positive one side of flat, negative the other), not an unsigned cost. It is local geometry scaffolding for hinge-aware zero modes and continuum smearing arguments, not a global Einstein-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.