primorial_product
plain-language theorem explainer
The product of the three recognition generators equals the third primorial. Spectrum decomposition researchers cite it to anchor the base case that every enumerated RS cardinality member factors through {2, 3, 5}. The proof reduces to a single decision procedure on natural numbers after the generator constants are substituted.
Claim. $2 · 3 · 5 = 30$
background
The Recognition Generators module introduces three primitive integer generators: the binary-face generator equal to 2, the spatial-dimension generator equal to 3, and the configuration-dimension generator equal to 5. These serve as the basis for expressing every integer in the RS cardinality spectrum via addition, multiplication, exponentiation, and binomial coefficients. The module states that no spectrum member lies outside such expressions, with explicit decompositions supplied for the members listed in C21. Upstream, the canonical arithmetic object supplies the realization-independent Peano structure that justifies treating these generators as ordinary natural numbers.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. After the definitions of the three generators are unfolded, decide computes the product directly and confirms equality to 30.
why it matters
This result populates the primorial_3 field inside the RecognitionGeneratorsCert structure, which certifies the full generator set for the spectrum. It directly supports the C27 meta-claim that every spectrum integer reduces to a polynomial in {2, 3, 5}. In the broader framework it supplies the numerical foundation for the eight-tick octave and the three spatial dimensions encoded by the generators. The downstream certificate uses this equality to close the generator verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.