DetectionMethod
The inductive type DetectionMethod enumerates the five standard techniques for registering particle interactions in high-energy experiments. Modelers of detector arrays or authors of simulation frameworks cite the enumeration when fixing the configuration dimension at five. The declaration is a direct inductive construction that derives decidable equality and finite cardinality without additional lemmas.
claimAn inductive type whose five constructors are tracking, calorimetry, time-of-flight measurement, Čerenkov radiation detection, and transition radiation detection.
background
In the Recognition Science setting a particle detector is treated as a recognition lattice for quantum-field events. The module equates five canonical detection methods with configuration dimension D = 5 and notes that six quark flavors and six lepton flavors each equal the number of faces on a cube. The inductive type supplies the concrete enumeration that makes the cardinality statement immediate.
proof idea
The declaration is an inductive definition introducing five constructors, followed by a deriving clause that installs DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters in Recognition Science
The type is required by the downstream theorem detectionMethodCount, which proves its cardinality equals five, and by the structure ParticlePhysicsDepthCert that records the five-detector, six-quark, six-lepton certification. It therefore realizes the module claim that five detectors equal configDim D = 5 inside the RS-native framework.
scope and limits
- Does not claim these five methods are exhaustive.
- Does not derive detection efficiencies or cross sections.
- Does not link individual methods to specific particle species.
formal statement (Lean)
20inductive DetectionMethod where
21 | tracking | calorimetry | timeOfFlight | cherenkov | transitionRadiation
22 deriving DecidableEq, Repr, BEq, Fintype
23