module module high

`IndisputableMonolith.CrossDomain.RecognitionGenerators`

The RecognitionGenerators module establishes that the set {2, 3, 5} is the smallest generating set for the spectrum. It supplies definitions for generators G2, G3, G5 together with decomposition lemmas for the listed composites. Researchers working on spectral structure in the phi-ladder would cite this module. The module is definitional with supporting lemmas.

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

background

The CrossDomain.RecognitionGenerators module sits inside the Recognition Science framework and treats the spectrum as the collection of values generated under the Recognition Composition Law. It introduces generators G2, G3, G5 for the primes 2, 3, 5 and supplies decomposition maps for the integers 4, 6, 7, 8, 10, 12, 15, 16, 25. These objects support constructions that appear in the forcing chain from T0 to T8 and in the phi-ladder mass formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the minimal generating set {2, 3, 5} that feeds all subsequent cross-domain recognition constructions. It directly implements the claim that this set is smallest, thereby grounding spectral decompositions used for the eight-tick octave and the derivation of constants such as hbar = phi^{-5}.

scope and limits

Does not prove uniqueness of the generating set beyond minimality.
Does not derive physical constants or alpha-band bounds.
Does not contain numerical evaluations or external data.

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