brgcPath

formal source

  40/-! ## The BRGC path as a Pattern-valued map -/
  41
  42/-- The BRGC path as a `Fin (2^d) → Pattern d`. -/
  43def brgcPath (d : Nat) : Fin (2 ^ d) → Pattern d :=
  44  fun i => binaryReflectedGray d i
  45
  46/-! ## One-bit adjacency of BRGC (bounded) -/
  47
  48/-! ### Wrap-around step (last → 0) is one-bit adjacent (axiom-free) -/
  49
  50private def allOnes (d : Nat) : Nat := 2 ^ d - 1
  51
  52private lemma allOnes_succ_eq_bit (t : Nat) :
  53    allOnes (t + 1) = Nat.bit true (allOnes t) := by
  54  have hpos1 : 1 ≤ 2 ^ (t + 1) := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1))
  55  have hpos0 : 1 ≤ 2 ^ t := Nat.succ_le_of_lt (pow_pos (by decide : 0 < (2 : Nat)) t)
  56  -- LHS + 1
  57  have hL : allOnes (t + 1) + 1 = 2 ^ (t + 1) := by
  58    simp [allOnes, Nat.sub_add_cancel hpos1]
  59  -- RHS + 1
  60  have hR : Nat.bit true (allOnes t) + 1 = 2 ^ (t + 1) := by
  61    have hge : 2 ≤ 2 * (2 ^ t) := by
  62      have h1 : 1 ≤ 2 ^ t := Nat.one_le_pow t 2 (by decide : 0 < (2 : Nat))
  63      -- multiply the inequality by 2
  64      simpa using (Nat.mul_le_mul_left 2 h1)
  65    calc
  66      Nat.bit true (allOnes t) + 1
  67          = (2 * (allOnes t) + 1) + 1 := by simp [Nat.bit_val, Nat.add_assoc]
  68      _ = 2 * (allOnes t) + 2 := by
  69          simp [Nat.add_assoc]
  70      _ = 2 * (2 ^ t - 1) + 2 := by
  71          simp [allOnes]
  72      _ = (2 * (2 ^ t) - 2) + 2 := by
  73          -- distribute `2 * (a - 1)` and simplify