English
A refined induction principle for the IsPos predicate along additive combinations of roots.
Русский
Усовершенствованная индукционная формула для IsPos вдоль сумм корней.
LaTeX
$$RootPairing.Base.IsPos.induction_on_add$$
Lean4
theorem induction_on_add {i : ι} (h₀ : b.IsPos i) {p : ι → Prop} (h₁ : ∀ i ∈ b.support, p i)
(h₂ : ∀ i j k, P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) : p i :=
by
generalize hN : b.height i = N
induction N using Int.induction_on generalizing i with
| zero => exact False.elim <| b.height_ne_zero i hN
| succ n ih =>
obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
rw [P.zero_lt_pairingIn_iff'] at hj'
rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij
have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; omega
have hkpos : b.IsPos k := by rw [isPos_iff']; omega
exact h₂ k j i (by rw [hk]; module) (ih hkpos hkn) hj
| pred n ih =>
rw [isPos_iff] at h₀
cutsat
