OAI/Algebra/GroupRing/ChunkComparisons.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ChunkComparisons.positionEquiv line 14
2. lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.positionEquiv_source line 21
3. lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.positionEquiv_coordinate line 24
4. def OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking.reindex line 29

   Source documentation

   Re-enumerating occurrence chunks does not change their geometric partition.

   def reindex (K : Chunking lp lt) (r : U ≃ T) (lu : U → ℕ) (hlen : ∀ u,lu u=lt (r u)) : Chunking lp lu where
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking

5. def OAI.TorsionFreeZeroDivisors.ChunkComparisons.multiplicity line 39
6. def OAI.TorsionFreeZeroDivisors.ChunkComparisons.enumeration line 43

   Source documentation

   Exact color-fibre enumeration, identifying the literal path traversals with the multiplicity-indexed traversal type used in every stage estimate.

   def enumeration : ((c : C) × Fin (multiplicity color c)) ≃ T :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ChunkComparisons.multiplicity

7. lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.enumeration_color line 47
8. lemma OAI.TorsionFreeZeroDivisors.ChunkComparisons.enumeration_length line 50
9. def OAI.TorsionFreeZeroDivisors.ChunkComparisons.repeated line 55

   Source documentation

   The complete finite reindexing into underlying chain and occurrence number.

   def repeated (K : Chunking lp lt) (len : C → ℕ) (hl : ∀ t,lt t=len (color t)) :
       Chunking lp (fun o : (c : C) × Fin (multiplicity color c) => len o.1) :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ChunkComparisons.Chunking, OAI.TorsionFreeZeroDivisors.ChunkComparisons.multiplicity

10. abbrev OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.lengths line 66
11. lemma OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.ofFn_lengths line 68
12. lemma OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.total_length line 72
13. lemma OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.start_eq line 75
14. lemma OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.get_flatMap line 81

    Source documentation

    Literal indexing through a list concatenation, including repeated chunks.

    lemma get_flatMap (i : Fin ds.length) (q : Fin (lengths ds word i)) :
        (ds.flatMap word)[start (lengths ds word) i+q.val]? = some ((word (ds.get i)).get q) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ListChunkCoordinates.lengths

15. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.orientation line 114
16. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.representative line 116
17. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.reversed line 117
18. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.oriented line 119
19. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.oriented_length line 122
20. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.word_get line 127
21. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.reverse_iter line 130
22. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.listDart line 145
23. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunks line 170
24. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunkLength line 171
25. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunkReverse line 172
26. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.color line 173
27. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.splitChunks line 175
28. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunkLength_eq line 178
29. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.pathLength_eq line 183
30. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunk_dart line 188

    Source documentation

    The original path's actual dart at the signed chunk image.

    lemma chunk_dart (x : Position (traversalLength (chunks Γ mark h2 paths) (chunkLength Γ mark h2 paths))) :
        ((paths x.1.1).flatMap w)[((splitChunks Γ mark h2 paths).equiv x).2.val.toNat]? =
          some (if (splitChunks Γ mark h2 paths).reverse x.1 then
            Γ.reverse (F^[x.2.val.toNat] (color Γ mark h2 paths x.1).val.val)
            else F^[x.2.val.toNat] (color Γ mark h2 paths x.1).val.val) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunks, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunkLength, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.splitChunks, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.color

31. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.originalDart line 222

    Source documentation

    Literal darts at all original path positions.

    def originalDart (x : Position (pathLength (chunks Γ mark h2 paths) (chunkLength Γ mark h2 paths))) : D :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunks, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunkLength

32. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.originalDart_get line 231
33. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.chunk_original line 235
34. def OAI.TorsionFreeZeroDivisors.ChainChunkTransport.repeatedChunks line 244
35. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.repeated_original line 247
36. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.signed_eq_or_reverse line 258
37. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.normalized_reduced line 269

    Source documentation

    Reduction survives signed normalization: neither orientation of an actual paired undirected edge can become the same chain-coordinate position.

    lemma normalized_reduced
        (hred : ∀ x e,cmp.side x=some e →
          originalDart Γ mark h2 paths x≠originalDart Γ mark h2 paths (cmp.pairing.partner x) ∧
          originalDart Γ mark h2 paths x≠Γ.reverse (originalDart Γ mark h2 paths (cmp.pairing.partner x))) :
        ∀ x a,((repeatedChunks Γ mark h2 paths).comparisons cmp lo hi hlo hhi).side x=some a →
          (x.1.1,x.2.val)≠
          ((((repeatedChunks Γ mark h2 paths).comparisons cmp lo hi hlo hhi).pairing.partner x).1.1,
           (((repeatedChunks Γ mark h2 paths).comparisons cmp lo hi hlo hhi).pairing.partner x).2.val) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainChunkTransport.originalDart, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.repeatedChunks

38. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.normalized_compatible line 294

    Source documentation

    Actual graph labels, including reversal, induce precisely the literal compatibility constraints used by the repeated-block entropy estimates.

    lemma normalized_compatible {A : Type*} (bar : A → A) (hb : Function.Involutive bar)
        (label : D → A) (hl : ∀ d,label (Γ.reverse d)=bar (label d))
        (hc : ∀ x e,cmp.side x=some e → label (originalDart Γ mark h2 paths x)=
          if cmp.reverse e then bar (label (originalDart Γ mark h2 paths (cmp.pairing.partner x)))
          else label (originalDart Γ mark h2 paths (cmp.pairing.partner x))) :
        ∀ x a,((repeatedChunks Γ mark h2 paths).comparisons cmp lo hi hlo hhi).side x=some a →
          label (F^[x.2.val.toNat] x.1.1.val.val)=
          if ((repeatedChunks Γ mark h2 paths).comparisons cmp lo hi hlo hhi).reverse a then
            bar (label (F^[(((repeatedChunks Γ mark h2 paths).pairing cmp).partner x).2.val.toNat]
              (((repeatedChunks Γ mark h2 paths).pairing cmp).partner x).1.1.val.val))
          else label (F^[(((repeatedChunks Γ mark h2 paths).pairing cmp).partner x).2.val.toNat]
              (((repeatedChunks Γ mark h2 paths).pairing cmp).partner x).1.1.val.val) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainChunkTransport.originalDart, OAI.TorsionFreeZeroDivisors.ChainChunkTransport.repeatedChunks

39. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.internal_step line 315

    Source documentation

    A step strictly inside a suppressed chain is an actual reduced graph passage, with both outgoing ports at precisely the same original vertex.

    lemma internal_step (d : B) (i : ℕ) (hi : i+1 < len d) :
        Γ.origin (F^[i+1] d.val)=Γ.origin (Γ.reverse (F^[i] d.val)) ∧
          F^[i+1] d.val≠Γ.reverse (F^[i] d.val) := by
    …

40. lemma OAI.TorsionFreeZeroDivisors.ChainChunkTransport.normalized_immersed line 331

    Source documentation

    Immersion of the literal labelled graph gives the reduced signed chain words required by every reflection and squared-word argument.

    lemma normalized_immersed {A : Type*} (bar : A → A) (label : D → A)
        (hl : ∀ d,label (Γ.reverse d)=bar (label d))
        (hinj : ∀ d e,Γ.origin d=Γ.origin e → label d=label e → d=e)
        (c : R) (q : ℤ) (hq : 0≤q) (hq' : q+1<repLength Γ mark h2 c) :
        label (F^[(q+1).toNat] c.val.val)≠bar (label (F^[q.toNat] c.val.val)) := by
    …

41. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.representative_val line 355
42. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.reverse_oriented line 359
43. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.representative_reverse line 372
44. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.unsigned line 377
45. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.signed_representative line 387
46. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.representative_iff line 391
47. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.sign_injective line 404
48. def OAI.TorsionFreeZeroDivisors.ChainMultiplicity.incidenceEquiv line 419

    Source documentation

    The incidence fibre used in the Euler-exponent proof is the exact colour fibre used in the chain/block first moment. Both chain orientations count once.

    def incidenceEquiv (c : R) :
        {o : (p : P) × (Fin (paths p).length × Bool) // PathIncidences.familyPort (S).reverse e o=c.val} ≃
          {t : tp // col t=c} where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.PathIncidences.familyPort

49. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.multiplicity_eq line 450
50. lemma OAI.TorsionFreeZeroDivisors.ChainMultiplicity.multiplicity_at line 457