CPViolationCert
plain-language theorem explainer
CPViolationCert is a structure that certifies exactly five canonical CP-violating processes exist in the Recognition Science model. Particle physicists studying CP violation in kaon and B-meson systems would cite it to tie the observed processes to the RS dimension parameter D equals 5. The declaration is a bare structure definition whose single field directly encodes the cardinality assertion via the Fintype instance on the enumerated process type.
Claim. The structure certifying CP violation is defined by the field asserting that the finite set of CP-violating processes has cardinality exactly 5, where the processes are the five canonical ones: indirect kaon decay, direct kaon decay, B-meson mixing, B to J/psi K_S decay, and D-meson mixing.
background
CPProcess is the inductive type that enumerates the five processes: indirect kaon, direct kaon, B-meson mixing, B to J/psi K_S, and D-meson mixing, and it derives a Fintype instance so that cardinality is well-defined. The module places this in the setting of CP violation from Recognition Science at S4 depth, where the process count is identified with configDim D equals 5 and the Jarlskog invariant is stated to lie in the J(phi)/45 band. The declaration depends only on this inductive enumeration and its derived Fintype structure.
proof idea
This is a structure definition with no proof body. It directly declares the field five_processes as the equality between Fintype.card of the process type and 5, using the automatically derived Fintype instance on the inductive enumeration.
why it matters
The structure supplies the type for the downstream concrete certificate that populates the field with the process count. It fills the opening claim in the CP Violation from RS module by fixing the five-process count that corresponds to D equals 5 in the Recognition Science forcing chain. This anchors the link between the RS-native constants and the five observed CP-violating channels without deriving their magnitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.