TransferGraph.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The graph update and the regular-row invariant in one transfer

def OAI.Ostmann.transferCopySign line 10
Source documentation
The true branch is the positive copy.
```
def transferCopySign (t : Bool) : ℤ := if t then 1 else -1
```

def OAI.Ostmann.transferredGraph line 14

Source documentation

none is the erased pivot; some (inl h) is a copied slot and some (inr y) is a shared outside slot.

def transferredGraph {H Y : Type*}
    (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) :
    ((Bool × H) ⊕ Y) → ((Bool × H) ⊕ Y) → ℤ
  | .inl (t, h), .inl (u, k) =>
      if t = u then transferCopySign t * b (some (.inl h)) (some (.inl k))
      else transferCopySign t * b (some (.inl h)) none
  | .inl (t, h), .inr y => transferCopySign t * b (some (.inl h)) (some (.inr y))
  | .inr y, .inl (t, h) => transferCopySign t * b (some (.inr y)) (some (.inl h))
  | .inr _, .inr _ => 0

Mentions: OAI.Ostmann.transferCopySign

def OAI.Ostmann.RegularGraphRow line 24
theorem OAI.Ostmann.transferredGraph_regular line 27
theorem OAI.Ostmann.transferredGraph_diagonal line 49

theorem OAI.Ostmann.transferredGraph_common_column line 59

Source documentation

A future pivot is retained in one fixed copy. Its incoming column is still constant on its constituent slots.

theorem transferredGraph_common_column {H Y : Type*}
    (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (K : Set H)
    (hc : ∀ i : Option (H ⊕ Y), (∀ h ∈ K, i ≠ some (.inl h)) →
      ∀ h ∈ K, ∀ k ∈ K, b i (some (.inl h)) = b i (some (.inl k)))
    (t : Bool) (i : (Bool × H) ⊕ Y)
    (hi : ∀ h ∈ K, i ≠ .inl (t, h)) :
    ∀ h ∈ K, ∀ k ∈ K,
      transferredGraph b i (.inl (t, h)) = transferredGraph b i (.inl (t, k)) := by
…

Mentions: OAI.Ostmann.transferredGraph