far_path3_polys
plain-language theorem explainer
Along the far-orbit edge path that varies only squared-length slot 3, the four cleared-denominator Gram numerators (apex dot product, two apex norms, hinge Gram determinant) are explicit quadratic polynomials in the path parameter t. Anyone differentiating the dihedral cosine along that path cites these identities. The proof is a direct simp-and-ring expansion of the four numerator definitions on the far flat edge vector.
Claim. For every real $t$, if one deforms only squared-edge coordinate $3$ of the far flat squared-length vector along the path $t\mapsto a(t)$, then the cleared-denominator apex inner-product numerator equals $8t-16$, the first apex-norm numerator equals the constant $8$, the second apex-norm numerator equals $-2t^2+8t-4$, and the hinge Gram determinant equals the constant $8$.
background
This module builds the full periodic-lattice star deficit kernel for the type-$(1,2)$ triangle hinge ${0,e_0,e_0+e_1+e_2}$ 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 cosine calculus rather than redefining it.
The four polynomials 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}$ and $|c'|^2\cdot\mathrm{hingeGramDet}$, $|d'|^2\cdot\mathrm{hingeGramDet}$ for the apex projections orthogonal to the hinge plane. The far flat squared-edge vector is the fixed 10-tuple $(1,3,1,2,2,2,1,4,1,3)$; farCoordPath 3 t replaces only slot $3$ by the free parameter $t$.
proof idea
Introduce the real parameter $t$. Split the four-way conjunction with refine, then on each conjunct unfold apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, farCoordPath, and farFlatSqEdges by simp and finish by ring. No external lemmas beyond those definitions are required; the identities are pure polynomial arithmetic on the far flat edge data.
why it matters
The lemma feeds hasDerivAt_far_slot3, which asserts that the dihedral cosine along this far path is differentiable at $t=2$ with derivative $8/(8\sqrt{2})$. That derivative is one coordinate of the full-star deficit class kernel on the 15 stencil classes (values $\pm\sqrt{2}/2$) for the type-$(1,2)$ hinge orbit.
In the module's deliverable list this is part of the kernel-checked increment after the type-$(1,1)$ seed: flat cosine multiset, flatness gate $4\cdot\arccos 0=2\pi$, and the subsequent gates (nonvacuity, swap symmetry, scaling decoy, homothety stationarity). It does not close the complement type-$(2,1)$ orbit, the remaining hinge orbits, flat Hessian assembly, or S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.