PlanarActivity.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.GraphMerge.reachable_eq_of_adj_eq line 10
def OAI.FKCRT.GraphMerge.componentEquiv line 17
lemma OAI.FKCRT.GraphMerge.sup_edge_reachable_of_reachable line 27
lemma OAI.FKCRT.GraphMerge.card_sup_edge_of_reachable line 42
lemma OAI.FKCRT.GraphMerge.card_sup_edge_of_not_reachable line 50
Source documentation
Adding one edge between distinct components merges precisely those two components, including graphs with other isolated vertices.
```
lemma card_sup_edge_of_not_reachable [Finite V] {u v : V} (h : ¬G.Reachable u v) :
    Nat.card (G⊔SimpleGraph.edge u v).ConnectedComponent+1=Nat.card G.ConnectedComponent := by
…
```
lemma OAI.FKCRT.spanningGraph_insert line 121
def OAI.FKCRT.submapComponents line 163
lemma OAI.FKCRT.components_insert_of_reachable line 166
lemma OAI.FKCRT.components_insert_of_not_reachable line 173
def OAI.FKCRT.submapDefect line 181
Source documentation
The orientable genus defect, on all spanning ribbon subgraphs.
```
def submapDefect (a s : Perm (Dart n)) (ha : Function.Involutive a) (A : Finset (Orbit a)) : ℤ :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.submapDefect_monotone line 185
lemma OAI.FKCRT.submapComponents_empty line 211
lemma OAI.FKCRT.submapDefect_empty line 220
lemma OAI.FKCRT.partialReversal_univ line 225
lemma OAI.FKCRT.submapDefect_univ line 231
theorem OAI.FKCRT.planar_boundary_card line 246
Source documentation
Exact planar spanning-subgraph Euler identity. This derives every subgraph's zero genus from the full-map Euler equality.
```
theorem planar_boundary_card (M : LabelledMap n) (A : Finset (Orbit M.val.1)) :
    Nat.card (Orbit (M.val.2*partialReversal M.val.1 M.property.1 A)) +
      Nat.card (Orbit M.val.2) = 2*submapComponents M.val.1 M.val.2 A+A.card := by
…
```
Mentions: OAI.FKCRT.LabelledMap, OAI.FKCRT.Orbit, OAI.FKCRT.partialReversal, OAI.FKCRT.submapComponents
def OAI.FKCRT.loopPolynomial line 267
Source documentation
The source's map marginal, with its common factor sqrt(q) removed.
```
def loopPolynomial (t : ℝ) (M : RootedMap n) : ℝ :=
…
```
Mentions: OAI.FKCRT.RootedMap
lemma OAI.FKCRT.fkWeight_eq_boundary line 271
theorem OAI.FKCRT.fk_marginal_loopPolynomial line 284
Source documentation
Exact finite FK-to-loop normalization, not an asymptotic equivalence.
```
theorem fk_marginal_loopPolynomial (q : ℝ) (hq : 0 < q) (M : RootedMap n) :
    (∑ A : Finset (Edge M),fkWeight q M A) = Real.sqrt q * loopPolynomial (Real.sqrt q) M := by
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge, OAI.FKCRT.fkWeight, OAI.FKCRT.loopPolynomial
def OAI.FKCRT.residualWeight line 312
Source documentation
Exact FK polynomial of the graph with C contracted and R remaining. Using connected-component counts avoids any relabelling or suppressed-edge convention for the residual multigraph.
```
def residualWeight (t : ℝ) (a s : Perm (Dart n)) (C B : Finset (Orbit a)) : ℝ :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
def OAI.FKCRT.residualPartition line 316
lemma OAI.FKCRT.residualPartition_initial line 319
lemma OAI.FKCRT.residualPartition_terminal line 331
lemma OAI.FKCRT.residualWeight_contract line 335

theorem OAI.FKCRT.residual_delete_contract line 346

Source documentation

A nonloop edge may be deleted or contracted without a multiplicative factor; even in the presence of loops and parallel edges.

theorem residual_delete_contract (t : ℝ) (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R : Finset (Orbit a)) (e : Orbit a) (he : e∉R)
    (hn : ¬(spanningGraph a s (C : Set (Orbit a))).Reachable (orbit s e.out) (orbit s (a e.out))) :
    residualPartition t a s C (insert e R)=
      residualPartition t a s C R+residualPartition t a s (insert e C) R := by
…

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

lemma OAI.FKCRT.residualWeight_loop line 358

theorem OAI.FKCRT.residual_loop line 371

Source documentation

A loop has precisely the source factor 1+t.

theorem residual_loop (t : ℝ) (ht : t≠0) (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R : Finset (Orbit a)) (e : Orbit a) (he : e∉R)
    (hl : (spanningGraph a s (C : Set (Orbit a))).Reachable (orbit s e.out) (orbit s (a e.out))) :
    residualPartition t a s C (insert e R)=(1+t)*residualPartition t a s C R := by
…

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

lemma OAI.FKCRT.residual_bridge_pair line 386

theorem OAI.FKCRT.residual_bridge line 414

Source documentation

A bridge has precisely the source factor 1+t; no residual-map isomorphism or unproved rank axiom is used.

theorem residual_bridge (t : ℝ) (ht : t≠0) (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (C R : Finset (Orbit a)) (e : Orbit a) (he : e∉R)
    (hb : ¬(spanningGraph a s ((C∪R : Finset (Orbit a)) : Set (Orbit a))).Reachable
      (orbit s e.out) (orbit s (a e.out))) :
    residualPartition t a s C (insert e R)=(1+t)*residualPartition t a s (insert e C) R := by
…

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

def OAI.FKCRT.Multiforest line 434
lemma OAI.FKCRT.Multiforest.mono line 439
lemma OAI.FKCRT.multiforest_of_tour line 443
lemma OAI.FKCRT.Multiforest.insert_not_reachable line 454
theorem OAI.FKCRT.Multiforest.components_card line 470
Source documentation
The usual forest rank identity includes isolated vertices and does not silently identify parallel map edges.
```
theorem Multiforest.components_card {a s : Perm (Dart n)} (ha : Function.Involutive a)
    {A : Finset (Orbit a)} (h : Multiforest a s A) :
    submapComponents a s A+A.card=Nat.card (Orbit s) := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.submapComponents
theorem OAI.FKCRT.Multiforest.sameCycle_iff_reachable line 484
Source documentation
Every component of a forest has one boundary cycle. Converse to the always-valid implication from a boundary cycle to graph reachability.
```
theorem Multiforest.sameCycle_iff_reachable {a s : Perm (Dart n)} (ha : Function.Involutive a)
    {A : Finset (Orbit a)} (h : Multiforest a s A) (d e : Dart n) :
    (s*partialReversal a ha A).SameCycle d e ↔
      (spanningGraph a s (A : Set (Orbit a))).Reachable (orbit s d) (orbit s e) := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.partialReversal, OAI.FKCRT.spanningGraph, OAI.FKCRT.orbit
lemma OAI.FKCRT.spanningGraph_edge_reachable line 520
lemma OAI.FKCRT.Multiforest.insert line 530

lemma OAI.FKCRT.spanningGraph_connected_erase line 561

Source documentation

The residual graph stays connected when an edge whose endpoints are already connected is removed.

lemma spanningGraph_connected_erase (a s : Perm (Dart n)) (ha : Function.Involutive a)
    (A : Finset (Orbit a)) (e : Orbit a)
    (hc : (spanningGraph a s ((insert e A : Finset (Orbit a)) : Set (Orbit a))).Connected)
    (hr : (spanningGraph a s (A : Set (Orbit a))).Reachable (orbit s e.out) (orbit s (a e.out))) :
    (spanningGraph a s (A : Set (Orbit a))).Connected := by
…

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

def OAI.FKCRT.treeExtensions line 572
Source documentation
Genuine multigraph spanning-tree completions of a partial exploration.
```
def treeExtensions (a s : Perm (Dart n)) (C R : Finset (Orbit a)) : Finset (Finset (Orbit a)) := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
lemma OAI.FKCRT.mem_treeExtensions line 577
lemma OAI.FKCRT.treeExtensions_terminal line 582
lemma OAI.FKCRT.treeExtensions_split line 592
lemma OAI.FKCRT.treeExtensions_loop line 620
lemma OAI.FKCRT.treeExtensions_bridge line 635
abbrev OAI.FKCRT.EdgeSelector line 655
def OAI.FKCRT.explorationActivity line 660
Source documentation
Number of forced bridge/loop decisions along the branch belonging to T. The next edge may depend on the entire previous partial branch, but not T.
```
def explorationActivity (a s : Perm (Dart n)) (select : EdgeSelector a)
    (C R T : Finset (Orbit a)) : ℕ → ℕ
  | 0 => 0
  | k+1 => if hR : R.Nonempty then
      let e := (select C R hR).val
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.EdgeSelector, OAI.FKCRT.Orbit
lemma OAI.FKCRT.explorationActivity_empty line 674
theorem OAI.FKCRT.adaptive_activity_expansion line 681
Source documentation
The source deletion/contraction expansion is valid for arbitrary history-dependent edge selection. It counts every genuine spanning tree once, including bridge/loop degeneracies. No activity expansion is assumed.
```
theorem adaptive_activity_expansion (t : ℝ) (ht : t≠0)
    (a s : Perm (Dart n)) (ha : Function.Involutive a) (select : EdgeSelector a)
    (k : ℕ) (C R : Finset (Orbit a)) (hk : R.card≤k)
    (hd : Disjoint C R) (hf : Multiforest a s C)
    (hc : (spanningGraph a s ((C∪R : Finset (Orbit a)) : Set (Orbit a))).Connected) :
    residualPartition t a s C R =
      ∑ T∈treeExtensions a s C R,(1+t)^explorationActivity a s select C R T k := by
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.EdgeSelector, OAI.FKCRT.Orbit, OAI.FKCRT.Multiforest, OAI.FKCRT.spanningGraph, OAI.FKCRT.residualPartition, OAI.FKCRT.treeExtensions, OAI.FKCRT.explorationActivity