hingeArea_t13
plain-language theorem explainer
For the committed flat triangle representative with edge parameters (1,3,4), the Heron hinge area equals √3/2. Anyone building type-(1,3) area gradients for the zero-momentum 4D Regge Hessian cites this closed value. The proof unfolds the square-root definition, inserts the already-proved square-area identity heronSq=3/4, and recovers the positive root.
Claim. The hinge area of the triangle with side parameters $a=1$, $b=3$, $c=4$ equals $\sqrt{3}/2$, where hinge area means the nonnegative square root of the Heron quadratic $(2ab+2bc+2ca-a^{2}-b^{2}-c^{2})/16$.
background
This module assembles the flat second-variation (Hessian) of the 4D Regge action at zero momentum. Edge-class perturbations are constant per cell; the deliverable replaces the provisional weight-1 stencil by true orbit-count weights times area gradients times deficit kernels.
Hinge area is defined locally as $\sqrt{\mathrm{heronSq}(a,b,c)}$, with $\mathrm{heronSq}$ the algebraic Heron form $A^{2}=(2ab+2bc+2ca-a^{2}-b^{2}-c^{2})/16$. The four committed flat representatives are $(1,1,2)$, $(1,2,3)$, $(1,3,4)$, and $(2,2,4)$. Upstream, heronSq_t13 already records that the square area on $(1,3,4)$ is exactly $3/4$ by direct arithmetic.
(The identically named constant in the Wick-interior-hinge module is a different object: the fixed spacelike value $\sqrt{3/16}$. Here the three-argument function is the variable Heron area used for gradients.)
proof idea
Unfold the definition hingeArea = √(heronSq). Establish the elementary identity $3/4=(\sqrt{3}/2)^{2}$ by rewriting the right-hand side via div_pow and sq_sqrt. Rewrite the goal with heronSq_t13 (which supplies heronSq 1 3 4 = 3/4) and that identity, then finish by Real.sqrt_sq with a positivity side condition.
why it matters
Closed area values are the first half of deliverable A in the module doc: explicit HasDerivAt theorems for ∂A/∂a, ∂A/∂b, ∂A/∂c on each flat representative. Downstream, areaGradA_t13, areaGradB_t13, and areaGradC_t13 all rewrite through this identity to obtain ∂A/∂a=√3/4, ∂A/∂b=√3/12, and ∂A/∂c=0 on the (1,3,4) orbit.
Those gradients enter the orbit-count-weighted sum (counts 72/48/48/24/24/24) that builds the true-weight zero-momentum Hessian. The campaign sits inside the QG full-theory track toward Regge recovery of Einstein–Hilbert, but the module explicitly does not claim S_RS_converges_EH_4d, does not flip gap_action_recovery, and leaves finite-momentum Bloch folding open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.