kappa_CP_pos
plain-language theorem explainer
The declaration establishes that the CP-odd coupling κ_CP is strictly positive. Baryogenesis calculations cite this when bounding the asymmetry parameter η_B from the nine ledger parities. The proof is a one-line term application of the real-power positivity lemma to the definition κ_CP = φ^{-9} with φ > 1.
Claim. $0 < κ_{CP}$ where $κ_{CP} = φ^{-9}$ and $φ > 1$ denotes the golden ratio.
background
The module formalizes the RS baryogenesis mechanism in which nine ledger parities select a unique CP-odd pseudoscalar channel. Core results include the CP-odd couplings λ_CP = φ^{-7} and κ_CP = φ^{-9} together with the recognition mass scale M_rec = 2√(2π) M_Pl and the predicted asymmetry η_B ≈ 5.1 × 10^{-10}. Upstream, kappa_CP is defined as the CP-odd electromagnetic coupling κ_CP = φ^{-9} that sets the strength of the χFF̃ term.
proof idea
The proof is a direct term-mode application of Real.rpow_pos_of_pos to the definition of kappa_CP together with the already-established positivity of phi.
why it matters
This result feeds kappa_CP_bounds, which in turn supports the baryon asymmetry prediction η_B ≈ 5.1 × 10^{-10} and the claim that both CP couplings lie in (0,1). It closes the positivity half of the parameter-free asymmetry derivation in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.