detectionMethodCount
plain-language theorem explainer
Five canonical detection methods are counted in the Recognition Science model of particle detectors. Detector modelers and RS theorists cite the result to confirm that the method count equals configDim D = 5. The proof is a one-line decision computation on the inductive type that enumerates the five constructors.
Claim. The finite cardinality of the type of detection methods equals five: $ |DetectionMethod| = 5 $, where DetectionMethod enumerates the constructors tracking, calorimetry, time-of-flight, Čerenkov, and transition radiation.
background
The module Particle Physics Depth from RS (B7/B8) treats a particle detector as a recognition lattice for quantum field events. It fixes five canonical methods (tracking, calorimetry, time-of-flight, Čerenkov, transition radiation) to match configDim D = 5, while separately noting that six quarks and six leptons each equal the number of cube faces. The upstream inductive definition DetectionMethod lists exactly these five constructors and derives the Fintype instance required for cardinality computation.
proof idea
The proof is a one-line term that invokes the decide tactic. Because DetectionMethod is an inductive type with five explicit constructors and carries a Fintype instance, decide evaluates the cardinality directly to 5.
why it matters
The theorem supplies the five_detectors field inside the ParticlePhysicsDepthCert definition, which certifies the B7/B8 depth claim for particle physics from RS. It anchors the detector configuration dimension at five, complementing the cube-face counts for quarks and leptons; this sits alongside the forcing-chain result T8 that forces spatial dimension D = 3 from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.