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

G5

show as:
view Lean formalization →

G5 assigns the integer constant 5 as the configuration dimension generator within the Recognition Science spectrum. Cross-domain proofs that decompose spectrum members such as 15 and 125 cite this value when applying multiplication and exponentiation to the base set. The definition is a direct constant assignment requiring no further reduction steps.

claim$G_5 = 5$, where $G_5$ denotes the configuration dimension generator in the set of primitive generators for the RS cardinality spectrum.

background

The Recognition Generators module shows that every integer in the RS spectrum reduces to polynomials in the generators G = {2, 3, 5} under addition, multiplication, exponentiation, and binomial coefficients. G5 supplies the third generator, fixed at 5 to match the configuration dimension. Upstream results define configDim as d + 2 for spatial dimension d, yielding 5 when d = 3, and similarly set the constant to 5 in cosmology and game-theory contexts.

proof idea

G5 is introduced by the direct definition assigning the natural number 5. Downstream theorems then invoke this constant inside equalities that are discharged by decide.

why it matters in Recognition Science

G5 completes the minimal generator triple whose products recover spectrum members and the third primorial 30. It is used by fifteen_decomp, oneTwentyFive_decomp, primorial_product, and the RecognitionGeneratorsCert structure. This placement supports the module meta-claim that the spectrum is generated from {2, 3, 5} and aligns with the framework forcing of three spatial dimensions plus two ledger degrees of freedom.

scope and limits

formal statement (Lean)

  43def G5 : ℕ := 5  -- configDim

proof body

Definition body.

  44
  45/-! ## Spectrum decompositions. -/
  46

used by (11)

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

depends on (3)

Lean names referenced from this declaration's body.