pith. sign in
module module moderate

IndisputableMonolith.Cosmology.BaryogenesisTrajectory

show as:
view Lean formalization →

The Cosmology.BaryogenesisTrajectory module defines and analyzes the baryon-to-photon ratio η_B at recognition e-folds N since the GUT epoch in RS-native units. Cosmologists working on discrete-time baryogenesis models would cite its lemmas for trajectory properties. The module is a collection of definitions and supporting theorems establishing sign, monotonicity, and specific values along the sequence.

claimLet η_B(N) be the baryon-to-photon ratio at recognition e-fold N since the GUT epoch, with τ_0 = 1 tick. The module supplies η_B(N) together with lemmas asserting η_B(N) > 0 for N > 0, η_B(0) = 0, and strict decrease under adjacent ratios.

background

Recognition Science quantizes time in fundamental ticks τ_0 = 1 from the imported Constants module. The present module operates in the cosmology domain and introduces the function etaBAt that returns η_B at integer e-fold N after the GUT epoch. Sibling declarations establish elementary properties of this sequence, including positivity, vanishing at N = 0, and ratio relations between adjacent steps.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the baryogenesis trajectory that later cosmology results would invoke when computing the observed η_B. It directly encodes the doc-comment statement that η_B is evaluated at recognition e-folds N since the GUT epoch and rests on the RS time quantum τ_0.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)