G3
plain-language theorem explainer
G3 is the constant natural number 3 that supplies the spatial dimension in the generator set {2, 3, 5} from which all Recognition Science spectrum integers are built by addition, multiplication, exponentiation and binomial coefficients. Cross-domain decompositions cite it when reducing members such as 15 or 45 back to the primitives. The declaration is a direct constant assignment with no computation or lemmas.
Claim. Let $G_3 = 3$ denote the spatial dimension in the generator triple $G = (G_2, G_3, G_5)$ with $G_2 = 2$ and $G_5 = 5$.
background
The module shows that every integer in the RS cardinality spectrum arises from the small set G = {2, 3, 5} via addition, multiplication, exponentiation and choose. Here 2 stands for the binary face, 3 for spatial dimension and 5 for configuration dimension; the claim is that no spectrum member lies outside the polynomials generated by these three values. This matches the framework landmark T8 that forces exactly three spatial dimensions.
proof idea
Direct definition that assigns the literal constant 3 to G3, with no tactics or upstream lemmas invoked beyond the upstream dim definition that sets the spatial dimension to D.
why it matters
G3 supplies the spatial factor required by the eleven downstream declarations in the same module, including fifteen_decomp (15 = G3 * G5), fortyfive_decomp (45 = G3² * G5), primorial_product (G2 * G3 * G5 = 30) and generators_minimal. It instantiates the T8 result D = 3 inside the RecognitionGeneratorsCert structure and thereby closes the meta-claim that the entire spectrum reduces to operations on {2, 3, 5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.