hasDerivAt_regularTriangleArea
plain-language theorem explainer
The regular triangular hinge area $A(a)=(\sqrt{3}/4)a^{2}$ is differentiable at every real edge length $a$, with derivative $(\sqrt{3}/2)a$. Anyone assembling the concrete Freudenthal/Regge component certificate cites this to show area weights are derivative-ready. The proof is a short calculus reduction: product rule on $a\cdot a$, rewrite as $a^{2}$, then scale by the constant $\sqrt{3}/4$.
Claim. For every real number $a$, the regular triangular hinge-area map $A(a)=\frac{\sqrt{3}}{4}a^{2}$ is differentiable at $a$ and its derivative equals $\frac{\sqrt{3}}{2}a$.
background
This module builds a fully concrete finite flat-sector Regge model that the weak-field bridge can consume without new geometric axioms. The Cayley–Menger stack already supplies regular tetrahedron data and dihedral angles, but it does not yet expose full CM determinants as differentiable functions of all edge lengths. The workaround is a regular hinge-area formula together with graph-Laplacian second-variation data.
The area weight used here is the elementary regular-triangle formula $A(a)=(\sqrt{3}/4)a^{2}$. Differentiability of this scalar map in the single edge length $a$ is the minimal calculus fact needed before packaging off-diagonal coefficients $M_{ij}=-A_{ij}$, row-sum zero, and the Dirichlet form of the second-order action.
Upstream, regularTriangleArea is exactly that closed-form definition. The surrounding certificate also needs the companion scale-invariance fact for the regular tetrahedral dihedral angle; non-uniform multi-edge derivatives remain deferred.
proof idea
Unfold the definition $A(a)=(\sqrt{3}/4)a^{2}$. Apply the product rule to $\mathrm{id}\cdot\mathrm{id}$ at $a$ to get derivative $a+a=2a$ for $x\mapsto x^{2}$ (after a ring conversion from $x\cdot x$ to $x^{2}$). Multiply by the constant $\sqrt{3}/4$ via const_mul, then ring-normalize the resulting coefficient $(\sqrt{3}/4)\cdot 2a$ to $(\sqrt{3}/2)a$. Pure real one-variable calculus; no geometry lemmas beyond the definition.
why it matters
This is the area_derivative field of freudenthalReggeComponentCert, the module's packaging theorem that asserts the concrete regular flat-sector model matches the bridge interface: off-diagonal $M_{ij}=-A_{ij}$, every row sums to zero, and the second variation equals the weighted Dirichlet form. Without a proved derivative for the hinge area, that certificate cannot close.
In the broader Recognition geometry stack this is the first fully concrete finite model the weak-field conformal Regge bridge can consume. It deliberately stops short of arbitrary Cayley–Menger / dihedral derivative data; the module doc states that full multi-edge differentiability is the remaining hard task. The companion hasDerivAt_regularDihedral_uniformScale records scale invariance of the regular tetrahedral dihedral angle, so together they pin the regular-star case while leaving non-uniform edge variations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.