G2

formal source

  38
  39/-! ## The three primitive RS generators. -/
  40
  41def G2 : ℕ := 2  -- binary face
  42def G3 : ℕ := 3  -- spatial dim
  43def G5 : ℕ := 5  -- configDim
  44
  45/-! ## Spectrum decompositions. -/
  46
  47theorem four_decomp : (4 : ℕ) = G2^2 := by decide
  48theorem six_decomp : (6 : ℕ) = G2 * G3 := by decide
  49theorem seven_decomp : (7 : ℕ) = G2^3 - 1 := by decide
  50theorem eight_decomp : (8 : ℕ) = G2^3 := by decide
  51theorem ten_decomp : (10 : ℕ) = G2 * G5 := by decide
  52theorem twelve_decomp : (12 : ℕ) = G2^2 * G3 := by decide
  53theorem fifteen_decomp : (15 : ℕ) = G3 * G5 := by decide
  54theorem sixteen_decomp : (16 : ℕ) = G2^4 := by decide
  55theorem twentyfive_decomp : (25 : ℕ) = G5^2 := by decide
  56theorem fortyfive_decomp : (45 : ℕ) = G3^2 * G5 := by decide
  57theorem seventy_decomp : (70 : ℕ) = Nat.choose (G2^3) (G2^2) := by decide
  58theorem oneTwentyFive_decomp : (125 : ℕ) = G5^3 := by decide
  59theorem twoSixteen_decomp : (216 : ℕ) = (G2 * G3)^3 := by decide
  60theorem twoFiftySix_decomp : (256 : ℕ) = G2^(G2^3) := by decide
  61theorem threeSixty_decomp : (360 : ℕ) = G2^3 * G3^2 * G5 := by decide
  62theorem threeOneTwentyFive_decomp : (3125 : ℕ) = G5^5 := by decide
  63
  64/-! ## Closure properties. -/
  65
  66/-- The set {2, 3, 5} is the smallest generating set for the spectrum. -/
  67theorem generators_minimal :
  68    G2 ≠ G3 ∧ G3 ≠ G5 ∧ G2 ≠ G5 := by
  69  refine ⟨?_, ?_, ?_⟩ <;> decide
  70
  71/-- The product of all three generators: 2 · 3 · 5 = 30 (= primorial p₃#). -/