lambda_CP_lt_one
plain-language theorem explainer
The theorem shows that the CP-odd gravitational coupling λ_CP equals φ to the power of negative seven is strictly less than one. Baryogenesis calculations in Recognition Science rely on this bound to ensure the CP-violating terms remain perturbative. The proof proceeds by rewriting one as φ to the zero power and invoking the strict increase of the power function for base φ greater than one.
Claim. Let φ be the golden ratio with φ > 1. Define the CP-odd gravitational coupling by λ_CP := φ^{-7}. Then λ_CP < 1.
background
The RS Baryogenesis module formalizes a parameter-free mechanism for matter-antimatter asymmetry. Nine ledger parities select a unique CP-odd pseudoscalar channel, with the gravitational coupling defined as λ_CP = φ^{-7} and the electromagnetic coupling as κ_CP = φ^{-9}. The upstream lemma one_lt_phi establishes φ > 1, which is required for all subsequent inequalities on negative powers.
proof idea
The proof unfolds the definition of λ_CP to φ^{-7}. It rewrites 1 as φ^0 and applies the lemma rpow_lt_rpow_of_exponent_lt, using one_lt_phi together with the fact that the exponent -7 is negative.
why it matters
This bound is used directly by lambda_CP_bounds and kappa_CP_lt_one, which together confirm that both CP couplings lie in (0,1). The result supports the baryogenesis prediction η_B ≈ 5.1 × 10^{-10} and aligns with the Recognition Science phi-ladder where φ is the self-similar fixed point. It closes the step that CP couplings must be less than one for the nine-parity selection mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.