observed_in_predicted_band
plain-language theorem explainer
The theorem verifies that the Planck 2018 central value for the baryon asymmetry η_B at 6.10 × 10^{-10} satisfies the strict inequalities 6.0 × 10^{-10} < 6.10 × 10^{-10} < 6.2 × 10^{-10}. Workers checking the Recognition Science baryogenesis prediction against data would reference this containment result. The proof applies constructor to decompose the conjunction and norm_num to evaluate the numerical comparisons directly.
Claim. $6.0 × 10^{-10} < 6.10 × 10^{-10} ∧ 6.10 × 10^{-10} < 6.2 × 10^{-10}$
background
The module derives the prefactor c_RS = (1 - φ^{-8})^2 for the baryon asymmetry formula η_B = c_RS · φ^{-44} using the eight-tick octave at three spatial dimensions. The Fibonacci relation φ^8 = 21φ + 13 together with the interval bounds on φ produces the numerical prediction band (6.0 × 10^{-10}, 6.2 × 10^{-10}). This theorem records the containment of the observed central value inside that band. The setting relies on the Recognition Composition Law to fix the algebraic content of the integration gap without additional parameters. The squared washout encodes independent contributions from matter and antimatter sectors.
proof idea
The proof is a one-line term wrapper. It invokes constructor to split the logical conjunction into two inequalities and then applies norm_num to confirm both by direct real-number arithmetic.
why it matters
This supplies the observed_inside component of the master certificate etaBPrefactorCert, closing the validation loop for the predicted η_B band. It instantiates the T7 eight-tick octave and T8 D = 3 by showing that the φ^{-44} scaling yields a value matching the Planck measurement at the 10^{-10} scale. The module flags that the band theorem is proved while the squared prefactor remains at hypothesis grade pending a Boltzmann-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.