lambda_gt_kappa
plain-language theorem explainer
The inequality establishes that the gravitational CP-odd coupling exceeds the electromagnetic counterpart, with the former given by phi to the power -7 and the latter by phi to the power -9. Researchers constructing parameter-free baryogenesis models cite the result to confirm gravitational dominance in the CP-violating sector. The argument reduces directly to the monotonicity of real exponentiation once the base exceeds one and the exponents are compared numerically.
Claim. $phi^{-7} > phi^{-9}$ (with $phi$ the golden ratio).
background
The RS Baryogenesis module defines the CP-odd gravitational coupling as phi raised to -7, entering the chi R Rtilde term, and the electromagnetic coupling as phi raised to -9 for the chi F Ftilde term. The module derives a baryon asymmetry of order 5.1 times 10 to the -10 from nine ledger parities selecting a unique CP-odd channel, with no free parameters. Upstream, one_lt_phi proves phi exceeds 1 via the quadratic equation satisfied by the golden ratio, a fact reused across Constants and PhiSupport.
proof idea
The proof unfolds the two coupling definitions to expose the powers of phi. It then applies Real.rpow_lt_rpow_of_exponent_lt to one_lt_phi together with the norm_num fact that -9 is strictly less than -7.
why it matters
The result supplies the grav_stronger field inside baryogenesis_cert and is chained via transitivity to obtain kappa_CP_lt_one. It completes the required ordering of CP couplings in the Recognition Science baryogenesis construction, consistent with phi as the self-similar fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.