mesonOctet_eq_2cubeD
plain-language theorem explainer
The theorem equates the meson octet count to eight, matching the eight-tick lattice period at three dimensions. Particle physicists applying the eight-fold way to hadron classification would cite it to anchor empirical octet size in Recognition Science periodicity. The proof is a direct decision procedure that evaluates the equality from the fixed definition of the count.
Claim. Let $N$ be the number of mesons in the octet. Then $N = 2^3$.
background
The module derives the eight-fold way from Recognition Science by mapping Gell-Mann octets and decuplets onto the eight-tick period and five-dimensional configuration space. The upstream definition fixes the meson octet count at eight. This supplies the concrete integer that the present equality compares against the power expression, confirming the lattice periodicity without further hypotheses.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the numerical identity between the predefined count and the expression two to the third power.
why it matters
The result supplies the octet_2cubeD field inside the EightFoldWayCert structure that certifies the full alignment of hadron families with RS. It instantiates the eight-tick octave (T7) and spatial dimension three (T8) from the forcing chain, showing that the observed meson octet size equals the lattice period 2^D at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.