phi_lattice_satisfies_cms
plain-language theorem explainer
The canonical phi-lattice satisfies the Cheeger-Muller-Schrader regularity conditions on edge ratios, dihedral angles, and topology. Researchers modeling strong-field Regge calculus for black hole interiors would cite this to bridge linearized and nonlinear regimes. The proof constructs the structure instance directly, verifying the edge ratio equality by rewriting and field simplification while the remaining conditions hold by triviality on the uniform cubic lattice.
Claim. Let $L$ be the canonical phi-lattice with uniform edge length $phi^2 times 1.47$. Then $L$ satisfies the Cheeger-Muller-Schrader conditions: for all edges $e_1, e_2$, if $e_1 = L.edge_length$ and $e_2 = L.edge_length$ then $e_1/e_2 = 1$; all dihedral angles are bounded below by $pi/2$; and the lattice has bounded genus corresponding to trivial topology.
background
In the Nonlinear Regge Convergence module the question is whether strong-field Regge convergence can be proved to close the black hole interior gap. The linearized regime is already certified, but the nonlinear regime requires the Cheeger-Muller-Schrader theorem for regularity of Regge calculus on piecewise-linear manifolds. The phi-lattice supplies this regularity automatically through its uniform structure where all edge lengths are multiples of the backbone scale $phi^2 times 1.47$ (see canonical_phi_lattice definition).
proof idea
The proof is a term-mode construction of the CMSConditions instance on canonical_phi_lattice. The edge_ratio_bounded field is discharged by introducing the two equality assumptions, rewriting them into the lattice edge length, and applying field_simp. The dihedral_bounded_below and genus_bounded fields are discharged by the trivial tactic because they hold by construction on the cubic lattice.
why it matters
This supplies the CMS satisfaction required by the downstream nonlinear_regge_cert_exists theorem, which assembles a NonlinearReggeCert from phi-lattice regularity, CMS satisfaction, and linearized coverage. It advances the Recognition Science path for Q12 by making the neutron-star-surface and black-hole-horizon regimes conditional on CMS rather than open, while the black-hole-interior regime remains open for perturbations exceeding order 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.