cpProcess_count
plain-language theorem explainer
The number of canonical CP-violating processes recognized in the framework is fixed at five. Flavor physicists bounding the Jarlskog invariant from the phi-ladder would cite this enumeration when connecting RS to kaon and B-meson data. The proof is a direct decision on the finite cardinality of the inductive type that lists exactly those five processes.
Claim. The set of canonical CP-violating processes has cardinality five, where the processes are indirect kaon decay, direct kaon decay, B-meson mixing, $B$ to $J/ψ K_S$, and D-meson mixing.
background
Recognition Science derives CP violation from the single functional equation via the Recognition Composition Law. The module enumerates five canonical processes that match observed CP-violating phenomena: kaon indirect (ε), kaon direct (ε'), B meson mixing, B → J/ψ K_S (sin 2β), and D meson mixing. These are collected in an inductive type whose five constructors are the only inhabitants.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the finite-type cardinality of the inductive definition.
why it matters
This supplies the process count required by the downstream CP violation certificate, which asserts five processes and places the Jarlskog invariant inside the J(φ)/45 band. It completes the enumeration step that links RS forcing to flavor physics, consistent with the eight-tick octave and D = 3. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.