module module high

`IndisputableMonolith.Cosmology.EtaBPrefactorDerivation`

This module derives the identity φ^8 = 21φ + 13 by iterated substitution from φ^2 = φ + 1, supplying the algebraic prefactor for the baryon asymmetry η_B. Researchers evaluating the phi-ladder in the T6 fixed-point and T8 cosmology sections cite it for numerical constants. Derivations are direct algebraic expansions that populate the sibling lemmas phi_pow_8_fib through c_RS_pos.

claim$\phi^8 = 21\phi + 13$ where $\phi$ satisfies $\phi^2 = \phi + 1$, together with the derived objects correctionFactor, c_RS, and c_RS_pos used for the η_B prefactor.

background

The module resides in the Cosmology domain and imports τ₀ = 1 tick from Constants plus the integration gap D²(D+2) = 45 at D = 3 from IntegrationGap. It works inside the self-similar fixed point T6 of the forcing chain, using the golden-ratio recurrence to build successive powers and the correction terms required for the eta_B worked example. The local setting is the eight-tick octave T7 and three spatial dimensions T8.

proof idea

This is a definition module, no proofs. The argument consists of repeated substitution of the base relation φ² = φ + 1 into higher powers, yielding the listed siblings phi_pow_8_fib, phi_pow_8_lower, correctionFactor, c_RS, and c_RS_pos by direct term collection.

why it matters in Recognition Science

The module supplies the φ^8 identity required by the root IndisputableMonolith module to close the two η_B worked-example modules cited in the companion paper. It supports numerical evaluation of cosmological constants inside the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.

scope and limits

Does not compute the numerical value of η_B itself.
Does not derive the forcing-chain steps T0 through T8.
Does not address the consciousness-gap interpretation of the integration gap.
Does not import or use the Recognition Composition Law.

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