hasDerivAt_opp_slot7
plain-language theorem explainer
Along the path that varies only opposite squared-edge slot 7 of the seed hinge, keeping all other edges flat, the dihedral cosine has derivative zero at the flat value t=4. The full opposite-coordinate stationarity theorem cites this as the Fin-10 case k=7. The proof feeds the class-7 Gram polynomials into the generic opposite-slot derivative lemma and clears the resulting algebraic identity by ring.
Claim. Let $\gamma_7(t)$ be the squared-edge assignment that sets opposite slot $7$ to $t$ and leaves every other opposite edge at its flat lattice value. Then $t \mapsto \cos\theta(\gamma_7(t))$, the seed-hinge dihedral cosine inside the corresponding 4-simplex, is differentiable at the flat point $t=4$ with derivative $0$.
background
This module is the next kernel-checked increment of the QG full-theory campaign after the two-simplex dihedral cosine calculus. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star (four unit cubes, six incident 4-simplices) in the integer lattice.
cosDihedral is the cosine of the seed-hinge dihedral angle inside one 4-simplex: apex-dot over the product of apex 3- and 4-norms. oppCoordPath k t freezes every opposite squared edge at its flat value except slot $k$, which is set to the real parameter $t$. Flat slot 7 sits at value 4.
The private lemma opp_path7_polys records the exact quadratic polynomials of the cleared-denominator Gram numerators along that path: apex-dot numerator is the constant 8, apex-3-norm numerator is $-t^2+8t-8$, apex-4-norm numerator is the constant 4, and the hinge Gram determinant is the constant 4. The generic hasDerivAt_opp_slot turns any such polynomial triple into a HasDerivAt statement for the dihedral cosine.
proof idea
One-shot application of the generic opposite-slot derivative lemma. Instantiate hasDerivAt_opp_slot at $k=7$, evaluation point $t_0=4$, with the twelve real coefficients read off opp_path7_polys (constants $0,0,8$ for the apex-dot numerator; $-1,8,-8$ for apex-3-norm; $0,0,4$ for apex-4-norm; $0,0,4$ for the Gram determinant). Four norm_num side goals discharge the arithmetic hypotheses of that lemma. The resulting derivative expression is converted to the target value $0$ by a one-line ring identity.
why it matters
Feeds the case split inside hasDerivAt_opp_coord, which asserts that every opposite-coordinate path has dihedral-cosine derivative equal to the opposite cosine kernel at the flat edge. That theorem is one of the stationarity gates of deliverable A in the module doc: the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, together with nonvacuity, swap-$2\leftrightarrow 3$ symmetry, uniform-scaling decoy, and homothety stationarity.
In the broader Recognition gravity stack this is pure Regge calculus infrastructure: it certifies that the flat lattice is a critical point of the star deficit under opposite-edge variations of class 7. It does not yet assemble the flat Hessian over all hinges, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4d, or flip gap_action_recovery. Other hinge orbits of the lattice remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.