pith. sign in
module module moderate

IndisputableMonolith.Gravity.RSBaryogenesis

show as:
view Lean formalization →

The RSBaryogenesis module defines the CP-odd gravitational coupling λ_CP = φ^{-7} together with κ_CP and the resulting baryon asymmetry η_B in Recognition Science gravity. Researchers modeling early-universe asymmetry from the phi-ladder would cite these constants when matching the observed η_B. The module consists entirely of definitions, positivity bounds, and one-line comparisons with no theorem proofs.

claimThe CP-odd coupling is defined by λ_CP = φ^{-7}, which fixes the strength of the χR R̃ term. Related quantities satisfy 0 < λ_CP < 1, λ_CP > κ_CP, and yield a positive predicted asymmetry η_B that lies inside the observed band.

background

Recognition Science obtains all scales from the J-function J(x) = (x + x^{-1})/2 - 1 and the self-similar fixed point φ. The module sits inside the gravity sector and supplies the CP-violating parameters that enter the baryogenesis calculation. Upstream, the Constants module fixes the RS time quantum τ₀ = 1 tick; the eight-tick octave (T7) and D = 3 then set the periodicity of the phi-ladder used for couplings.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the CP-violation input required by the eta_B_prediction and eta_B_observed siblings. They close the CP-odd step that follows T5 J-uniqueness and T6 phi fixation in the forcing chain, allowing the mass formula and alpha band to be extended to gravitational baryogenesis.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (22)