nonlinear_regge_cert_exists
plain-language theorem explainer
The theorem asserts existence of a NonlinearReggeCert structure on the canonical phi-lattice. Researchers closing the gap between linearized and strong-field Regge calculus in gravity would cite it to certify coverage up to neutron-star and horizon regimes. The proof is a direct term construction that packages the canonical lattice definition, the CMS satisfaction theorem, and the observational coverage result into the required certificate.
Claim. There exists a structure $C$ such that $C$ records a regular phi-lattice with uniform edge lengths $phi^2 times 1.47$, the Cheeger-Muller-Schrader conditions hold for this lattice, and the linearized approximation covers all observational regimes.
background
The module addresses nonlinear Regge convergence (Q12) by extending the linearized certification from CubicReggeProof.lean to strong-field regimes. PhiLatticeRegularity is the structure whose fields are edge_length := phi^2 * 1.47, edge_positive, edge_uniform, and edge_from_phi. CMSConditions phi_lattice_regular encodes the Cheeger-Muller-Schrader requirements: bounded edge ratios, dihedral angles bounded below, and bounded genus. The local setting is the phi-lattice's automatic satisfaction of these regularity conditions because all edges are multiples of the backbone length phi^2 * 1.47.
proof idea
The proof is a one-line term wrapper. It supplies canonical_phi_lattice for the regularity field, phi_lattice_satisfies_cms for the CMS field, and observational_regime_covered for the linearized_sufficient field, then packages them inside the NonlinearReggeCert constructor.
why it matters
This declaration supplies the top-level existence witness for the nonlinear regime in the Regge convergence question. It feeds the framework's claim that the phi-lattice closes the gap between linearized (|h| << 1) and horizon (|h| ~ O(1)) regimes via T5 J-uniqueness and the eight-tick octave. The module document notes that black-hole interiors remain open; the certificate therefore marks the boundary of current coverage rather than a full resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.