CanonicalBijection.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.sameCycle_edge_out line 14
lemma OAI.FKCRT.orbit_opener_injective line 21

theorem OAI.FKCRT.fundamentalCross_tree_chord line 33

Source documentation

Exact fundamental-cut incidence for a selected tree edge in canonical rooted tour order. All representative choices have been removed.

theorem fundamentalCross_tree_chord (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (T : Finset (Orbit a)) (hT : Multiforest a s T)
    (ht : s*partialReversal a ha T=(List.finRange (2*(n+1))).formPerm)
    (x y : Opener a) (hx : orbit a x.val∈T) (hne : x≠y) :
    FundamentalCross a s T (orbit a x.val) (orbit a y.val) ↔ Cross a x y := by
…

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

theorem OAI.FKCRT.fundamentalCross_iff_chord line 57

Source documentation

In a genuine planar two-colour canonical tour, fundamental incidence is exactly alternating chords. The dual maximal-orbit condition excludes crossings between two non-tree edges.

theorem fundamentalCross_iff_chord (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (T : Finset (Orbit a)) (hT : Multiforest a s T)
    (ht : s*partialReversal a ha T=(List.finRange (2*(n+1))).formPerm)
    (hdual : Nat.card (Orbit (partialReversal a ha Tᶜ*(List.finRange (2*(n+1))).formPerm))=
      Nat.card (Orbit (List.finRange (2*(n+1))).formPerm)+Tᶜ.card)
    (x y : Opener a) (hne : x≠y) :
    FundamentalCross a s T (orbit a x.val) (orbit a y.val) ↔ Cross a x y := by
…

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

def OAI.FKCRT.relabelPerm line 87
lemma OAI.FKCRT.relabelPerm_apply line 89
lemma OAI.FKCRT.relabelPerm_mul line 92
lemma OAI.FKCRT.relabelPerm_involutive line 95
lemma OAI.FKCRT.relabelPerm_no_fixed line 101
def OAI.FKCRT.relabelOrbit line 107
lemma OAI.FKCRT.relabelOrbit_apply line 113
lemma OAI.FKCRT.card_orbit_relabel line 116
def OAI.FKCRT.relabelEdges line 119
lemma OAI.FKCRT.mem_relabelEdges line 122
lemma OAI.FKCRT.card_relabelEdges line 126
lemma OAI.FKCRT.relabelEdges_compl line 129
lemma OAI.FKCRT.partialReversal_relabel line 132
lemma OAI.FKCRT.tourNumbering_relabel line 141
lemma OAI.FKCRT.formPerm_finRange_eq_rotate line 159

theorem OAI.FKCRT.map_tour_identified_word line 170

Source documentation

Every genuine rooted planar map/tree tour has a successful identified inventory word. Its stack inverse is root-isomorphic to the initial map, with both permutation identities (and hence the cyclic seam) literal.

theorem map_tour_identified_word (M : LabelledMap n) (A : Finset (Orbit M.val.1))
    (ht : ∀ d e,(M.val.2*partialReversal M.val.1 M.property.1 A).SameCycle d e) :
    ∃ (r : Perm (Dart n)) (w : Dart n→TypedLetter) (E F : List (Dart n×Dart n)),
      r 0=0 ∧ stackTypedRun ((List.finRange (2*(n+1))).map w) []=some [] ∧
      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) ∧
      (∀ d,M.val.1 (r d)=r (turns (E++F) d)) ∧
      (∀ d,M.val.2 (r d)=r (((List.finRange (2*(n+1))).formPerm*turns E) d)) := by
…

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

lemma OAI.FKCRT.opener_orbit_surjective line 238
def OAI.FKCRT.openerOrbitEquiv line 250
lemma OAI.FKCRT.canonical_tourNumbering line 253
lemma OAI.FKCRT.edgeFirst_canonical line 260

theorem OAI.FKCRT.orderedActive_chord line 276

Source documentation

The ordered fundamental activity of any edge is precisely the absence of a later-first chord crossing.

theorem orderedActive_chord (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (hf : ∀ d,a d≠d) (T : Finset (Orbit a)) (hT : Multiforest a s T)
    (hp : ∀ d e,(s*partialReversal a ha T).SameCycle d e)
    (ht : s*partialReversal a ha T=(List.finRange (2*(n+1))).formPerm)
    (hdual : Nat.card (Orbit (partialReversal a ha Tᶜ*(List.finRange (2*(n+1))).formPerm))=
      Nat.card (Orbit (List.finRange (2*(n+1))).formPerm)+Tᶜ.card)
    (x : Opener a) :
    OrderedActive a s T (edgeFirst a (s*partialReversal a ha T) hp) (orbit a x.val) ↔
      ¬∃ j : Dart n,x.val < j ∧ j < a x.val ∧ a x.val < a j := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.partialReversal, OAI.FKCRT.OrderedActive, OAI.FKCRT.edgeFirst, OAI.FKCRT.orbit

lemma OAI.FKCRT.sum_closers_eq_openers line 304

Source documentation

Counting openers or their matching closers gives the identical activity exponent, including deterministic one-edge cases.

lemma sum_closers_eq_openers (a : Perm (Dart n)) (ha : Function.Involutive a) :
    (∑ i : Dart n,if a i < i ∧ ¬∃ j : Dart n,a i < j ∧ j < i ∧ i < a j then 1 else 0)=
      ∑ x : Opener a,if ¬∃ j : Dart n,x.val < j ∧ j < a x.val ∧ a x.val < a j then 1 else 0 := by
…

Mentions: OAI.FKCRT.Dart

lemma OAI.FKCRT.canonical_tour_maximal line 331

theorem OAI.FKCRT.canonical_activity_eq_flexible line 358

Source documentation

The actual adaptive FK expansion exponent is the number of flexible closing positions in the true identified word. No weight identity is assumed.

theorem canonical_activity_eq_flexible (M : LabelledMap n) (T : Finset (Orbit M.val.1))
    (hT : T∈treeExtensions M.val.1 M.val.2 ∅ Finset.univ)
    (ht : M.val.2*partialReversal M.val.1 M.property.1 T=(List.finRange (2*(n+1))).formPerm) :
    explorationActivity M.val.1 M.val.2 (tourSelector M.val.1 M.val.2 M.property.1)
      ∅ Finset.univ T (Fintype.card (Orbit M.val.1))=
      flexibleCount (List.ofFn (matchingWord M.val.1 T)) [] := by
…

Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.partialReversal, OAI.FKCRT.explorationActivity, OAI.FKCRT.tourSelector

structure OAI.FKCRT.CanonicalTreeMap line 407
Source documentation
Literal rooted-tour normal form, not a map with an assumed word inverse.
```
structure CanonicalTreeMap (n : ℕ) where
…
```
abbrev OAI.FKCRT.SuccessfulWord line 414
def OAI.FKCRT.CanonicalTreeMap.word line 417
lemma OAI.FKCRT.matchingWord_color line 422
lemma OAI.FKCRT.matchingWord_set_injective line 427
lemma OAI.FKCRT.CanonicalTreeMap.word_injective line 438
lemma OAI.FKCRT.matchingWord_of_matchings line 463
lemma OAI.FKCRT.CanonicalTreeMap.word_surjective line 490
def OAI.FKCRT.canonicalWordEquiv line 505
Source documentation
Exact finite bimapping of the genuine canonical rooted planar tree maps and successful typed words; no symmetry divisor and no assumed inverse.
```
def canonicalWordEquiv (n : ℕ) : CanonicalTreeMap n ≃ SuccessfulWord n :=
…
```
Mentions: OAI.FKCRT.CanonicalTreeMap, OAI.FKCRT.SuccessfulWord