eightFoldWayCert
plain-language theorem explainer
The eightFoldWayCert definition assembles a record that certifies the meson octet has size eight, the baryon decuplet has size ten, and exactly five hadron families exist, all obtained from the Recognition Science lattice period at three dimensions. Hadron classification theorists extending Gell-Mann's eight-fold way would cite it when linking multiplet sizes to the eight-tick octave. The construction is a direct record literal that supplies the three fields from prior decide lemmas.
Claim. Let $C$ be the structure whose fields assert that the meson octet cardinality equals $2^3$, the baryon decuplet cardinality equals $2 times 5$, and the cardinality of the type of hadron families equals 5. Then eightFoldWayCert is the instance of $C$ obtained by setting the first field to the equality meson octet count = $2^3$, the second field to baryon decuplet count = $2 times 5$, and the third field to the cardinality of HadronFamily = 5.
background
The module derives the eight-fold way from Recognition Science by identifying the octet size with the lattice period $2^D$ at $D=3$ and the decuplet size with twice the configuration dimension. Five canonical families (pion, kaon, eta, rho, omega) are taken to equal that same dimension. The upstream theorems establish each count by direct computation: meson octet count equals $2^3$, baryon decuplet count equals $2 times 5$, and the cardinality of HadronFamily equals 5.
proof idea
The definition constructs the EightFoldWayCert record by assigning the octet field to the theorem mesonOctet_eq_2cubeD, the decuplet field to decuplet_eq_2_times_5, and the family field to hadronFamilyCount. Each supplying theorem is itself a one-line result proved by decide, so the definition performs no additional reasoning beyond the record construction.
why it matters
This definition supplies the concrete certificate that realises the module claim linking Gell-Mann's eight-fold way to the Recognition Science eight-tick octave at $D=3$ and the configuration dimension five. It closes the local development of hadron multiplet sizes under T7 and the spatial dimension result T8. No downstream uses appear yet, leaving open its role in larger spectrum derivations that would invoke the phi-ladder or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.