far_path1_polys
plain-language theorem explainer
Along the far flat squared-edge orbit, deforming stencil slot 1 by a real parameter t makes the four cleared Gram numerators (apex inner product, two apex norms, hinge Gram determinant) into explicit quadratic polynomials in t. Anyone differentiating the far-orbit dihedral cosine at the flat point needs these expansions. The proof is pure simplification plus ring normalization of the four polynomial identities.
Claim. For every real $t$, if $a(t)$ is the far flat squared-edge 10-tuple with coordinate $1$ replaced by $t$, then the apex-dot numerator equals $-4t+12$, the third-apex norm-squared numerator equals $-2t^2+12t-10$, the fourth-apex norm-squared numerator equals $-t^2+6t-5$, and the hinge Gram determinant equals $-t^2+6t-1$.
background
This module is the type-$(1,2)$ full-star kernel for a Regge 4D triangle hinge on the periodic Freudenthal lattice (masks $0,1,7$). It enumerates the four incident 4-simplices, checks flat cosines, and builds the 15-class deficit stencil; it does not yet assemble the global flat Hessian or recover Einstein–Hilbert.
Squared edge lengths live in a 10-slot stencil SqEdges4. The far flat background farFlatSqEdges is one of the two local squared-length orbits on the star. The path farCoordPath 1 t freezes that background and varies only slot $1$.
Dihedral data are computed in cleared-denominator form: 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 the projected apex inner product and norms times that determinant. Together they feed the committed cosDihedral calculus.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine, then on each goal unfold the four numerator definitions together with farCoordPath and farFlatSqEdges. After substitution the expressions are ordinary polynomials in $t$; ring normalizes each to the stated monic form. No external lemmas beyond definitional unfolding are required.
why it matters
The sole downstream consumer is hasDerivAt_far_slot1, which feeds these exact coefficient tuples into the generic one-slot derivative lemma hasDerivAt_far_slot to obtain
$$\frac{d}{dt}\cos\mathrm{Dihedral}(\mathrm{farCoordPath},1,t)\Big|_{t=3}=\frac{-4}{8\sqrt{2}}.$$
That derivative is part of the full-star deficit class kernel on the type-$(1,2)$ hinge orbit (deliverable A of the module): flatness gate, nonvacuity, and the $\pm\sqrt{2}/2$ stencil values. In the broader QG campaign this is the next kernel-checked increment after the type-$(1,1)$ seed orbit; complement type $(2,1)$ and the remaining hinge orbits stay open, and nothing here closes S_RS_converges_EH_4d or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.