kappa_CP_bounds
plain-language theorem explainer
The bound 0 < κ_CP < 1 holds for the CP-odd coupling κ_CP = φ^{-9} where φ > 1 is the self-similar fixed point. Baryogenesis calculations cite this result to place the χFF̃ interaction strength inside the open unit interval with no free parameters. The proof is a one-line wrapper that pairs the positivity lemma with the strict upper-bound lemma.
Claim. Let κ_CP = φ^{-9} where φ > 1 is the self-similar fixed point. Then 0 < κ_CP < 1.
background
The RS Baryogenesis module formalizes a mechanism in which nine ledger parities select a unique CP-odd pseudoscalar channel. The coupling κ_CP = φ^{-9} sets the strength of the χFF̃ term and enters the prediction η_B ≈ 5.1 × 10^{-10}. The module documentation states that the baryon asymmetry follows from the CP-odd couplings, the inflaton dynamics, and the freeze-out temperature, with zero free parameters.
proof idea
The proof is a one-line wrapper that applies the positivity lemma for κ_CP together with the lemma establishing κ_CP < 1.
why it matters
This bound supplies the kappa_from_phi field inside the baryogenesis_cert theorem that assembles the full certification of the RS baryogenesis mechanism. It confirms that the CP-odd coupling derived from φ^{-9} satisfies the interval required for the asymmetry prediction to lie within 20 percent of the observed value. The construction ties to the forcing chain step that fixes φ as the unique self-similar point, ensuring the coupling emerges without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.