cpViolationCert
plain-language theorem explainer
This definition assembles the CP violation certificate by setting the count of canonical processes to five in the Recognition Science model. Researchers studying CP violation in meson systems would reference it to connect the five processes to the framework's dimension D equals 5. It is constructed as a direct instantiation of the certificate structure using the decidable cardinality result.
Claim. A certificate for CP violation is the record asserting that the number of canonical CP-violating processes equals five.
background
The module derives CP violation from Recognition Science at S4 depth, identifying five processes: kaon indirect (ε), kaon direct (ε'), B meson mixing, B → J/ψ K_S (sin 2β), and D meson mixing. The Jarlskog invariant J_CP is bounded within the J(φ)/45 band. The upstream theorem proves that the number of these CP processes is exactly five using a decision procedure. This count populates the certificate structure whose sole field requires this cardinality equality.
proof idea
The definition is a one-line wrapper that applies the cardinality theorem for the CP process set to fill the five_processes field of the certificate structure.
why it matters
This definition supplies the concrete CP violation certificate required by the Recognition Science framework for its S4 depth analysis. It completes the enumeration of five processes that follows from the J-uniqueness and phi fixed point in the forcing chain. No parent theorems are yet recorded as using it, leaving open the explicit derivation of the Jarlskog bound from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.