lambda_CP_pos
plain-language theorem explainer
The theorem establishes that the CP-odd gravitational coupling λ_CP is strictly positive. Baryogenesis calculations cite it to fix the sign of the χRR̃ source term before bounding η_B. The proof is a one-line term application of the real-power positivity lemma to the base φ > 1 in the definition λ_CP = φ^{-7}.
Claim. $0 < λ_{CP}$ where $λ_{CP} := φ^{-7}$.
background
The RS Baryogenesis module defines the CP-odd gravitational coupling as λ_CP = φ^{-7}, which sets the strength of the χRR̃ term in the CP-violating Lagrangian. The module derives a parameter-free baryon asymmetry η_B ≈ 5.1 × 10^{-10} from nine ledger parities and the Recognition mass scale M_rec = 2√(2π) M_Pl. The upstream definition is the noncomputable declaration λ_CP : ℝ := phi ^ (-(7 : ℝ)).
proof idea
The proof is a direct term-mode application of Real.rpow_pos_of_pos to the hypothesis phi_pos.
why it matters
This supplies the left conjunct of lambda_CP_bounds, which feeds the positivity claim for η_B. It realizes the core result λ_CP = φ^{-7} stated in the module documentation. The argument rests on the self-similar fixed point φ from the T6 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.