`exists_grayCycle`

proved

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCycleGeneral
domain: Patterns
line: 320 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Patterns.GrayCycleGeneral on GitHub at line 320.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 317
 318    This theorem provides the unconditional existence witness by delegating to
 319    the recursive BRGC construction in `GrayCycleBRGC.lean`. -/
 320theorem exists_grayCycle {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCycle d, w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
 321  ⟨GrayCycleBRGC.brgcGrayCycle d hdpos, rfl⟩
 322
 323/-- **THEOREM (GENERAL)**: There exists a Gray cover for any dimension `d > 0`. -/
 324theorem exists_grayCover {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCover d (2 ^ d), w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
 325  ⟨GrayCycleBRGC.brgcGrayCover d hdpos, rfl⟩
 326
 327theorem exists_grayCycle_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 328    ∃ w : GrayCycle d, w.path = brgcPath d :=
 329  ⟨brgcGrayCycle d hdpos hd, rfl⟩
 330
 331theorem exists_grayCover_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 332    ∃ w : GrayCover d (2 ^ d), w.path = brgcPath d :=
 333  ⟨brgcGrayCover d hdpos hd, rfl⟩
 334
 335end GrayCycleGeneral
 336
 337end Patterns
 338end IndisputableMonolith

papers checked against this theorem

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