c_RS_lt_one
plain-language theorem explainer
The theorem establishes that the Recognition Science prefactor c_RS equals (1 - φ^{-8})^2 and is strictly less than one. Baryogenesis calculations citing the eta_B formula would invoke this bound to keep the washout factor order-one. The proof rewrites via the expanded definition, inserts the pre-proved interval 0.978 < (1 - φ^{-8}) < 0.979, and concludes by nonlinear arithmetic.
Claim. Let φ be the golden ratio. The Recognition Science washout prefactor satisfies $(1 - φ^{-8})^2 < 1$.
background
The EtaBPrefactorDerivation module defines the prefactor c_RS as the square of a correction factor that encodes two-sided washout at the eight-tick octave. Explicitly, c_RS := (1 - φ^{-8})^2, where the squared form arises because matter and antimatter sectors each carry one integration-gap worth of fermionic degrees of freedom washed out at rate φ^{-8} (one rung per fundamental tick at D = 3). The module derives φ^8 = 21φ + 13 from the Fibonacci identity and obtains the numerical band 0.956 < c_RS < 0.959.
proof idea
The term-mode proof first rewrites the goal using the theorem c_RS_expanded, which unfolds c_RS to (1 - φ^{-8})^2. It then introduces the lower bound hl from one_minus_phi_neg8_lower and the upper bound hu from one_minus_phi_neg8_upper. The tactic nlinarith [hl, hu] applies nonlinear arithmetic to these interval facts to conclude that the square lies below one.
why it matters
The result feeds directly into etaBPrefactorCert, which packages the unit interval bounds, the expanded form, and the prediction that c_RS · φ^{-44} lies inside the observed Planck band for η_B. It closes the T7 eight-tick octave step of the forcing chain by guaranteeing the washout prefactor remains positive and less than unity. The module records that the numerical band is theorem-grade while the squared interpretive form remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.