starDeficit_convention_note
plain-language theorem explainer
Records that the star-local Regge deficit on the one-parameter four-tetrahedron hinge family equals $2\pi$ minus a sum of four equal dihedral angles at the shared hinge, matching the standard sum-over-incident-tets convention. Anyone aligning the abstract star deficit with the concrete Regge deficit-angle functional would cite this. The proof is pure bookkeeping: unfold the $4\cdot\theta$ definition and rewrite it as a constant sum over $\mathrm{Fin}\,4$.
Claim. For every real $h$, the star-local hinge deficit at parameter $h$ equals $2\pi$ minus the sum, over four indices in $\mathrm{Fin}\,4$, of the dihedral angle at hinge edge $0$ of the squared-edge star with rim length $p(h)=\frac{3}{2}(1-h)$.
background
The module builds signed Regge-convention deficits on an abstract four-tet star: four congruent tetrahedra share hinge AB in a closed 4-cycle link, given as squared-edge data (hinge and spokes fixed at 1, rim $p$) and certified nondegenerate by Cayley-Menger sign, not as an encoded triangulation.
The deformation $p(h)=\frac{3}{2}(1-h)$ forces the common dihedral cosine at AB to equal $h$. The star deficit is defined pointwise as $2\pi-4\theta(h)$, where $\theta$ is the repository dihedral angle from squared edges (arccos of the Cayley-Menger cosine on edge 0).
Upstream, hinge deficit is the classical $2\pi-\sum\theta$ (DihedralAngle and Schlaefli). The doc-comment frames this lemma as a convention note only: same $2\pi$ minus sum-over-incident-tets shape, same angle primitive, as the concrete Regge deficit angle; it does not build a triangulation instance.
proof idea
Unfold the star-deficit definition $2\pi-4\cdot\theta$. Rewrite the right-hand sum of a constant over $\mathrm{Fin},4$ via Finset.sum_const, Finset.card_univ, Fintype.card_fin, and nsmul_eq_mul, so the sum becomes $4\cdot\theta$. Close the numeral identity with norm_num. No geometric lemma is used.
why it matters
Keeps the abstract four-tet star deficit notationally aligned with the repository's $2\pi-\sum\theta$ Regge convention, so later comparison to the concrete deficit-angle functional is a pure rewrite rather than a definition chase. The module doc positions this file as the first kernel-checked signed Regge deficits on an abstract star in the weak-field regime; this note is the thin convention bridge inside that stack.
Doc-comment is explicit that the lemma is not a triangulation bridge: instantiating the concrete deficit on an encoded Triangulation3D remains future work. No downstream consumers are recorded yet. In the broader Recognition geometry track it supports discrete-curvature bookkeeping (hinge deficits feeding Regge-style action and ledger analysis) without claiming the full mesh embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.