lambda_CP_bounds
The theorem establishes that the CP-odd gravitational coupling satisfies 0 < λ_CP < 1. Cosmologists formalizing parameter-free baryogenesis in Recognition Science cite this to confirm the coupling derived solely from the golden ratio. The proof is a term-mode conjunction that directly pairs the separate positivity and upper-bound results.
claim$0 < λ_{CP} ∧ λ_{CP} < 1$, where $λ_{CP} = φ^{-7}$ and $φ > 1$ denotes the golden ratio.
background
In the RS Baryogenesis module the CP-odd gravitational coupling is defined by λ_CP = φ^{-7}, fixing the strength of the χ R R̃ term in the CP-violating Lagrangian. This rests on the PrimitiveDistinction theorem that extracts four structural conditions plus three definitional facts from seven independent axioms. The positivity lemma states λ_CP > 0 while the upper-bound lemma shows λ_CP < 1 because φ > 1 and the exponent is negative.
proof idea
The proof is a one-line term wrapper that constructs the conjunction from the positivity theorem and the strict upper-bound theorem. It applies Real.rpow_pos_of_pos to the definition λ_CP = φ^{-7} for the lower bound and Real.rpow_lt_rpow_of_exponent_lt (with one_lt_phi and norm_num) for the upper bound.
why it matters in Recognition Science
The bound supplies the lambda_from_phi field inside the baryogenesis_cert theorem that certifies the full mechanism, including η_B ≈ 5.1 × 10^{-10}. It completes the step in the RS Baryogenesis paper where the CP-odd couplings are shown positive and sub-unity, consistent with the phi-ladder and T6 self-similar fixed point. No open scaffolding remains.
scope and limits
- Does not compute the numerical value of λ_CP.
- Does not establish the corresponding bounds for κ_CP.
- Does not derive the baryon asymmetry η_B.
- Does not connect to the inflaton parameter α_infl.
formal statement (Lean)
57theorem lambda_CP_bounds : 0 < lambda_CP ∧ lambda_CP < 1 :=
proof body
Term-mode proof.
58 ⟨lambda_CP_pos, lambda_CP_lt_one⟩
59
60/-- κ_CP < 1 (follows from κ < λ < 1). -/