flatSqrtEdgeDeriv
plain-language theorem explainer
Per-edge derivative of square-root length with respect to squared length, evaluated on the six flat Freudenthal tetrahedron edges: 1/(2√a_f). Gate 0c of the Regge TT continuum-symbol campaign cites it as one of the three named shared-stencil objects both lanes must mirror. The body is the elementary closed-form calculus identity, not a derived lemma.
Claim. For each local edge index $f\in\{0,\ldots,5\}$, the flat sqrt-edge derivative is $\frac{d\sqrt{a}}{da}\big|_{a=a_f^{\mathrm{flat}}}=\frac{1}{2\sqrt{a_f^{\mathrm{flat}}}}$, where $a^{\mathrm{flat}}$ is the Freudenthal tetrahedron squared-edge tuple (three unit steps, two face diagonals, one body diagonal).
background
This module is Stage 2, Gate 0 / Lane A of the Regge TT continuum-symbol program: first-derivative structure of the true nonlinear Regge action at the flat point of a single tetrahedron, plus flat-neighborhood nondegeneracy. Nothing here approaches the continuum TT symbol value; that target stays open with Stage-1 status flag false.
The Freudenthal squared-edge tuple is the local six-edge data every tetrahedron of the unit-cube triangulation sees when the lattice is flat: three unit step edges, two face diagonals, and one body diagonal (values in ${1,2,3}$). Gate 0c packages three named stencil objects both analytic and numeric lanes must reference: that flat tuple, the closed-form flat angle Jacobian $\partial\theta_f/\partial a_k$, and these sqrt-edge derivatives.
The elementary identity $d\sqrt{x}/dx=1/(2\sqrt{x})$ is well-defined on the flat tuple because every squared edge is strictly positive.
proof idea
One-line definition: the real number $1/(2\sqrt{a_f})$ with $a$ the Freudenthal flat squared-edge tuple. No tactics, no lemmas, no reduction. Differentiability of $\sqrt{\cdot}$ at those positive points is discharged later by a separate theorem that applies the standard HasDerivAt rule for square root.
why it matters
Gate 0c deliverable: the third named component of the shared per-tetrahedron stencil. It is wired into the canonical stencil-moment record (flat squared edges, angle Jacobian, sqrt-edge derivatives), which Lane B numerics is required to mirror exactly. A sibling theorem then certifies that this constant is the genuine Fréchet derivative of Real.sqrt at each flat squared edge.
Downstream first-derivative assembly of the plane-wave Regge action profile at flat needs these factors whenever edge lengths enter through $\sqrt{a}$. The module explicitly does not prove second-derivative existence of the action profile (stage 2a) nor the continuum TT symbol; those remain open. Within Recognition Science gravity analysis this is scaffolding for the discrete-to-continuum TT gate, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.