NonlinearReggeCert
plain-language theorem explainer
NonlinearReggeCert packages the conditions needed to certify Regge convergence on the φ-lattice in the nonlinear regime. A physicist addressing strong-field gravity or black-hole interiors in the Recognition Science framework would cite this certificate to bridge from linearized results to CMS regularity. The declaration is a structure that simply records three fields: lattice regularity, CMS satisfaction, and confirmation of linearized observational coverage.
Claim. A nonlinear Regge certificate consists of a φ-lattice regularity structure (uniform positive edge lengths φ² × 1.47), the Cheeger-Muller-Schrader conditions holding on that lattice (edge ratios exactly 1, dihedral angles π/2, trivial topology), and the boolean assertion that the linearized regime covers all observational data.
background
The module examines whether strong-field Regge convergence can be proved to close the black-hole interior gap. Linearized regimes (|h_μν| ≪ 1) are already certified; the nonlinear regime requires the Cheeger-Muller-Schrader theorem on piecewise-linear manifolds. The φ-lattice supplies the needed regularity automatically because all edges are multiples of the same backbone length derived from φ. Upstream, PhiLatticeRegularity requires positive uniform edges with length exactly φ² × 1.47. CMSConditions then demands bounded edge ratios of 1, dihedrals at π/2 on the cubic lattice, and bounded genus. linearized_covers_observational returns true precisely when both linearized and weak-field regimes are covered.
proof idea
This is a structure definition with no proof body. It declares a record type whose three fields are supplied directly by sibling definitions: the canonical φ-lattice instance, the lemma that the lattice satisfies CMSConditions, and the boolean that linearized coverage holds.
why it matters
The certificate is consumed by the existence theorem nonlinear_regge_cert_exists, which builds a concrete instance from canonical_phi_lattice and phi_lattice_satisfies_cms. It supplies the conditional coverage for neutron-star surfaces and black-hole horizons in the regime table, advancing the RS path for strong-field convergence. The construction sits inside the forcing chain after T8 (D = 3) and uses the φ-ladder for lattice spacing; the black-hole interior regime remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.