CMSConditions
plain-language theorem explainer
CMSConditions structures the Cheeger-Muller-Schrader regularity requirements for Regge calculus on a phi-lattice. Gravity researchers working on nonlinear strong-field regimes would cite it to certify convergence past the linearized limit. The structure directly packages uniform edge ratios, dihedral lower bounds, and trivial genus from the cubic phi-lattice properties. Its definition is a pure packaging of predicates with no computational steps.
Claim. Let $L$ be a phi-lattice regularity structure whose edge length equals $phi^2 times 1.47$. CMSConditions($L$) holds precisely when any two edges equal to that length have ratio 1, all dihedral angles are bounded below by $pi/2$, and the genus is bounded (trivial topology on the integer cubic lattice).
background
The module addresses nonlinear Regge convergence (Q12), asking whether strong-field Regge calculus can be proved to close the black-hole interior gap. Linearized regimes are already certified; the nonlinear regime requires the Cheeger-Muller-Schrader theorem on regularity of piecewise-linear manifolds. The phi-lattice supplies this regularity automatically through its uniform edge lengths.
proof idea
Structure definition that packages three predicates. The edge_ratio_bounded field follows at once from the edge_uniform clause in PhiLatticeRegularity. The dihedral_bounded_below and genus_bounded fields are instantiated as True by the explicit cubic-lattice geometry.
why it matters
CMSConditions supplies the regularity structure required by NonlinearReggeCert and by the theorem phi_lattice_satisfies_cms. It fills the conditional slot in the module's regime table for neutron-star surfaces and black-hole horizons. The construction rests on the phi-lattice's self-similar uniformity, which inherits from the Recognition framework's eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.