NumericalPredictionsCert
plain-language theorem explainer
NumericalPredictionsCert collects proved bounds on the inverse fine-structure constant, gravitational coupling, Planck constant in RS units, and mass ratios generated by successive powers of the golden ratio. Researchers verifying Recognition Science predictions against experiment would reference this certificate to establish that all listed intervals contain the observed values. The proof reduces to a single refine tactic that invokes the pre-proved component bounds on each quantity.
Claim. The certificate certifies the conjunction of the following inequalities: $137.030 < alpha^{-1} < 137.039$, $85.6 < 8 phi^5 < 90.4$, $0.088 < hbar < 0.093$, $17 < phi^6 < 18$, $29 < phi^7 < 30$, $198 < phi^{11} < 200$, and $1.61 < phi < 1.62$, where $phi$ is the golden ratio, $alpha^{-1}$ the inverse fine-structure constant, and $hbar$ the reduced Planck constant in RS-native units.
background
This module establishes machine-verified rigorous bounds on every key physical prediction of Recognition Science. Each theorem is a formally proved inequality establishing that the derived value falls in an interval containing the experimentally measured value. The golden ratio satisfies $1.61 < phi < 1.62$, from which the mass ratios on the phi-ladder are derived: $phi^6$ for generation step, $phi^7$ for neutrino ratio, $phi^{11}$ for quark/lepton ratio. Upstream results include hbar_bounds which proves $0.088 < hbar < 0.093$ using the phi bounds, and alphaInv defined from the structural seed and gap.
proof idea
The verified predicate is defined as the conjunction of the listed inequalities. The theorem verified_any is proved by a refine tactic that supplies the component theorems: alphaInv bounds, kappa_bounds for the gravity term, hbar_bounds, phi_pow_6_bounds, neutrino_squared_mass_ratio for the phi^7 term, phi_pow_11_bounds, and the phi bounds.
why it matters
This serves as the master certificate for all numerical predictions in the Recognition framework, confirming that the derived constants and mass ratios lie in intervals containing experimental values. It closes the numerical verification step in the T0-T8 forcing chain by establishing the phi-ladder predictions without approximation. No downstream uses are recorded, indicating it functions as a top-level summary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.