six_decomp
plain-language theorem explainer
The equality 6 equals the product of the binary-face generator 2 and the spatial-dimension generator 3 holds in the natural numbers. Cross-domain Recognition Science work cites this when confirming spectrum cardinalities reduce to the primitive set {2, 3, 5}. The proof applies a decision procedure to the arithmetic identity.
Claim. $6 = 2 × 3$, where 2 is the binary-face generator and 3 is the spatial-dimension generator.
background
The module establishes a structural meta-claim: every integer in the RS cardinality spectrum is generated by a small set of primitive operations on three integer generators G = {2, 3, 5}, corresponding to binary face, spatial dimension, and configDim. Operations include addition, multiplication, exponentiation, and choose. The listed examples include 6 = 2 · 3 as one of the spectrum members enumerated in C21.
proof idea
One-line wrapper that applies the decide tactic to the equality.
why it matters
This decomposition supports recognitionGeneratorsCert, which certifies the generators via rfl equalities and related minimality results. It fills in the claim that no spectrum member lies outside polynomials in {2, 3, 5}. The generators tie to framework landmarks T8 (D = 3) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.