OAI/Probability/FKMaps/WordMaps.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Inventory.TypedLetter.color line 11
2. def OAI.FKCRT.Inventory.TypedLetter.step line 15
3. lemma OAI.FKCRT.Inventory.colorWord_map line 19
4. theorem OAI.FKCRT.Inventory.identified_matchings line 30

   Source documentation

   Actual identified words produce a complete pair of noncrossing matchings; the labels on each pair are the matching burger and fixed order.

   theorem identified_matchings {n : ℕ} (w : Dart n→TypedLetter)
       (hw : stackTypedRun ((List.finRange (2*(n+1))).map w) []=some []) :
       ∃ E F : List (Dart n × Dart n),
         Arches (List.finRange (2*(n+1))) E ∧
         Arches (List.finRange (2*(n+1))) F ∧
         (endpoints (E++F)).Perm (List.finRange (2*(n+1))) ∧
         (∀ e∈E,w e.1=.burger true ∧ w e.2=.order true) ∧
         (∀ e∈F,w e.1=.burger false ∧ w e.2=.order false) := by
   …

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

5. theorem OAI.FKCRT.Inventory.identified_map_exists line 69

   Source documentation

   The finite inverse in words.tex is defined on every nonempty identified word, and lands in the exact genus-zero maps rather than an auxiliary class.

   theorem identified_map_exists {n : ℕ} (w : Dart n→TypedLetter)
       (hw : stackTypedRun ((List.finRange (2*(n+1))).map w) []=some []) :
       ∃ E F : List (Dart n × Dart n),
         MapConditions (turns (E++F),(List.finRange (2*(n+1))).formPerm * turns E) ∧
         (∀ e∈E,w e.1=.burger true ∧ w e.2=.order true) ∧
         (∀ e∈F,w e.1=.burger false ∧ w e.2=.order false) := by
   …

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

6. def OAI.FKCRT.MapCycles.scanArches line 88

   Source documentation

   Deterministic stack matching of one colour; none skips the other colour.

   def scanArches (f : α→Option Bool) : List α → List α → Option (List α × List (α×α))
     | [],S => some (S,[])
     | a::l,S => match f a with
         | none => scanArches f l S
         | some true => scanArches f l (a::S)
         | some false => match S with
           | [] => none
           | b::S => (scanArches f l S).map (fun z => (z.1,(b,a)::z.2))

7. lemma OAI.FKCRT.MapCycles.scanArches_append line 97
8. lemma OAI.FKCRT.MapCycles.Arches.mem_endpoints line 117
9. theorem OAI.FKCRT.MapCycles.Arches.scan line 126

   Source documentation

   Noncrossing typed pairings are uniquely recovered by the stack. In particular no hidden choice of an arch pairing enters the map inverse.

   theorem Arches.scan {l : List α} {E : List (α×α)} (h : Arches l E)
       (hn : l.Nodup) (f : α→Option Bool)
       (hp : ∀ e∈E,f e.1=some true ∧ f e.2=some false)
       (hc : ∀ x∈l,f x≠none → x∈MapCycles.endpoints E) (S : List α) :
       ∃ F,scanArches f l S=some (S,F) ∧ F.Perm E := by
   …

   Mentions: OAI.FKCRT.MapCycles.Arches, OAI.FKCRT.MapCycles.endpoints, OAI.FKCRT.MapCycles.scanArches

10. theorem OAI.FKCRT.MapCycles.arches_unique line 174

    Source documentation

    Uniqueness is literal up to the irrelevant order of disjoint pairs.

    theorem arches_unique {l : List α} {E F : List (α×α)}
        (hE : Arches l E) (hF : Arches l F) (hn : l.Nodup) (f : α→Option Bool)
        (hpE : ∀ e∈E,f e.1=some true ∧ f e.2=some false)
        (hpF : ∀ e∈F,f e.1=some true ∧ f e.2=some false)
        (hcE : ∀ x∈l,f x≠none → x∈MapCycles.endpoints E)
        (hcF : ∀ x∈l,f x≠none → x∈MapCycles.endpoints F) : E.Perm F := by
    …

    Mentions: OAI.FKCRT.MapCycles.Arches, OAI.FKCRT.MapCycles.endpoints

11. lemma OAI.FKCRT.MapCycles.endpoints_perm line 194
12. lemma OAI.FKCRT.MapCycles.turns_perm line 199
13. def OAI.FKCRT.Inventory.colorInstruction line 216

    Source documentation

    The one-colour stack instruction attached to a typed inventory symbol.

    def colorInstruction (c : Bool) : TypedLetter→Option Bool
      | .burger b => if b=c then some true else none
      | .order b => if b=c then some false else none

    Mentions: OAI.FKCRT.Inventory.TypedLetter

14. lemma OAI.FKCRT.Inventory.matching_color_coverage line 220
15. theorem OAI.FKCRT.Inventory.typed_matchings_unique line 246

    Source documentation

    Literal uniqueness of the inverse map's two matchings, including empty colour classes. This removes all pairing choices in identified_map_exists.

    theorem typed_matchings_unique (w : α→TypedLetter) (l : List α) (hn : l.Nodup)
        (E F E' F' : List (α×α))
        (hE : Arches l E) (hF : Arches l F) (hE' : Arches l E') (hF' : Arches l F')
        (hc : (endpoints (E++F)).Perm l) (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)
        (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) :
        E.Perm E' ∧ F.Perm F' := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter

16. theorem OAI.FKCRT.Inventory.typed_map_unique line 277

    Source documentation

    In particular the reconstructed edge and vertex permutations are independent of the proof/choice of Dyck pairing.

    theorem typed_map_unique (w : α→TypedLetter) (l : List α) (hn : l.Nodup)
        (E F E' F' : List (α×α))
        (hE : Arches l E) (hF : Arches l F) (hE' : Arches l E') (hF' : Arches l F')
        (hc : (endpoints (E++F)).Perm l) (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)
        (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) :
        turns (E++F)=turns (E'++F') ∧ l.formPerm*turns E=l.formPerm*turns E' := by
    …

    Mentions: OAI.FKCRT.Inventory.TypedLetter

17. theorem OAI.FKCRT.MapCycles.arches_of_noncrossing line 303

    Source documentation

    A closed involutive noncrossing colour matching admits exactly the recursive arch decomposition. No Jordan-curve principle is assumed.

    theorem arches_of_noncrossing (a : α→α) (ha : Function.Involutive a)
        (P : α→Bool) (hP : ∀ x,P (a x)=P x) (l : List α)
        (hs : l.Pairwise (·<·))
        (hc : ∀ x∈l,P x=true → a x∈l)
        (hf : ∀ x∈l,P x=true → a x≠x)
        (hn : ∀ x∈l,∀ y∈l,P x=true → P y=true → x<y → y<a x → a x<a y → False) :
        ∃ E,Arches l E ∧ (endpoints E).Perm (l.filter P) ∧
          ∀ e∈E,e.2=a e.1 ∧ P e.1=true := by
    …

    Mentions: OAI.FKCRT.MapCycles.Arches, OAI.FKCRT.MapCycles.endpoints

18. lemma OAI.FKCRT.MapCycles.orbitList_formPerm line 395
19. lemma OAI.FKCRT.MapCycles.ordered_four_sublist line 413
20. theorem OAI.FKCRT.ordered_no_crossing line 431

    Source documentation

    The orbit-maximal planar matching has the ordinary increasing-position noncrossing property, with root/end seam retained exactly.

    theorem ordered_no_crossing (a : Perm (Dart n)) (ha : Function.Involutive a)
        (l : List (Dart n)) (hs : l.Pairwise (·<·)) (hc : ∀ x,x∈l)
        (A : Finset (Orbit a))
        (hmax : Nat.card (Orbit (partialReversal a ha A*l.formPerm))=Nat.card (Orbit l.formPerm)+A.card)
        (x y : Dart n) (hx : orbit a x∈A) (hy : orbit a y∈A)
        (hxy : x<y) (hyx : y<a x) (haxy : a x<a y) : False := by
    …

    Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.orbit

21. theorem OAI.FKCRT.maximal_matching_arches line 460

    Source documentation

    Every orbit-maximal one-colour matching is an actual stack matching.

    theorem maximal_matching_arches (a : Perm (Dart n)) (ha : Function.Involutive a)
        (hf : ∀ x,a x≠x) (A : Finset (Orbit a))
        (hmax : Nat.card (Orbit (partialReversal a ha A*(List.finRange (2*(n+1))).formPerm))=
          Nat.card (Orbit (List.finRange (2*(n+1))).formPerm)+A.card) :
        ∃ E,Arches (List.finRange (2*(n+1))) E ∧
          (endpoints E).Perm ((List.finRange (2*(n+1))).filter (fun x => decide (orbit a x∈A))) ∧
          ∀ e∈E,e.2=a e.1 ∧ orbit a e.1∈A := by
    …

    Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.orbit

22. lemma OAI.FKCRT.Inventory.scanArches_prefix line 487
23. lemma OAI.FKCRT.Inventory.scanArches_color_balance line 496
24. theorem OAI.FKCRT.Inventory.typedRun_of_matchings line 533

    Source documentation

    Complete noncrossing matchings give successful typed inventory reduction, not merely two balanced endpoint counts.

    theorem typedRun_of_matchings (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) :
        stackTypedRun (l.map w) []=some [] := by
    …

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

25. lemma OAI.FKCRT.MapCycles.Arches.increasing line 584
26. def OAI.FKCRT.Inventory.matchingWord line 605

    Source documentation

    The actual two-colour opening/closing word in canonical rooted tour order.

    def matchingWord (a : Perm (Dart n)) (A : Finset (Orbit a)) (i : Dart n) : TypedLetter :=
    …

    Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Inventory.TypedLetter

27. theorem OAI.FKCRT.Inventory.maximal_matching_word line 610

    Source documentation

    Surjectivity of the stack correspondence on canonical two-colour tours, with the complete literal inverse pairing and rotation.

    theorem maximal_matching_word (a : Perm (Dart n)) (ha : Function.Involutive a)
        (hf : ∀ i,a i≠i) (A : Finset (Orbit a))
        (hE : Nat.card (Orbit (partialReversal a ha A*(List.finRange (2*(n+1))).formPerm))=
          Nat.card (Orbit (List.finRange (2*(n+1))).formPerm)+A.card)
        (hF : Nat.card (Orbit (partialReversal a ha Aᶜ*(List.finRange (2*(n+1))).formPerm))=
          Nat.card (Orbit (List.finRange (2*(n+1))).formPerm)+Aᶜ.card) :
        stackTypedRun ((List.finRange (2*(n+1))).map (matchingWord a A)) []=some [] ∧
        ∃ E F,Arches (List.finRange (2*(n+1))) E ∧ Arches (List.finRange (2*(n+1))) F ∧
          (endpoints (E++F)).Perm (List.finRange (2*(n+1))) ∧
          (∀ e∈E,matchingWord a A e.1=.burger true ∧ matchingWord a A e.2=.order true) ∧
          (∀ e∈F,matchingWord a A e.1=.burger false ∧ matchingWord a A e.2=.order false) ∧
          turns (E++F)=a ∧ turns E=partialReversal a ha A := by
    …

    Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.matchingWord