mesonFamily_count
plain-language theorem explainer
mesonFamily_count fixes the number of meson families at five in the Recognition Science phi-ladder spectrum. Modelers of meson masses via adjacent-family ratios cite the count to certify completeness of the classification. The proof is a direct decision on the finite inductive type with five constructors.
Claim. $|M| = 5$ where $M$ is the finite set of meson families consisting of the pseudoscalar, vector, scalar, axial-vector, and tensor cases.
background
The module defines the meson spectrum from the phi-ladder at S2 depth, with five canonical families matching configuration dimension D = 5. MesonFamily is the inductive type whose constructors are exactly pseudoscalar, vector, scalar, axialVector, and tensor, each equipped with DecidableEq, Repr, BEq, and Fintype instances. The module imports Constants and states that adjacent-family mass ratios follow the phi-ladder while the full spectrum carries zero sorry or axiom.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression for MesonFamily. The tactic enumerates the five constructors and returns the equality directly.
why it matters
The result supplies the five_families field inside the downstream mesonSpectrumCert definition, which also records the phi_ratio and mass positivity. It therefore anchors the five-family structure required for the S2-depth meson spectrum certification in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.