ParticlePhysicsDepthCert
plain-language theorem explainer
ParticlePhysicsDepthCert records that five detector types exist, together with the six-quark and six-lepton flavor counts. A particle physicist mapping RS recognition lattices to collider observables would cite the structure when confirming that detector dimensionality matches the cube-face count for flavors. The definition is a direct record whose three fields are discharged by the cardinality of the DetectionMethod inductive type and the two constant definitions for quark and lepton flavors.
Claim. Let DetectionMethod be the inductive type whose five constructors are tracking, calorimetry, time-of-flight, Čerenkov, and transition-radiation detectors. The structure ParticlePhysicsDepthCert asserts that the cardinality of this type equals five, that the number of quark flavors equals six, and that the number of lepton flavors equals six.
background
The module treats a particle detector as a recognition lattice for quantum-field events. DetectionMethod is the inductive type with exactly the five constructors tracking, calorimetry, timeOfFlight, cherenkov, and transitionRadiation; its Fintype instance therefore supplies the cardinality five. The sibling constants quarkFlavors and leptonFlavors are each defined to be the numeral 6, each carrying the annotation that this count equals the number of cube faces.
proof idea
The declaration is the structure definition itself. Its three fields are filled by the Fintype.card lemma applied to DetectionMethod together with the two constant definitions quarkFlavors and leptonFlavors; no separate tactic script or lemma application is required.
why it matters
The structure supplies the concrete counts that the downstream definition particlePhysicsDepthCert packages into a single certificate. It thereby closes the B7/B8 step that equates detector dimensionality with the cube-face count for both quark and lepton flavors, linking the five canonical detection methods to the RS recognition lattice while leaving the spatial-dimension count D = 3 untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.