far_path7_polys
plain-language theorem explainer
Along the far-cube squared-edge path that varies only stencil slot 7, the four cleared-denominator Gram numerators (apex inner product, two apex norms, hinge Gram determinant) are explicit quadratics in the path parameter t. Downstream derivative lemmas for the dihedral cosine cite these identities to obtain a concrete HasDerivAt value at the flat point. The proof is pure algebraic simplification after unfolding the path and numerator definitions.
Claim. For every real $t$, if $a(t)$ is the far-cube squared-edge 10-vector equal to the flat far configuration except that stencil coordinate $7$ is set to $t$, then the cleared-denominator apex inner-product numerator is $4t-16$, the first apex-norm numerator is $-t^2+8t-8$, the second apex-norm numerator is the constant $4$, and the hinge Gram determinant is the constant $8$.
background
This module builds the full periodic Freudenthal star kernel for the type-(1,2) triangle hinge in 4D Regge calculus (masks 0,1,7). Squared edge lengths live in a 10-slot stencil SqEdges4. The far cube contributes one local squared-length orbit farFlatSqEdges with fixed values (slot 7 equals 4 at flatness). The one-parameter path farCoordPath 7 t replaces only that slot by the real parameter $t$, holding the other nine edges at their far-flat values.
Dihedral cosine is computed from Gram data via cleared-denominator numerators imported 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 pair; apexDotNum, apex3NormSqNum, and apex4NormSqNum are the corresponding numerators for the projected apex inner product and squared norms (each scaled by the hinge Gram factor). Explicit polynomial control of these four quantities along each stencil path is the algebraic input to differentiation of cosDihedral.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine, then on each goal unfold apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, farCoordPath, and farFlatSqEdges by simp and finish by ring. No external lemmas beyond definitional unfolding are required; the identities are pure polynomial arithmetic on the substituted far-flat constants.
why it matters
The sole consumer is hasDerivAt_far_slot7, which feeds the four coefficient triples from this lemma into the generic path-derivative theorem hasDerivAt_far_slot and obtains
HasDerivAt (fun t => cosDihedral (farCoordPath 7 t)) (4/(8√2)) 4
at the flat value $t=4$. That derivative is part of the type-(1,2) full-star deficit-class kernel campaign: after star enumeration and flat cosine multiset (all four simplices have flat cosine 0), one needs first-order control of dihedral angles under each of the 15 stencil edge moves to assemble the deficit-class kernel values $\pm\sqrt{2}/2$ and the listed gates (nonvacuity, swap symmetry, uniform-scaling decoy, homothety stationarity).
The module explicitly does not close flat Hessian assembly over all hinges, does not prove $S_{RS}$ converges to Einstein–Hilbert in 4D, and leaves the complement orbit (2,1) open. This lemma is a local algebraic brick inside that kernel-checked increment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.