EightFoldWayCert
plain-language theorem explainer
The EightFoldWayCert structure packages the three numerical identities that recover Gell-Mann's octet and decuplet counts from the Recognition Science lattice at D=3. A physicist modeling hadron spectroscopy would cite it to tie the 8-tick period directly to the observed multiplet sizes. The definition records the equalities mesonOctetCount=8, baryonDecupletCount=10, and five hadron families by direct field assignment.
Claim. Let $M$ be the meson octet count, $B$ the baryon decuplet count, and $H$ the inductive type of hadron families. The certificate asserts $M=2^3$, $B=2×5$, and $|H|=5$.
background
In the Eight-Fold Way from RS module the constants are fixed by definition: mesonOctetCount equals 8 and baryonDecupletCount equals 10. HadronFamily is the inductive type whose five constructors are pion, kaon, eta, rho, and omega, so its Fintype cardinality is 5. The module places these counts against the eight-tick octave at three spatial dimensions, where 8 equals 2 to the power D and 10 equals twice the configuration dimension.
proof idea
The structure is introduced by direct field assignment of the three equalities. No tactics are used; the supporting counts are supplied by the sibling definitions mesonOctetCount and baryonDecupletCount together with the derived Fintype instance on HadronFamily.
why it matters
This certificate supplies the concrete numerical anchors consumed by the downstream eightFoldWayCert construction. It thereby embeds the eight-fold way inside the T7 eight-tick octave and T8 three-dimensional lattice of the unified forcing chain. The module states that the counts are obtained by decide with zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.