kappa_CP_lt_one
plain-language theorem explainer
The theorem shows that the CP-odd coupling κ_CP is strictly less than one. Researchers modeling parameter-free baryon asymmetry cite this bound to control the χFF̃ interaction strength. The proof is a one-line wrapper that applies transitivity of the less-than relation to the chain κ_CP < λ_CP < 1.
Claim. The CP-odd electromagnetic coupling satisfies $κ_{CP} < 1$, where $κ_{CP} = φ^{-9}$ and $φ > 1$ is the golden ratio.
background
The RS Baryogenesis module formalizes a mechanism in which nine ledger parities select a unique CP-odd pseudoscalar channel, producing η_B ≈ 5.1 × 10^{-10} with no free parameters. Core definitions set λ_CP = φ^{-7} and κ_CP = φ^{-9}. The upstream lemma lt_trans supplies transitivity of the strict order on the reals, while lambda_CP_lt_one proves λ_CP < 1 via rpow comparison and lambda_gt_kappa proves κ_CP < λ_CP because the exponent -9 is smaller than -7 when the base exceeds 1.
proof idea
The proof is a one-line wrapper that applies lt_trans to lambda_gt_kappa and lambda_CP_lt_one.
why it matters
This result supplies the missing upper bound inside kappa_CP_bounds, which then feeds eta_B_prediction and eta_B_positive. It completes the CP-coupling chain step required by the baryogenesis paper proposition. The surrounding framework fixes the couplings via the phi self-similar fixed point and the eight-tick octave, with D = 3 and the alpha band emerging from the same ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.