kappa_CP
plain-language theorem explainer
The definition fixes the CP-odd electromagnetic coupling at the golden ratio to the negative ninth power. Cosmologists deriving a parameter-free baryon asymmetry from ledger parities cite this value when fixing the strength of the pseudoscalar interaction. The assignment is a direct substitution of the self-similar fixed point into the reals, with no further computation required.
Claim. The CP-odd electromagnetic coupling is defined by $k_{CP} := phi^{-9}$, where $phi$ is the golden ratio. This sets the coefficient of the $chi F tilde{F}$ term in the effective Lagrangian for baryogenesis.
background
The RS Baryogenesis module constructs a mechanism in which nine ledger parities select a unique CP-odd pseudoscalar channel, producing a baryon-to-photon ratio near the observed value with all scales fixed by the golden ratio alone. The two CP-odd couplings are assigned as lambda_CP = phi^{-7} and k_CP = phi^{-9}, entering the Lagrangian through the chi F tilde{F} interaction whose magnitude is controlled by k_CP. Upstream results establish that the underlying simplicial structures and collision-free programs remain axiom-free, supplying the ledger parities without additional hypotheses.
proof idea
This is a direct definition that assigns the real number phi raised to the power of negative nine. No lemmas or tactics are invoked; the value is substituted explicitly from the module constants.
why it matters
The definition supplies the smaller CP-odd coupling required by the BaryogenesisCert structure, which certifies the eta_B prediction, the spectral index bounds, and the inequality k_CP less than lambda_CP. It implements the paper's assignment of k_CP = phi^{-9} derived solely from the golden ratio. In the Recognition framework this traces to the self-similar fixed point forced at T6 of the unified forcing chain, enabling the eight-tick octave and three spatial dimensions to generate the observed asymmetry without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.