MapEncoding.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

The exact edge-reversal tour of the rotation-system maps.

lemma OAI.FKCRT.orbit_eq_iff line 11
lemma OAI.FKCRT.orbit_perm line 14
lemma OAI.FKCRT.closed_of_sameCycle line 19
lemma OAI.FKCRT.connected_dart_induction line 31
Source documentation
Graph connectivity propagates a dart property through the two generating permutations. This is the precise permutation form of connected rooted-map rigidity, including loops and repeated edges.
```
lemma connected_dart_induction {n : ℕ} {a s : Equiv.Perm (Dart n)}
    (ha : Function.Involutive a) (hc : (spanningGraph a s univ).Connected)
    {P : Dart n → Prop} {d₀ : Dart n} (h₀ : P d₀)
    (haP : ∀ d,P d → P (a d)) (hsP : ∀ d,P d → P (s d)) : ∀ d,P d := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.spanningGraph
lemma OAI.FKCRT.MapIso.refl line 53
lemma OAI.FKCRT.MapIso.symm line 56
lemma OAI.FKCRT.MapIso.trans line 67
lemma OAI.FKCRT.mapIso_eqvGen line 78
lemma OAI.FKCRT.rooted_automorphism_eq_one line 91
Source documentation
A rooted connected rotation system has no nontrivial automorphisms. Consequently the source's distinguished corners carry no symmetry divisor.
```
lemma rooted_automorphism_eq_one {n : ℕ} (M : LabelledMap n) (r : Equiv.Perm (Dart n))
    (h₀ : r 0=0) (ha : ∀ d,M.val.1 (r d)=r (M.val.1 d))
    (hs : ∀ d,M.val.2 (r d)=r (M.val.2 d)) : r=1 := by
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Dart
lemma OAI.FKCRT.root_isomorphism_unique line 102
abbrev OAI.FKCRT.MapFinite.CycleQuot line 136
instance OAI.FKCRT.MapFinite.(instance at line 138) line 138
lemma OAI.FKCRT.MapFinite.sameCycle_involution line 140
lemma OAI.FKCRT.MapFinite.mk_eq_iff_involution line 160
lemma OAI.FKCRT.MapFinite.card_orbit_fiber line 169
lemma OAI.FKCRT.MapFinite.fixed_out_iff line 185
def OAI.FKCRT.MapFinite.fixedOrbitEquiv line 195
lemma OAI.FKCRT.MapFinite.twice_card_orbits line 211
Source documentation
Orbit count for an involution, retaining its fixed points. A reversal has no fixed darts, whereas the path-map vertex rotation has exactly two.
```
lemma twice_card_orbits {α : Type*} [Fintype α] (s : Equiv.Perm α)
    (hs : Function.Involutive s) :
    2*Fintype.card (CycleQuot s)=Fintype.card α+Fintype.card {d : α // s d=d} := by
…
```
Mentions: OAI.FKCRT.MapFinite.CycleQuot
lemma OAI.FKCRT.spanningGraph_reachable_reversal line 236
lemma OAI.FKCRT.spanningGraph_connected_of_face_cycle line 244
def OAI.FKCRT.pathRotation line 260
lemma OAI.FKCRT.pathRotation_val line 262
lemma OAI.FKCRT.pathRotation_involutive line 273
lemma OAI.FKCRT.pathRotation_fixed line 280
lemma OAI.FKCRT.pathRotation_fixed_card line 285
lemma OAI.FKCRT.pathRotation_orbits line 298
lemma OAI.FKCRT.rotate_sameCycle line 306
lemma OAI.FKCRT.pathRotation_face line 315
lemma OAI.FKCRT.rotate_orbits line 319
def OAI.FKCRT.pathLabelledMap line 328
Source documentation
A concrete genus-zero path map with every positive edge size.
```
def pathLabelledMap (n : ℕ) : LabelledMap n := ⟨(Fin.revPerm,pathRotation n),by
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.pathRotation
instance OAI.FKCRT.rootedMap_nonempty line 341
lemma OAI.FKCRT.partition_pos line 343
lemma OAI.FKCRT.partial_involutive line 367
def OAI.FKCRT.partialReversal line 377
lemma OAI.FKCRT.partialReversal_apply line 382
lemma OAI.FKCRT.partialReversal_involutive line 386
lemma OAI.FKCRT.partialReversal_empty line 390
lemma OAI.FKCRT.partialReversal_self line 396
lemma OAI.FKCRT.partialReversal_compl line 402
lemma OAI.FKCRT.partialReversal_insert line 412
lemma OAI.FKCRT.card_orbit_mul_swap_le line 435
lemma OAI.FKCRT.card_orbit_partialReversal_le line 440
lemma OAI.FKCRT.card_orbit_eq_one_iff line 451
lemma OAI.FKCRT.spanningGraph_reachable_partial line 464
lemma OAI.FKCRT.spanningGraph_connected_of_tour line 476
lemma OAI.FKCRT.reversal_card line 494
theorem OAI.FKCRT.tour_edge_card line 510
Source documentation
A one-cycle tour in a genuine planar map has exactly V-1 chosen edges. The proof uses the Euler equality and the two complementary tour bounds, so loops and parallel edges are fully retained.
```
theorem tour_edge_card (M : LabelledMap n) (A : Finset (Orbit M.val.1))
    (hc : ∀ d e, (M.val.2 * partialReversal M.val.1 M.property.1 A).SameCycle d e) :
    Nat.card (Orbit M.val.2) = A.card + 1 := by
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal
def OAI.FKCRT.edgeEnds line 551
Source documentation
An edge's unordered endpoints; representatives do not change this pair.
```
def edgeEnds (a s : Perm (Dart n)) (e : Orbit a) : Sym2 (Orbit s) :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.edgeEnds_orbit line 554
lemma OAI.FKCRT.spanningGraph_edgeSet_subset line 563
lemma OAI.FKCRT.spanningGraph_card_edgeSet_le line 577
theorem OAI.FKCRT.tour_spanningTree line 589
Source documentation
The selected edges of a one-cycle planar tour form an actual spanning tree of the all-edge graph. There are no suppressed loop/parallel edges in its size: the cardinality equality forces every chosen edge to be distinct and non-loop.
```
theorem tour_spanningTree (M : LabelledMap n) (A : Finset (Orbit M.val.1))
    (hc : ∀ d e, (M.val.2 * partialReversal M.val.1 M.property.1 A).SameCycle d e) :
    (spanningGraph M.val.1 M.val.2 (A : Set (Orbit M.val.1))).IsTree ∧
      Nat.card (spanningGraph M.val.1 M.val.2 (A : Set (Orbit M.val.1))).edgeSet = A.card := by
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.spanningGraph
lemma OAI.FKCRT.card_orbit_mul_comm line 612
lemma OAI.FKCRT.card_orbit_partialReversal_mul_le line 622
lemma OAI.FKCRT.edgeSwap_eq line 628
lemma OAI.FKCRT.partialReversal_insert_orbit line 636

lemma OAI.FKCRT.crossing_two_swaps line 642

Source documentation

Alternating chords first split and then rejoin a tour cycle.

lemma crossing_two_swaps (p : Perm (Dart n)) (x y z w : Dart n)
    (L M N R : List (Dart n))
    (he : MapCycles.orbitList p x = x :: (L ++ y :: (M ++ z :: (N ++ w :: R)))) :
    Nat.card (Orbit (swap y w * (swap x z * p))) = Nat.card (Orbit p) := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.MapCycles.orbitList, OAI.FKCRT.Orbit

theorem OAI.FKCRT.no_crossing_of_maximal_orbits line 687

Source documentation

An orbit-count-maximal matching on a tour has no alternating pair of selected edges. This is the exact combinatorial planarity criterion needed for the two parenthesis families, rather than a topological picture.

theorem no_crossing_of_maximal_orbits (a p : Perm (Dart n)) (ha : Function.Involutive a)
    (A : Finset (Orbit a))
    (hmax : Nat.card (Orbit (partialReversal a ha A * p)) = Nat.card (Orbit p) + A.card)
    (x y : Dart n) (hx : orbit a x ∈ A) (hy : orbit a y ∈ A)
    (hxy : orbit a x ≠ orbit a y) (L M N R : List (Dart n)) :
    MapCycles.orbitList p x ≠ x :: (L ++ y :: (M ++ a x :: (N ++ a y :: R))) := by
…

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

theorem OAI.FKCRT.planar_tour_no_crossing line 727

Source documentation

For every actual planar map and every one-cycle tour, both edge colours are noncrossing in that tour.

theorem planar_tour_no_crossing (M₀ : LabelledMap n) (A : Finset (Orbit M₀.val.1))
    (hc : ∀ d e, (M₀.val.2 * partialReversal M₀.val.1 M₀.property.1 A).SameCycle d e)
    (x y : Dart n) (hx : orbit M₀.val.1 x ∈ A) (hy : orbit M₀.val.1 y ∈ A)
    (hxy : orbit M₀.val.1 x ≠ orbit M₀.val.1 y) (L M N R : List (Dart n)) :
    MapCycles.orbitList (M₀.val.2 * partialReversal M₀.val.1 M₀.property.1 A) x ≠
      x :: (L ++ y :: (M ++ M₀.val.1 x :: (N ++ M₀.val.1 y :: R))) := by
…

Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.Dart, OAI.FKCRT.orbit, OAI.FKCRT.MapCycles.orbitList

lemma OAI.FKCRT.dualRotation_mul line 750
lemma OAI.FKCRT.spanningGraph_dual_connected line 756
def OAI.FKCRT.dualLabelledMap line 777
Source documentation
The combinatorial dual in the dart convention. Choosing the inverse face orientation is unnecessary: this rotation gives the same planar oriented dual after reversing edge darts.
```
def dualLabelledMap (M : LabelledMap n) : LabelledMap n :=
…
```
Mentions: OAI.FKCRT.LabelledMap
lemma OAI.FKCRT.dual_tour line 783
theorem OAI.FKCRT.planar_tour_compl_card line 796

theorem OAI.FKCRT.planar_tour_compl_no_crossing line 806

Source documentation

The non-tree pairs are noncrossing in precisely the same rooted tour order, proved via actual dual rotation systems rather than a disk axiom.

theorem planar_tour_compl_no_crossing (M₀ : LabelledMap n) (A : Finset (Orbit M₀.val.1))
    (hc : ∀ d e, (M₀.val.2 * partialReversal M₀.val.1 M₀.property.1 A).SameCycle d e)
    (x y : Dart n) (hx : orbit M₀.val.1 x ∉ A) (hy : orbit M₀.val.1 y ∉ A)
    (hxy : orbit M₀.val.1 x ≠ orbit M₀.val.1 y) (L M N R : List (Dart n)) :
    MapCycles.orbitList (M₀.val.2 * partialReversal M₀.val.1 M₀.property.1 A) x ≠
      x :: (L ++ y :: (M ++ M₀.val.1 x :: (N ++ M₀.val.1 y :: R))) := by
…

Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.Dart, OAI.FKCRT.orbit, OAI.FKCRT.MapCycles.orbitList

lemma OAI.FKCRT.spanningGraph_mono line 837
lemma OAI.FKCRT.spanningGraph_reachable_of_sameCycle line 845
lemma OAI.FKCRT.spanningGraph_edgeSet_of_card line 858
lemma OAI.FKCRT.spanningGraph_delete_edge_le line 875

theorem OAI.FKCRT.forest_tour_cycle_card line 891

Source documentation

Each chosen forest edge joins two tour cycles, hence the exact cycle count.

theorem forest_tour_cycle_card (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (A : Finset (Orbit a))
    (ht : (spanningGraph a s (A : Set (Orbit a))).IsAcyclic)
    (hn : ∀ e ∈ A, orbit s e.out ≠ orbit s (a e.out))
    (hi : Set.InjOn (edgeEnds a s) (A : Set (Orbit a))) :
    Nat.card (Orbit (s * partialReversal a ha A)) + A.card = Nat.card (Orbit s) := by
…

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

theorem OAI.FKCRT.spanningTree_one_cycle_tour line 934

Source documentation

No suppressed parallel edge or loop is allowed in a multigraph tree; the cardinality condition records precisely this source convention.

theorem spanningTree_one_cycle_tour (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (A : Finset (Orbit a))
    (ht : (spanningGraph a s (A : Set (Orbit a))).IsTree)
    (hc : Nat.card (spanningGraph a s (A : Set (Orbit a))).edgeSet = A.card) :
    ∀ d e, (s * partialReversal a ha A).SameCycle d e := by
…

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

lemma OAI.FKCRT.reconstructed_tour line 966
lemma OAI.FKCRT.reconstructed_face line 971

theorem OAI.FKCRT.reconstruction_conditions line 978

Source documentation

Reconstructing a two-coloured noncrossing tour gives a genuine connected planar map, including the empty-tree and all-loop cases.

theorem reconstruction_conditions (a t : Perm (Dart n)) (ha : Function.Involutive a)
    (hf : ∀ d,a d ≠ d) (A : Finset (Orbit a))
    (ht : ∀ d e,t.SameCycle d e)
    (hv : Nat.card (Orbit (t * partialReversal a ha A)) = A.card+1)
    (hF : Nat.card (Orbit (t * partialReversal a ha Aᶜ)) = Aᶜ.card+1) :
    MapConditions (a,t * partialReversal a ha A) := by
…

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

lemma OAI.FKCRT.reconstruction_inverse line 997
Source documentation
The inverse is literal permutation multiplication, so it retains the cyclic seam and the designated root dart without any quotient choice.
```
lemma reconstruction_inverse (M : LabelledMap n) (A : Finset (Orbit M.val.1)) :
    (M.val.2 * partialReversal M.val.1 M.property.1 A) *
      partialReversal M.val.1 M.property.1 A = M.val.2 :=
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal
theorem OAI.FKCRT.spanningTree_colour_euler line 1005
Source documentation
Both maximum orbit counts follow from a genuine map and any genuine spanning tree. Together with reconstruction this is an algebraic form of the classical tree-rooted-map/two-colour matching correspondence.
```
theorem spanningTree_colour_euler (M : LabelledMap n) (A : Finset (Orbit M.val.1))
    (ht : (spanningGraph M.val.1 M.val.2 (A : Set (Orbit M.val.1))).IsTree)
    (hc : Nat.card (spanningGraph M.val.1 M.val.2 (A : Set (Orbit M.val.1))).edgeSet = A.card) :
    let t := M.val.2 * partialReversal M.val.1 M.property.1 A
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.spanningGraph, OAI.FKCRT.partialReversal
def OAI.FKCRT.matchingEdges line 1036
Source documentation
Edges of the first colour, in the edge-orbit quotient of the complete matching.
```
def matchingEdges (E F : List (Dart n × Dart n)) : Finset (Orbit (turns (E++F))) :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.mem_matchingEdges line 1039
lemma OAI.FKCRT.partialReversal_matchingEdges line 1058
lemma OAI.FKCRT.turns_mul_complete line 1068

theorem OAI.FKCRT.matching_map_conditions line 1083

Source documentation

Two complete noncrossing colour matchings construct an actual planar rotation system in the map model, with no topological assumptions.

theorem matching_map_conditions (E F : List (Dart n × Dart n))
    (hE : Arches (List.finRange (2*(n+1))) E)
    (hF : Arches (List.finRange (2*(n+1))) F)
    (hc : (endpoints (E++F)).Perm (List.finRange (2*(n+1)))) :
    MapConditions (turns (E++F),(List.finRange (2*(n+1))).formPerm * turns E) := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.MapConditions