module module high

`IndisputableMonolith.CrossDomain.RecognitionGenerators`

RecognitionGenerators asserts that the set {2, 3, 5} is the smallest generating set for the spectrum. It supplies definitions G2, G3, G5 together with decomposition maps for the listed composites. The module contains only definitions and no theorems or proofs.

claimThe set $\{2, 3, 5\}$ is the smallest generating set for the spectrum.

background

This module belongs to the CrossDomain section and imports only Mathlib. It introduces the generators G2, G3, G5 for the primes 2, 3, 5 and the decomposition functions four_decomp through twentyfive_decomp. The local setting is the construction of the spectrum from a minimal integer set under the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds spectrum-generation steps used by cross-domain recognition results. It directly encodes the claim that {2, 3, 5} is the minimal generating set, supporting the phi-ladder and mass-formula constructions in the overall framework.

scope and limits

Does not prove that {2, 3, 5} generates every spectrum element.
Does not define the spectrum itself.
Does not connect the generators to specific constants such as alpha or G.
Does not contain any Lean theorems or proofs.

declarations in this module (25)

def G2 L41
def G3 L42
def G5 L43
theorem four_decomp L47
theorem six_decomp L48
theorem seven_decomp L49
theorem eight_decomp L50
theorem ten_decomp L51
theorem twelve_decomp L52
theorem fifteen_decomp L53
theorem sixteen_decomp L54
theorem twentyfive_decomp L55
theorem fortyfive_decomp L56
theorem seventy_decomp L57
theorem oneTwentyFive_decomp L58
theorem twoSixteen_decomp L59
theorem twoFiftySix_decomp L60
theorem threeSixty_decomp L61
theorem threeOneTwentyFive_decomp L62
theorem generators_minimal L67
theorem primorial_product L72
theorem second_primorial L76
theorem third_primorial L77
structure RecognitionGeneratorsCert L79
def recognitionGeneratorsCert L92