eventually_pathGoodAt
plain-language theorem explainer
Near zero amplitude, every plane-wave edge length stays positive and every tetrahedron stays nondegenerate with interior dihedral cosines. Anyone differentiating the Regge action profile along the TT plane-wave path needs this open neighborhood of good points. The proof is continuity of the affine edge paths plus the derivative gate's flat nondegeneracy neighborhood, combined by filter_upwards.
Claim. For any polarization $E:\{0,1,2\}^2\to\mathbb{R}$ and wavevector $k\in\mathbb{R}^3$, there is a neighborhood of amplitude $t=0$ on which the path is good: every periodic edge has strictly positive plane-wave length, and every periodic tetrahedron has positive Cayley–Menger volume, positive squared edge lengths, and dihedral cosines strictly in $(-1,1)$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign. The action profile is the true Regge action evaluated on a one-parameter plane-wave deformation of the flat edge field; first and second variations at flat are the Gate A2 targets.
PathGoodAt is the open condition under which every edge length is positive and every tetrahedron is nondegenerate with strictly interior dihedral cosines (via the Cayley–Menger polynomial cm3 and the cofactor cosine dihedralCos3Sq). At $t=0$ the path is the flat lattice, already known good by pathGoodAt_zero.
Upstream geometry supplies the periodic Freudenthal edge and tet types, the six squared-edge slots, and the flat nondegeneracy neighborhood from ReggeTTDerivativeGate.flat_nondegeneracy_eventually: near the flat squared-edge vector, cm3>0, edges stay positive, and cosines stay in $(-1,1)$.
proof idea
Split the predicate into edges and tets, prove each eventually, then combine.
Edges: rewrite with Filter.eventually_all. For each periodic edge, the plane-wave edge field is continuous in $t$ (from planeWaveEdgeValue_contDiff). At $t=0$ it is positive by pathGoodAt_zero, so Tendsto.eventually with eventually_gt_nhds keeps it positive near zero.
Tets: again eventually_all. Continuity of the six squared edges along the path (planeWaveTetSqEdges_contDiff), rewritten at zero via planeWaveTetSqEdges_zero, pushes forward the open flat nondegeneracy set from ReggeTTDerivativeGate.flat_nondegeneracy_eventually. A mono step packages the volume, edge, and cosine bounds into the tet clause of PathGoodAt.
filter_upwards on the two eventualities yields the conjunction.
why it matters
Gate A2 needs derivatives of the action profile not only at flat but on a punctured neighborhood, so that Schläfli cancellation of the $\sqrt{\ell},\delta'$ block holds identically near zero and no second derivative of $\arccos$ enters the two-jet. This theorem supplies the open set of good amplitudes on which those derivative formulas are stated.
The sole direct consumer is deriv_actionProfile_eventuallyEq_reduced: it filter-upwards this result and rewrites deriv S via hasDerivAt_planeWaveActionProfile at every good $t$, obtaining eventual equality with the reduced first variation. That reduced form is what feeds the pathwise Schläfli kill and the flat first- and second-variation gates (A2(a)–(b)).
In the broader QG campaign this is scaffolding hygiene rather than a new physical constant: it closes the analytic domain so the continuum TT symbol can be read off the Schläfli-reduced two-jet without arccos second derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.