pathGoodAt_zero
plain-language theorem explainer
At vanishing plane-wave amplitude the path is good: every edge length-squared is a positive displacement class, every tetrahedron is the Freudenthal cell with Cayley–Menger determinant 8, and every dihedral cosine lies strictly in (−1,1). Anyone differentiating the true Regge action along plane waves near flat cites this base point. The proof is a direct constructor split: simplify the affine edge field at t=0, then invoke Freudenthal positivity and the derivative-gate flat cosine bounds.
Claim. For any polarization $E:\{0,1,2\}^2\to\mathbb{R}$ and wavevector $k\in\mathbb{R}^3$, the plane-wave edge field at amplitude $t=0$ satisfies the goodness predicate: every periodic edge has positive length-squared, and every periodic tetrahedron has positive Cayley–Menger determinant with all six squared edge lengths positive and all six dihedral cosines strictly interior to $(-1,1)$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The object of study is the true Regge action profile along a plane-wave deformation of the flat lattice metric, with amplitude parameter $t$. Differentiability and the first- and second-variation formulae are stated only at amplitudes where the configuration is nondegenerate.
Goodness (PathGoodAt) packages exactly those nondegeneracy conditions: positive edge values under the plane-wave edge field, positive Cayley–Menger $cm_3$ on every periodic tetrahedron, and dihedral cosines strictly inside $(-1,1)$. At $t=0$ the edge field collapses to pure squared displacements, and every tetrahedron becomes the standard Freudenthal tetrahedron of the cube triangulation (whose $cm_3$ equals 8).
Upstream, the derivative gate already supplies flat cosine interior bounds and Freudenthal edge positivity; arithmetic identities zero_mul and add_zero clear the linear plane-wave terms at vanishing amplitude.
proof idea
Term-mode proof by constructor on the two conjuncts of goodness.
First conjunct (edge positivity): introduce an arbitrary periodic edge, simplify the plane-wave edge field at $t=0$ with zero_mul and add_zero, and apply periodicDispSqEdge_pos on the residual displacement class.
Second conjunct (tetrahedra): rewrite squared edges via planeWaveTetSqEdges_zero. The $cm_3$ goal becomes the Freudenthal identity cm3_freudenthalTetSqEdges, discharged by norm_num ($8>0$). For each of the six local faces, pair freudenthalTet.sqEdge_pos with ReggeTTDerivativeGate.flatCos_bounds to get positive squared lengths and strictly interior flat cosines.
why it matters
This is the base-point certificate that every subsequent flat-variation argument needs. Downstream, eventually_pathGoodAt lifts it by continuity to a neighborhood of $t=0$; hasDerivAt_planeWaveActionProfile and Gate A2(a) trueReggeAction_firstVariation_flat_eq_zero invoke it to justify differentiating the action at flat; firstVariationIntegrand_zero, hasDerivAt_reducedFirstVariation_flat, and edgeSqrtDeriv_differentiableAt all open with the edge-positivity half.
In the panel protocol this closes the nondegeneracy hypothesis of Gate A2: first variation vanishes at flat (Stage-1 kernel plus pathwise Schläfli kill), and the second variation reduces to a pure first-jet formula with no arccos second derivatives. It sits inside the gravity/Regge analysis lane rather than the T0–T8 forcing chain, but it is the concrete lattice realization of a flat background against which continuum TT symbols are extracted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.