particlePhysicsDepthCert
plain-language theorem explainer
This definition packages the particle physics depth certificate by binding the detector count to 5 and the quark and lepton flavor counts to 6. Researchers mapping particle spectra onto the RS recognition lattice would cite it to record the numerical agreement with cube geometry. The construction is a direct structure literal that pulls the three field values from sibling theorems.
Claim. The particle physics depth certificate is the structure asserting that the cardinality of detection methods equals 5, the number of quark flavors equals 6, and the number of lepton flavors equals 6.
background
In the Recognition Science setting, a particle detector functions as a recognition lattice for quantum field events. The structure ParticlePhysicsDepthCert collects three assertions: the cardinality of the DetectionMethod type is 5 (corresponding to tracking, calorimetry, time-of-flight, Čerenkov, and transition radiation detectors), quarkFlavors equals 6, and leptonFlavors equals 6. Both flavor counts are interpreted as matching the six faces of a cube.
proof idea
The definition constructs an instance of ParticlePhysicsDepthCert by direct field assignment: five_detectors receives the value of detectionMethodCount, six_quarks receives quarkFlavors_eq_cubeFaces, and six_leptons receives leptonFlavors_eq_cubeFaces. It is a one-line structure literal that assembles the three pre-established equalities.
why it matters
This definition supplies the terminal certificate for the B7/B8 claims in the particle physics depth module. It records the concrete numerical matches (five detectors, six quarks, six leptons) that align with the cube-face geometry and configDim D = 5. No downstream theorems depend on it, so it functions as a packaged fact for potential later use in the forcing chain or mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.