DetectionMethod
plain-language theorem explainer
DetectionMethod enumerates the five standard techniques for registering particle events. Recognition Science researchers cite it to anchor the detector configuration dimension at five. The declaration is an inductive type whose Fintype instance follows directly from the five listed constructors.
Claim. Let $D$ be the finite set whose elements are the five detection techniques: tracking, calorimetry, time-of-flight measurement, Čerenkov radiation, and transition radiation.
background
The module treats a particle detector as a recognition lattice for quantum-field events. Five canonical methods are identified with the configuration dimension $D=5$. The same section notes that six quarks and six leptons each equal the number of faces of a cube.
proof idea
The declaration is an inductive definition with five constructors. The deriving clause supplies the DecidableEq, Repr, BEq and Fintype instances automatically.
why it matters
DetectionMethod supplies the five_detectors component of ParticlePhysicsDepthCert and is the subject of the cardinality theorem detectionMethodCount. It realizes the B7/B8 claim that detector methods fix configDim $D=5$ and aligns the flavor counts (six quarks, six leptons) with cube faces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.