AnchorGraphEvolution.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The anchor coefficients through their actual creation and later copies

def OAI.Ostmann.anchorIncoming line 10
Source documentation
The incoming anchor edge before normalization by the bulk parity.
```
def anchorIncoming {n : ℕ} (α : Fin n → ℤ) (t : Fin n → Bool)
    (j : Fin n) (b : Bool) : ℤ :=
…
```
theorem OAI.Ostmann.copyPathParity_snoc_prefix line 14
theorem OAI.Ostmann.anchorCodeEntry_snoc line 23
theorem OAI.Ostmann.anchorIncoming_snoc_old line 33
Source documentation
This is exactly the outside-anchor row of transferredGraph: every later copy multiplies its incoming coefficient by that copy's sign.
```
theorem anchorIncoming_snoc_old {n : ℕ} (α : Fin (n + 1) → ℤ)
    (t : Fin n → Bool) (u b : Bool) (j : Fin n) :
    anchorIncoming α (Fin.snoc t u) j.castSucc b =
      transferCopySign u * anchorIncoming (fun j => α j.castSucc) t j b := by
…
```
Mentions: OAI.Ostmann.anchorIncoming, OAI.Ostmann.transferCopySign
theorem OAI.Ostmann.anchorIncoming_snoc_new line 40

theorem OAI.Ostmann.anchorIncoming_created_by_transfer line 56

Source documentation

At its reserved step the unnormalized coefficient is precisely the edge created by the graph transfer, for either clone of the fresh anchor.

theorem anchorIncoming_created_by_transfer {H Y : Type*}
    (graph : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (a i : H)
    {n : ℕ} (α : Fin (n + 1) → ℤ) (t : Fin n → Bool) (u b : Bool)
    (hincoming : graph (some (.inl a)) (some (.inl i)) = finalCopyParity t)
    (hpivot : graph (some (.inl a)) none = α (Fin.last n)) :
    anchorIncoming α (Fin.snoc t u) (Fin.last n) b =
      transferredGraph graph (.inl (b, a)) (.inl (u, i)) := by
…

Mentions: OAI.Ostmann.finalCopyParity, OAI.Ostmann.anchorIncoming, OAI.Ostmann.transferredGraph