DetectionMethod
plain-language theorem explainer
The inductive type enumerates the five standard particle detection techniques employed in high-energy experiments. Modelers of detector lattices inside the Recognition Science framework cite it to fix the configuration dimension at five. The declaration is a direct inductive enumeration that derives DecidableEq, Repr, BEq and Fintype instances with no additional proof obligations.
Claim. The finite set of particle detection methods is defined as the inductive type whose constructors are tracking, calorimetry, time-of-flight, Čerenkov detection and transition-radiation detection.
background
Module ParticlePhysicsDepthFromRS treats a particle detector as a recognition lattice for quantum-field events and sets the configuration dimension D equal to the number of canonical detection methods. The local setting equates this count to five while separately recording that six quark flavors and six lepton flavors each match the number of faces of a cube. No upstream lemmas are required; the definition stands as the module's opening enumeration.
proof idea
The declaration is the base inductive definition itself. It carries no proof body and relies on the automatic derivation of the four type-class instances listed in the signature.
why it matters
The definition supplies the five_detectors component of the ParticlePhysicsDepthCert structure and is the target of the detectionMethodCount theorem that asserts cardinality five. It fills the B7/B8 slot by anchoring the detector configuration dimension inside the Recognition Science lattice picture, consistent with the framework's separation of spatial dimension D=3 from auxiliary configuration dimensions. No open questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.