cubic_lattice_flatSum
plain-language theorem explainer
Four right dihedral angles from the cube sum exactly to 2π, confirming the flat-sum condition at a cubic lattice hinge. Regge calculus and discrete gravity researchers cite this as the zero-curvature baseline for Z³ lattices. The proof is a direct term reduction that unfolds the sum predicate, substitutes the known π/2 value for each cube angle, and closes by ring arithmetic.
Claim. The flat-sum condition holds for the list of four cube dihedral angles: if each angle satisfies θ = π/2 then ∑_{i=1}^4 θ_i = 2π.
background
The DihedralAngle module constructs dihedral angles from Cayley-Menger data for simplicial complexes, as Phase C2 toward discharging the Regge deficit linearization hypothesis. It defines DihedralAngleData to carry a cosine value obeying −1 ≤ cos ≤ 1, sets θ = arccos(cos), and records the flat-space hinge condition as the proposition FlatSumCondition(ds) ≔ sumThetas(ds) = 2π. The cube dihedral angle is supplied upstream as the constant π/2, the right angle between adjacent faces of the cubic lattice.
proof idea
Term-mode proof. Unfold FlatSumCondition and sumThetas, then apply simp on the list constructors together with the cube_dihedral_theta lemma to reduce the sum of four identical π/2 terms; ring closes the equality to 2π.
why it matters
The result populates the cubic_flat_sum field of the DihedralAngleCert certificate and is invoked directly by cubic_lattice_deficit_zero to obtain deficit = 0. It encodes the classical Z³ lattice is flat statement quoted in the declaration comment, anchoring the flat baseline before curved or higher-genus cases are treated. In the Recognition framework it supplies the geometric identity required for the three-dimensional spatial structure (T8) prior to deficit linearization on general simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.