OAI/Probability/FKMaps/CoreCompression.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.Inventory.StackMatching.empty_interval_preserves line 12
2. lemma OAI.FKCRT.Inventory.formPerm_append_comm line 24
3. lemma OAI.FKCRT.Inventory.StackMatching.empty_interval_rotation line 33

   Source documentation

   Cutting any nonempty successful insertion interval is a literal one-vertex split of the original rotation. No random root/rotation is used.

   lemma StackMatching.empty_interval_rotation {w : α→TypedLetter}
       (u L z : List α) (a b : α) (R : List α)
       (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
       (hcomp : z++u=b::R) :
       (u++((a::L)++z)).formPerm*turns M.first=
         swap a b*((a::L).formPerm*(b::R).formPerm*turns M.first) := by
   …

   Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching

4. def OAI.FKCRT.Inventory.StackMatching.empty_interval_wedge line 52

   Source documentation

   The two graph pieces retain every edge, including both matching colours. This is the actual all-edge graph at an arbitrary insertion interval.

   def StackMatching.empty_interval_wedge {w : α→TypedLetter}
       (u L z : List α) (a b : α) (R : List α)
       (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
       (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R) :
       let p := (a::L).formPerm*(b::R).formPerm*turns M.first
   …

   Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map

5. theorem OAI.FKCRT.Inventory.StackMatching.empty_interval_pole line 77

   Source documentation

   The first dart following the successful subword and its first dart are literally in the same original rotation vertex. This is the pole identity.

   theorem StackMatching.empty_interval_pole {w : α→TypedLetter}
       (u L z : List α) (a b : α) (R : List α)
       (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
       (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R) :
       vertex ((u++((a::L)++z)).formPerm*turns M.first) a=
         vertex ((u++((a::L)++z)).formPerm*turns M.first) b := by
   …

   Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map

6. lemma OAI.FKCRT.PermutationWedge.sameCycle_congr_on line 101
7. def OAI.FKCRT.PermutationWedge.sideCongr line 122

   Source documentation

   Changing the ambient permutation off a retained invariant dart set does not change its actual rotation vertices.

   def sideCongr {p q : Perm α} {S : Set α}
       (hp : ∀ d,p d∈S ↔ d∈S) (hq : ∀ d,q d∈S ↔ d∈S)
       (he : ∀ d∈S,p d=q d) : Side p S ≃ Side q S :=
   …

   Mentions: OAI.FKCRT.PermutationWedge.Side

8. lemma OAI.FKCRT.PermutationWedge.sideCongr_mk line 127
9. def OAI.FKCRT.PermutationWedge.sideGraphCongr line 134

   Source documentation

   The all-edge graph is invariant under restriction/normalization on a closed set of darts; only the two literal permutation actions are used.

   def sideGraphCongr {p q e f : Perm α} {S : Set α}
       (hp : ∀ d,p d∈S ↔ d∈S) (hq : ∀ d,q d∈S ↔ d∈S)
       (he : ∀ d,e d∈S ↔ d∈S) (hf : ∀ d,f d∈S ↔ d∈S)
       (hpq : ∀ d∈S,p d=q d) (hef : ∀ d∈S,e d=f d) :
       sideGraph e p S he ≃g sideGraph f q S hf where
   …

   Mentions: OAI.FKCRT.PermutationWedge.sideGraph

10. def OAI.FKCRT.PermutationWedge.fullInclusion line 169
11. lemma OAI.FKCRT.PermutationWedge.fullInclusion_mk line 173
12. lemma OAI.FKCRT.PermutationWedge.fullInclusion_injective line 177
13. lemma OAI.FKCRT.PermutationWedge.fullRetract_wellDefined line 190
14. def OAI.FKCRT.PermutationWedge.fullRetract line 202
15. lemma OAI.FKCRT.PermutationWedge.fullRetract_mk line 208
16. lemma OAI.FKCRT.PermutationWedge.fullRetract_inclusion line 215
17. def OAI.FKCRT.PermutationWedge.fullInclusionHom line 221
18. lemma OAI.FKCRT.PermutationWedge.fullRetract_edge line 231
19. theorem OAI.FKCRT.PermutationWedge.fullInclusion_edist line 253

    Source documentation

    Other invariant components, including isolated deleted darts, cannot shorten distances in a retained component.

    theorem fullInclusion_edist {p e : Perm α} {S : Set α}
        (hp : ∀ d,p d∈S ↔ d∈S) (he : ∀ d,e d∈S ↔ d∈S)
        (x y : Side p S) :
        (dartGraph e p).edist (fullInclusion p S x) (fullInclusion p S y)=
          (sideGraph e p S he).edist x y := by
    …

    Mentions: OAI.FKCRT.PermutationWedge.Side, OAI.FKCRT.PermutationWedge.dartGraph, OAI.FKCRT.PermutationWedge.fullInclusion, OAI.FKCRT.PermutationWedge.sideGraph

20. theorem OAI.FKCRT.Chords.reachable_lift line 281

    Source documentation

    Reachability lifts through a strictly increasing matching embedding whenever its image contains the whole component being lifted.

    theorem reachable_lift (a : Perm (Fin N)) (b : Perm (Fin K))
        (e : Fin K ↪o Fin N) (hmatch : ∀ i,a (e i)=e (b i))
        (r : Opener b)
        (himage : ∀ x : Opener a,(graph a).Reachable (openerEmbedding a b e hmatch r) x →
          x.val∈Set.range e) :
        ∀ x : Opener a,(graph a).Reachable (openerEmbedding a b e hmatch r) x →
          ∃ y : Opener b,openerEmbedding a b e hmatch y=x ∧ (graph b).Reachable r y := by
    …

    Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.graph, OAI.FKCRT.Chords.openerEmbedding

21. theorem OAI.FKCRT.Chords.component_compression line 301
22. lemma OAI.FKCRT.Inventory.StackMatching.pair_mask line 336
23. def OAI.FKCRT.Inventory.StackMatching.filter line 343
24. lemma OAI.FKCRT.Inventory.StackMatching.filter_mate line 357
25. lemma OAI.FKCRT.MapCycles.turns_filter_on line 383
26. lemma OAI.FKCRT.MapCycles.perm_preserves_of_fixed line 398
27. lemma OAI.FKCRT.Inventory.StackMatching.filter_first line 413
28. lemma OAI.FKCRT.Inventory.StackMatching.filter_mate_on line 420
29. lemma OAI.FKCRT.Inventory.StackMatching.filter_mate_fixed line 427
30. lemma OAI.FKCRT.Inventory.StackMatching.filter_first_fixed line 435
31. lemma OAI.FKCRT.GraphWedge.iso_edist line 453
32. lemma OAI.FKCRT.Inventory.filter_delete_interval line 464
33. def OAI.FKCRT.Inventory.StackMatching.deleteInterval line 486

    Source documentation

    The actual retained matching after a successful insertion is erased.

    def StackMatching.deleteInterval {w : α→TypedLetter} {u v z : List α}
        (M : StackMatching w (u++(v++z))) (hn : (u++(v++z)).Nodup)
        (hv : stackTypedRun (v.map w) []=some []) : StackMatching w (u++z) := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun

34. lemma OAI.FKCRT.Inventory.StackMatching.cast_first line 498
35. theorem OAI.FKCRT.Inventory.StackMatching.delete_interval_distance line 504

    Source documentation

    Removing any genuine successful interval preserves all-edge distances between retained darts, not just spanning-tree distances. The resulting rotation is that of the original ordered word with the interval deleted.

    theorem StackMatching.delete_interval_distance {w : α→TypedLetter}
        (u L z : List α) (a b : α) (R : List α)
        (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R)
        (x y : α) (hx : x∉a::L) (hy : y∉a::L) :
        let D := M.deleteInterval hn hv
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map, OAI.FKCRT.Inventory.D

36. theorem OAI.FKCRT.Inventory.StackMatching.empty_interval_gate line 588

    Source documentation

    Each genuine inserted successful word has precisely one metric gate in its complement in the original all-edge map. This equality is in the original graph, not an independently postulated block-tree metric.

    theorem StackMatching.empty_interval_gate {w : α→TypedLetter}
        (u L z : List α) (a b : α) (R : List α)
        (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R)
        (x y : α) (hx : x∈a::L) (hy : y∉a::L) :
        let s := (u++((a::L)++z)).formPerm*turns M.first
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map

37. lemma OAI.FKCRT.Inventory.complement_disjoint_interval line 625
38. def OAI.FKCRT.Inventory.StackMatching.distance line 636

    Source documentation

    A notation for the actual original all-edge distance of a typed matching.

    def StackMatching.distance {w : α→TypedLetter} {l : List α}
        (M : StackMatching w l) (x y : α) : ℕ∞ :=
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching

39. lemma OAI.FKCRT.Inventory.StackMatching.distance_cast line 641
40. lemma OAI.FKCRT.Inventory.StackMatching.erase_distance line 647

    Source documentation

    Erasing a possibly empty successful interval does not shorten any retained all-edge distance. Both vertices are kept literal dart vertices.

    lemma StackMatching.erase_distance [Fintype α] {w : α→TypedLetter}
        (u v z : List α) (M : StackMatching w (u++(v++z)))
        (hn : (u++(v++z)).Nodup) (hv : stackTypedRun (v.map w) []=some [])
        (hc : u++z≠[]) (x y : α) (hx : x∈u++z) (hy : y∈u++z) :
        ∃ D : StackMatching w (u++z),M.distance x y=D.distance x y := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

41. def OAI.FKCRT.Inventory.dartInsert line 668

    Source documentation

    Literal dart order for all successive corner insertions.

    def dartInsert (l : List (α×List α)) : List α := l.flatMap fun p => p.1::p.2
    …

42. lemma OAI.FKCRT.Inventory.core_sublist_insert line 671
43. theorem OAI.FKCRT.Inventory.StackMatching.core_distance line 681

    Source documentation

    Iterated exact preservation of INTERIOR CORE distances under all its actual successful corner insertions, including trivial leaf intervals. No stochastic estimate and no replacement metric is assumed.

    theorem StackMatching.core_distance [Fintype α] {w : α→TypedLetter}
        (p : List α) (l : List (α×List α))
        (M : StackMatching w (p++dartInsert l)) (hn : (p++dartInsert l).Nodup)
        (he : ∀ c∈l,stackTypedRun (c.2.map w) []=some [])
        (hc : p++l.map Prod.fst≠[]) (x y : α)
        (hx : x∈p++l.map Prod.fst) (hy : y∈p++l.map Prod.fst) :
        ∃ D : StackMatching w (p++l.map Prod.fst),M.distance x y=D.distance x y := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.dartInsert, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

44. lemma OAI.FKCRT.Inventory.filter_keep_interval line 727
45. def OAI.FKCRT.Inventory.StackMatching.keepInterval line 748

    Source documentation

    The literal restricted successful matching, retaining an inserted word.

    def StackMatching.keepInterval {w : α→TypedLetter} {u v z : List α}
        (M : StackMatching w (u++(v++z))) (hn : (u++(v++z)).Nodup)
        (hv : stackTypedRun (v.map w) []=some []) : StackMatching w v := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun

46. theorem OAI.FKCRT.Inventory.StackMatching.keep_interval_distance line 761

    Source documentation

    All-edge distances inside inserted words are unchanged in the ambient map, and agree with the actual isolated typed matching of that word.

    theorem StackMatching.keep_interval_distance {w : α→TypedLetter}
        (u L z : List α) (a b : α) (R : List α)
        (M : StackMatching w (u++((a::L)++z))) (hn : (u++((a::L)++z)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (hcomp : z++u=b::R)
        (x y : α) (hx : x∈a::L) (hy : y∈a::L) :
        M.distance x y=(M.keepInterval hn hv).distance x y := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching.map, OAI.FKCRT.Inventory.StackMatching.distance