correctionFactor
plain-language theorem explainer
The single-tick correction factor equals 1 minus phi to the negative eighth power. Researchers assembling the RS baryogenesis prefactor cite this definition to construct the squared washout term c_RS. The declaration is a direct abbreviation with no proof obligations.
Claim. The single-tick correction factor is defined by $1 - phi^{-8}$.
background
Recognition Science derives the baryon asymmetry prefactor from the eight-tick structure. The tick is the fundamental time quantum tau_0 = 1. The golden ratio phi is the self-similar fixed point forced as the fixed point of the composition law. The module sets eta_B = c times algebraic content from the integration gap, with c_RS = (1 - phi^{-8})^2. The correctionFactor supplies the single-tick term 1 - phi^{-8}, squared to encode washout in both matter and antimatter sectors per the module documentation.
proof idea
The declaration is a direct definition of correctionFactor as 1 - phi ^ (-8 : Z). It is a one-line abbreviation used by unfolding in the definitions of c_RS and related theorems.
why it matters
This definition supplies the base for c_RS, which is expanded in the theorem c_RS_expanded and shown positive in c_RS_pos. It fills the single-tick washout slot in the two-sided 8-tick prefactor for eta_B, matching the eight-tick octave from the unified forcing chain. The module documentation states that the predicted eta_B band contains the Planck 2018 value, with the squared form remaining hypothesis-grade pending a Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.