lambda_gt_kappa
plain-language theorem explainer
The inequality between the CP-odd gravitational and electromagnetic couplings holds strictly in the Recognition Science baryogenesis model. Cosmologists modeling parameter-free matter-antimatter asymmetry cite this to establish dominance of the gravitational channel over the electromagnetic one. The proof reduces directly to the monotonicity of real exponentiation for base phi greater than one.
Claim. $phi^{-7} > phi^{-9}$ where $phi$ denotes the golden ratio satisfying $phi > 1$, with the left side defining the gravitational CP-odd coupling and the right side the electromagnetic one.
background
The RS Baryogenesis module defines the CP-odd couplings from powers of the golden ratio alone. lambda_CP equals phi to the power negative seven and sets the strength of the chi R R tilde term in the CP-violating Lagrangian, while kappa_CP equals phi to the power negative nine and sets the strength of the chi F F tilde term. The module derives a baryon asymmetry eta_B approximately 5.1 times 10 to the minus ten with no free parameters, using nine ledger parities to select a unique channel.
proof idea
The term proof unfolds the definitions of lambda_CP and kappa_CP, then applies Real.rpow_lt_rpow_of_exponent_lt to the base phi greater than one together with the numerical fact that negative nine is less than negative seven.
why it matters
This result supplies the grav_stronger component inside the BaryogenesisCert structure that certifies the full mechanism. It fills the step in the RS Baryogenesis paper that shows the gravitational CP-odd coupling exceeds the electromagnetic one, consistent with the Recognition Science forcing chain where phi is the unique self-similar fixed point. The downstream kappa_CP_lt_one theorem chains directly from it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.