RecognitionGeneratorsCert
plain-language theorem explainer
RecognitionGeneratorsCert packages the assignments of the three base integers 2, 3 and 5 together with their product equaling 30, pairwise distinctness, and explicit reductions of spectrum values such as 4 as 2 squared, 6 as 2 times 3, 45 as 3 squared times 5, 125 as 5 cubed, and 360 as 2 cubed times 3 squared times 5. A researcher working on integer reductions in the RS cardinality spectrum would cite the certificate to fix the generator set. The structure is filled by direct reflexivity on the constant definitions plus two short lemmas for a
Claim. The structure asserts that the generators satisfy $G_2=2$, $G_3=3$, $G_5=5$, that $G_2 G_3 G_5=30$, that the three generators are pairwise distinct, and that the spectrum integers decompose as $4=G_2^2$, $6=G_2 G_3$, $45=G_3^2 G_5$, $125=G_5^3$, $360=G_2^3 G_3^2 G_5$.
background
The module treats the RS cardinality spectrum as generated from the three primitive integers 2 (binary face), 3 (spatial dimension), and 5 (configuration dimension). These are fixed by the sibling definitions G2, G3, and G5. The surrounding documentation for C27 states that every enumerated spectrum member reduces to a polynomial expression in this set via multiplication, exponentiation, and binomial coefficients, with explicit examples including 4=2², 6=2·3, 45=3²·5, 125=5³, and 360=2³·3²·5.
proof idea
The declaration is a bare structure definition. Its fields are populated in the downstream definition recognitionGeneratorsCert by reflexivity on the three generator constants together with the lemmas primorial_product and generators_minimal.
why it matters
The certificate fixes the generator triple that supports the C27 claim that the entire enumerated spectrum decomposes over {2,3,5}. It is instantiated by the definition recognitionGeneratorsCert and thereby supplies the integer basis used in cross-domain spectrum arguments. The choice of generators aligns with the spatial dimension D=3 and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.