regularTetrahedralDihedralAngle
plain-language theorem explainer
Names the constant dihedral angle of a regular tetrahedron as a real number, taken from the existing DihedralAngle package (cosine 1/3). Geometry and weak-field Regge authors cite it when fixing hinge angles in the concrete Freudenthal flat-sector model. The body is a one-line projection onto the angle field of that packaged data.
Claim. Let $\theta_{\mathrm{tet}}$ denote the interior dihedral angle of a regular tetrahedron. As a real constant it is the angle whose cosine is $1/3$, i.e. $\theta_{\mathrm{tet}} = \arccos(1/3)$, exported from the standard regular-tetrahedron dihedral data.
background
The module builds a concrete finite flat-sector Regge component that the weak-field bridge can consume without new geometric axioms. Area weights come from the regular hinge-area formula; second-variation data is the graph-Laplacian Regge package already on the bridge. Off-diagonal coefficients satisfy $M_{ij}=-A_{ij}$, rows sum to zero, and the second-order action reduces to a Dirichlet form with those weights.
Upstream, the DihedralAngle module packages a regular tetrahedron by fixing cosine equal to $1/3$ (with elementary bounds). The angle field of that package is the geometric dihedral angle. Full Cayley-Menger determinants as differentiable functions of all edge lengths, and arbitrary-triangulation dihedral derivatives, are still out of scope; only this regular model is closed here.
proof idea
One-line definitional wrapper: project the packaged regular-tetrahedron dihedral data onto its angle field. No tactic proof; the equality with $\arccos(1/3)$ is discharged later by reflexivity against that package.
why it matters
Supplies the fixed hinge angle used by the concrete Freudenthal/Regge component certificate. Downstream, the uniform-scale derivative theorem records that this angle is scale-invariant (derivative zero under global edge rescaling), which is the easy half of the second-variation story; non-uniform edge derivatives remain the open Cayley-Menger task. The certificate structure lists that derivative fact beside the regular-triangle area derivative and the off-diagonal $M_{ij}=-A_{ij}$ identities, so the second-order Regge action equals half the geometric Dirichlet form on the concrete area weights. This is the first fully concrete finite model the weak-field bridge can target, not a claim for arbitrary Regge triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.