`triangular_2`

proved

show as: view math explainer →

module: IndisputableMonolith.Gap45.PhysicalMotivation
domain: Gap45
line: 93 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.PhysicalMotivation on GitHub at line 93.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  90@[simp] lemma triangular_1 : triangular 1 = 1 := rfl
  91
  92/-- T(2) = 3. -/
  93@[simp] lemma triangular_2 : triangular 2 = 3 := rfl
  94
  95/-- T(3) = 6. -/
  96@[simp] lemma triangular_3 : triangular 3 = 6 := rfl
  97
  98/-- T(4) = 10. -/
  99@[simp] lemma triangular_4 : triangular 4 = 10 := rfl
 100
 101/-- T(5) = 15. -/
 102@[simp] lemma triangular_5 : triangular 5 = 15 := rfl
 103
 104/-- T(8) = 36. -/
 105@[simp] lemma triangular_8 : triangular 8 = 36 := rfl
 106
 107/-- **KEY RESULT**: T(9) = 45. -/
 108@[simp] theorem triangular_9_is_45 : triangular 9 = 45 := rfl
 109
 110/-! ## The Closure Principle -/
 111
 112/-- The 8-tick period (from ledger coverage of 2^D with D=3). -/
 113def eight_tick : ℕ := 8
 114
 115/-- The closure number: to close an 8-tick cycle, you need 8+1 = 9 steps.
 116    This is the "fence-post" principle: 8 sections need 9 posts. -/
 117def closure_number : ℕ := eight_tick + 1
 118
 119/-- Closure number = 9. -/
 120@[simp] theorem closure_number_eq_9 : closure_number = 9 := rfl
 121
 122/-! ## Cumulative Phase as Triangular Number -/
 123

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.