pith. machine review for the scientific record. sign in
def definition def or abbrev

brgcGrayCover

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 302noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) (hd : d ≤ 64) : GrayCover d (2 ^ d) :=

proof body

Definition body.

 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`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.