decuplet_eq_2_times_5
plain-language theorem explainer
The declaration equates the baryon decuplet count to the product of two and five. Particle physicists reconstructing Gell-Mann's eight-fold way inside Recognition Science cite this factorization when building the certification record for hadron multiplets. The proof is a one-line decision procedure that confirms the numerical identity by direct computation from the upstream definition.
Claim. The baryon decuplet cardinality equals $2 times 5$.
background
The Eight-Fold Way from RS module assigns the baryon decuplet a count of ten and factors it as two times five, matching the configuration dimension D equal to five. This sits inside the local setting where eight equals two to the power D for the octet structures while the decuplet uses the product form. The upstream definition baryonDecupletCount : Nat := 10 supplies the left-hand side of the equality.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality between the constant definition of ten and the arithmetic expression two times five.
why it matters
This supplies the decuplet_2times5 field inside the EightFoldWayCert definition, which also records the octet equality to two cubed D and the five-family count. It realizes the module statement that the baryon decuplet is ten equals two times five, connecting to the eight-tick octave at D equals three. No open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.