edgeSqrtDeriv_differentiableAt
plain-language theorem explainer
At the flat background the edge sqrt-derivative factor of the plane-wave Regge profile is differentiable in the amplitude parameter. Anyone building the product-rule derivative of the reduced first variation cites this lemma. The proof writes the factor as a t-independent edge coefficient over twice the square root of the edge field, uses path-goodness positivity at zero, and applies the quotient rule.
Claim. For any amplitude matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wavevector $k\in\mathbb{R}^3$, and periodic edge $e$, the map $t\mapsto \ell'_e(t)/(2\sqrt{\ell_e(t)})$ (the closed-form edge sqrt-derivative factor of the plane-wave edge field) is differentiable at the flat point $t=0$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The plane-wave action profile $S(t)$ is the Regge action evaluated on a one-parameter family of edge lengths $\ell_e(t)$ built from a flat background plus a plane-wave amplitude $t$. At every good amplitude the first derivative admits the closed form
$S'(t)=\sum_e\bigl[(\ell'_e/(2\sqrt{\ell_e})),\delta_e+\sqrt{\ell_e},\delta'_e\bigr]$,
where the first coefficient is the edge sqrt-derivative factor treated here.
Path-goodness at zero (pathGoodAt_zero) guarantees every edge length is strictly positive on the flat background, so square roots and their derivatives are well-defined. The sibling hasDerivAt_sqrtEdge already supplies the derivative of $\sqrt{\ell_e(t)}$ at any good $t$. The edge coefficient itself is independent of $t$.
proof idea
Positivity of the plane-wave edge field at $t=0$ is immediate from path-goodness at zero. That feeds hasDerivAt_sqrtEdge, giving a derivative of $\sqrt{\ell_e(t)}$ at zero and hence differentiability of the denominator $2\sqrt{\ell_e(t)}$. The same positivity implies the denominator is nonzero. The numerator (edge coefficient) is constant in $t$, so the quotient rule yields differentiability of the full factor at zero.
why it matters
The sole downstream consumer is hasDerivAt_reducedFirstVariation_flat: the reduced first variation is a sum of products (sqrt-derivative factor)$\times$(deficit), and the product rule needs differentiability of each factor at flat. Only the $L'_e(0)\cdot\delta'_e(0)$ group survives there, because flat deficits vanish; the derivative of the sqrt-factor multiplies a zero deficit and never enters the reduced second-variation formula.
That reduced derivative is the bridge from Gate A2(a) (first variation vanishes at flat) to Gate A2(b) (Schläfli-reduced second variation expressed solely through flat slot sqrt-derivatives and the flat angle Jacobian). The pathwise Schläfli identity already kills every $\sqrt{\ell},\delta'$ summand identically near zero, so no second derivative of arccos appears. The lemma is pure analytic bookkeeping inside that chain; it does not itself invoke the Recognition forcing steps T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.