star_mesh_bound
plain-language theorem explainer
For the one-parameter four-tet hinge star at deformation parameter h with |h|≤1, every squared edge is at most 3. The weak-field signed-deficit pair certificate cites this as mesh control on both deformed configurations. Proof: case-split on the six edges; five are identically 1, and the rim edge is bounded by linear arithmetic from |h|≤1.
Claim. Let $p(h)=\tfrac{3}{2}(1-h)$ be the rim squared-length of the four-tet star (hinge and legs fixed at squared length $1$). If $|h|\le 1$, then every squared edge of that configuration is at most $3$.
background
The module builds 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 the panel $(l,m,m,m,m,p)$ with hinge edge $0$; the kernel-checked slice is $l=m=1$. The rim parameter is the one free length $p$.
At $l=m=1$ the flat value is $p_0=3/2$ (hinge cosine $q=0$, dihedral $\pi/2$, four copies close flat). The deformation family used here is $p(h)=\tfrac{3}{2}(1-h)$, so the configuration map starP/starSq places five squared edges at $1$ and the sixth at $p(h)$. The common hinge cosine collapses to $q=h$, and the star-local Regge deficit is $2\pi-4\arccos(h)$.
A mesh bound is the elementary size control needed before quoting deficit signs, antisymmetry, or Cayley–Menger nondegeneracy on the same family: no edge may run away while $|h|\le 1$.
proof idea
Unpack $|h|\le 1$ into $-1\le h\le 1$. Unfold the rim map and apply nonlinear arithmetic to get $p(h)\le 3$. Case-split on the six edge indices (fin_cases). The first five goals are the constant edges $1\le 3$ (norm_num). The last goal is exactly the rim bound already proved. No dihedral, Cayley–Menger, or deficit lemmas are used.
why it matters
This is the mesh clause in the module’s weak-field signed-pair certificate (fourTet_weak_pair, Test B): for $0<h<1$ the pair of configurations at deformation $\pm h^2$ must have all squared edges $\le 3$, alongside rational hinge cosines $\pm h^2$, opposite deficit signs, exact antisymmetry, cm3>0, and the magnitude bound $|\mathrm{deficit}|\le 2\pi h^2$.
In the broader Recognition geometry stack the result is local infrastructure, not a forcing-chain step (T0–T8). It keeps the first kernel-checked signed Regge deficits on an abstract four-tet star inside a uniform edge-size window, so later curvature and continuum comparisons are not polluted by uncontrolled mesh growth. It does not itself produce continuum Regge calculus or a global Triangulation3D embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.