OAI/Probability/FKMaps/CornerInverse.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Chords.openerEmbedding line 11

   Source documentation

   Transport a core matching through its strictly increasing position map.

   def openerEmbedding (a : Perm (Fin N)) (b : Perm (Fin K))
       (e : Fin K ↪o Fin N) (h : ∀ i,a (e i)=e (b i)) : Opener b ↪ Opener a where
   …

   Mentions: OAI.FKCRT.Chords.Opener

2. lemma OAI.FKCRT.Chords.cross_embedding line 16
3. def OAI.FKCRT.Chords.graphHom line 23
4. lemma OAI.FKCRT.Chords.opener_range line 28
5. lemma OAI.FKCRT.Chords.core_closed_of_chunks line 40

   Source documentation

   Once every unmarked interval is matched internally, the core mask is also matched internally; this is forced by the actual involution.

   lemma core_closed_of_chunks (a : Perm (Fin N)) (ha : Function.Involutive a)
       (p : Fin N→Bool) (hN : 0<N) (hp : p ⟨0,hN⟩=true)
       (hchunks : ∀ x∈(CornerSplit.split p (List.finRange N)).2,∀ d∈x.2,a d∈x.2) :
       ∀ d,p (a d)=p d := by
   …

   Mentions: OAI.FKCRT.CornerSplit.split

6. theorem OAI.FKCRT.Chords.root_component_insertion line 61

   Source documentation

   Inserting internally matched words in the corners of a connected core leaves precisely that core as the root crossing component.

   theorem root_component_insertion (a : Perm (Fin N)) (ha : Function.Involutive a)
       (hf : ∀ d,a d≠d) (b : Perm (Fin K)) (e : Fin K ↪o Fin N)
       (hmatch : ∀ i,a (e i)=e (b i)) (r : Opener b) (hr : (e r.val).val=0)
       (hconnected : ∀ x : Opener b,(graph b).Reachable r x)
       (hchunks : ∀ x∈(CornerSplit.split (fun d => decide (d∈Set.range e)) (List.finRange N)).2,
         ∀ d∈x.2,a d∈x.2) :
       componentDarts a (openerEmbedding a b e hmatch r)=Finset.univ.filter (fun d => d∈Set.range e) := by
   …

   Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.graph, OAI.FKCRT.CornerSplit.split, OAI.FKCRT.Chords.componentDarts, OAI.FKCRT.Chords.openerEmbedding

7. lemma OAI.FKCRT.CornerSplit.skeleton_sublist line 90
8. lemma OAI.FKCRT.MapCycles.scanArches_corners_subset line 101
9. lemma OAI.FKCRT.Inventory.typed_corner_scans line 119
10. theorem OAI.FKCRT.Inventory.corner_core_pairs line 137

    Source documentation

    Actual core pairs remain the same pairs after inserting arbitrary successful corner words. This controls the adaptive matching itself.

    theorem corner_core_pairs (w : α→TypedLetter) (l : List (α×List α))
        (hn : (CornerSplit.join l).Nodup)
        (hw : ∀ x∈l,stackTypedRun (x.2.map w) []=some [])
        (E F C D : List (α×α))
        (hE : Arches (CornerSplit.join l) E) (hF : Arches (CornerSplit.join l) F)
        (hc : (endpoints (E++F)).Perm (CornerSplit.join l))
        (htE : ∀ e∈E,w e.1=.burger true ∧ w e.2=.order true)
        (htF : ∀ e∈F,w e.1=.burger false ∧ w e.2=.order false)
        (hC : Arches (l.map Prod.fst) C) (hD : Arches (l.map Prod.fst) D)
        (hd : (endpoints (C++D)).Perm (l.map Prod.fst))
        (htC : ∀ e∈C,w e.1=.burger true ∧ w e.2=.order true)
        (htD : ∀ e∈D,w e.1=.burger false ∧ w e.2=.order false) :
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.CornerSplit.join, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

11. theorem OAI.FKCRT.Inventory.corner_core_turns line 170

    Source documentation

    The exact matching restriction, stated on every actual core endpoint.

    theorem corner_core_turns (w : α→TypedLetter) (l : List (α×List α))
        (hn : (CornerSplit.join l).Nodup)
        (hw : ∀ x∈l,stackTypedRun (x.2.map w) []=some [])
        (E F C D : List (α×α))
        (hE : Arches (CornerSplit.join l) E) (hF : Arches (CornerSplit.join l) F)
        (hc : (endpoints (E++F)).Perm (CornerSplit.join l))
        (htE : ∀ e∈E,w e.1=.burger true ∧ w e.2=.order true)
        (htF : ∀ e∈F,w e.1=.burger false ∧ w e.2=.order false)
        (hC : Arches (l.map Prod.fst) C) (hD : Arches (l.map Prod.fst) D)
        (hd : (endpoints (C++D)).Perm (l.map Prod.fst))
        (htC : ∀ e∈C,w e.1=.burger true ∧ w e.2=.order true)
        (htD : ∀ e∈D,w e.1=.burger false ∧ w e.2=.order false) :
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.CornerSplit.join, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

12. lemma OAI.FKCRT.CornerSplit.join_perm_parts line 206
13. lemma OAI.FKCRT.CornerSplit.own_mask line 217
14. def OAI.FKCRT.Chords.partialOpener line 232
15. def OAI.FKCRT.Chords.partialGraphHom line 237
16. theorem OAI.FKCRT.Chords.root_component_partial line 249
17. theorem OAI.FKCRT.Inventory.connected_corner_inverse line 275

    Source documentation

    Exact inverse of root-component extraction. Connectivity here specifies which finite words are cores; all corner matching and separation facts are proved from the original stack algorithm.

    theorem connected_corner_inverse (w : Fin N→TypedLetter)
        (l : List (Fin N×List (Fin N))) (hjoin : CornerSplit.join l=List.finRange N)
        (hw : ∀ x∈l,stackTypedRun (x.2.map w) []=some [])
        (E F C D : List (Fin N×Fin N))
        (hE : Arches (List.finRange N) E) (hF : Arches (List.finRange N) F)
        (hc : (endpoints (E++F)).Perm (List.finRange N))
        (htE : ∀ e∈E,w e.1=.burger true ∧ w e.2=.order true)
        (htF : ∀ e∈F,w e.1=.burger false ∧ w e.2=.order false)
        (hC : Arches (l.map Prod.fst) C) (hD : Arches (l.map Prod.fst) D)
        (hd : (endpoints (C++D)).Perm (l.map Prod.fst))
        (htC : ∀ e∈C,w e.1=.burger true ∧ w e.2=.order true)
        (htD : ∀ e∈D,w e.1=.burger false ∧ w e.2=.order false)
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.CornerSplit.join, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.D

18. lemma OAI.FKCRT.MapCycles.Arches.map line 338
19. lemma OAI.FKCRT.MapCycles.endpoints_map line 346
20. lemma OAI.FKCRT.MapCycles.Arches.filter line 354
21. lemma OAI.FKCRT.MapCycles.endpoints_filter line 375
22. theorem OAI.FKCRT.Inventory.matching_subword_empty line 393

    Source documentation

    Restrict the actual successful word to any union of its matched pairs. This includes both its root component and each real corner interval.

    theorem matching_subword_empty (w : α→TypedLetter) (l : List α) (hn : l.Nodup)
        (E F : List (α×α)) (hE : Arches l E) (hF : Arches l F)
        (hc : (endpoints (E++F)).Perm l)
        (htE : ∀ e∈E,w e.1=.burger true ∧ w e.2=.order true)
        (htF : ∀ e∈F,w e.1=.burger false ∧ w e.2=.order false)
        (p : α→Bool) (hp : ∀ d∈l,p (turns (E++F) d)=p d) :
        stackTypedRun ((l.filter p).map w) []=some [] := by
    …

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

23. lemma OAI.FKCRT.MapCycles.turns_map_on line 425
24. structure OAI.FKCRT.Inventory.StackMatching line 443

    Source documentation

    A certificate for the actual two stack matchings of a finite typed word. The matching uniqueness theorem makes its induced mate choice-independent.

    structure StackMatching (w : α→TypedLetter) (l : List α) where
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter

25. def OAI.FKCRT.Inventory.StackMatching.ofEmpty line 455
26. def OAI.FKCRT.Inventory.StackMatching.mate line 461
27. lemma OAI.FKCRT.Inventory.StackMatching.empty line 463
28. lemma OAI.FKCRT.Inventory.StackMatching.unique_mate line 468
29. lemma OAI.FKCRT.Inventory.StackMatching.involutive line 474
30. lemma OAI.FKCRT.Inventory.StackMatching.no_fixed line 477
31. lemma OAI.FKCRT.Inventory.StackMatching.endpoints_mem line 482
32. def OAI.FKCRT.Inventory.StackMatching.map line 487
33. lemma OAI.FKCRT.Inventory.StackMatching.map_mate line 505
34. lemma OAI.FKCRT.Inventory.StackMatching.cast_mate line 513
35. def OAI.FKCRT.Inventory.positionEmbedding line 520

    Source documentation

    The literal increasing compression map, not a fresh random matching.

    def positionEmbedding (l : List α) (hs : l.Pairwise (·<·)) : Fin l.length ↪o α :=
    …

36. lemma OAI.FKCRT.Inventory.positions_word line 524
37. theorem OAI.FKCRT.Inventory.normalized_matching_mate line 529

    Source documentation

    Normalization preserves the actual mate permutation on all positions.

    theorem normalized_matching_mate (w : α→TypedLetter) (l : List α) (hs : l.Pairwise (·<·))
        (M : StackMatching w l) :
        ∃ P : StackMatching (w ∘ l.get) (List.finRange l.length),
          ∀ i,M.mate (l.get i)=l.get (P.mate i) := by
    …

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

38. lemma OAI.FKCRT.MapCycles.turns_sublist_preserves line 557
39. lemma OAI.FKCRT.Inventory.StackMatching.empty_prefix_preserves line 578
40. def OAI.FKCRT.Inventory.StackMatching.empty_prefix_wedge line 593

    Source documentation

    A genuine successful inserted interval of the actual typed matching creates a one-vertex union for the full, all-edge map graph. The local graph metric conclusions now follow unconditionally from GraphWedge.Data.

    def StackMatching.empty_prefix_wedge {w : α→TypedLetter} (a b : α) (L R : List α)
        (M : StackMatching w ((a::L)++(b::R))) (hn : ((a::L)++(b::R)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) :
        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

41. theorem OAI.FKCRT.Inventory.StackMatching.empty_prefix_distance line 615

    Source documentation

    Literal all-edge distance preservation for actual typed insertion, not merely the selected spanning tree or a replacement metric.

    theorem StackMatching.empty_prefix_distance {w : α→TypedLetter} (a b : α) (L R : List α)
        (M : StackMatching w ((a::L)++(b::R))) (hn : ((a::L)++(b::R)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (x y : α)
        (hx : x∈a::L) (hy : y∈a::L) :
        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

42. theorem OAI.FKCRT.Inventory.StackMatching.empty_prefix_cross_distance line 637

    Source documentation

    Cross-block distances in the original all-edge map add through the unique identified vertex. This includes coincident poles and loop edges.

    theorem StackMatching.empty_prefix_cross_distance {w : α→TypedLetter} (a b : α) (L R : List α)
        (M : StackMatching w ((a::L)++(b::R))) (hn : ((a::L)++(b::R)).Nodup)
        (hv : stackTypedRun ((a::L).map w) []=some []) (x y : α)
        (hx : x∈a::L) (hy : y∉a::L) :
        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