OAI/Algebra/GroupRing/RawDecomposition.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.RawDecomposition.marks line 17
2. abbrev OAI.TorsionFreeZeroDivisors.RawDecomposition.mark line 18
3. abbrev OAI.TorsionFreeZeroDivisors.RawDecomposition.degree_two line 19
4. abbrev OAI.TorsionFreeZeroDivisors.RawDecomposition.Seeds line 20
5. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.decomposition line 24
6. def OAI.TorsionFreeZeroDivisors.RawDecomposition.paths line 31
7. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.expands line 33
8. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.nonempty line 36
9. abbrev OAI.TorsionFreeZeroDivisors.RawDecomposition.lengths line 42
10. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.length_eq line 45
11. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.lengths_eq line 48
12. def OAI.TorsionFreeZeroDivisors.RawDecomposition.dart line 51

    Source documentation

    Positions remember their literal original dart, without a choice of orientation.

    def dart (x : Position (fun p => (raw p).length)) : D := (raw x.1).get ⟨x.2.val.toNat,by
    …

13. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.dart_get line 57
14. def OAI.TorsionFreeZeroDivisors.RawDecomposition.position line 60
15. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.dart_eq line 63
16. lemma OAI.TorsionFreeZeroDivisors.RawDecomposition.source_eq line 71
17. def OAI.TorsionFreeZeroDivisors.ComparisonGeometry.cast line 92
18. def OAI.TorsionFreeZeroDivisors.ComparisonGeometry.castIso line 93
19. lemma OAI.TorsionFreeZeroDivisors.ComparisonGeometry.Iso.unpaired line 99
20. def OAI.TorsionFreeZeroDivisors.ComparisonGeometry.castBackIso line 110
21. structure OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data line 133

    Source documentation

    The data of a literal bounded family of immersed graph paths. The finite image graph is arbitrary; only the source's bounds on path and comparison counts, total length and proportion of unpaired letters are stated here.

    structure Data (B K I rep : ℕ) where
    …

22. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.vertices line 176
23. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.mark line 177
24. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.degree_two line 178
25. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.decomposed line 179
26. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.decomposed_nonempty line 180
27. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.lengths_eq line 181
28. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.comparison line 182
29. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.iso line 183
30. abbrev OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.position line 184
31. lemma OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.expands line 186
32. lemma OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.length_eq line 188
33. lemma OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.dart_eq line 191
34. lemma OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.position_iso line 195
35. def OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.suppressed line 199

    Source documentation

    All suppression data is constructed from the literal paths, with no bounds on a suppressed skeleton included among the raw data.

    def suppressed : SourcePattern.Data B K I rep where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SourcePattern.Data

36. def OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.event line 246

    Source documentation

    The event reads the literal original path label, and pins the actual initial vertex of the exceptional interval on its prescribed side.

    def event (x : Types.VertexA rep) (y : Types.VertexB rep) (r : Match rep) : Prop :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB

37. lemma OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data.suppressed_event line 262
38. theorem OAI.TorsionFreeZeroDivisors.RawSourcePattern.eventually_avoids line 282

    Source documentation

    Literal immersed source paths, not assumed to come with a suppression or finite encoding, are avoided by an actual pair of high-girth typed graphs.

    theorem eventually_avoids (B K I : ℕ) (hK : 0<K) (hI : 0<I) :
        ∀ᶠ rep in atTop,∀ (x : Types.VertexA rep) (y : Types.VertexB rep),
          ∃ r∈samples rep,∀ a : Data B K I rep,¬a.event x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data

39. def OAI.TorsionFreeZeroDivisors.DiameterCounting.ports line 305
40. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.mem_ports line 308
41. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.card_ports line 312
42. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.card_ports_le line 327
43. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.card_ports_ge line 335
44. def OAI.TorsionFreeZeroDivisors.DiameterCounting.possible line 344

    Source documentation

    All potential unordered prescribed matching pairs within a vertex set. Keeping infeasible ones is a harmless overcount.

    def possible (S : Finset V) : Finset (Sym2 D) :=
    …

45. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.mk_mem_possible line 348
46. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.possible_card line 353
47. def OAI.TorsionFreeZeroDivisors.DiameterCounting.closedNeighbors line 362
48. def OAI.TorsionFreeZeroDivisors.DiameterCounting.incidentEdges line 365
49. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.incident_possible line 369
50. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.contains_incident line 379
51. lemma OAI.TorsionFreeZeroDivisors.DiameterCounting.twice_incident line 388
52. theorem OAI.TorsionFreeZeroDivisors.DiameterCounting.dense_witness line 407

    Source documentation

    The literal dense set forced by a failure of the required doubling. It keeps distinct matching prescriptions rather than counting occurrences.

    theorem dense_witness (r : Matching label bar) (k d₀ : ℕ)
        (hd₀ : ∀ v, d₀ ≤ Nat.card {e : D // origin e=v})
        (hk : 2*k ≤ Fintype.card V) (S : Finset V) (hS : S.card=k)
        (hfail : (closedNeighbors origin r S).card ≤ 2*k) :
        ∃ U : Finset V, U.card=2*k ∧
          ∃ C : Finset (Sym2 D), C ⊆ possible origin U ∧
            C.card=(d₀*k+1)/2 ∧ r.Contains C := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.DiameterCounting.closedNeighbors, OAI.TorsionFreeZeroDivisors.DiameterCounting.possible

53. def OAI.TorsionFreeZeroDivisors.DiameterCounting.denseEvent line 425

    Source documentation

    Union of all dense witnesses of a fixed vertex and prescription size.

    def denseEvent (N m t : ℕ) : Finset (Matching label bar) :=
    …

54. theorem OAI.TorsionFreeZeroDivisors.DiameterCounting.dense_count line 433

    Source documentation

    The exact finite union bound in the girth-conditioned space. The two binomial factors count sets, avoiding the spurious extra power of k that would arise if one counted ordered lists of edge prescriptions.

    theorem dense_count (N m t d R : ℕ) (hbar : ∀ t, bar t ≠ t) (h2 : 2≤d)
        (hd : ∀ v, Nat.card {e : D // origin e=v} ≤ d)
        (hR : ∀ x, R+t+4*d^(2*N+1) ≤ Nat.card {e : D // label e=label x}) :
        (denseEvent (label := label) (bar := bar) origin N m t).card * R^t ≤
    …

    Mentions: OAI.TorsionFreeZeroDivisors.DiameterCounting.denseEvent

55. theorem OAI.TorsionFreeZeroDivisors.DiameterCounting.mem_dense_of_failure line 477

    Source documentation

    A failing set in an actual girth-conditioned sample occurs in the counted union. No labels, vertex names or repeated traversals have been discarded.

    theorem mem_dense_of_failure (N k d₀ : ℕ) (r : Matching label bar)
        (hr : r∈Matching.conditioned (label := label) (bar := bar) origin N ∅)
    …