EtaBPrefactorCert
plain-language theorem explainer
The structure certifies that the Recognition Science prefactor for baryon asymmetry equals (1 minus phi to the negative eight) squared and lies between 0.956 and 0.959. This produces a predicted eta_B interval of (6.0 times 10 to the minus ten, 6.2 times 10 to the minus ten) that contains the Planck 2018 central value 6.10 times 10 to the minus ten. Cosmologists comparing RS predictions against observation would cite the certificate. It is a structure definition that assembles algebraic identities and numerical inequalities already derived in-s
Claim. Let $c_{RS} = (1 - phi^{-8})^2$. Then $0 < c_{RS} < 1$, $0.956 < c_{RS} < 0.959$, the corrected baryon asymmetry satisfies $6.0 times 10^{-10} < eta_B < 6.2 times 10^{-10}$, and the observed central value satisfies $6.0 times 10^{-10} < 6.10 times 10^{-10} < 6.2 times 10^{-10}$.
background
In the Recognition Science framework the baryon asymmetry parameter is expressed as eta_B = c_RS times phi to the power minus 44, where the prefactor c_RS encodes the two-sided 8-tick washout of matter and antimatter sectors. The module document states that each sector carries one integration-gap worth of fermionic degrees of freedom washed out at rate phi^{-8} (one rung per fundamental tick at D = 3), so the squared form encodes two independent channels. Upstream results supply the definition c_RS := correctionFactor squared together with eta_B_corrected := c_RS times phi^{-44}; sibling lemmas establish the Fibonacci identity phi^8 = 21 phi + 13 and the numerical interval phi^{-8} in (0.02126, 0.02137).
proof idea
The declaration is a structure definition whose fields directly record the required properties. The algebraic expansion is asserted by the expanded field, which rests on the sibling definitions of correctionFactor and the phi_pow_8 identities. The numerical bands for c_RS and eta_B_corrected are supplied by prior lemmas c_RS_lower, c_RS_upper and eta_B_corrected_in_observed_band; the containment of the observed 6.10e-10 is discharged by the one-line tactic proof observed_in_predicted_band that applies constructor followed by norm_num.
why it matters
This certificate is consumed by the master theorem etaBPrefactorCert in the same module, which constructs the full structure to assert that the predicted band contains the Planck measurement. It realizes the eight-tick octave (T7) and three spatial dimensions (T8) from the unified forcing chain by deriving the phi^{-8} washout factor at the integration-gap rung. The module document notes that the band-level theorem is proved while the interpretive squared form remains hypothesis-grade pending a first-principles Boltzmann-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.