areaGradA_t13
plain-language theorem explainer
Evaluates the partial derivative of triangle area with respect to the first edge length at the flat side lengths (1,3,4), equaling $\sqrt{3}/4$. Gravity analysts assembling the zero-momentum 4D Regge Hessian cite it for the type-(1,3) orbit. The proof unfolds the closed-form gradient, substitutes the known area value, and finishes by field simplification and arithmetic.
Claim. For the Heron area gradient $\partial A/\partial a = (b+c-a)/(16 A)$ at side lengths $a=1$, $b=3$, $c=4$, one has $\partial A/\partial a = \sqrt{3}/4$.
background
In 4D Regge calculus the second variation of the action pairs area gradients of triangular hinges with deficit-angle kernels. This module assembles those pieces at zero momentum (constant edge-class perturbation) for the flat 4-simplex, using committed orbit geometry rather than reverse-engineered Einstein–Hilbert weights.
The four flat triangle representatives are $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, and $(2,2,4)$. Area is the positive square root of the Heron quadratic $A^2=(2ab+2bc+2ca-a^2-b^2-c^2)/16$. The closed gradient formula areaGradA is $(b+c-a)/(16A)$. Upstream, hingeArea_t13 already records $A(1,3,4)=\sqrt{3}/2$.
proof idea
Unfold the definition of the gradient to $(3+4-1)/(16\cdot A(1,3,4))$. Rewrite the area via hingeArea_t13, obtaining $6/(16\cdot\sqrt{3}/2)$. After noting $\sqrt{3}\neq 0$, field_simp clears the denominator; squaring $\sqrt{3}$ and a final norm_num yield $\sqrt{3}/4$.
why it matters
This is one of the four explicit flat area-gradient evaluations listed under deliverable A of the Regge 4D flat Hessian assembly. Downstream, hasDerivAt_area_t13_a quotes it to certify HasDerivAt of $t\mapsto A(t,3,4)$ at $t=1$ with derivative $\sqrt{3}/4$, feeding the orbit-weighted sum that builds the true-weight zero-momentum Hessian.
That Hessian kills pure gauge (evaluations on decoy gauge and trace modes vanish), improving on the provisional weight-1 stencil. The result stays inside the zero-momentum, per-cell scope: it does not address Bloch phase folding, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.