grayCycle3_bijective

formal source

 134  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
 135  exact gray8At_injective h0
 136
 137theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
 138  classical
 139  -- card(Fin 8) = 8
 140  have hFin : Fintype.card (Fin 8) = 8 := by simp
 141  -- card(Pattern 3) = 2^3 = 8
 142  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
 143    simpa using (Patterns.card_pattern 3)
 144  have hPow : (2 ^ 3 : Nat) = 8 := by decide
 145  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
 146  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
 147    -- rewrite both sides to 8
 148    calc
 149      Fintype.card (Fin 8) = 8 := hFin
 150      _ = Fintype.card (Pattern 3) := by simpa [hPat]
 151  -- injective + card equality ⇒ bijective
 152  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩
 153
 154theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
 155  (grayCycle3_bijective).2
 156
 157theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
 158  intro i
 159  -- 8 explicit cases; each step flips exactly one of the three bits.
 160  fin_cases i
 161  · -- 0 -> 1 (flip bit 0)
 162    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 163    · simp [grayCycle3Path, gray8At, pattern3]
 164    · intro k hk
 165      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 166  · -- 1 -> 3 (flip bit 1)
 167    refine ⟨⟨1, by decide⟩, ?_, ?_⟩