areaGradB
plain-language theorem explainer
Closed-form partial of Heron triangle area with respect to the second edge length: (a+c−b)/(16A). Gravity analysts cite it when wiring area covectors into the zero-momentum 4D Regge Hessian. It is a pure algebraic definition, not a proved identity; the matching HasDerivAt lemmas live beside it.
Claim. For real edge lengths $a,b,c$ and hinge area $A(a,b,c)=\sqrt{\mathrm{heronSq}(a,b,c)}$, the $b$-component of the area gradient is $\partial A/\partial b=(a+c-b)/(16A)$.
background
This module assembles the flat second-variation quadratic of the 4D Regge action at zero momentum. Per-orbit star deficit kernels are combined with Heron area gradients and $S_4$ orbit counts (72/48/48/24/24/24), replacing the provisional weight-1 stencil.
Hinge area is $A=\sqrt{\mathrm{heronSq}(a,b,c)}$, with the quadratic Heron form $A^2=(2ab+2bc+2ca-a^2-b^2-c^2)/16$. The three coordinate gradients $\partial A/\partial a$, $\partial A/\partial b$, $\partial A/\partial c$ are recorded as named defs; this one is the $b$-slot. Flat triangle seeds used downstream are the four committed representatives $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, $(2,2,4)$.
A separate constant hingeArea in the Wick-action module is the fixed spacelike value $\sqrt{3/16}$ and is not the three-argument function used here.
proof idea
Definition only: the body is the single rational expression $(a+c-b)/(16\cdot\mathrm{hingeArea},a,b,c)$. No tactics, no lemmas. Closed values at the flat seeds (e.g. $1/4$ on $(1,1,2)$, $\sqrt{2}/8$ on $(1,2,3)$) are proved later by unfolding this def and simplifying against the corresponding area evaluations.
why it matters
Area gradients are deliverable A of the flat Hessian campaign: they supply the $dA$ factors in the orbit-weighted sum $(dA\cdot c)(d\delta\cdot c)$ that defines the true-weight zero-momentum Hessian. Downstream, areaCov11_eq_grads, areaCov12_eq_grads, and areaCov22_eq_grads pin the nonzero support of each area covector to these Heron gradients; orbitAreaCov_uses_heron_grads re-exports that commitment into the Bloch-orbit symbol layer. Seed evaluations areaGradB_t11 through areaGradB_t22 discharge the numeric entries.
True weights kill pure gauge on decoyGauge and decoyTrace at zero momentum (provisional weight-1 did not). Finite-momentum Bloch phase folding and the full $S_{RS}\to EH$ convergence remain open; this def does not touch those gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.