sqrtEdge_planeWave_contDiffAt
plain-language theorem explainer
Along any plane-wave edge deformation, the map t ↦ √(edge length squared) is C^n-smooth at t = 0 for every finite order n. Gravity analysts cite this when assembling the nonlinear Regge action profile's smoothness. The proof applies ContDiffAt.sqrt to the already-smooth edge field and checks positivity at the flat point via the periodic displacement squared edge bound.
Claim. For every polarization matrix $E$, wave vector $k$, periodic edge $e$ on the $N^3$ lattice, and every extended natural $n$, the real function $t \mapsto \sqrt{\text{plane-wave edge field at }(t,e)}$ is continuously differentiable of order $n$ at $t = 0$.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign. The goal is local existence of the fixed-$N$ TT Bloch symbol for the true nonlinear Regge action along plane-wave families.
A plane-wave edge field deforms each squared edge length affinely through the flat Freudenthal background: at $t = 0$ the value equals periodicDispSqEdge, which takes values in ${1,2,3}$ and is therefore strictly positive. The square-root hinge factor of each edge in the Regge action is then well-defined in a neighborhood of the flat configuration.
Upstream, planeWaveEdgeValue_contDiff already gives that the unsquared edge field is $C^n$ everywhere (as an affine path). The positivity lemma periodicDispSqEdge_pos supplies the open condition needed to differentiate under the square root at the origin.
proof idea
Term-mode application of Mathlib's ContDiffAt.sqrt. First feed the edge-field smoothness from planeWaveEdgeValue_contDiff (converted to a pointwise ContDiffAt fact). The remaining side goal is that the edge field at $t = 0$ is nonzero. Unfolding planeWaveEdgeField and simplifying with zero_mul and add_zero reduces the value exactly to periodicDispSqEdge e.disp, which is strictly positive by periodicDispSqEdge_pos, hence nonzero.
why it matters
This is the square-root safety step in clause (c) of the module: every edge contribution to the nonlinear Regge action carries a $\sqrt{\ell^2}$ hinge factor, and those factors must be $C^n$ at the flat point before the full action profile can be. The sole downstream consumer is planeWaveActionProfile_contDiffAt, which sums the edge square roots against dihedral-angle terms and concludes that the plane-wave action $S(t)$ itself is ContDiffAt of every finite order at $t = 0$.
That smoothness is the hypothesis for the reusable centered-second-difference lemma, which identifies $S''(0)$ and thereby proves fixed-$N$ TT Bloch symbol existence (planeWave_TTBlochSymbolIs_secondVariation). In the broader QG campaign this closes Gate A1 Crux-1(c) without invoking any global $C^4$ continuum-limit route forbidden by the panel protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.