second_primorial
plain-language theorem explainer
The product of the binary-face generator and the spatial-dimension generator equals the second primorial. Researchers enumerating the Recognition Science cardinality spectrum cite this to anchor the decomposition of 6 from the primitive set. The proof evaluates the multiplication directly via a decision procedure after substitution.
Claim. Let $G_2 = 2$ be the binary face generator and $G_3 = 3$ the spatial dimension generator. Then $G_2 G_3 = 6$.
background
The module proves that every integer in the RS cardinality spectrum reduces to a polynomial in the generators G = {2, 3, 5} via addition, multiplication, exponentiation, and binomial coefficients. Concrete reductions listed include 6 = 2 · 3, 4 = 2², 12 = 2² · 3, and 30 = 2 · 3 · 5. The local claim is that no spectrum member lies outside this closure.
proof idea
One-line wrapper that applies the decide tactic to the substituted equality G2 * G3 = 6.
why it matters
This verifies the second primorial inside the structural meta-claim of C27 that the RS spectrum is generated from {2, 3, 5}. It supplies the base case for the primorial sequence p₁# = 2, p₂# = 6, p₃# = 30 that appears in the module documentation. No downstream theorems are recorded, yet the result closes one elementary step in the zero-sorry enumeration of spectrum members.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.