theorem proved term proof

`eight_tick_is_minimal`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 173theorem eight_tick_is_minimal :
 174    ∀ T : ℕ, (∃ (compatible : Bool), compatible = true ∧ T ≥ 8) ∨ T < 8 := by

proof body

Term-mode proof.

 175  intro T
 176  by_cases h : T < 8
 177  · right; exact h
 178  · left; use true; constructor; rfl; omega
 179
 180/-! ## Main Uniqueness Theorem -/
 181
 182/-- The RS Ledger structure (abstract). -/

depends on (3)

Lean names referenced from this declaration's body.

compatible in IndisputableMonolith.Complexity.SAT.Backprop decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use