Unit pair height cutoff from orders
ProvedD1Bound5.unit_pair_height_cutoff_from_ordersdiophantine-tuplesnumber-theory
The unit-pair cubic iteration and the actual all-order inequalities force the first extension below 10^4. The conditional input merely restricts the analytic estimates to the large regime where they apply.
Preamble
import Mathlib.Algebra.Order.Floor.Semiring import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Tactic
Formal statement
section
namespace D1Bound5
theorem _root_.D1Bound5.unit_pair_height_cutoff_from_orders (S D Z : ℝ)
(hS : 0 < S) (hD : 0 < D) (hZ : 1 ≤ Z) (hprod : S*D < 2*Z^2)
(hgrowth : S^27/8192 < D)
(horders : 10000 ≤ S → ∀ k : ℕ, 1 ≤ k →
1 < 3*S*(42*S)^k/Z+Z/(2*(27*(S-1)^2/64)^k)) : S < 10000 := by sorry
end D1Bound5
end
Source
D1Bound5/UnitPairHeightCutoff.lean, lines 51-72, SHA-256 0c2e2f5d6333fc3971f549ba84e0129a097627670f990f7ead321a035b9be11c. Project: https://github.com/tomislav-math/d1-bound5-lean