CPProcess
plain-language theorem explainer
The inductive type enumerates the five canonical CP-violating processes (kaon indirect, kaon direct, B meson mixing, B to J/psi Ks, D meson mixing) that Recognition Science identifies with configuration dimension D = 5. High-energy physicists studying epsilon, sin 2beta, or Jarlskog bounds would cite the enumeration when certifying process completeness or applying the J(phi)/45 band. The definition is a direct inductive construction that derives Fintype to support immediate cardinality results.
Claim. Let $P$ be the finite set of canonical CP-violating processes, defined by the five constructors: kaon indirect violation ($varepsilon$), kaon direct violation ($varepsilon'$), B-meson mixing, $B to J/psi K_S$ (sin $2beta$), and D-meson mixing.
background
The module models CP violation inside Recognition Science by fixing exactly five processes whose count equals the configuration dimension D = 5. These processes are kaon indirect (epsilon), kaon direct (epsilon-prime), B meson mixing, B to J/psi Ks (sin 2beta), and D meson mixing. The local setting states that the Jarlskog invariant J_CP is bounded by the canonical J(phi)/45 band, where phi is the self-similar fixed point from the forcing chain.
proof idea
The declaration is an inductive definition that introduces the five named constructors and derives the instances DecidableEq, Repr, BEq, and Fintype in a single step.
why it matters
This enumeration supplies the concrete list required by the downstream theorem cpProcess_count (Fintype.card CPProcess = 5) and the structure CPViolationCert. It realizes the configDim D = 5 step in the CP-violation analysis and anchors the Jarlskog bound inside the Recognition Science S4 depth treatment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.