starP
plain-language theorem explainer
Defines the one-parameter rim squared length p(h)=(3/2)(1-h) for the abstract four-tet hinge star at unit hinge and leg edges. Flat geometry sits at h=0 (p=3/2), where the common hinge dihedral cosine vanishes. Downstream nondegeneracy, cosine identity, signed deficit, and weak-field pair theorems all specialize through this slice. Pure algebraic abbreviation; no proof content.
Claim. For a real deformation parameter $h$, the rim squared edge length of the star is $p(h) = \frac{3}{2}(1-h)$. At $h=0$ one recovers the flat value $p=3/2$.
background
The module studies signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link. Squared-edge data are locked to $(l,m,m,m,m,p)$ with hinge edge 0; the kernel-checked slice is $l=m=1$.
On that slice the Cayley-Menger cofactor formula yields hinge dihedral cosine $q(p)=(3-2p)/3$. The flat closing value is $p_0=3/2$ (where $q=0$ and each dihedral is $\pi/2$). The linear family $p(h)=(3/2)(1-h)$ is chosen so that $q=h$ identically, converting the sign of the star-local deficit $2\pi-4\arccos(h)$ into the sign of the rational parameter $h$.
Realizability as a Euclidean tetrahedron is certified by strict positivity of the Cayley-Menger polynomial $\mathrm{cm}_3$, not by an embedded triangulation.
proof idea
Definitional abbreviation only: the body is the scalar expression $(3/2)\cdot(1-h)$. No tactics, no lemmas. Downstream proofs unfold this name and reduce by ring or nlinarith.
why it matters
This is the panel-locked deformation coordinate for the whole FourTetSignedDeficit development. It feeds star_q (hinge cosine equals $h$ exactly), fourTet_nondegenerate ($\mathrm{cm}_3>0$ for $|h|<1$), starDeficit and its convention note, star_mesh_bound, and the weak-field signed pair fourTet_weak_pair that certifies opposite-sign deficits at $\pm h^2$ without arccos numerics.
Outside the module it is cited by the gravity-side mesh geometric deficit convention check. In the broader Recognition geometry stack it supplies the first kernel-checked signed Regge deficit on an abstract 4-tet star, a local geometric ingredient for discrete curvature bookkeeping; it does not itself touch the T0-T8 forcing chain or the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.