ChainCoverage.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.ChainCoverage.Covered line 15
Source documentation
A dart lying in one of the actual maximal marked chains.
```
def Covered (d : D) : Prop :=
…
```
lemma OAI.TorsionFreeZeroDivisors.ChainCoverage.covered_fixed line 19
lemma OAI.TorsionFreeZeroDivisors.ChainCoverage.covered_next line 22
lemma OAI.TorsionFreeZeroDivisors.ChainCoverage.covered_reverse line 36
Source documentation
Reversing an original dart stays in the opposite oriented marked chain.
```
lemma covered_reverse {d : D} (hd : Covered σ τ hσ hτ d) :
    Covered σ τ hσ hτ (σ d) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ChainCoverage.Covered
lemma OAI.TorsionFreeZeroDivisors.ActualMarkedChains.forced_turn line 64
lemma OAI.TorsionFreeZeroDivisors.ActualMarkedChains.covered_step line 72
lemma OAI.TorsionFreeZeroDivisors.ActualMarkedChains.covered_path line 84

theorem OAI.TorsionFreeZeroDivisors.ActualMarkedChains.actual_image_covered line 108

Source documentation

Every dart of the actual image belongs to a marked chain. No circle component is dropped: a path start is marked in every component.

theorem actual_image_covered {J : Type*} (paths : J → List D)
    (hpaths : ∀ j, (paths j).IsChain (WeightedMoore.PortWalk.step Γ.origin Γ.reverse))
    (hstarts : ∀ j d, d∈(paths j).head? → mark (Γ.origin d))
    (himage : ∀ d : D, ∃ j, d∈paths j ∨ Γ.reverse d∈paths j) :
    ∀ d, Covered Γ.reverse (turn Γ.origin mark h2) Γ.reverse_reverse
      (turn_involutive Γ.origin mark h2) d := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step

theorem OAI.TorsionFreeZeroDivisors.ActualMarkedChains.actual_chain_total line 126

Source documentation

Exact length accounting after suppressing the actual image, rather than only the inequality for a possibly incomplete set of marked components.

theorem actual_chain_total {J : Type*} (paths : J → List D)
    (hpaths : ∀ j, (paths j).IsChain (WeightedMoore.PortWalk.step Γ.origin Γ.reverse))
    (hstarts : ∀ j d, d∈(paths j).head? → mark (Γ.origin d))
    (himage : ∀ d : D, ∃ j, d∈paths j ∨ Γ.reverse d∈paths j) :
    ∑ d : {d : D // turn Γ.origin mark h2 d=d}, chainLength Γ mark h2 d = Fintype.card D := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step

def OAI.TorsionFreeZeroDivisors.MarkedChainBound.marks line 148
Source documentation
Mark all irregular vertices and the specified start/end vertices.
```
def marks (M : Finset V) (v : V) : Prop := degree Γ Finset.univ v ≠ 2 ∨ v∈M
…
```
lemma OAI.TorsionFreeZeroDivisors.MarkedChainBound.marks_degree_two line 151
lemma OAI.TorsionFreeZeroDivisors.MarkedChainBound.marked_dart_bound line 156
lemma OAI.TorsionFreeZeroDivisors.MarkedChainBound.chain_dart_card line 176

theorem OAI.TorsionFreeZeroDivisors.MarkedChainBound.bounded_marked_chains line 186

Source documentation

Uniformly bounded many marked chains of the actual image, before choosing any label assignments. The bound depends only on C and K.

theorem bounded_marked_chains (C : ℝ) (hC : 0≤C) (K : ℕ) :
    ∃ R : ℕ, ∀ {V D : Type} [Fintype V] [Fintype D] (Γ : PortGraph V D)
      (L : ℝ) (_ : 0<L) (_ : (Fintype.card D:ℝ)≤2*C*L)
      (_ : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
        L≤WeightedCycles.weight (WeightedPortMoore.edgeWeight (fun _ : D => (1:ℝ))) c)
      (_ : (Finset.univ.filter (fun v => degree Γ Finset.univ v=1)).card≤2)
      (M : Finset V) (_ : M.card≤2*K),
      Fintype.card {d : D // turn Γ.origin (marks Γ M) (marks_degree_two Γ M) d=d}≤R := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedCycles.weight, OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight, OAI.TorsionFreeZeroDivisors.MarkedChainBound.marks, OAI.TorsionFreeZeroDivisors.MarkedChainBound.marks_degree_two

def OAI.TorsionFreeZeroDivisors.ChainPaths.word line 216
Source documentation
The literal nonempty word of original darts in one oriented marked chain.
```
def word (d : B) : List D := outWord (iterChain F (len d-1) d.val)
…
```
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.outWord_length line 219
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.outWord_last line 225
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.word_length line 232
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.word_end line 237

lemma OAI.TorsionFreeZeroDivisors.ChainPaths.iter_chain_prefix line 246

Source documentation

A reduced path cannot stop before the end of its current marked chain: its prescribed last vertex is marked, while all interior chain vertices are not.

lemma iter_chain_prefix (n : ℕ) (x : D) (p : List D)
    (hp : p.IsChain (PortWalk.step Γ.origin Γ.reverse)) (hh : p.head?=some x)
    (ht : ∀ d∈p.getLast?, mark (Γ.origin (Γ.reverse d)))
    (hn : ∀ i : ℕ, 0 < i → i ≤ n → ¬mark (Γ.origin (F^[i] x))) :
    outWord (iterChain F n x) <+: p := by
…

lemma OAI.TorsionFreeZeroDivisors.ChainPaths.word_prefix line 291
theorem OAI.TorsionFreeZeroDivisors.ChainPaths.path_decomposes line 305
Source documentation
Every original path traverses whole marked chains. This includes a path that returns to a mark, and does not require it embedded.
```
theorem path_decomposes (p : List D)
    (hp : p.IsChain (PortWalk.step Γ.origin Γ.reverse))
    (hs : ∀ d∈p.head?, mark (Γ.origin d))
    (ht : ∀ d∈p.getLast?, mark (Γ.origin (Γ.reverse d))) :
    ∃ ds : List B, ds.flatMap (word Γ mark h2)=p := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ChainPaths.word
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.outWord_iterChain line 342
Source documentation
Enumerating a chain lists precisely the forward iterates before its first mark.
```
lemma outWord_iterChain (f : D → D) (n : ℕ) (x : D) :
    outWord (iterChain f n x) = (List.range (n+1)).map (fun i => f^[i] x) := by
…
```
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.word_eq_range line 351
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.mem_word_iff line 358
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.word_nodup line 367
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.words_disjoint line 377
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.count_word line 386
lemma OAI.TorsionFreeZeroDivisors.ChainPaths.multiplicity_constant line 398
Source documentation
Every directed edge in one chain has the same traversal multiplicity, namely the number of occurrences of that oriented chain in the decomposition.
```
lemma multiplicity_constant (ds : List B) (d : B) (x : D)
    (hx : x∈word Γ mark h2 d) :
    (ds.flatMap (word Γ mark h2)).count x = ds.count d := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ChainPaths.word