WeightedPortMoore.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.WeightedPortMoore.Good line 14

Source documentation

Validity as a chain of actual nonbacktracking directed edges.

def Good : {k : ℕ} → Chain D k → Prop
  | 0, _ => True
  | _+1, p => PortWalk.step Γ.origin Γ.reverse p.1 (head p.2) ∧ Good p.2

/-- The physical port walk, starting and ending at the first/last ports.
It has one middle edge per macro-edge, and two spokes between them. -/

def OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw line 20

Source documentation

The physical port walk, starting and ending at the first/last ports. It has one middle edge per macro-edge, and two spokes between them.

def draw : {k : ℕ} → (p : Chain D k) → Good Γ p →
    Γ.subdivision.Walk (.inr (head p)) (.inr (Γ.reverse (last p)))
  | 0, d, _ => Walk.cons (show Γ.subdivision.Adj (.inr d) (.inr (Γ.reverse d)) from rfl) Walk.nil
  | _+1, p, h =>
    Walk.cons (show Γ.subdivision.Adj (.inr p.1) (.inr (Γ.reverse p.1)) from rfl)
      (Walk.cons (show Γ.subdivision.Adj (.inr (Γ.reverse p.1)) (.inl (Γ.origin (Γ.reverse p.1))) from rfl)
        (Walk.cons (show Γ.subdivision.Adj (.inl (Γ.origin (Γ.reverse p.1))) (.inr (head p.2)) from h.1.1.symm)
          (draw p.2 h.2)))

Mentions: OAI.TorsionFreeZeroDivisors.WeightedPortMoore.Good

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw_head_edge line 29
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.middle_spoke_ne line 33
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw_reduced line 37
def OAI.TorsionFreeZeroDivisors.WeightedPortMoore.portWord line 64
Source documentation
Recording ports from the physical walk recovers each directed macro-edge.
```
def portWord : {k : ℕ} → Chain D k → List D
  | 0, d => [d,Γ.reverse d]
  | _+1, p => p.1 :: Γ.reverse p.1 :: portWord p.2
```
def OAI.TorsionFreeZeroDivisors.WeightedPortMoore.onlyPort line 68
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw_portWord line 72
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.portWord_injective line 81
def OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight line 90
Source documentation
Nonnegative symmetric length on the subdivision; spokes cost zero.
```
def edgeWeight (len : D → ℝ) : Sym2 (V ⊕ D) → ℝ :=
…
```
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight_nonneg line 95
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight_spoke line 107
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight_middle line 110
theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.draw_weight line 115

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.positive_good line 129

Source documentation

Positive chain mass certifies every actual allowed transition.

theorem positive_good [Fintype D]
    (ht : Transition (PortWalk.transition Γ.origin Γ.reverse))
    {k : ℕ} (p : Chain D k)
    (hp : 0 < mass (PortWalk.transition Γ.origin Γ.reverse) p) : Good Γ p := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedPortMoore.Good

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.short_cycle line 148

Source documentation

The weighted Moore collision in an actual port multigraph gives an actual simple cycle in its faithful subdivision, with exactly the expanded cost bound.

theorem short_cycle [Fintype D] [Nonempty D]
    (hdeg : ∀ d, 3 ≤ (PortWalk.out Γ.origin (Γ.origin d)).card)
    (len : D → ℝ) (hlen : ∀ d, 0 < len d)
    (hsym : ∀ d, len (Γ.reverse d) = len d) :
    let k := Nat.log 2 (Fintype.card D) + 2
…

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.dart_count_inequality line 182

Source documentation

Consequence used after suppressing degree-two core chains in the manuscript. No bound on cycle rank or on the number of chains is assumed in this theorem.

theorem dart_count_inequality [Fintype D] [Nonempty D]
    (hdeg : ∀ d, 3 ≤ (PortWalk.out Γ.origin (Γ.origin d)).card)
    (len : D → ℝ) (hlen : ∀ d, 0 < len d)
    (hsym : ∀ d, len (Γ.reverse d) = len d)
    (L C : ℝ) (hL : 0 < L) (_hC : 0 ≤ C)
    (htotal : ∑ d, len d ≤ 2*C*L)
    (hgirth : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle → L ≤ weight (edgeWeight len) c) :
    (Fintype.card D : ℝ) ≤ 8*C*(Nat.log 2 (Fintype.card D)+3:ℝ) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.logarithmic_inequality_bounded line 201
Source documentation
The logarithmic Moore inequality bounds the number of darts uniformly in all positive edge lengths and in the girth scale.
```
theorem logarithmic_inequality_bounded (A : ℝ) (hA : 0 ≤ A) :
    ∃ R : ℕ, ∀ n : ℕ, (n : ℝ) ≤ A*((Nat.log 2 n:ℝ)+3) → n ≤ R := by
…
```

theorem OAI.TorsionFreeZeroDivisors.WeightedPortMoore.uniform_dart_bound line 225

Source documentation

Fully uniform form of the weighted Moore bound needed by the actual-image complexity argument; the bound is independent of L and of the multigraph.

theorem uniform_dart_bound (C : ℝ) (hC : 0 ≤ C) :
    ∃ R : ℕ, ∀ {V' D' : Type} [Fintype D'] [Nonempty D']
      (Γ' : PortGraph V' D')
      (_ : ∀ d, 3 ≤ (PortWalk.out Γ'.origin (Γ'.origin d)).card)
      (len : D' → ℝ) (_ : ∀ d, 0 < len d)
      (_ : ∀ d, len ((Γ').reverse d) = len d)
      (L : ℝ) (_ : 0 < L)
      (_ : ∑ d, len d ≤ 2*C*L)
      (_ : ∀ a (c : Γ'.subdivision.Walk a a), c.IsCycle →
        L ≤ weight (edgeWeight len) c), Fintype.card D' ≤ R := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight

def OAI.TorsionFreeZeroDivisors.ChainSuppression.next line 251
Source documentation
The edge reversal followed by the unique turn at an unmarked degree-two vertex. At marked vertices the turn fixes all outgoing darts.
```
def next : D → D := τ ∘ σ
…
```
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.next_injective line 255
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.folded_step line 257
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.folded_iterate line 261
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.reverse_segment line 268
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.exists_positive_return line 277
def OAI.TorsionFreeZeroDivisors.ChainSuppression.length line 282
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.length_pos line 285
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.length_fixed line 288
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.no_internal_mark line 293
def OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint line 301
Source documentation
The opposite end of the maximal chain, given as its outgoing port.
```
def endpoint (x : {x : D // τ x=x}) : {x : D // τ x=x} :=
…
```
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint_reverse line 305
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint_return line 313
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.length_endpoint line 318
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint_involutive line 340
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.endpoint_ne line 348
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.chain_dart_injective line 373
Source documentation
Each directed edge can be traversed at most once among all oriented maximal chains. This is the exact disjoint-interior count, not a bound supplied as an extra hypothesis.
```
lemma chain_dart_injective :
    Injective (fun p : (x : {x : D // τ x=x}) × Fin (length σ τ hσ hτ x.val x.property) =>
      (next σ τ)^[p.2.val] p.1.val) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ChainSuppression.length, OAI.TorsionFreeZeroDivisors.ChainSuppression.next
lemma OAI.TorsionFreeZeroDivisors.ChainSuppression.total_length_le line 405