English
The ramification index can be characterized as the least n for which a certain comparison holds; equal to Nat.find under an appropriate predicate.
Русский
Индекс рамификации равен наименьшему n, удовлетворяющему неким условиям сравнения; равен Nat.find под подходящим предикатом.
LaTeX
$$$ramificationIdx f p P = Nat.find h$$$
Lean4
theorem ramificationIdx_spec {n : ℕ} (hle : map f p ≤ P ^ n) (hgt : ¬map f p ≤ P ^ (n + 1)) :
ramificationIdx f p P = n := by
classical
let Q : ℕ → Prop := fun m => ∀ k : ℕ, map f p ≤ P ^ k → k ≤ m
have : Q n := by
intro k hk
refine le_of_not_gt fun hnk => ?_
exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
rw [ramificationIdx_eq_find ⟨n, this⟩]
refine le_antisymm (Nat.find_min' _ this) (le_of_not_gt fun h : Nat.find _ < n => ?_)
obtain this' := Nat.find_spec ⟨n, this⟩
exact h.not_ge (this' _ hle)
