`IndisputableMonolith.URCAdapters.EightBeat`

IndisputableMonolith/URCAdapters/EightBeat.lean · 15 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Patterns
   3
   4namespace IndisputableMonolith
   5namespace URCAdapters
   6
   7/-- Eight‑beat existence (period exactly 8). -/
   8def eightbeat_prop : Prop := ∃ w : IndisputableMonolith.Patterns.CompleteCover 3, w.period = 8
   9
  10lemma eightbeat_holds : eightbeat_prop := by
  11  simpa using IndisputableMonolith.Patterns.period_exactly_8
  12
  13end URCAdapters
  14end IndisputableMonolith
  15

source mirrored from github.com/jonwashburn/shape-of-logic