FlatSimplicialComplex
plain-language theorem explainer
The flat simplicial complex structure packages finitely many hinges and edges such that each hinge satisfies the flat dihedral sum condition and all edge lengths are positive reals. Researchers linearizing the Regge deficit around flat backgrounds cite this to anchor the unperturbed geometry before introducing length perturbations. The definition directly composes the hinge data with the flat-sum predicate and positivity constraints.
Claim. A flat simplicial complex with $n_H$ hinges and $n_E$ edges consists of a map assigning to each hinge index a simplicial hinge datum, a map assigning to each edge index a positive real length, and the requirement that the dihedral angles of every hinge sum to $2π$.
background
Recognition Science linearizes the Regge deficit angle around a flat simplicial complex as part of discharging the Piran-Williams hypothesis in Phase C4. A simplicial hinge datum records the combinatorial incidence and dihedral angles at each hinge. The flat-sum condition requires that the sum of dihedral angles around any hinge equals exactly $2π$, which forces the deficit to vanish in the background. The module imports the Cayley-Menger determinant for volumes, the dihedral angle computation, and Schläfli's identity for the variation of deficits. Upstream results supply the nuclear tier structure and the J-cost functional, but the local geometry rests on the flat-sum predicate: sumThetas ds = 2 * Real.pi, with the deficit defined as 2π minus that sum.
proof idea
The declaration is a structure definition that directly assembles the hinge map, the positive edge-length map, and the universal quantification of the flat-sum condition over all hinges. No lemmas are applied; the flatness constraint is imposed by reference to the DihedralAngle.FlatSumCondition predicate.
why it matters
This structure supplies the flat background required for the linearization of the Regge action in the DeficitLinearization module. It is used by WellShapedData to bundle the complex with its linearization coefficients and the Schläfli identity. The construction fills the Phase C4 slot in the program to obtain a quadratic action from conformal perturbations of edge lengths, consistent with the eight-tick octave and D=3 spatial dimensions of the Recognition framework. It touches the open question of extending the linearization from the cubic lattice to general simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.