`brgcGrayCover`

definition

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCycleGeneral
domain: Patterns
line: 302 · 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 302.

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

used by

formal source

 299}
 300
 301/-- A packaged Gray cover (surjective + one-bit steps) derived from `brgcGrayCycle`. -/
 302noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) (hd : d ≤ 64) : GrayCover d (2 ^ d) :=
 303{ path := brgcPath d
 304  complete := by
 305    classical
 306    have h_inj : Function.Injective (brgcPath d) := brgcPath_injective (d := d) hdpos hd
 307    have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
 308      simp [Patterns.card_pattern]
 309    have h_bij : Function.Bijective (brgcPath d) := by
 310      -- Use the `Fintype` lemma: injective + equal card ⇒ bijective.
 311      exact (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
 312    exact h_bij.2
 313  oneBit_step := brgc_oneBit_step (d := d) hdpos hd
 314}
 315
 316/-- **THEOREM (GENERAL)**: There exists a Gray cycle for any dimension `d > 0`.
 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 :=

papers checked against this theorem

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