This definition gives the library's named construction or computation for “twist”.
def twist (n : ℕ) : Equiv.Perm (Fin (2 ^ n) × Fin 2) where
toFun pair := (pair.1, if pair.1.val % 2 = 0 then pair.2 else flipBit pair.2)
invFun pair := (pair.1, if pair.1.val % 2 = 0 then pair.2 else flipBit pair.2)
left_inv pair := by by_cases h : pair.1.val % 2 = 0 <;> simp [h]
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “equiv”.
def equiv : (n : ℕ) → Fin (2 ^ n) ≃ PrimitiveBasis n
| 0 => (primitiveBasisLEEquiv 0).symm
| n + 1 =>
(finCongr (pow_succ 2 n)).trans finProdFinEquiv.symm
|>.trans (twist n)
|>.trans (Equiv.prodCongr (equiv n) (Equiv.refl (Fin 2)))
|>.trans (Equiv.prodComm _ _)
|>.trans (Fin.consEquiv (fun _ : Fin (n + 1) => Fin 2))
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “head bit”.
def headBit (index : ℕ) : Fin 2 :=
if (index / 2) % 2 = 0 then ⟨index % 2, by omega⟩
else flipBit ⟨index % 2, by omega⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv head”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem equiv_head (n : ℕ) (index : Fin (2 ^ (n + 1))) :
equiv (n + 1) index 0 = headBit index.val := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv tail”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem equiv_tail (n : ℕ) (index : Fin (2 ^ (n + 1))) (wire : Fin n) :
equiv (n + 1) index wire.succ =
equiv n ⟨index.val / 2, by
have bound : index.val < 2 ^ n * 2 := by simpa only [pow_succ] using index.isLt
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “head bit even”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem headBit_even (index : ℕ) (even : index % 2 = 0) :
headBit (index + 1) = flipBit (headBit index) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “head bit odd”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem headBit_odd (index : ℕ) (odd : index % 2 = 1) :
headBit (index + 1) = headBit index := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “adjacent”; the hypotheses and conclusion in the code panel fix its exact scope. Numerically adjacent Gray labels differ by exactly one physical X action.
theorem adjacent {n : ℕ} (first second : Fin (2 ^ n))
(next : first.val + 1 = second.val) :
∃ target : Fin n, equiv n second = xBasisAction target (equiv n first) := by
commit-pinned source · Verso Blueprint panel