regular_tet_dihedral
plain-language theorem explainer
The definition supplies the DihedralAngleData record for a regular tetrahedron by fixing its cosine at 1/3. Workers on Regge calculus and simplicial gravity cite it when evaluating edge deficits in tetrahedral meshes. The construction is a direct record literal whose bound hypotheses are discharged by numerical normalization.
Claim. The dihedral angle data for a regular tetrahedron is the structure with cosine equal to $1/3$ together with the bounds $-1 ≤ 1/3$ and $1/3 ≤ 1$, so that the associated angle is $θ = arccos(1/3)$.
background
The DihedralAngle module implements Phase C2 of the program to discharge the Regge deficit linearization hypothesis. It defines the structure DihedralAngleData carrying a real cosine value together with explicit bounds $-1 ≤ cosine ≤ 1$; the associated angle is recovered by $θ = arccos(cos)$. This structure is required to match the one already present in ReggeCalculus so that deficit sums can be formed at edges of tetrahedra. The module also records the flat-space sum condition $Σ θ_σ = 2π$ and proves the range $θ ∈ [0, π]$ for any admissible cosine.
proof idea
The definition is a direct record literal that populates the cosine field with the constant 1/3 and discharges the two bound hypotheses by norm_num.
why it matters
This definition supplies the canonical regular-tetrahedron value required by DihedralAngleCert, regular_tet_dihedral_theta and regular_tet_dihedral_in_open_interval. It completes the Phase C2 setup that feeds Schläfli's identity in Phase C3 and the final simplicial discharge in Phase C5. Within the Recognition framework it provides the explicit geometric input for Regge deficit calculations on tetrahedral complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.