OAI/Algebra/GroupRing/LinkComponents.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.LinkComponents.Occurrence line 12
2. def OAI.TorsionFreeZeroDivisors.LinkComponents.graph line 15
3. abbrev OAI.TorsionFreeZeroDivisors.LinkComponents.Component line 22
4. def OAI.TorsionFreeZeroDivisors.LinkComponents.HasSelf line 24
5. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.partner_component line 30

   Source documentation

   Matched block occurrences always stay in their link component.

   theorem partner_component (o : Occurrence m) :
       (graph m P).connectedComponentMk (P.partner o).1 = (graph m P).connectedComponentMk o.1 := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Occurrence, OAI.TorsionFreeZeroDivisors.LinkComponents.graph

6. abbrev OAI.TorsionFreeZeroDivisors.LinkComponents.ComponentOccurrence line 38
7. def OAI.TorsionFreeZeroDivisors.LinkComponents.restrict line 41
8. def OAI.TorsionFreeZeroDivisors.LinkComponents.unmatched line 45
9. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.card_occurrences line 49

   Source documentation

   Counting actual occurrences, including repeats, gives the sum of block multiplicities in the component.

   theorem card_occurrences (c : Component m P) :
       Fintype.card (ComponentOccurrence m P c) = ∑ i : c, m i.val := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component, OAI.TorsionFreeZeroDivisors.LinkComponents.ComponentOccurrence

10. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.card_block_occurrences line 59
11. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.balance line 73

    Source documentation

    Literal link balance in a component without a self-link.

    theorem balance (c : Component m P) (hn : ¬HasSelf m P c) (i : c) :
        2*m i.val ≤ (∑ j : c, m j.val) + unmatched m P c := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component, OAI.TorsionFreeZeroDivisors.LinkComponents.HasSelf, OAI.TorsionFreeZeroDivisors.LinkComponents.unmatched

12. def OAI.TorsionFreeZeroDivisors.LinkComponents.maximum line 86

    Source documentation

    The maximum multiplicity is present exactly in the active components.

    def maximum (c : Component m P) : ℕ :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component

13. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.le_maximum line 90
14. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.maximum_mem line 95
15. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.maximum_balance line 101
16. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.active_iff line 107
17. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.sum_components line 117

    Source documentation

    Components partition the underlying blocks, including the isolated ones.

    theorem sum_components {R : Type*} [AddCommMonoid R] (a : I → R) :
        (∑ c : Component m P, ∑ i : c, a i.val) = ∑ i, a i := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component

18. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.sum_unmatched line 126

    Source documentation

    Fixed occurrences are partitioned by precisely the same components.

    theorem sum_unmatched :
        (∑ c : Component m P, unmatched m P c) = Fintype.card P.Unmatched := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component, OAI.TorsionFreeZeroDivisors.LinkComponents.unmatched

19. def OAI.TorsionFreeZeroDivisors.LinkComponents.minimumRoot line 142

    Source documentation

    The bin-minimizing root need not be present at a given stage.

    def minimumRoot (d : I → ℝ) (c : Component m P) : c :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.Component

20. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.minimumRoot_le line 146
21. def OAI.TorsionFreeZeroDivisors.LinkComponents.componentLabelCost line 151
22. def OAI.TorsionFreeZeroDivisors.LinkComponents.stageCost line 156

    Source documentation

    The actual label/block part of the stage exponent, before embedding and uniform error terms are added. Stages are indexed from zero.

    def stageCost (M : ℕ) (d : I → ℝ) (δ s : ℝ) (j : Fin M) : ℝ :=
    …

23. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.sum_stageCost line 162

    Source documentation

    Summing the actual link-component exponents gives decay and only the globally counted unmatched correction. No coverage identity is assumed.

    theorem sum_stageCost (M : ℕ) (hm : ∀ i, m i ≤ M) (d : I → ℝ) (δ s a : ℝ)
        (hδ : 0 ≤ δ) (hs : 0 ≤ s) (ha : 0 ≤ a)
        (hlow : ∀ i, δ*s/2 ≤ d i) (hhigh : ∀ i, d i ≤ a*s) :
        (∑ j : Fin M, stageCost m P M d δ s j) ≤
          a*s*(Fintype.card P.Unmatched : ℝ) - δ/2*s*(∑ i, (m i : ℝ)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.stageCost

24. theorem OAI.TorsionFreeZeroDivisors.LinkComponents.sum_stageBound line 209

    Source documentation

    A numerical bound for actual stages: the Euler terms need only have nonpositive total, exactly as supplied by the immersed traversal argument.

    theorem sum_stageBound (M : ℕ) (hm : ∀ i, m i ≤ M) (d : I → ℝ) (δ s a logn : ℝ)
        (power err : Fin M → ℝ)
        (hδ : 0 ≤ δ) (hs : 0 ≤ s) (ha : 0 ≤ a) (hn : 0 ≤ logn)
        (hlow : ∀ i, δ*s/2 ≤ d i) (hhigh : ∀ i, d i ≤ a*s)
        (hpower : (∑ j : Fin M, power j) ≤ 0) :
        (Finset.univ.sum (fun j : Fin M => power j*logn + stageCost m P M d δ s j + err j)) ≤
          a*s*(Fintype.card P.Unmatched : ℝ) - δ/2*s*(∑ i, (m i : ℝ)) + (∑ j : Fin M, err j) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.LinkComponents.stageCost

25. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.transport line 227
26. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.transport_joined line 238
27. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.transport_partner line 241
28. abbrev OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Traversal line 266
29. abbrev OAI.TorsionFreeZeroDivisors.RepeatedBlocks.traversalLength line 267
30. abbrev OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying line 268
31. abbrev OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Occurrence line 269
32. abbrev OAI.TorsionFreeZeroDivisors.RepeatedBlocks.multiplicity line 270
33. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.occurrenceEquiv line 273

    Source documentation

    The occurrence index is retained separately from the common chain grid.

    def occurrenceEquiv : Occurrence s len m ≃ LinkComponents.Occurrence (multiplicity s len m) where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Occurrence, OAI.TorsionFreeZeroDivisors.LinkComponents.Occurrence, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.multiplicity

34. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.color line 279
35. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.height line 281
36. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.lower line 283
37. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.upper line 284
38. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.block_interval line 286
39. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.wordCoordinate line 290

    Source documentation

    Literal increasing edge coordinates shared by every repetition.

    def wordCoordinate (i : Underlying s len) : block s i.2.val ≃ Fin (height s len i) :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.height

40. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.wordCoordinate_val line 295
41. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.blockPositionEquiv line 299
42. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.coordinate line 315
43. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.coordinate_val line 319
44. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.data line 326
45. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.repeatedCoordinate line 330
46. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.links line 336
47. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.links_graph line 340
48. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.links_deficit line 343
49. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.links_consistent line 348
50. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.integerSlice_self line 359
51. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_slice_card line 370
52. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_comparison line 383

    Source documentation

    The original letter comparison restricts to precisely this integer slice.

    theorem self_comparison {A : Type*} (bar : A → A) (w : C → ℤ → A)
        (hcompare : ∀ x e, cmp.side x = some e →
          w x.1.1 x.2.val = if cmp.reverse e then
            bar (w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
          else w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
        (i : Underlying s len) (k t : Fin (m i.1)) (e : E)
        (hsource : (⟨i.1,k⟩ : Traversal m) = cmp.source e)
        (htarget : (⟨i.1,t⟩ : Traversal m) = cmp.source (cmp.flip e))
        (q : ℤ) (hq : q ∈ IntervalSelfLinks.selfSlice (lower s len i) (upper s len i)
          ⌈cmp.lo e-1/2⌉ ⌈cmp.hi e-1/2⌉ (cmp.reverse e) (cmp.offset e)) :
        w i.1 q = if cmp.reverse e then bar (w i.1 (affine (cmp.reverse e) (cmp.offset e) q))
          else w i.1 (affine (cmp.reverse e) (cmp.offset e) q) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Traversal, OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.selfSlice, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.lower, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.upper

53. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_shift_ne_zero line 408

    Source documentation

    Literal edge reduction rules out zero shift, rather than assuming that self-links are nontrivial translations.

    theorem self_shift_ne_zero
        (hreduced : ∀ x e, cmp.side x = some e →
          (x.1.1,x.2.val) ≠ ((cmp.pairing.partner x).1.1,(cmp.pairing.partner x).2.val))
        (i : Underlying s len) (k t : Fin (m i.1)) (e : E)
        (hne : ((data s hs len m cmp err).slice e ⟨i,k⟩ ⟨i,t⟩).Nonempty)
        (hrev : cmp.reverse e = false) : cmp.offset e ≠ 0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.data

54. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_link_translation line 427

    Source documentation

    A near-full actual self-link is a nonzero translation. Reversed self-links are infeasible for an immersed block, by the midpoint obstruction.

    theorem self_link_translation {A : Type*} (bar : A → A)
        (hbar : Function.Involutive bar) (hfree : ∀ a, bar a ≠ a)
        (w : C → ℤ → A)
        (hcompare : ∀ x e, cmp.side x = some e →
          w x.1.1 x.2.val = if cmp.reverse e then
            bar (w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
          else w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
        (hwordred : ∀ (i : Underlying s len) q,
          lower s len i ≤ q → q+1 < upper s len i → w i.1 (q+1) ≠ bar (w i.1 q))
        (hreduced : ∀ x e, cmp.side x = some e →
          (x.1.1,x.2.val) ≠ ((cmp.pairing.partner x).1.1,(cmp.pairing.partner x).2.val))
        (i : Underlying s len) (k t : Fin (m i.1)) (e : E)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.lower, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.upper

55. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.height_eq line 462
56. def OAI.TorsionFreeZeroDivisors.RepeatedBlocks.word line 467

    Source documentation

    The actual word on an underlying block, in its chain orientation.

    def word (w : C → ℤ → A) (i : Underlying s len) (k : Fin (height s len i)) : A :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.height

57. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.word_at_coordinateN line 470
58. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_translation_constraints line 480

    Source documentation

    A chosen literal self-comparison yields a fixed translation forest that works for all compatible words. Its cardinality is the original slice's, not an unrelated proxy for the number of constraints.

    theorem self_translation_constraints
        (i : Underlying s len) (k t : Fin (m i.1)) (e : E)
        (hsource : (⟨i.1,k⟩ : Traversal m) = cmp.source e)
        (htarget : (⟨i.1,t⟩ : Traversal m) = cmp.source (cmp.flip e))
        (hrev : cmp.reverse e = false) (hz : cmp.offset e ≠ 0) :
        ∃ tr : BlockConstraints.Translation (height s len i),
          tr.domain.card = ((data s hs len m cmp err).slice e ⟨i,k⟩ ⟨i,t⟩).card ∧
          ∀ (A : Type*) (bar : A → A) (w : C → ℤ → A),
            (∀ x e, cmp.side x = some e →
              w x.1.1 x.2.val = if cmp.reverse e then
                bar (w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
              else w (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val) →
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Traversal, OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.height, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.data

59. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.positions_height line 505
60. theorem OAI.TorsionFreeZeroDivisors.RepeatedBlocks.self_component_translation line 513

    Source documentation

    Every literal self-linked component has a root and a translation forest of the prescribed deficit. A single feasible immersed labeling rules out the reflection case; the resulting forest then constrains every feasible labeling.

    theorem self_component_translation [Fintype C]
        {A : Type*} (bar : A → A) (hbar : Function.Involutive bar) (hfree : ∀ a, bar a ≠ a)
        (w₀ : C → ℤ → A)
        (hcompare₀ : ∀ x e, cmp.side x = some e →
          w₀ x.1.1 x.2.val = if cmp.reverse e then
            bar (w₀ (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
          else w₀ (cmp.pairing.partner x).1.1 (cmp.pairing.partner x).2.val)
        (hwordred : ∀ (i : Underlying s len) q,
          lower s len i ≤ q → q+1 < upper s len i → w₀ i.1 (q+1) ≠ bar (w₀ i.1 q))
        (hreduced : ∀ x e, cmp.side x = some e →
          (x.1.1,x.2.val) ≠ ((cmp.pairing.partner x).1.1,(cmp.pairing.partner x).2.val))
        (c : LinkComponents.Component (multiplicity s len m) (data s hs len m cmp err).matching)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RepeatedBlocks.Underlying, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.lower, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.upper, OAI.TorsionFreeZeroDivisors.LinkComponents.Component, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.multiplicity, OAI.TorsionFreeZeroDivisors.RepeatedBlocks.data