freudenthalSchlaefliPolySummandNormTable
plain-language theorem explainer
A fully expanded 6×6 lookup table of rationalized Schläfli poly-summand norms on the Freudenthal tetrahedron edge set. Gravity and discrete-geometry proofs cite it whenever a closed-form coefficient is needed instead of re-evaluating the polynomial. The body is a pure match on edge indices, so every entry is a concrete real constant.
Claim. Define a table $T:\{0,\ldots,5\}\times\{0,\ldots,5\}\to\mathbb{R}$ by listing the evaluated rationalized Schläfli summand norms on the six squared edge lengths of the Freudenthal tetrahedron: $T(0,4)=-1$, $T(0,5)=2$, $T(1,1)=2$, $T(1,2)=-2$, $T(1,3)=-4$, $T(1,4)=4$, $T(1,5)=-2$, $T(2,1)=-3$, $T(2,2)=2$, $T(2,3)=6$, $T(2,4)=-3$, $T(3,1)=-2$, $T(3,2)=2$, $T(3,3)=2$, $T(3,4)=-2$, $T(4,0)=-2$, $T(4,1)=4$, $T(4,2)=-2$, $T(4,3)=-4$, $T(4,4)=2$, $T(5,0)=2$, $T(5,1)=-1$, and $0$ on all remaining pairs.
background
The Freudenthal–Kuhn triangulation splits the unit cube into six congruent tetrahedra. Each tetrahedron has six edges; their squared lengths form the fixed list freudenthalTetSqEdges. The Schläfli identity relates dihedral angles of a tetrahedron to those edge lengths via a rationalized polynomial summand (the “poly summand norm”).
This module packages the full $6\times 6$ evaluation of that summand on the Freudenthal edge set, together with the induced closed-form table for the local-pair Schläfli coefficients that appear in length-chain derivatives. The table is the concrete numerical skeleton on which later certificates rest: once every entry is named, equality proofs reduce to fin_cases and norm_num.
Downstream gravity code (axis stencil coefficients, six-tet cubic Dirichlet instances) reads these constants when assembling discrete Laplace or dihedral contributions along coordinate axes.
proof idea
Pure definition by exhaustive pattern match. Each pair of indices $(e,k)\in\mathrm{Fin},6\times\mathrm{Fin},6$ is assigned a literal real constant; there is no computation or lemma application inside the body. Later theorems such as freudenthalSchlaefliPolySummandNorm_eq_table discharge the claim that these literals equal the evaluated polynomial by citing one sibling lemma per cell.
why it matters
The table is the single source of truth for all Freudenthal Schläfli summand values used in the gravity stack. freudenthalSchlaefliPolySummandNorm_eq_table proves it matches the polynomial evaluator; snormRat_cast_eq_freudenthalSchlaefliTable equates a rational presentation to the same entries. Physical six-tet cubic Dirichlet lemmas (axisWitnessPairSummand_00, _10, _23, …) and axis-stencil coefficient certificates read the table when summing closed-form length derivatives along active edges. In the Recognition geometry pipeline this supplies the discrete dihedral data needed for cubic lattice gravity without re-deriving Schläfli polynomials at each call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.