FlatSumCondition
FlatSumCondition encodes the requirement that the sum of dihedral angles around an edge equals exactly 2π. Workers in Regge calculus and discrete gravity cite this as the local flatness test at hinges. The definition is a direct equality between the summed angles from the list of data structures and 2π.
claimFor a finite list $ds$ of dihedral angle data structures (each carrying a cosine value in $[-1,1]$), the condition holds when the sum of the associated angles equals $2π$, where each angle is recovered via arccos of its cosine.
background
Dihedral angle data structures package a real cosine bounded in $[-1,1]$, from which the angle is recovered as arccos of that value and lies in $[0,π]$. The summation of dihedral angles over a list aggregates these values, while the deficit subtracts the aggregate from $2π$ to quantify curvature at a hinge. This module is Phase C2 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes, recording the classical flat-space identity at a non-singular edge as a Prop-valued predicate matching Regge calculus usage.
proof idea
The declaration is a one-line definition equating the summation of dihedral angles over the input list to $2π$.
why it matters in Recognition Science
This predicate supplies the atomic flatness condition consumed by the flat simplicial complex structure, which assembles finitely many hinges each obeying the condition. It directly supports the theorem establishing zero deficit from the flat condition, the cubic lattice flat sum theorem, and the certificate for the Schläfli identity together with the theorem on total deficit vanishing under flat conditions. The definition completes the Phase C2 setup, supplying the zero-deficit baseline that later phases contrast with curvature and anchoring the geometric layer for simplicial complexes in three dimensions.
scope and limits
- Does not assert the condition for any concrete list of angles.
- Does not derive the value of individual dihedral angles.
- Does not address higher-dimensional or non-simplicial complexes.
- Does not incorporate curvature or deficit calculations.
formal statement (Lean)
130def FlatSumCondition (ds : List DihedralAngleData) : Prop :=
proof body
Definition body.
131 sumThetas ds = 2 * Real.pi
132
133/-- The deficit at a hinge is `2π − Σ θ`. -/