BoundedSystem.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem.data line 17
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem.event line 44
theorem OAI.TorsionFreeZeroDivisors.SampleGraph.exists_avoiding line 52
Source documentation
A literal finite typed graph on both sides, simultaneously with diameter, large girth, and exclusion of every bounded nearly-paired rooted path system. This is an actual-word theorem, not a condition on encoded surrogate patterns.
```
theorem exists_avoiding (Bnd K I : ℕ) (hK : 0<K) (hI : 0<I) :
    ∀ᶠ rep in Filter.atTop,∀ (x : VA rep) (y : VB rep),
      ∃ r∈samples rep,GraphSample.Diameters rep r ∧
        IsEmpty (BoundedSystem Bnd K I rep r x y) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.VA, OAI.TorsionFreeZeroDivisors.SampleGraph.VB, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem
def OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint line 72
Source documentation
Terminal vertex of a literal path, including the empty path at z.
```
def endpoint (l : List D) : V := ((l.getLast?).map (fun d => Γ.origin (Γ.reverse d))).getD z
…
```
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint_nil line 75
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint_append line 77
def OAI.TorsionFreeZeroDivisors.ShortClosure.choices line 80
def OAI.TorsionFreeZeroDivisors.ShortClosure.walks line 83
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.mem_walks_succ line 88
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.length_mem line 94
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.chain_mem line 102
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.allowed_mem line 118
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.head_mem line 132
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.choices_card line 150
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.card_walks_succ line 178
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.card_walks line 197
def OAI.TorsionFreeZeroDivisors.ShortClosure.Collision line 208
Source documentation
Collision of equal-length nonbacktracking paths, before any cancellation.
```
def Collision (k : ℕ) : Prop :=
…
```
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.collision_exists line 211
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.chain_reverse line 221

theorem OAI.TorsionFreeZeroDivisors.ShortClosure.based_loop line 234

Source documentation

A based reduced loop with excluded darts never used. No cyclic reduction at its base is asserted or needed. Least collision length avoids common suffixes.

theorem based_loop (k : ℕ) (hk : Fintype.card V<2^k)
    (hdeg : ∀ v,3≤(Finset.univ.filter (fun d => allowed d ∧ Γ.origin d=v)).card)
    (hsymm : ∀ d,allowed d → allowed (Γ.reverse d)) :
    ∃ l : List D,l≠[] ∧ l.length≤2*k ∧
      l.IsChain (PortWalk.step Γ.origin Γ.reverse) ∧
      (∀ d∈l,allowed d) ∧ (∀ d∈l.head?,Γ.origin d=z) ∧ endpoint Γ z l=z := by
…

Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint

theorem OAI.TorsionFreeZeroDivisors.ShortClosure.logarithmic_based_loop line 311

Source documentation

A logarithmic loop bound, valid even before excluding loops and parallel edges.

theorem logarithmic_based_loop
    (hdeg : ∀ v,3≤(Finset.univ.filter (fun d => allowed d ∧ Γ.origin d=v)).card)
    (hsymm : ∀ d,allowed d → allowed (Γ.reverse d)) :
    ∃ l : List D,l≠[] ∧ l.length≤2*(Nat.log 2 (Fintype.card V)+1) ∧
      l.IsChain (PortWalk.step Γ.origin Γ.reverse) ∧
      (∀ d∈l,allowed d) ∧ (∀ d∈l.head?,Γ.origin d=z) ∧ endpoint Γ z l=z :=
…

Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint

structure OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath line 324
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint_append_list line 329
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.nil_iff line 336
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.last line 337
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.append line 341
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.cyclic_join line 356
def OAI.TorsionFreeZeroDivisors.ShortClosure.forbidden line 364
Source documentation
Excluding an undirected edge means excluding both of its darts.
```
def forbidden (d e : D) : Finset D := {d,Γ.reverse d,e,Γ.reverse e}
```
def OAI.TorsionFreeZeroDivisors.ShortClosure.avoids line 365
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.avoids_symm line 366
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.avoids_left line 377
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.avoids_right line 381
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.avoiding_degree line 388
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.avoiding_loop line 411
Source documentation
Literal reduced based loops avoiding both prescribed unoriented edges.
```
lemma avoiding_loop (d e : D) (z : V)
    (hdeg : ∀ v,7≤(Finset.univ.filter (fun x : D => Γ.origin x=v)).card) :
    ∃ l : List D,l≠[] ∧ l.length≤2*(Nat.log 2 (Fintype.card V)+1) ∧
      ReducedPath Γ z z l ∧ ∀ x∈l,avoids Γ d e x := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath, OAI.TorsionFreeZeroDivisors.ShortClosure.avoids
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.mem_head_eq line 420
lemma OAI.TorsionFreeZeroDivisors.ShortClosure.mem_last_eq line 425

theorem OAI.TorsionFreeZeroDivisors.ShortClosure.extend_of_return line 432

Source documentation

Short closure, before the uniform logarithmic-to-L bound. Only a reduced return path is used; its length need not be minimal.

theorem extend_of_return {a b : V} {p q : List D}
    (hp : ReducedPath Γ a b p) (hpn : p≠[]) (hq : ReducedPath Γ b a q)
    (hdeg : ∀ v,7≤(Finset.univ.filter (fun x : D => Γ.origin x=v)).card) :
    ∃ t : List D,t.length≤q.length+4*(Nat.log 2 (Fintype.card V)+1) ∧
      ReducedPath Γ a a (p++t) ∧
      ∀ᵉ (x∈(p++t).getLast?) (y∈(p++t).head?),PortWalk.step Γ.origin Γ.reverse x y := by
…

Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath