BallWeights.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The independent-pair bounds, including the equality exception, used by manuscript Lemma finite:ball-bounds.

theorem OAI.CycleClique.Construction.independent_pair_of_not_clique line 14
theorem OAI.CycleClique.Construction.independent_pair_of_card_gt_cliqueNum line 23
theorem OAI.CycleClique.Construction.outsideBall_initial_pair line 33
Source documentation
At radius zero, equality with the maximum clique size already forces a pair, because every vertex of the ball sees its base.
```
theorem outsideBall_initial_pair {X : Finset V} {x : V} {t : ℕ}
    (hx : x ∈ X) (ht : G.cliqueNum ≤ t)
    (hcard : t ≤ (outsideBallFinset G X x 0).card) :
    HasIndependent (G.induce (outsideBallFinset G X x 0 : Set V)) 2 := by
…
```
Mentions: OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.HasIndependent

theorem OAI.CycleClique.Construction.outsideBall_exception_pair line 55

Source documentation

The equality exception does not need any extra Hamiltonicity input. If two successive balls could be the same maximum clique, singleton expansion would force every vertex of that clique to see its base.

theorem outsideBall_exception_pair {X A : Finset V} {x : V} {r k t : ℕ}
    (hx : x ∈ X) (hAX : A ⊆ X) (hxA : x ∉ A)
    (ht : G.cliqueNum ≤ t)
    (hprev : t ≤ (outsideBallFinset G X x r).card)
    (hnum : X.card + t ≤ k + 1 + A.card)
    (hexpand : ∀ v, k + 1 ≤ (closedNeighborhood G {v}).card)
    (hforbid : ∀ y ∈ A, ∀ d, 1 ≤ d → d ≤ r + 1 →
      ¬ PositiveOutsidePath G (X : Set V) x y d) :
    HasIndependent (G.induce (outsideBallFinset G X x (r + 1) : Set V)) 2 := by
…

Mentions: OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.closedNeighborhood, OAI.CycleClique.Construction.PositiveOutsidePath, OAI.CycleClique.Construction.HasIndependent