module module high

`IndisputableMonolith.Cosmology.EtaBPrefactorDerivation`

The module derives the identity φ^8 = 21φ + 13 from φ^2 = φ + 1, together with bounds, inverses, and the expanded form of c_RS used for the η_B prefactor. Cosmologists citing the Recognition Science treatment of baryon asymmetry reference these algebraic steps. Each result follows from direct recurrence expansion or interval arithmetic on the golden-ratio powers.

claim$\phi^8 = 21\phi + 13$ where $\phi^2 = \phi + 1$, with companion bounds $\phi^8_\text{lower} \le \phi^8 \le \phi^8_\text{upper}$, the inverse relation $\phi^{-8} = \phi^8 - 21\phi - 12$, and the RS speed $c_\text{RS} = \phi^5/\pi$ expanded via the same identity.

background

The module belongs to the cosmology section of Recognition Science and imports the base time quantum τ₀ = 1 tick together with the integration-gap integer D²(D+2) = 45 at D = 3. It works entirely inside the phi-ladder generated by the fixed-point relation φ² = φ + 1 that appears at T6 of the forcing chain. The listed sibling declarations (phi_pow_8_fib, phi_zpow_neg8_eq_inv, correctionFactor, c_RS, c_RS_expanded, c_RS_pos) supply the concrete algebraic objects needed for the η_B prefactor.

proof idea

The module consists of short, independent theorems. Each applies the recurrence φ^n = φ^{n-1} + φ^{n-2} (or its negative-power form) a fixed number of times; interval bounds are obtained by monotonicity of the increasing function x ↦ x^8 on the positive reals. No external lemmas beyond the defining relation are required.

why it matters in Recognition Science

These identities close the algebraic layer required for the η_B worked examples cited in the companion paper and are imported by the root IndisputableMonolith module. They therefore sit inside the T7–T8 segment of the forcing chain that fixes the eight-tick octave and D = 3. The module supplies the concrete prefactor expressions that later stages of the cosmology chain consume.

scope and limits

Does not evaluate the numerical size of η_B itself.
Does not incorporate loop corrections or running couplings.
Does not address the consciousness-gap interpretation of the integration gap.
Does not prove that the phi ladder is the unique self-similar solution.

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