   9noncomputable section
  10
  11/-- The local quarter-turn core is modeled as a ququart carrier. -/
  12abbrev QuquartState := Fin 4 → ℂ
  13
  14/-- The standard basis ket `|m⟩`. -/
  15def basisKet (m : Fin 4) : QuquartState :=
  16  fun n => if n = m then 1 else 0
  17
  18/-- Previous index modulo `4`; this realizes the shift convention
  19`X|m⟩ = |m+1 mod 4⟩`. -/
  20def prev4 (m : Fin 4) : Fin 4 :=
  21  ⟨(m.val + 3) % 4, by omega⟩
  22
  23/-- Addition modulo `4`. -/
  24def add4 (a b : Fin 4) : Fin 4 :=
  25  ⟨(a.val + b.val) % 4, by omega⟩
  26
  27/-- Subtraction modulo `4`. -/
  28def sub4 (a b : Fin 4) : Fin 4 :=
  29  ⟨(a.val + (4 - b.val)) % 4, by omega⟩
  30
  31/-- Mod-4 subtraction undoes mod-4 addition. -/
  32theorem sub4_add4_cancel_core (a s : Fin 4) :
  33    sub4 (add4 a s) a = s := by
  34  fin_cases a <;> fin_cases s <;> rfl
  35
  36/-- Mod-4 addition undoes mod-4 subtraction. -/
  37theorem add4_sub4_cancel_core (m a : Fin 4) :
  38    add4 a (sub4 m a) = m := by
  39  fin_cases m <;> fin_cases a <;> rfl
  40
  41/-- For fixed `s`, the left addend is recoverable from `add4 a s`. -/
  42theorem add4_eq_add4_iff_left_core (a a' s : Fin 4) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.