hasDerivAt_regularDihedral_uniformScale
plain-language theorem explainer
Uniform rescaling of a regular tetrahedron leaves its dihedral angle fixed, so the derivative of that angle in a global scale parameter is identically zero at every real point. Anyone packaging the concrete Freudenthal-local Regge certificate cites this scale-invariance fact. The proof is a one-line appeal to the constant-function derivative rule.
Claim. For every real number $a$, the constant map $s \mapsto \theta_{\mathrm{tet}}$ (the dihedral angle of a regular tetrahedron) is differentiable at $a$ with derivative $0$.
background
The module builds a fully concrete finite flat-sector Regge package that the weak-field bridge can consume without new geometric axioms. Area weights come from the regular triangular hinge formula; second-variation data is the graph-Laplacian Regge matrix already used by the bridge (off-diagonal $M_{ij}=-A_{ij}$, rows sum to zero, action equals a Dirichlet form).
The regular tetrahedral dihedral angle is a fixed real constant attached to the equilateral tetrahedron; it does not depend on overall size. The Cayley-Menger stack already supplies that constant and related regular CM values, but does not yet expose full multi-edge dihedral derivatives for arbitrary triangulations.
Uniform scale invariance of angles is the elementary geometric fact recorded here. Non-uniform edge-length derivatives remain the hard open Cayley-Menger task flagged by the module scope note.
proof idea
One-line term proof. The map is definitionally independent of the scale argument, so Mathlib's hasDerivAt_const applies directly at the evaluation point $a$ and yields derivative zero.
why it matters
This is one of five fields of freudenthalReggeComponentCert, the certificate that the concrete regular flat-sector / Freudenthal-local model matches the bridge interface: area derivative, dihedral uniform-scale derivative, off-diagonal coefficients, row-sum zero, and Dirichlet second variation.
It closes the scale-invariance half of the dihedral data for that model. The module is explicit that this is not a general Cayley-Menger derivative theorem; it is the exact interface a future full multi-edge derivative computation must hit. Within Recognition geometry it supplies the concrete finite model the weak-field conformal Regge bridge can already consume, while leaving arbitrary-triangulation dihedral derivatives as scaffolding for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.