epsilon_CP
plain-language theorem explainer
This definition supplies the base CP violation parameter ε_CP = 0.001 drawn from the eight-tick phase structure. Baryogenesis calculations in Recognition Science cite it when linking the 8-tick asymmetry to the observed matter excess η. The assignment is a direct constant definition with no further reduction steps.
Claim. $ε_{CP} := 10^{-3}$, where $ε_{CP}$ is the CP violation parameter arising from phase asymmetry in the eight-tick structure (with the Standard Model scale for K-meson decays).
background
The Cosmology.MatterAntimatter module targets derivation of the baryon-to-photon ratio η ≈ 6.1 × 10^{-10} from the φ-structure. The eight-tick octave supplies intrinsic phase asymmetry that produces CP violation; ε_CP parameterizes the resulting charge-parity mismatch before dilution. The module doc states that η emerges directly from this CP violation once Sakharov conditions are met.
proof idea
Direct definition that assigns the real constant 1e-3. No lemmas or tactics are invoked; the value is taken as the observed scale in K-meson decays.
why it matters
The definition supplies the starting scale for the relation η = ε_CP × dilutionFactor that appears in sibling declarations such as eta_from_epsilon. It instantiates the T7 eight-tick octave landmark, where phase asymmetry supplies the CP violation required by the Sakharov conditions. It leaves open the precise mechanism that supplies the additional suppression to reach the observed 10^{-10}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.