six_partition
plain-language theorem explainer
The theorem fixes the quark flavour count as three generations times two charge types in the Recognition Science phi-ladder model. Physicists deriving the six-flavour mass hierarchy cite it to anchor the structural input for u, d, s, c, b, t. The proof is a one-line decision procedure that discharges the arithmetic equality directly.
Claim. $6 = 3 times 2$, where the left side counts the six quark flavours and the right side factors into three generations and two charge types (up-type and down-type).
background
The module places six quark flavours (u, d, s, c, b, t) on a phi-ladder mass scale and treats adjacent-flavour ratios as coarse structural data. It records that six equals three generations times two charge types. No upstream lemmas are invoked; the statement is pure arithmetic inside the Recognition Science constants and forcing chain setup.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality 6 = 3 * 2.
why it matters
It supplies the six_is_three_times_two field inside the quarkMassCert definition that assembles the full quark mass certificate. The result completes the flavour-count step required by the module's phi-ladder construction and feeds the mass formula yardstick * phi^(rung - 8 + gap(Z)). It anchors the T6 self-similar fixed point to the observed quark spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.