Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder

show as:
view Lean formalization →

This module assembles the phi-ladder machinery needed to compute the RS-native baryon asymmetry eta_B, including explicit rung placements and the inequality phi^8 > 46. Cosmologists studying baryogenesis in Recognition Science frameworks would cite these results when matching observed eta_B to the phi recurrence. The module is organized as a sequence of definitions and direct algebraic checks on powers of phi.

claim$\phi^8 = 21\phi + 13 > 46$, together with $\eta_B^{RS}$ and the certified baryon asymmetry on the phi-ladder.

background

The module sits in the cosmology domain and imports only the Constants module, whose sole documented object is the RS time quantum $\tau_0 = 1$ tick. It introduces the phi-ladder (the discrete self-similar sequence generated by the fixed point $\phi$ of the Recognition Composition Law) and places baryons on specific rungs via baryonRung and baryonRung_gap45. The asymmetry parameter etaB_RS is defined directly from these rungs, with auxiliary facts such as phi8_val, phi8_gt_46, phi16_gt_2000 and the final BaryonAsymmetryCert.

proof idea

This is a definition module, no proofs. The structure consists of successive definitions (baryonRung, etaB_RS) followed by direct verification of the listed inequalities on powers of phi.

why it matters in Recognition Science

The module supplies the explicit phi-ladder values and the BaryonAsymmetryCert that later cosmological constructions in Recognition Science rely upon. It directly encodes the DOC_COMMENT relation $\phi^8 = 21\phi + 13 > 46$ as the entry point for baryon asymmetry calculations.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)