module module high

`IndisputableMonolith.Cosmology.EtaBPrefactorDerivation`

The module derives the algebraic prefactor for the baryon asymmetry parameter eta_B by establishing phi^8 = 21 phi + 13 from the recurrence phi^2 = phi + 1, together with auxiliary bounds and the RS constant c_RS. Cosmologists applying the Recognition Science framework to early-universe calculations cite these identities for the numerical prefactor. The module consists of direct algebraic lemmas and definitions with no external hypotheses.

claimThe module establishes that where phi satisfies phi^2 = phi + 1, one has phi^8 = 21 phi + 13, along with the derived RS constant c_RS and its expanded form that supplies the prefactor in the eta_B expression.

background

Recognition Science obtains all physics from a single functional equation whose self-similar fixed point is the golden ratio phi (T6). The module imports the fundamental RS time quantum tau_0 = 1 tick from Constants and the integration gap D^2(D+2) = 45 at D = 3 from IntegrationGap. It works entirely within the phi-ladder, expressing higher powers via Fibonacci coefficients to obtain the concrete prefactor needed for the cosmological eta_B worked example.

proof idea

The module proceeds by successive multiplication from phi^2 = phi + 1 to reach the exact identity phi^8 = 21 phi + 13, with separate lemmas supplying lower and upper bounds. These identities are then used to define correctionFactor, expand c_RS, and isolate the positive value c_RS_pos.

why it matters in Recognition Science

The module supplies the explicit prefactor for the eta_B calculation cited in the companion paper and feeds directly into the root IndisputableMonolith module that exposes the master forcing-chain theorem. It closes the algebraic step linking the eight-tick octave (T7) to the D = 3 cosmological observables.

scope and limits

Does not compute the full numerical value of eta_B.
Does not address the consciousness-gap interpretation of the integration gap.
Does not prove any of the T0-T8 forcing-chain steps.
Does not incorporate the full Standard-Model Higgs chain.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.IntegrationGap module_import

declarations in this module (28)

theorem phi_pow_8_fib L51
theorem phi_pow_8_lower L64
theorem phi_pow_8_upper L70
lemma phi_zpow_neg8_eq_inv L77
theorem phi_zpow_neg8_lower L80
theorem phi_zpow_neg8_upper L90
def correctionFactor L103
def c_RS L106
theorem c_RS_expanded L108
theorem one_minus_phi_neg8_lower L111
theorem one_minus_phi_neg8_upper L115
theorem c_RS_pos L119
theorem c_RS_lt_one L124
theorem c_RS_lower L131
theorem c_RS_upper L138
theorem phi_pow_fib L147
theorem phi_pow_44_fib L164
lemma phi_zpow_neg44_eq_inv L172
theorem phi_zpow_neg44_lower L175
theorem phi_zpow_neg44_upper L188
def eta_B_corrected L204
theorem eta_B_corrected_pos L206
theorem eta_B_corrected_lower L211
theorem eta_B_corrected_upper L220
theorem eta_B_corrected_in_observed_band L229
theorem observed_in_predicted_band L234
structure EtaBPrefactorCert L242
theorem etaBPrefactorCert L250