CycleSums.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.WLIdentification.CycleRows.rectangle line 13

Source documentation

The rectangular difference of a vanishing cycle sum isolates one edge. No finiteness or cardinality assumption on the coordinate alphabets is needed.

theorem rectangle {I : Type} [Fintype I] [DecidableEq I]
    (s : Equiv.Perm I) (hs : ∀ i, s i ≠ i) (hs2 : ∀ i, s (s i) ≠ i)
    (A : I → Type) (g : (i : I) → A i → A (s i) → Bit)
    (hzero : ∀ a : (i : I) → A i, ∑ i, g i (a i) (a (s i)) = 0)
    (b : (i : I) → A i) (i : I) (u : A i) (v : A (s i)) :
    g i u v + g i u (b (s i)) + g i (b i) v + g i (b i) (b (s i)) = 0 := by
…

Mentions: OAI.WLIdentification.Bit

theorem OAI.WLIdentification.CycleRows.adjacent_deviation line 46

Source documentation

Varying a single coordinate equates the two adjacent one-coordinate deviations.

theorem adjacent_deviation {I : Type} [Fintype I] [DecidableEq I]
    (s : Equiv.Perm I) (hs : ∀ i, s i ≠ i)
    (A : I → Type) (g : (i : I) → A i → A (s i) → Bit)
    (hzero : ∀ a : (i : I) → A i, ∑ i, g i (a i) (a (s i)) = 0)
    (b : (i : I) → A i) (i : I) (v : A (s i)) :
    g i (b i) v + g i (b i) (b (s i)) =
      g (s i) v (b (s (s i))) + g (s i) (b (s i)) (b (s (s i))) := by
…

Mentions: OAI.WLIdentification.Bit

theorem OAI.WLIdentification.CycleRows.rotate_val line 72
theorem OAI.WLIdentification.CycleRows.rotate_ne_self line 89
theorem OAI.WLIdentification.CycleRows.rotate_twice_ne_self line 95
theorem OAI.WLIdentification.CycleRows.integrate_constants line 104
Source documentation
Integrating constants around a finite cycle needs exactly the zero-sum condition.
```
theorem integrate_constants {n : ℕ} (c : Fin n → Bit) (hc : ∑ i, c i = 0) :
    ∃ C : Fin n → Bit, ∀ i, C i + C (finRotate n i) = c i := by
…
```
Mentions: OAI.WLIdentification.Bit
theorem OAI.WLIdentification.CycleRows.cycle_lifting line 129