pith. machine review for the scientific record. sign in
def definition def or abbrev high

G3

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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}.

scope and limits

formal statement (Lean)

  42def G3 : ℕ := 3  -- spatial dim

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.