OAI/Algebra/GroupRing/MatchedLabels.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.MatchedLabels.graph line 17
2. structure OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness line 24
3. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.exists_witness line 35
4. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.domain line 52
5. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.originCoordinate line 54
6. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.targetCoordinate line 57
7. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.includeDomain line 60
8. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.compareTarget line 67
9. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.known line 70
10. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.known_card line 73
11. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.recover line 76
12. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.recover_spec line 79
13. def OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.source line 83
14. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.Witness.deficit line 86
15. def OAI.TorsionFreeZeroDivisors.MatchedLabels.chooseWitness line 95
16. def OAI.TorsionFreeZeroDivisors.MatchedLabels.links line 98
17. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.links_deficit line 108
18. theorem OAI.TorsionFreeZeroDivisors.MatchedLabels.links_consistent line 115

    Source documentation

    Any actual comparison-compatible labeling induces full feasible words on all blocks, including those not present at a chosen multiplicity stage.

    theorem links_consistent (letters : Ω → A) (words : (i : I) → Fin (h i) → A)
        (hcompare : ∀ x e, D.side x = some e → letters x = symbol e (letters (D.pairing.partner x)))
        (hwords : ∀ b (x : D.positions b), words (color b) (coordinate b x) = letters x.val) :
        (links D color h coordinate symbol).Consistent words := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MatchedLabels.links

19. structure OAI.TorsionFreeZeroDivisors.BlockConstraints.ParentMap line 148

    Source documentation

    A partial parent map strictly decreasing the position index.

    structure ParentMap (h : ℕ) where
    …

20. def OAI.TorsionFreeZeroDivisors.BlockConstraints.ParentMap.Root line 157

    Source documentation

    Roots are precisely the positions not constrained to earlier positions.

    def Root := {j : Fin h // P.parent j = none}

21. def OAI.TorsionFreeZeroDivisors.BlockConstraints.ParentMap.Consistent line 159
22. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.ParentMap.determined_by_roots line 163

    Source documentation

    The letters at roots determine every consistent word.

    theorem determined_by_roots {w v : Fin h → T}
        (hw : P.Consistent w) (hv : P.Consistent v)
        (hr : ∀ r : P.Root, w r.val = v r.val) : w = v := by
    …

23. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.ParentMap.card_consistent_le line 180

    Source documentation

    A forest of equality constraints costs one free letter per root.

    theorem card_consistent_le [Fintype T] :
        Nat.card {w : Fin h → T // P.Consistent w} ≤
          (Fintype.card T) ^ Nat.card P.Root := by
    …

24. structure OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation line 197

    Source documentation

    A set of translated positions; the integral shift is positive.

    structure Translation (h : ℕ) where
    …

25. def OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.target line 208

    Source documentation

    The image position of a prescribed comparison.

    def target (i : D.domain) : Fin h := ⟨i.val.val + D.shift, D.bounded i.val i.property⟩

26. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.target_injective line 210
27. def OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.parents line 218
28. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.root_iff line 233
29. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.card_roots line 239

    Source documentation

    Each distinct translated edge removes exactly one root.

    theorem card_roots : Nat.card D.parents.Root = h - D.domain.card := by
    …

30. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation.word_count line 252

    Source documentation

    Equalities along a nonzero translation form a forest, even without the additional contiguous-domain hypothesis in the manuscript.

    theorem word_count {T : Type*} [Fintype T] :
        Nat.card {w : Fin h → T // ∀ i : D.domain, w (D.target i) = w i.val} ≤
          (Fintype.card T) ^ (h - D.domain.card) := by
    …

31. theorem OAI.TorsionFreeZeroDivisors.BlockConstraints.reflection_impossible line 285

    Source documentation

    A reflection self-link on an overlapping interval contradicts either fixed-point-freeness of inversion or the reduced-word condition. Indices are integers; half-integer manuscript positions have been shifted by 1/2.

    theorem reflection_impossible {T : Type*} (bar : T → T)
        (hbar : Function.Involutive bar) (hfree : ∀ t, bar t ≠ t)
        (w : ℤ → T) (h reducedLo reducedHi lo hi b : ℤ)
        (hlo : 0 ≤ lo) (hhi : hi < h) (_hne : lo ≤ hi)
        (himagelo : 0 ≤ b - hi) (himagehi : b - lo < h)
        (hlarge : h < 2 * (hi - lo + 1))
        (hredlo : reducedLo ≤ lo) (hredhi : hi ≤ reducedHi)
        (hred : ∀ i : ℤ, reducedLo ≤ i → i + 1 ≤ reducedHi → w (i+1) ≠ bar (w i))
        (hcompare : ∀ i : ℤ, lo ≤ i → i ≤ hi → w i = bar (w (b-i))) : False := by
    …

32. def OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinate line 323

    Source documentation

    The literal increasing coordinate on a contiguous block of integer edge indices (the manuscript's half-integer centers shifted by 1/2).

    def coordinate (lo hi : ℤ) : (Finset.Ico lo hi) ≃ Fin (hi-lo).toNat where
    …

33. theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinate_val line 341
34. def OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.domainEmbedding line 350
35. def OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.positiveTranslation line 357
36. theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.positive_card line 369
37. theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.positive_consistent line 372
38. theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.translation_representation line 391

    Source documentation

    Either direction of a nonzero translation yields exactly |D| distinct forest constraints, without requiring a substring to contain the entire block.

    theorem translation_representation (a : ℤ) (D : Finset ℤ) (ha : a ≠ 0)
        (hD : ∀ q ∈ D, q ∈ Finset.Ico lo hi ∧ q+a ∈ Finset.Ico lo hi) :
        ∃ tr : Translation (hi-lo).toNat, tr.domain.card = D.card ∧
          ∀ (A : Type*) (w : Fin (hi-lo).toNat → A),
            (∀ q (hq : q ∈ D),
              w (coordinate lo hi ⟨q+a,(hD q hq).2⟩) = w (coordinate lo hi ⟨q,(hD q hq).1⟩)) →
              ∀ k : tr.domain, w (tr.target k) = w k.val := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinate

39. theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.reflection_excluded line 420

    Source documentation

    Direct reflection obstruction on literal interval coordinates. The reduced word is the actual block word; no cyclic reduction or external extension is used.

    theorem reflection_excluded {A : Type*} (bar : A → A)
        (hbar : Function.Involutive bar) (hfree : ∀ x, bar x ≠ x)
        (w : ℤ → A) (L U l u b : ℤ)
        (hl : L ≤ l) (hu : u ≤ U) (_hne : l < u)
        (htl : L ≤ b-(u-1)) (htu : b-l < U)
        (hmass : U-L < 2*(u-l))
        (hred : ∀ q, L ≤ q → q+1 < U → w (q+1) ≠ bar (w q))
        (hcompare : ∀ q, l ≤ q → q < u → w q = bar (w (b-q))) : False := by
    …