Finite selection of denominators meeting successive weight thresholds
ProvedOAI.PiExponent.select_separated_denominatorsIf an arbitrary relation admits nonzero integer numerators and denominators at least two with unbounded logarithmic weights, select any prescribed finite number of such pairs. Each weight exceeds a common lower bound and a threshold depending only on previously selected weights. Finite recursive choice proves the assertion. For zero pairs both conclusions are vacuous; no positivity of the common lower bound or any monotonicity of the threshold function is needed.
Preamble
import Definitions.Def_PiExponent_DeterminantSetup
Formal statement
theorem OAI.PiExponent.select_separated_denominators
(R : ℤ → ℕ → Prop)
(hR : ∀ L : ℕ, ∃ (p : ℤ) (q : ℕ),
2 ≤ q ∧ p ≠ 0 ∧ L ≤ Nat.ceil (Real.log (q : ℝ)) ∧ R p q)
(m W : ℕ) (S : List ℕ → ℕ) :
∃ (p : Fin m → ℤ) (q : Fin m → ℕ),
(∀ i : Fin m, 2 ≤ q i ∧ p i ≠ 0 ∧
W ≤ Nat.ceil (Real.log (q i : ℝ)) ∧ R (p i) (q i)) ∧
OAI.PiExponent.separatedWeights S
(fun i : Fin m => Nat.ceil (Real.log (q i : ℝ))) := by sorrySource