areaGradB_t22
plain-language theorem explainer
On the flat triangle with squared edges (2,2,4), the Heron-area partial in the middle edge equals 1/4. Analysts wiring zero-momentum 4D Regge Hessians cite this closed gradient when assembling orbit-(2,2) true weights. The proof unfolds the algebraic gradient formula and substitutes the known unit area of that triangle.
Claim. For the flat triangle with squared edge lengths $a=2$, $b=2$, $c=4$, the $b$-partial of the Heron area is $\frac{a+c-b}{16\,A(a,b,c)}=\frac{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.
The Heron squared-area form is $A^2=(2ab+2bc+2ca-a^2-b^2-c^2)/16$. The $b$-gradient is the closed expression $(a+c-b)/(16A)$. Four flat triangle representatives are fixed: $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, $(2,2,4)$. Upstream, the area of the last representative is already proved equal to $1$ by reducing the squared Heron polynomial to $1$ and taking the positive square root.
proof idea
One-line wrapper: unfold the algebraic definition of the $b$-gradient, rewrite the denominator via the unit-area theorem for edges $(2,2,4)$, then finish by numeric normalization ($(2+4-2)/(16\cdot 1)=1/4$).
why it matters
Delivers the closed $b$-gradient on the type-$(2,2)$ flat representative, one of the four area-gradient evaluations required by deliverable A of the Regge flat Hessian campaign. Downstream, it is simp-inlined into the covariance identification that equates orbit-$(2,2)$ area-covector slots to the three partials, and it is simpa'd into the HasDerivAt theorem for $A(2,t,4)$ at $t=2$ with derivative $1/4$. Those derivatives feed the orbit-count-weighted sum $(dA\cdot c)(d\delta\cdot c)$ that kills pure gauge on the decoy modes at zero momentum. It does not touch the open finite-momentum folding or the still-unproved continuum EH limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.