twoPow_succ_eq_add

formal source

  44
  45/-! ## The recursive BRGC path -/
  46
  47private lemma twoPow_succ_eq_add (d : Nat) : 2 ^ (d + 1) = 2 ^ d + 2 ^ d := by
  48  -- `2^(d+1) = 2^d * 2 = 2 * 2^d = 2^d + 2^d`
  49  simpa [pow_succ, Nat.mul_comm, Nat.two_mul]
  50
  51/-- The recursive BRGC path as a `Fin (2^d) → Pattern d`. -/
  52def brgcPath : (d : Nat) → Fin (2 ^ d) → Pattern d
  53  | 0, _ =>
  54      -- unique 0-bit pattern
  55      fun _ => False
  56  | (d + 1), i =>
  57      let T : Nat := 2 ^ d
  58      let hTT : 2 ^ (d + 1) = T + T := by
  59        simpa [T, twoPow_succ_eq_add d]
  60      let i' : Fin (T + T) := i.cast hTT
  61      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
  62      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
  63      Fin.append left right i'
  64
  65/-! ## Injectivity (no repeats) -/
  66
  67private lemma cast_add_one {n m : Nat} [NeZero n] [NeZero m] (h : n = m) (i : Fin n) :
  68    (i + 1).cast h = (i.cast h) + 1 := by
  69  subst h
  70  simp
  71
  72theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
  73  | 0 => by
  74      intro i j _
  75      -- `Fin 1` is a subsingleton (only `0`)
  76      simpa [Fin.eq_zero i, Fin.eq_zero j]
  77  | (d + 1) => by