observational_regime_covered
plain-language theorem explainer
The theorem asserts that the linearized Regge approximation covers every current observational regime in gravity. Researchers extending Regge calculus to strong fields or black-hole interiors would cite it to lock down the weak-field baseline. The proof is a one-line decision procedure that evaluates the boolean constant directly.
Claim. The linearized gravitational perturbation $h$ with $|h|ll 1$ covers all observational regimes (solar-system, galactic, gravitational-wave, and CMB data).
background
The module addresses Q12: whether strong-field Regge convergence can be proved to close the black-hole interior gap. The linearized regime is already certified in CubicReggeProof; the nonlinear regime invokes the Cheeger-Muller-Schrader theorem on piecewise-linear manifolds. The φ-lattice supplies the required regularity automatically because all edge lengths are multiples of the backbone spacing φ² × 1.47. Upstream results supply the J-cost structure and φ-ladder tiers used to define the lattice spacing.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the boolean constant linearized_covers_observational.
why it matters
The result is invoked inside nonlinear_regge_cert_exists to assemble the full NonlinearReggeCert triple (phi_lattice_regular, cms_satisfied, linearized_sufficient). It therefore discharges the observational half of the Q12 question before the CMS regularity step is applied to the nonlinear regime. In the Recognition Science chain this step sits between the phi-lattice construction (T6–T8) and the eight-tick octave periodicity that forces D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.