near_path9_polys
plain-language theorem explainer
Along the near-orbit path that varies only squared edge slot 9, the four cleared-denominator Gram numerators (apex dot product, two apex norms, hinge Gram determinant) collapse to explicit quadratic polynomials in the path parameter t. Anyone differentiating the dihedral cosine at the flat point needs these identities. The proof is a direct simp-and-ring evaluation of the polynomial definitions on the path.
Claim. For every real $t$, if one replaces squared-edge coordinate $9$ of the near-orbit flat edge vector by $t$ and leaves the other nine coordinates fixed, then the apex-dot numerator equals $-8t+16$, the third-apex norm-squared numerator equals $4$, the fourth-apex norm-squared numerator equals $8$, and the hinge Gram determinant equals $8$ (all written as quadratics with vanishing $t^2$ coefficients where appropriate).
background
This module builds the full periodic-lattice star deficit kernel for the type-$(1,2)$ triangle hinge in 4D Regge calculus (masks $0,1,7$). It sits in the QG campaign after the type-$(1,1)$ seed orbit and reuses the committed Gram-projection / cleared-denominator cosine calculus without redefining its API.
The four numerators come from the dihedral kernel: hingeGramDet is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$ for the hinge edge-vectors; apexDotNum, apex3NormSqNum, and apex4NormSqNum are the numerators of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$, $|c'|^2\cdot\mathrm{hingeGramDet}$, and $|d'|^2\cdot\mathrm{hingeGramDet}$ for the apex projections orthogonal to the hinge plane. The path nearCoordPath 9 t freezes the near-orbit flat squared-edge vector except at index $9$, which is set to the free real parameter $t$. The flat background values are the fixed 10-tuple $(1,3,2,4,2,1,3,1,1,2)$.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine, then for each conjunct unfold the four numerator definitions together with nearCoordPath and nearFlatSqEdges by simp, and finish by ring. No external lemmas are required beyond definitional unfolding; the identities are pure polynomial arithmetic on the substituted edge vector.
why it matters
The lemma supplies the exact polynomial coefficients that feed hasDerivAt_near_slot9, which asserts
$$\mathrm{HasDerivAt}\bigl(t\mapsto\cos\mathrm{Dihedral}(\mathrm{nearCoordPath},9,t),;(-8)/(8\sqrt{2}),;2\bigr).$$
That derivative is one slot of the full-star deficit-class kernel on the 15 stencil classes (values $\pm\sqrt{2}/2$) for the type-$(1,2)$ hinge. The module's deliverable is the flat cosine multiset, the $2\pi$ flatness gate, and the nonvacuity / swap / scaling / homothety gates; this path identity is the algebraic fuel for the slot-9 derivative gate. It does not close the complementary type-$(2,1)$ orbit, the global flat Hessian, or S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.