SecondSwap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.SecondTransfer.rowFactorSwap line 9
Source documentation
Swap two factor positions in one nonzero row, leaving all other rows fixed.
```
def rowFactorSwap {r b : ℕ} (i : Fin r) (j l : Fin b) :
    Fin (r+1) → Equiv.Perm (Fin b) :=
…
```

theorem OAI.Problem346.SecondTransfer.update_label_eq_progress_rowSwap line 15

Source documentation

Changing any remaining source factor to the common block agrees with progressing the prefix count, after a permutation internal to that row.

theorem update_label_eq_progress_rowSwap
    {r b : ℕ} (k : Fin r → ℕ) (i : Fin r) (hi : k i < b)
    (j : Fin b) (hj : k i ≤ j.val) (p : Fin (r+1) × Fin b) :
    Function.update (label k) (i.succ, j) none p =
      label (Function.update k i (k i+1))
        (p.1, rowFactorSwap i j ⟨k i, hi⟩ p.1 p.2) := by
…

Mentions: OAI.Problem346.SecondTransfer.label, OAI.Problem346.SecondTransfer.rowFactorSwap

theorem OAI.Problem346.SecondTransfer.invariant_update_label_eq_progress line 53

Source documentation

Any expression invariant under permutations of factors within each row takes the same value on a derivative label update and the progressed prefix labels.

theorem invariant_update_label_eq_progress
    {r b : ℕ} {A : Type*}
    (F : ((Fin (r+1) × Fin b) → Block r) → A)
    (hF : ∀ (l : (Fin (r+1) × Fin b) → Block r)
      (σ : Fin (r+1) → Equiv.Perm (Fin b)),
      F (fun p => l (p.1, σ p.1 p.2)) = F l)
    (k : Fin r → ℕ) (i : Fin r) (hi : k i < b)
    (j : Fin b) (hj : k i ≤ j.val) :
    F (Function.update (label k) (i.succ,j) none) =
      F (label (Function.update k i (k i+1))) := by
…

Mentions: OAI.Problem346.SecondTransfer.Block, OAI.Problem346.SecondTransfer.label