BallRecurrence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The numerical size/weight recurrence of finite:ball-bounds. Negative size lower bounds may be truncated to zero, because a radius-zero option is used only when its lower bound is positive.

def OAI.CycleClique.Construction.nextBallSize line 11
def OAI.CycleClique.Construction.ordinaryBallWeight line 13
def OAI.CycleClique.Construction.nextBallWeight line 16
theorem OAI.CycleClique.Construction.outsideBall_initial_bounds line 23
theorem OAI.CycleClique.Construction.outsideBall_growth_of_weight line 40

theorem OAI.CycleClique.Construction.outsideBall_recursive_bounds line 56

Source documentation

One recursive step, retaining the exact strict pair/triple thresholds and the equality exception under the alpha-two Hamiltonicity hypothesis.

theorem outsideBall_recursive_bounds (hCE : CEAlphaTwo)
    {X A : Finset V} {x : V} {r k t b u : ℕ}
    (hk : 5 ≤ k) (ht : 1 ≤ t) (hx : x ∈ X) (hAX : A ⊆ X) (hxA : x ∉ A)
    (hcycle : ¬ HasCycle G (k + 1)) (hclique : G.cliqueNum ≤ t)
    (hbpos : 0 < b) (hb : b ≤ (outsideBallFinset G X x r).card) (hu : 0 < u)
    (hind : HasIndependent (G.induce (outsideBallFinset G X x r : Set V)) u)
    (hexpand : ∀ I : Finset V, G.IsIndepSet (I : Set V) → I.Nonempty →
      k * I.card + 1 ≤ (closedNeighborhood G I).card)
    (hforbid : ∀ y ∈ A, ∀ d, 1 ≤ d → d ≤ r + 1 →
      ¬ PositiveOutsidePath G (X : Set V) x y d) :
    nextBallSize k X.card A.card b u ≤ (outsideBallFinset G X x (r + 1)).card ∧
      HasIndependent (G.induce (outsideBallFinset G X x (r + 1) : Set V))
…

Mentions: OAI.CycleClique.Construction.CEAlphaTwo, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.closedNeighborhood, OAI.CycleClique.Construction.PositiveOutsidePath, OAI.CycleClique.Construction.nextBallSize