areaGradA_t11
plain-language theorem explainer
At the flat triangle with edge lengths (1,1,2), the Heron area gradient with respect to the first edge equals 1/4. Gravity analysts assembling the zero-momentum 4D Regge Hessian cite this closed value when wiring orbit-type (1,1) area factors into the second-variation quadratic. The proof is a one-line unfold of the gradient formula, substitution of the known area 1/2, and arithmetic.
Claim. For the flat triangle with edge lengths $a=1$, $b=1$, $c=2$, the Heron area gradient $\partial A/\partial a = (b+c-a)/(16A)$ evaluates to $1/4$.
background
This module assembles the zero-momentum per-cell Hessian of the 4D Regge action from committed star-deficit kernels and Heron area gradients, replacing the provisional weight-1 aggregate. Scope is constant edge-class perturbations only; finite-momentum Bloch folding remains open, and the work does not claim Einstein–Hilbert recovery.
Triangle area is the Heron form $A=\sqrt{(2ab+2bc+2ca-a^2-b^2-c^2)/16}$. The partial $\partial A/\partial a$ is packaged as $(b+c-a)/(16A)$. The four committed flat representatives are $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, and $(2,2,4)$.
Upstream, the area of the $(1,1,2)$ triangle is already fixed: $A(1,1,2)=1/2$, obtained by evaluating the squared Heron polynomial and taking the positive square root.
proof idea
One-line wrapper. Unfold the definition of the $a$-gradient, which is $(b+c-a)/(16A)$. Rewrite the denominator using the upstream evaluation $A(1,1,2)=1/2$, then finish by norm_num: numerator $1+2-1=2$ over $16\cdot(1/2)=8$ yields $1/4$.
why it matters
Delivers the first closed area-gradient value in deliverable A of the Regge flat Hessian campaign (explicit $\partial A/\partial a$ at each committed flat triangle). Downstream, it is the witness that the type-(1,1) covariance slot equals this gradient, and it supplies the derivative constant in the HasDerivAt theorem for $t\mapsto A(t,1,2)$ at $t=1$.
Those facts feed the orbit-count-weighted sum $(dA\cdot c)(d\delta\cdot c)$ over the six $S_4$ types (counts $72/48/48/24/24/24$) that defines the true-weight zero-momentum Hessian. With true weights the quadratic vanishes on pure-gauge decoys (provisional weight-1 did not). The result stays inside the zero-momentum tier; it does not close finite-momentum folding or the EH convergence gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.