English
There exists an index i at which no counterexample to the satellite configuration inequality exists; more precisely, the set of i with the property that no b satisfies a certain covering inequality is nonempty.
Русский
Существует индекс i, для которого не существует контрпримерa к неравенству конфигураций спутников; иначе говоря, множество i с отсутствием подходящего b непусто.
LaTeX
$$$\{i \mid \neg\exists b:\n\; p. c b \notin p.iUnionUpTo i \land p.R i \le p.τ \cdot p.r b\}\not= \emptyset.$$$
Lean4
theorem lastStep_nonempty : {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty :=
by
by_contra h
suffices H : Function.Injective p.index from not_injective_of_ordinal p.index H
intro x y hxy
wlog x_le_y : x ≤ y generalizing x y
· exact (this hxy.symm (le_of_not_ge x_le_y)).symm
rcases eq_or_lt_of_le x_le_y with (rfl | H); · rfl
simp only [nonempty_def, not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq, not_forall] at h
specialize h y
have A : p.c (p.index y) ∉ p.iUnionUpTo y :=
by
have : p.index y = Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
rw [TauPackage.index]; rfl
rw [this]
exact (Classical.epsilon_spec h).1
simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and, Subtype.exists] at A
specialize A x H
replace A : p.r (p.index y) ≤ 0 := by simpa [hxy] using A
exact (lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim
