PathGoodAt
plain-language theorem explainer
Goodness of a plane-wave Regge amplitude at path parameter t: every periodic edge length is positive, every tetrahedron is nondegenerate (positive Cayley–Menger volume), and every dihedral cosine is strictly interior. Downstream derivative and Schläfli-kill theorems take this predicate as their domain hypothesis. Pure definitional conjunction of positivity and interior-angle bounds on the affine edge field.
Claim. For amplitude matrix $E$, wavevector $k$, and path parameter $t\in\mathbb{R}$, the path is good at $t$ when: (i) every periodic edge value of the plane-wave edge field is strictly positive; (ii) for every periodic tetrahedron $\tau$, the Cayley–Menger cubic $\mathrm{cm}_3$ of its six squared edge lengths is positive; (iii) each of those six squared lengths is positive; and (iv) each squared dihedral cosine of $\tau$ lies in $(-1,1)$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. It studies the true Regge action along a plane-wave edge-length path on the periodic $N^3$ lattice, aiming at the first and second variations at the flat background.
The plane-wave edge field is an affine path in edge lengths parameterized by $t$, with polarization $E$ and wavevector $k$. Geometric ingredients are the Cayley–Menger cubic $\mathrm{cm}_3$ (nondegeneracy of a tetrahedron from its six squared edge lengths) and the squared dihedral cosines $\mathrm{dihedralCos3Sq}$ built from the same data. Deficits and the Regge action are only classically differentiable when edges stay positive and angles stay interior.
The predicate packages exactly those open conditions so that later theorems can differentiate edge sqrts, slot angles, and edge deficits without leaving the smooth locus.
proof idea
Definitional: a single Prop that is the conjunction of universal quantifiers over periodic edges and tetrahedra. No proof obligations. The edge clause demands strict positivity of the plane-wave edge field; the tet clause demands $\mathrm{cm}_3>0$, positive squared edge lengths on all six slots, and $-1<\mathrm{dihedralCos3Sq}<1$ on each face index.
why it matters
Gate A2 needs a uniform domain on which the action profile is differentiable and the pathwise Schläfli identity applies. This predicate is that domain. It is discharged at flat by pathGoodAt_zero (Freudenthal tet, $\mathrm{cm}_3=8$, interior flat cosines) and extended to a neighborhood by eventually_pathGoodAt.
Every major theorem in the module takes it as hypothesis: hasDerivAt_planeWaveActionProfile (closed-form $S'(t)$), hasDerivAt_deficit, the pathwise Schläfli kill sum_sqrt_deficitDeriv_eq_zero (which erases the entire $\sum\sqrt{l_e},\delta'_e$ group and all arccos second derivatives from the second variation), and the reduction firstVariationIntegrand_eq_reduced. Without it, Gate A2(a)–(b) (vanishing first variation and Schläfli-reduced second variation at flat) have no legitimate differentiation site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.