recognitionGeneratorsCert
plain-language theorem explainer
This definition assembles a certificate confirming that the integers 2, 3, and 5 generate the Recognition Science spectrum through addition, multiplication, and exponentiation. Cross-domain researchers would cite it when verifying that enumerated spectrum members reduce to these three generators without external primitives. The construction fills each field of the RecognitionGeneratorsCert structure by direct reflexivity for the base values and by substitution of the pre-proven decomposition theorems for the derived integers.
Claim. Let $G_2=2$, $G_3=3$, $G_5=5$. The certificate asserts $G_2 G_3 G_5=30$, that the three generators are pairwise distinct, and supplies the decompositions $4=G_2^2$, $6=G_2 G_3$, $45=G_3^2 G_5$, $125=G_5^3$, and $360=G_2^3 G_3^2 G_5$.
background
The module defines generators $G_2:=2$, $G_3:=3$, $G_5:=5$ and packages them inside the structure RecognitionGeneratorsCert. This structure records the base equalities, the primorial product $G_2 G_3 G_5=30$, pairwise distinctness, and explicit decompositions of spectrum members into polynomials over these generators. The local theoretical setting is the C27 meta-claim that every integer in the RS cardinality spectrum arises from a small set of operations on {2, 3, 5}, corresponding to binary face, spatial dimension, and configuration dimension.
proof idea
The definition constructs the RecognitionGeneratorsCert instance by assigning rfl to the three generator equalities and by direct substitution of the upstream decomposition theorems into the remaining fields. It invokes primorial_product for the product equality, generators_minimal for distinctness, four_decomp for the power-of-two case, six_decomp for the product of two generators, fortyfive_decomp for the square-times-five case, oneTwentyFive_decomp for the cube of five, and threeSixty_decomp for the mixed product.
why it matters
The definition supplies the concrete witness for the C27 structural meta-claim that the RS spectrum is generated by {2, 3, 5}. It collects the individual decomposition results (four_decomp, six_decomp, fortyfive_decomp, oneTwentyFive_decomp, threeSixty_decomp, primorial_product, generators_minimal) into a single reusable certificate. Within the framework this supports the forcing chain by confirming that the integer generators align with the eight-tick octave and the emergence of D=3 spatial dimensions, though no open questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.