apex3NormSqNum_t13
plain-language theorem explainer
For the type-(1,3) flat squared-edge data on a 4D Regge triangle hinge, the cleared-denominator numerator of the squared third-apex norm times the hinge Gram determinant equals 8. Cosine-of-dihedral evaluations at the flat point cite this constant. The proof is a one-line numerical unfolding of the polynomial definitions.
Claim. On the flat type-$(1,3)$ local squared-edge assignment (hinge slots ordered so the triangle occupies indices $0,1,2$), the numerator of $|c'|^2$ times the hinge Gram determinant equals $8$.
background
This module builds the type-$(1,3)$ star deficit kernel for 4D Regge calculus on the periodic Freudenthal lattice. The hinge is the triangle with absolute masks ${0,1,15}$ (difference masks $(1,14)$, flat squared lengths $(1,3,4)$); six Kuhn simplices in the origin cube meet it, and the complementary type $(3,1)$ remains open for transport.
The hinge Gram determinant is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$ for the two hinge edge-vectors from vertex 0 (four times the squared hinge-area factor). The apex-3 norm-squared numerator is the cleared-denominator polynomial for $|c'|^2$ times that determinant, with $c'$ the projection of the third apex orthogonal to the hinge plane.
The flat squared-edge 10-tuple used here reorders every star member so the hinge occupies slots $(0,1,2)$ and the two apexes follow Freudenthal chain order: values $(1,4,2,3,3,1,2,2,1,1)$.
proof idea
One-line wrapper: norm_num unfolds the three definitions (apex-3 norm-squared numerator, hinge Gram determinant, and the flat type-$(1,3)$ squared-edge assignment) and evaluates the resulting rational arithmetic to the constant 8.
why it matters
Feeds the flat cosine identity for this configuration: the dihedral cosine is rewritten in numerator form, and this constant (together with the matching apex-4 numerator and the Gram determinant value) cancels to give $\cos=1/2$. That identity is the shared Gram input for the six-simplex flat cosine multiset, which forces the star angle sum $6\cdot\arccos(1/2)=2\pi$ (flatness gate) and the subsequent ten coordinate derivatives at the cleared-denominator point $(N,P,Q)=(8,8,8)$.
Inside the QG full-theory campaign this is a kernel-checked increment after the type-$(1,1)$ seed orbit: it supplies the numerical hinge of the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$. It does not yet assemble the flat Hessian over all hinges, prove continuum EH recovery, or close the action-gap flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.