areaGradB_t12
plain-language theorem explainer
At the flat triangle with edge lengths (1,2,3), the Heron area gradient in the middle edge equals √2/8. Analysts wiring the zero-momentum 4D Regge Hessian cite this closed value when matching orbit-(1,2) area covariants and when stating HasDerivAt for the b-coordinate. The proof unfolds the gradient formula, inserts the known hinge area √2/2, and finishes by field arithmetic.
Claim. For the Heron area gradient $\partial A/\partial b=(a+c-b)/(16A)$ at edge lengths $(a,b,c)=(1,2,3)$, one has $\partial A/\partial b=\sqrt{2}/8$.
background
This module builds 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 four flat triangle representatives are $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, and $(2,2,4)$. For sides $a,b,c$, the hinge area $A$ is the positive square root of the Heron quadratic $(2ab+2bc+2ca-a^2-b^2-c^2)/16$. The middle-edge gradient is the closed form $(a+c-b)/(16A)$.
Upstream, the hinge area at $(1,2,3)$ is already evaluated: $A(1,2,3)=\sqrt{2}/2$. That identity is the only geometric input needed here.
proof idea
One-line algebraic evaluation. Unfold the gradient definition to $(1+3-2)/(16\cdot A(1,2,3))$. Rewrite the area by the upstream identity $A(1,2,3)=\sqrt{2}/2$. After recording $\sqrt{2}\neq 0$, field_simp clears the denominator; replace $(\sqrt{2})^2$ by $2$ via sq_sqrt, then norm_num yields $\sqrt{2}/8$.
why it matters
Closes one of the four explicit flat area-gradient values required by deliverable A of the Regge flat Hessian assembly (module campaign: true-weight second variation from geometry, not reverse-engineered EH weights).
Downstream, areaCov12_eq_grads identifies the three nonzero area-covariant slots on the $(1,2)$ orbit with the three gradients at $(1,2,3)$, quoting this value for the middle slot. Separately, hasDerivAt_area_t12_b discharges HasDerivAt of $t\mapsto A(1,t,3)$ at $t=2$ with derivative $\sqrt{2}/8$ by simp-rewriting through this theorem.
Those gradient 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. The assembly kills pure gauge on the decoy directions where weight-1 failed; it still does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.