regular_tet_dihedral_in_open_interval
plain-language theorem explainer
The theorem shows that the regular tetrahedron dihedral angle θ equals arccos(1/3) and satisfies 0 < θ < π. Workers on Regge calculus and simplicial gravity cite it to confirm the angle lies in the open interval required for deficit calculations. The tactic proof rewrites θ via the companion equality theorem, applies arccos positivity after norm_num for the lower bound, and derives the strict upper bound by contradiction with arccos_eq_pi and linarith.
Claim. $0 < θ < π$ where $θ = arccos(1/3)$ is the dihedral angle of the regular tetrahedron.
background
The module sets up dihedral angles for simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis. A DihedralAngleData structure carries a cosine with bounds −1 ≤ cos ≤ 1; the angle is then θ = arccos(cos), and the module proves θ ∈ [0, π] in general. The regular tetrahedron is defined with cosine 1/3, and the companion result states that its angle equals arccos(1/3).
proof idea
The tactic proof splits the conjunction with refine. The left conjunct rewrites via regular_tet_dihedral_theta to arccos(1/3) > 0 and closes with Real.arccos_pos.mpr after norm_num. The right conjunct uses Real.arccos_le_pi to obtain ≤ π, then assumes equality, rewrites with Real.arccos_eq_pi, and reaches a contradiction by linarith to obtain the strict inequality.
why it matters
The result is invoked inside dihedralAngleCert to certify that the regular tetrahedron angle lies in the open interval, enabling the flat-sum and zero-deficit properties for cubic lattices and the general theta_in_range map. It completes the unconditional evaluation step required by the module's Phase C2 scope for simplicial Regge calculus in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.