areaGradC_t22
plain-language theorem explainer
For the flat triangle with edge lengths (2,2,4), the closed-form Heron partial of area with respect to the third edge vanishes. Gravity analysts assembling the zero-momentum 4D Regge Hessian cite this as the type-(2,2) area gradient on the c-slot. The proof unfolds the gradient formula, substitutes the unit hinge area, and evaluates by arithmetic.
Claim. At the flat triangle with edge lengths $a=2$, $b=2$, $c=4$, the $c$-partial of Heron area equals zero: $\partial A/\partial c = (a+b-c)/(16A) = 0$.
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 stencil. Scope is constant edge-class perturbations only; finite-momentum Bloch folding remains open.
Heron area is $A=\sqrt{(2ab+2bc+2ca-a^2-b^2-c^2)/16}$. The closed $c$-gradient is $\mathrm{areaGradC}(a,b,c)=(a+b-c)/(16A)$. The four flat triangle representatives are $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, and $(2,2,4)$.
Upstream, $\mathrm{hingeArea},2,2,4=1$ is already proved by reducing the squared Heron polynomial to $1$ and taking the positive square root. That unit area is the only geometric input needed here.
proof idea
One-line wrapper: unfold the definition of the $c$-gradient, rewrite the denominator via the unit-area lemma for edges $(2,2,4)$, then finish by norm_num. Numerator $2+2-4=0$ forces the whole fraction to zero once the area is known and nonzero.
why it matters
Delivers the closed $c$-gradient value for the type-$(2,2)$ flat triangle, one of the four area-gradient facts listed as deliverable A in the module campaign. Downstream, areaCov22_eq_grads identifies the covariant area slots on edge classes $2,11,14$ with the three partials at $(2,2,4)$, and hasDerivAt_area_t22_c packages the same vanishing value as a HasDerivAt statement for $t\mapsto A(2,2,t)$ at $t=4$.
Those derivatives feed the orbit-count-weighted sum $(dA\cdot c)(d\delta\cdot c)$ that builds the true-weight zero-momentum Hessian. True weights kill pure gauge on the decoy modes (provisional weight-1 did not). The result does not touch continuum EH recovery or the gap-action flag; it is pure discrete geometry input to the flat second-variation class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.