TourActivity.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.oneCycle_isCycleOn line 11
lemma OAI.FKCRT.oneCycle_numbering_bijective line 15
def OAI.FKCRT.tourNumbering line 31
Source documentation
Tour positions with initial position the original root dart.
```
def tourNumbering (p : Perm (Dart n)) (h : ∀ d e,p.SameCycle d e) : Perm (Dart n) :=
…
```
Mentions: OAI.FKCRT.Dart
lemma OAI.FKCRT.tourNumbering_apply line 34
lemma OAI.FKCRT.tourNumbering_zero line 37
lemma OAI.FKCRT.tourNumbering_successor line 40

lemma OAI.FKCRT.tourNumbering_unique line 54

Source documentation

The root-preserving numbering is uniquely determined by the tour.

lemma tourNumbering_unique (p : Perm (Dart n)) (h : ∀ d e,p.SameCycle d e)
    (r : Perm (Dart n)) (hr : r 0=0)
    (hp : ∀ i,r (finRotate (2*(n+1)) i)=p (r i)) : r=tourNumbering p h := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.tourNumbering

def OAI.FKCRT.tourSelector line 87
Source documentation
Source exploration: start at the root and follow decided tree/non-tree rules until the first as-yet undecided edge. The fallback is only for states without a spanning-tree completion; it is never used on a valid branch.
```
def tourSelector (a s : Perm (Dart n)) (ha : Function.Involutive a) : EdgeSelector a := fun C R hR =>
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.EdgeSelector
lemma OAI.FKCRT.partial_tour_eq_outside line 92
lemma OAI.FKCRT.partial_tour_prefix line 101

theorem OAI.FKCRT.tourSelector_first line 113

Source documentation

The next chosen edge is exactly the first undecided edge of every completed tree tour. In particular it depends only on previous choices.

theorem tourSelector_first (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R T : Finset (Orbit a)) (hR : R.Nonempty) (hC : C⊆T) (hT : T⊆C∪R)
    (ht : ∀ d e,(s*partialReversal a ha T).SameCycle d e) :
    ∃ k : ℕ, orbit a (((s*partialReversal a ha T)^k) 0)=(tourSelector a s ha C R hR).val ∧
      orbit a (((s*partialReversal a ha T)^k) 0)∈R ∧
      ∀ j<k,orbit a (((s*partialReversal a ha T)^j) 0)∉R := by
…

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

lemma OAI.FKCRT.treeExtension_tour line 139

theorem OAI.FKCRT.loopPolynomial_tour_activity line 147

Source documentation

Exact rooted-tour adaptive expansion of the finite FK loop polynomial.

theorem loopPolynomial_tour_activity (t : ℝ) (ht : t≠0) (M : RootedMap n) :
    loopPolynomial t M = ∑ T∈treeExtensions (reversal M) (rotation M) ∅ Finset.univ,
      (1+t)^explorationActivity (reversal M) (rotation M)
        (tourSelector (reversal M) (rotation M) M.out.property.1) ∅ Finset.univ T (n+1) := by
…

Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.loopPolynomial, OAI.FKCRT.treeExtensions, OAI.FKCRT.reversal, OAI.FKCRT.rotation, OAI.FKCRT.explorationActivity, OAI.FKCRT.tourSelector

lemma OAI.FKCRT.Multiforest.edgeEnds_mem_iff line 181

theorem OAI.FKCRT.Multiforest.reachable_iff_all_cuts line 198

Source documentation

A subtree connects two vertices precisely when it retains every edge of their unique tree path, expressed without choosing that path.

theorem Multiforest.reachable_iff_all_cuts {a s : Perm (Dart n)} (ha : Function.Involutive a)
    {C T : Finset (Orbit a)} (h : Multiforest a s T) (hC : C⊆T)
    (hc : (spanningGraph a s (T : Set (Orbit a))).Connected) (u v : Orbit s) :
    (spanningGraph a s (C : Set (Orbit a))).Reachable u v ↔
      ∀ e∈T, e∉C → (spanningGraph a s ((T.erase e : Finset (Orbit a)) : Set (Orbit a))).Reachable u v := by
…

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

lemma OAI.FKCRT.spanningGraph_reachable_mono_relation line 237
lemma OAI.FKCRT.Multiforest.erase_components_two line 251
lemma OAI.FKCRT.Multiforest.erase_component_dichotomy line 264

theorem OAI.FKCRT.Multiforest.residual_bridge_iff line 286

Source documentation

A residual edge is a bridge exactly when no retained edge crosses its fundamental tree cut. No simplicity assumption on the original map.

theorem Multiforest.residual_bridge_iff {a s : Perm (Dart n)} (ha : Function.Involutive a)
    {T B : Finset (Orbit a)} (h : Multiforest a s T)
    (hc : (spanningGraph a s (T : Set (Orbit a))).Connected) {e : Orbit a} (he : e∈T)
    (hB : T.erase e⊆B) :
    ¬(spanningGraph a s (B : Set (Orbit a))).Reachable (orbit s e.out) (orbit s (a e.out)) ↔
      ∀ f∈B,(spanningGraph a s ((T.erase e : Finset (Orbit a)) : Set (Orbit a))).Reachable
        (orbit s f.out) (orbit s (a f.out)) := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.spanningGraph, OAI.FKCRT.orbit

def OAI.FKCRT.FundamentalCross line 321
Source documentation
Symmetric fundamental-cut incidence. For distinct edges of a planar tree tour this is precisely alternation of their two darts.
```
def FundamentalCross (a s : Perm (Dart n)) (T : Finset (Orbit a)) (e f : Orbit a) : Prop :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.fundamentalCross_symm line 327
lemma OAI.FKCRT.fundamentalCross_tree line 330
lemma OAI.FKCRT.fundamentalCross_nontree line 341

theorem OAI.FKCRT.treeExtension_loop_iff_no_cross line 349

Source documentation

Exact non-tree forced-loop condition, in terms of the undecided edges.

theorem treeExtension_loop_iff_no_cross (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R T : Finset (Orbit a)) (hT : T∈treeExtensions a s C R) (hd : Disjoint C R)
    {e : Orbit a} (he : e∉T) :
    (spanningGraph a s (C : Set (Orbit a))).Reachable (orbit s e.out) (orbit s (a e.out)) ↔
      ∀ f∈R,¬FundamentalCross a s T e f := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.spanningGraph, OAI.FKCRT.orbit, OAI.FKCRT.FundamentalCross

theorem OAI.FKCRT.treeExtension_bridge_iff_no_cross line 367

Source documentation

Exact tree forced-bridge condition. The contracted/deleted state is the one used by the genuine adaptive FK polynomial recursion.

theorem treeExtension_bridge_iff_no_cross (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R T : Finset (Orbit a)) (hT : T∈treeExtensions a s C R) (hd : Disjoint C R)
    {e : Orbit a} (he : e∈T) (heR : e∈R) :
    ¬(spanningGraph a s ((C∪R.erase e : Finset (Orbit a)) : Set (Orbit a))).Reachable
      (orbit s e.out) (orbit s (a e.out)) ↔
      ∀ f∈R.erase e,¬FundamentalCross a s T e f := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.spanningGraph, OAI.FKCRT.orbit, OAI.FKCRT.FundamentalCross

lemma OAI.FKCRT.fundamental_cut_tour line 395
theorem OAI.FKCRT.fundamentalCross_tour_cut line 405
Source documentation
Fundamental tree cuts are exactly the two cycles obtained by cutting the tour at the two darts of that edge. This is the algebraic contour-cut identity.
```
theorem fundamentalCross_tour_cut (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (T : Finset (Orbit a)) (hT : Multiforest a s T) {e f : Orbit a}
    (he : e∈T) (hne : e≠f) :
    FundamentalCross a s T e f ↔
      ¬((s*partialReversal a ha T)*swap e.out (a e.out)).SameCycle f.out (a f.out) := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.FundamentalCross, OAI.FKCRT.partialReversal
lemma OAI.FKCRT.MapCycles.disjoint_formPerm_action line 423
lemma OAI.FKCRT.MapCycles.disjoint_formPerm_sameCycle line 434
theorem OAI.FKCRT.MapCycles.swap_tour_sameCycle line 458
Source documentation
Cutting a cyclic tour at x,z separates precisely its two contour intervals, including intervals with no interior darts.
```
theorem swap_tour_sameCycle (p : Perm α) (x z : α) (L R : List α)
    (he : orbitList p x=x::(L++z::R)) (hc : ∀ d e,p.SameCycle d e) (y w : α) :
    (swap x z*p).SameCycle y w ↔ (y∈x::L ↔ w∈x::L) := by
…
```
Mentions: OAI.FKCRT.MapCycles.orbitList

theorem OAI.FKCRT.MapCycles.tour_swap_sameCycle line 475

Source documentation

Right and left cuts have the same partition on darts other than the two cut endpoints, which is exactly what is needed for distinct paired edges.

theorem tour_swap_sameCycle (p : Perm α) (x z : α) (L R : List α)
    (he : orbitList p x=x::(L++z::R)) (hc : ∀ d e,p.SameCycle d e)
    (y w : α) (hyx : y≠x) (hyz : y≠z) (hwx : w≠x) (hwz : w≠z) :
    (p*swap x z).SameCycle y w ↔ (y∈L ↔ w∈L) := by
…

Mentions: OAI.FKCRT.MapCycles.orbitList

lemma OAI.FKCRT.MapCycles.ordered_two_sublist line 496
lemma OAI.FKCRT.MapCycles.ordered_middle line 507

theorem OAI.FKCRT.MapCycles.ordered_tour_cut line 529

Source documentation

An ordered cyclic tour, cut at x<z, separates the strict linear interval (x,z) from its complement, on all other darts.

theorem ordered_tour_cut (l : List α) (hs : l.Pairwise (·<·)) (hc : ∀ x,x∈l)
    (x z : α) (hxz : x<z) (y w : α)
    (hyx : y≠x) (hyz : y≠z) (hwx : w≠x) (hwz : w≠z) :
    (l.formPerm*swap x z).SameCycle y w ↔ ((x<y ∧ y<z) ↔ (x<w ∧ w<z)) := by
…

def OAI.FKCRT.edgeFirst line 562
Source documentation
First occurrence of an edge in a fixed rooted one-cycle tour.
```
def edgeFirst (a p : Perm (Dart n)) (hp : ∀ d e,p.SameCycle d e) (e : Orbit a) : ℕ :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.edgeFirst_lt line 565
lemma OAI.FKCRT.edgeFirst_orbit line 569
lemma OAI.FKCRT.edgeFirst_injective line 580
lemma OAI.FKCRT.edgeFirst_le_position line 585

theorem OAI.FKCRT.tourSelector_least line 602

Source documentation

The adaptive tour selector is the least first occurrence in every completed tree tour, with no choice-dependent ordering assumed.

theorem tourSelector_least (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R T : Finset (Orbit a)) (hR : R.Nonempty) (hC : C⊆T) (hT : T⊆C∪R)
    (ht : ∀ d e,(s*partialReversal a ha T).SameCycle d e) :
    ∀ f∈R,edgeFirst a (s*partialReversal a ha T) ht (tourSelector a s ha C R hR).val≤
      edgeFirst a (s*partialReversal a ha T) ht f := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.edgeFirst, OAI.FKCRT.tourSelector

lemma OAI.FKCRT.treeExtension_next line 629
lemma OAI.FKCRT.explorationActivity_step_cross line 650
def OAI.FKCRT.OrderedActive line 700

theorem OAI.FKCRT.explorationActivity_eq_orderedActive line 706

Source documentation

Any increasing adaptive selector counts exactly the active edges of the completed branch. This is an equality for the original forced-choice count.

theorem explorationActivity_eq_orderedActive (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (select : EdgeSelector a) (T : Finset (Orbit a)) (rank : Orbit a→ℕ)
    (hi : Function.Injective rank)
    (hmin : ∀ C R hR, T∈treeExtensions a s C R →
      ∀ f∈R,rank (select C R hR).val≤rank f)
    (k : ℕ) (C R : Finset (Orbit a)) (hk : R.card≤k)
    (hT : T∈treeExtensions a s C R) (hd : Disjoint C R)
    (hsuf : ∀ e∈R,∀ f,rank e<rank f → f∈R) :
    explorationActivity a s select C R T k=(R.filter (OrderedActive a s T rank)).card := by
…

Mentions: OAI.FKCRT.Dart, OAI.FKCRT.EdgeSelector, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.explorationActivity, OAI.FKCRT.OrderedActive

theorem OAI.FKCRT.tourActivity_eq_card line 767
Source documentation
Specialization to the actual rooted-tour selector. Thus the exponent in loopPolynomial_tour_activity is the exact ordered fundamental activity.
```
theorem tourActivity_eq_card (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (T : Finset (Orbit a)) (hT : T∈treeExtensions a s ∅ Finset.univ) :
    explorationActivity a s (tourSelector a s ha) ∅ Finset.univ T (Fintype.card (Orbit a)) =
      (Finset.univ.filter (OrderedActive a s T
        (edgeFirst a (s*partialReversal a ha T) (treeExtension_tour a s ha ∅ Finset.univ T hT)))).card := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.treeExtensions, OAI.FKCRT.explorationActivity, OAI.FKCRT.tourSelector, OAI.FKCRT.OrderedActive, OAI.FKCRT.edgeFirst, OAI.FKCRT.partialReversal, OAI.FKCRT.treeExtension_tour