starSq
plain-language theorem explainer
Squared-edge assignment for one tetrahedron in the abstract four-tet hinge star: hinge and four spokes fixed at squared length 1, rim free at parameter p. Anyone citing the kernel-checked dihedral cosine q=(3-2p)/3 or the signed Regge deficit family uses this as the input configuration. Pure Fin-6 pattern match; no proof content.
Claim. For $p \in \mathbb{R}$, define the squared-edge map $a : \{0,\ldots,5\} \to \mathbb{R}$ by $a(i)=1$ for $i=0,\ldots,4$ and $a(5)=p$. Equivalently $(a_0,a_1,a_2,a_3,a_4,a_5)=(1,1,1,1,1,p)$, with hinge AB as edge 0.
background
The module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tetrahedra around a common interior edge AB in a closed 4-cycle link. Each tet is specified only by squared-edge data, not by a coordinate embedding or a Triangulation3D instance.
SqEdges is the type of maps from six edge indices to reals (the six squared lengths of a tetrahedron). In the repository convention, vertex 0 = A, vertex 1 = B, and vertices 2,3 are the equatorial pair, so the general panel is $(l,m,m,m,m,p)$ with hinge edge 0. This definition locks the kernel-checked slice $l=m=1$, leaving only the rim squared length $p$ free.
The flat closing value is $p_0=3/2$ (hinge dihedral cosine zero, angle $\pi/2$). The deformation family later sets $p(h)=(3/2)(1-h)$ so the cosine equals $h$ exactly and the deficit sign tracks $\mathrm{sign}(h)$ without evaluating arccos.
proof idea
Definition by exhaustive match on Fin 6: indices 0 through 4 return the constant 1; index 5 returns the parameter $p$. The residual case $n+6$ is discharged by absurd plus omega (impossible index). No lemmas are invoked; the body is the data.
why it matters
This is the configuration carrier for the whole four-tet signed-deficit development. Downstream, star_cm3 evaluates the Cayley-Menger polynomial to $2p(3-p)$; the cofactor theorems (star_cofactor_33, star_cofactor_34, star_cofactor_44) feed fourTet_centralDihedralCosine, which proves the hinge cosine equals $(3-2p)/3$. Nondegeneracy (fourTet_nondegenerate), the regular sanity anchor at $p=1$ (cosine $1/3$), and the weak-field signed pair (fourTet_weak_pair) all instantiate this map.
In the broader Recognition geometry stack it supplies the first kernel-checked signed Regge deficit on an abstract star, with explicit mesh bounds and no interval arithmetic. It does not itself touch the T0-T8 forcing chain or the mass ladder; it is local discrete-geometry infrastructure for curvature sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.