pith. sign in
module module high

IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder

show as:
view Lean formalization →

This module computes the baryon asymmetry eta_B on the phi-ladder in Recognition Science cosmology, starting from the identity phi^8 = 21 phi +13 >46. A cosmologist working on matter-antimatter imbalance from the J-uniqueness fixed point would cite the certified bounds etaB_RS and BaryonAsymmetryCert. The module consists of direct algebraic definitions and inequality verifications on successive powers of phi.

claimThe module supplies rung values on the phi-ladder together with the asymmetry parameter eta_B^{RS} derived from phi^8 = 21 phi +13 >46, including explicit bounds phi^{16}>2000, phi^{32}>4M, and the certified small value eta_B small.

background

Recognition Science places all constants on the phi-ladder generated by the self-similar fixed point of the J-cost J(x)=(x+x^{-1})/2-1. The module imports the fundamental RS time quantum tau_0=1 tick from Constants and applies the mass formula yardstick * phi^(rung-8+gap(Z)) to baryons. It defines baryonRung and etaB_RS as the concrete objects that convert the eight-tick octave into a numerical asymmetry.

proof idea

This is a definition and calculation module. Each sibling is obtained by direct substitution into the minimal polynomial of phi or by successive powering; inequalities such as phi8_gt_46 are verified by arithmetic reduction without tactics beyond rfl or norm_num.

why it matters in Recognition Science

The module supplies BaryonAsymmetryCert that later cosmology results depend on. It closes the step from the T5-T8 forcing chain to the observed small eta_B by exhibiting explicit ladder values that remain inside the alpha band. It touches the open question of whether the same ladder also fixes the observed baryon-to-photon ratio without extra parameters.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)