mesonFamily_count
plain-language theorem explainer
The theorem asserts that the meson families enumerated in the Recognition Science phi-ladder model total exactly five. A physicist certifying the meson spectrum would cite this cardinality when populating the five_families slot of the spectrum certificate. The proof is a one-line decision procedure that checks the finite type with five explicit constructors.
Claim. The set of meson families has cardinality five, where the families comprise the pseudoscalar, vector, scalar, axial-vector, and tensor cases: $|M| = 5$ with $M$ the enumerated set of five families.
background
The module on the meson spectrum from the φ-ladder at S2 depth introduces five canonical meson families that realize configDim D = 5. These are the pseudoscalar (π, K, η), vector (ρ, ω, K*, φ), scalar (a₀, f₀), axial vector (a₁, b₁), and tensor (a₂, f₂) families, with adjacent-family mass ratios governed by the φ-ladder. The upstream inductive definition enumerates precisely these five cases and derives the Fintype instance used for cardinality.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance of the inductive type with five constructors.
why it matters
This result supplies the five_families field inside the mesonSpectrumCert definition. It realizes the five-family structure asserted in the module documentation for the φ-ladder meson spectrum. In the Recognition framework the count fixes configDim D = 5 for mesons, complementing the spatial dimension D = 3 obtained from the forcing chain at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.