OAI/Algebra/GroupRing/MatchingGraphs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.MatchingGraphs.subdivision_degree line 15

   Source documentation

   All degrees are controlled by the fixed port fibers.

   theorem subdivision_degree (Γ : PortGraph V D) (d : ℕ) (h2 : 2 ≤ d)
       (hd : ∀ v, Nat.card {e : D // Γ.origin e = v} ≤ d) (a : V ⊕ D) :
       (graphNeighbors Γ.subdivision a).card ≤ d := by
   …

2. theorem OAI.TorsionFreeZeroDivisors.MatchingGraphs.exists_far_port line 25

   Source documentation

   Uniformly many ports of one label lie outside both endpoint neighborhoods.

   theorem exists_far_port (Γ : PortGraph V D) (label : D → T)
       (d R : ℕ) (h2 : 2 ≤ d)
       (hd : ∀ v, Nat.card {e : D // Γ.origin e = v} ≤ d)
       (x : D) (hbig : 4*d^(R+1) < Nat.card {e : D // label e = label x}) :
       ∃ e : D, label e = label x ∧
         ∀ a ∈ ({Sum.inr x,Sum.inr (Γ.reverse x)} : Set (V ⊕ D)),
         ∀ b ∈ ({Sum.inr e,Sum.inr (Γ.reverse e)} : Set (V ⊕ D)),
         ∀ p : Γ.subdivision.Walk a b, R < p.length := by
   …

3. theorem OAI.TorsionFreeZeroDivisors.MatchingGraphs.subdivision_switch line 74

   Source documentation

   The conjugation switch is exactly the graph two-switch used in girth repair.

   theorem subdivision_switch (Γ : PortGraph V D) (x e : D)
       (hxe : x ≠ e) (hxr : x ≠ Γ.reverse e) :
       (Γ.switch x e).subdivision =
         addEdge (addEdge (Γ.subdivision.deleteEdges
           {s(Sum.inr x,Sum.inr (Γ.reverse x)),s(Sum.inr e,Sum.inr (Γ.reverse e))})
           (Sum.inr x) (Sum.inr (Γ.reverse e))) (Sum.inr e) (Sum.inr (Γ.reverse x)) := by
   …

4. abbrev OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching line 108

   Source documentation

   A matching on the signed labelled port set; inverse labels have no fixed points. Keeping the origin function separate fixes the vertex types.

   abbrev Matching (label : D → T) (bar : T → T) :=
   …

5. instance OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.(instance at line 114) line 114
6. instance OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.(instance at line 115) line 115
7. instance OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.(instance at line 119) line 119
8. def OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.graph line 121
9. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.reverse_reverse line 124
10. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.label_reverse line 125
11. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.ext line 128
12. def OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch line 134

    Source documentation

    Conjugating by the transposition of equally labelled ports.

    def switch (r : Matching label bar) (x e : D) (he : label x = label e) : Matching label bar :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

13. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch_apply line 147
14. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch_switch line 150
15. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.graph_switch line 155
16. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch_recover line 161

    Source documentation

    Given the new matching and the fixed old pair x,y, the auxiliary port is forced. This is the reconstructibility behind the conditional estimate.

    theorem switch_recover (r : Matching label bar) (x y e : D)
        (he : label x = label e) (hxy : r x = y)
        (hbar : ∀ t, bar t ≠ t) : r.switch x e he y = e := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

17. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch_injective line 174

    Source documentation

    Distinct input-matching/auxiliary-port pairs always give distinct outputs.

    theorem switch_injective (x y : D) (hbar : ∀ t, bar t ≠ t) :
        Function.Injective (fun p : {r : Matching label bar // r x = y} ×
          {e : D // label x = label e} => p.1.val.switch x p.2.val p.2.property) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

18. def OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.Contains line 188

    Source documentation

    Prior prescriptions are undirected matching edges, counted once.

    def Contains (r : Matching label bar) (C : Finset (Sym2 D)) : Prop :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

19. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.edge_name_injective line 193

    Source documentation

    A signed label chooses a unique orientation of each matching edge.

    theorem edge_name_injective (r : Matching label bar) (x : D)
        (hbar : ∀ t, bar t ≠ t) :
        Function.Injective (fun e : {e : D // label e = label x} => s(e.val,r e.val)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

20. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.switch_contains line 204

    Source documentation

    Switching two edges disjoint from the prior prescriptions preserves them.

    theorem switch_contains (r : Matching label bar) (C : Finset (Sym2 D))
        (hC : r.Contains C) (x e : D) (he : label x = label e)
        (hxC : s(x,r x) ∉ C) (heC : s(e,r e) ∉ C) : (r.switch x e he).Contains C := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching, OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.Contains

21. def OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.admissible line 226

    Source documentation

    All allowed transpositions for the distinguished port, omitting prior edges and both radius-R endpoint balls.

    def admissible (r : Matching label bar) (origin : D → V) (x : D)
        (R : ℕ) (C : Finset (Sym2 D)) : Finset {e : D // label e = label x} := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

22. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.admissible_card line 236

    Source documentation

    The excluded prior set costs exactly one port per prior edge, not two.

    theorem admissible_card (r : Matching label bar) (origin : D → V)
        (hbar : ∀ t, bar t ≠ t) (d : ℕ) (h2 : 2 ≤ d)
        (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
        (x : D) (R : ℕ) (C : Finset (Sym2 D)) :
        Nat.card {e : D // label e = label x} - C.card - 4*d^(R+1) ≤
          (r.admissible origin x R C).card := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

23. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.admissible_preserves line 265

    Source documentation

    The girth condition is preserved by each counted auxiliary port.

    theorem admissible_preserves (r : Matching label bar) (origin : D → V)
        (x : D) (N : ℕ) (C : Finset (Sym2 D))
        (hC : r.Contains C) (hxC : s(x,r x) ∉ C)
        (hg : (N : ℕ∞) ≤ (r.graph origin).subdivision.egirth)
        (e : {e : D // label e = label x}) (he : e ∈ r.admissible origin x (2*N) C) :
        (r.switch x e.val e.property.symm).Contains C ∧
          (N : ℕ∞) ≤ ((r.switch x e.val e.property.symm).graph origin).subdivision.egirth := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching, OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.Contains, OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.graph

24. def OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned line 303

    Source documentation

    The exact finite space conditioned on girth and prior prescriptions.

    def conditioned (origin : D → V) (N : ℕ) (C : Finset (Sym2 D)) :
        Finset (Matching label bar) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

25. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned_count line 311

    Source documentation

    Direct double counting on the whole tuple space, with all other matchings retained in the output. No independence after conditioning is used.

    theorem conditioned_count (origin : D → V) (N : ℕ) (C : Finset (Sym2 D))
        (hbar : ∀ t, bar t ≠ t) (d : ℕ) (h2 : 2 ≤ d)
        (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
        (x y : D) (hxy : s(x,y) ∉ C) :
        ((conditioned (label := label) (bar := bar) origin N C).filter (fun r => r x = y)).card *
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned

26. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.contains_insert line 372

    Source documentation

    Adding one undirected prescription is exactly one matching-coordinate condition; the reverse orientation is automatic, not an extra constraint.

    theorem contains_insert (r : Matching label bar) (C : Finset (Sym2 D)) (x y : D) :
        r.Contains (insert s(x,y) C) ↔ r.Contains C ∧ r x = y := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching

27. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned_insert line 386
28. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.prescriptions_count line 397

    Source documentation

    The simultaneous-prescription bound obtained by successive conditioning. No independence is asserted, even for prescriptions on distinct labels.

    theorem prescriptions_count (origin : D → V) (N : ℕ)
        (hbar : ∀ t, bar t ≠ t) (d : ℕ) (h2 : 2 ≤ d)
        (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
        (R : ℕ) (C : Finset (Sym2 D))
        (hR : ∀ x, R + C.card + 4*d^(2*N+1) ≤ Nat.card {e : D // label e = label x}) :
        (conditioned (label := label) (bar := bar) origin N C).card * R^C.card ≤
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned

29. theorem OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned_probability line 429

    Source documentation

    The uniform one-prescription bound for the actual girth-conditioned model.

    theorem conditioned_probability (origin : D → V) (N : ℕ) (C : Finset (Sym2 D))
        (hbar : ∀ t, bar t ≠ t) (d : ℕ) (h2 : 2 ≤ d)
        (hd : ∀ v, Nat.card {e : D // origin e = v} ≤ d)
        (x y : D) (hxy : s(x,y) ∉ C)
        (hΩ : (conditioned (label := label) (bar := bar) origin N C).Nonempty)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching.conditioned