third_primorial
plain-language theorem explainer
The product of the three recognition generators equals 30. Researchers verifying integer spectrum decompositions in Recognition Science cite this base case when checking primorial constructions from the set {2, 3, 5}. The proof is a direct arithmetic evaluation via the decide tactic after unfolding the generator definitions.
Claim. Let $G_2 = 2$ be the binary face generator, $G_3 = 3$ the spatial dimension generator, and $G_5 = 5$ the configuration dimension generator. Then $G_2 G_3 G_5 = 30$.
background
The RecognitionGenerators module establishes that every integer in the RS cardinality spectrum arises from the three primitive generators G = {2, 3, 5} via addition, multiplication, exponentiation, and binomial coefficients. G2 is defined as 2 (binary face), G3 as 3 (spatial dim), and G5 as 5 (configDim). The module documentation for C27 lists explicit reductions such as 30 = 2·3·5 and asserts that no spectrum member falls outside polynomials in these generators, with Lean status showing zero sorry or axiom.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality after the definitions of G2, G3, and G5 are unfolded.
why it matters
This equality anchors the primorial base within the generator set that the module claims exhausts the RS spectrum members enumerated in C21. It directly supports the structural meta-claim that every spectrum integer reduces to a polynomial in {2, 3, 5}, consistent with the eight-tick octave and D = 3 landmarks in the forcing chain. No downstream theorems are recorded, leaving it as a closed base case rather than an open interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.