GraphQuotient.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Sharp level-selection arithmetic for the planar-separator dependency. The profile is the actual number of vertices on each integer BFS level. No planar separator is assumed or concluded here: the bounded-radius geometric step is separate.

lemma OAI.TorsionFreeZeroDivisors.GraphQuotient.reachable line 13
lemma OAI.TorsionFreeZeroDivisors.GraphQuotient.connected line 23
lemma OAI.TorsionFreeZeroDivisors.GraphQuotient.distance_sub line 31
structure OAI.TorsionFreeZeroDivisors.PlanarMap.Model line 60
Source documentation
A concrete finite rotation map, with its exact Euler equality and an isomorphism to the represented simple graph. Loops and parallel darts are allowed; no abstract planar-minor or separator hypotheses are used.
```
structure Model where
…
```
def OAI.TorsionFreeZeroDivisors.PlanarMap.Model.induced line 71

theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.radius_separator line 84

Source documentation

Sharp radius separation transported along the actual graph isomorphism.

theorem Model.radius_separator (M : Model G) (hc : G.Connected) (root : V) (r : ℕ)
    (hr : ∀ v,G.dist root v≤r) (active : Finset V) :
    ∃ cut side : Finset V,root∈cut ∧ cut.card≤2*r+1 ∧ (cut.erase root).card≤2*r ∧
      3*(active.filter (fun v=>v∉cut ∧ v∈side)).card≤2*active.card ∧
      3*(active.filter (fun v=>v∉cut ∧ v∉side)).card≤2*active.card ∧
      ∀ v w,v∉cut→w∉cut→G.Adj v w→(v∈side↔w∈side) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model

structure OAI.TorsionFreeZeroDivisors.PlanarMap.Contraction line 139
def OAI.TorsionFreeZeroDivisors.PlanarMap.Model.contract line 154
Source documentation
A connected induced set is contracted by choosing its literal spanning submatching and replacing the rotations by the contour permutation.
```
def Model.contract (M : Model G) (hB : (G.induce B).Connected) : Contraction G B := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model, OAI.TorsionFreeZeroDivisors.PlanarMap.Contraction
theorem OAI.TorsionFreeZeroDivisors.CutTransfer.pullback line 197

theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.annular_separator line 258

Source documentation

Root-saving radius separation after literal connected lower-ball contraction. Only vertices of active are charged or retained.

theorem Model.annular_separator (M : Model G) (hc : G.Connected) (root : V)
    (lo hi : ℕ) (active : Finset V)
    (hA : ∀ v∈active,lo<G.dist v root ∧ G.dist v root≤hi) :
    ∃ cut side : Finset V,cut⊆active ∧ cut.card≤2*(hi-lo) ∧
      3*(active.filter (fun v=>v∉cut ∧ v∈side)).card≤2*active.card ∧
      3*(active.filter (fun v=>v∉cut ∧ v∉side)).card≤2*active.card ∧
      ∀ v∈active,∀ w∈active,v∉cut→w∉cut→G.Adj v w→(v∈side↔w∈side) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model

theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.ball_separator line 314

Source documentation

The uncontracted alternative, needed when the selected lower level is negative. Its extra root vertex fits strictly within the level-gap budget.

theorem Model.ball_separator (M : Model G) (hc : G.Connected) (root : V)
    (hi : ℕ) (active : Finset V) (hA : ∀ v∈active,G.dist v root≤hi) :
    ∃ cut side : Finset V,cut⊆active ∧ cut.card≤2*hi+1 ∧
      3*(active.filter (fun v=>v∉cut ∧ v∈side)).card≤2*active.card ∧
      3*(active.filter (fun v=>v∉cut ∧ v∉side)).card≤2*active.card ∧
      ∀ v∈active,∀ w∈active,v∉cut→w∉cut→G.Adj v w→(v∈side↔w∈side) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model

theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.twice_sum_succ line 352

theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.triangular_bound line 359

Source documentation

The exact discrete triangle under a minimum level cost.

theorem triangular_bound (m : ℕ) (c : ℕ → ℕ)
    (hc : ∀ k < m/2, m ≤ c k + 2*(k+1)) :
    m^2 ≤ 4*(∑ k ∈ Finset.range (m/2), c k) + 2*m := by
…

theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.exists_minimum line 372
theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.select line 383
Source documentation
A nonnegative integer profile with total mass at most N has two levels whose combined width plus twice their separation is at most sqrt(8*N). The center level is counted only once in the mass estimate.
```
theorem select (a : ℤ → ℕ) (N : ℕ) (center : ℤ)
    (mass : ∀ s : Finset ℤ, ∑ z ∈ s,a z ≤ N) :
    ∃ kL kR : ℕ,
      (a (center-kL) + a (center+kR) + 2*(kL+kR) : ℝ) ≤
        2*Real.sqrt 2*Real.sqrt N := by
…
```