diff --git a/FormalConjectures/OEIS/261865.lean b/FormalConjectures/OEIS/261865.lean
new file mode 100644
index 0000000000..eb67c8f581
--- /dev/null
+++ b/FormalConjectures/OEIS/261865.lean
@@ -0,0 +1,51 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjectures.OEIS.«261865Solution»
+
+@[expose] public section
+
+/-!
+# OEIS A261865 / Peter Kagey's Problem 13
+
+For a positive integer `n`, OEIS A261865 is the least positive integer `k`
+for which a positive integer multiple of `√k` lies strictly between `n` and
+`n + 1`.
+
+For every squarefree `j ≥ 2`, the indices where `j` is the least successful
+radicand have density
+
+`(1 / √j) * ∏_{2 ≤ s < j, Squarefree s} (1 - 1 / √s)`.
+-/
+
+namespace OeisA261865
+
+/--
+**Peter Kagey's Problem 13 / OEIS A261865.**
+
+For every squarefree `j ≥ 2`, the set of positive indices where the least
+successful radicand is `j` has the stated natural density.
+
+The mathematical proof and Lean development were produced by
+ProofOrchestrator, using OpenAI GPT-5.6 Thinking, under Dominic Dabish's
+supervision.
+-/
+theorem density_formula (j : ℕ) (hj : 2 ≤ j) (hsq : Squarefree j) :
+    {n : ℕ | 0 < n ∧ IsValue n j}.HasDensity (predictedDensity j) :=
+  density_formula_solution j hj hsq
+
+end OeisA261865
diff --git a/FormalConjectures/OEIS/261865FinalAudit.lean b/FormalConjectures/OEIS/261865FinalAudit.lean
new file mode 100644
index 0000000000..6425a00ba6
--- /dev/null
+++ b/FormalConjectures/OEIS/261865FinalAudit.lean
@@ -0,0 +1,30 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.OEIS.«261865»
+
+namespace OeisA261865
+
+/-- Exact-statement audit wrapper for Peter Kagey's Problem 13 / OEIS A261865. -/
+theorem density_formula_final_audit (j : ℕ) (hj : 2 ≤ j) (hsq : Squarefree j) :
+    {n : ℕ | 0 < n ∧ IsValue n j}.HasDensity (predictedDensity j) :=
+  density_formula j hj hsq
+
+#print axioms density_formula_solution
+#print axioms density_formula
+#print axioms density_formula_final_audit
+
+end OeisA261865
diff --git a/FormalConjectures/OEIS/261865Solution.lean b/FormalConjectures/OEIS/261865Solution.lean
new file mode 100644
index 0000000000..b85a6fa1a7
--- /dev/null
+++ b/FormalConjectures/OEIS/261865Solution.lean
@@ -0,0 +1,160 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjectures.OEIS.A261865Base
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.TerminalBox
+
+@[expose] public section
+
+open Filter
+open scoped BigOperators Topology
+
+namespace OeisA261865
+
+/-- The reciprocal-square-root rotation parameters lie strictly between zero and one. -/
+theorem alpha_pos_of_two_le {s : ℕ} (hs : 2 ≤ s) : 0 < alpha s := by
+  unfold alpha
+  exact one_div_pos.mpr (Real.sqrt_pos.2 (by positivity))
+
+theorem alpha_lt_one_of_two_le {s : ℕ} (hs : 2 ≤ s) : alpha s < 1 := by
+  have hspos : (0 : ℝ) < s := by positivity
+  have hsqrtpos : (0 : ℝ) < Real.sqrt (s : ℝ) := Real.sqrt_pos.2 hspos
+  have hsqrtsq : (Real.sqrt (s : ℝ)) ^ 2 = (s : ℝ) := Real.sq_sqrt hspos.le
+  have hsqrtone : 1 < Real.sqrt (s : ℝ) := by
+    nlinarith [show (2 : ℝ) ≤ s by exact_mod_cast hs]
+  unfold alpha
+  exact (div_lt_one hsqrtpos).2 hsqrtone
+
+/-- The distinguished element `j` as an element of the relevant-radicand subtype. -/
+noncomputable def distinguishedRadicand (j : ℕ) : relevantRadicands j :=
+  ⟨j, by simp⟩
+
+/-- The generic terminal-box event is exactly the A261865 least-radicand event. -/
+theorem orbit_mem_terminalBox_iff (n j : ℕ) (hj : 2 ≤ j) :
+    n • (fun s : relevantRadicands j => (alpha s.1 : UnitAddCircle)) ∈
+        UnitAddTorus.terminalBox (distinguishedRadicand j)
+          (fun s : relevantRadicands j => alpha s.1) ↔
+      0 < n ∧ IsValue n j := by
+  classical
+  have hge : ∀ s : relevantRadicands j, 2 ≤ s.1 := by
+    intro s
+    rcases mem_relevantRadicands.mp s.2 with hsj | hs
+    · simpa [hsj] using hj
+    · exact hs.1
+  have ha0 : ∀ s : relevantRadicands j, 0 < alpha s.1 :=
+    fun s => alpha_pos_of_two_le (hge s)
+  have ha1 : ∀ s : relevantRadicands j, alpha s.1 < 1 :=
+    fun s => alpha_lt_one_of_two_le (hge s)
+  rw [UnitAddTorus.nsmul_mem_terminalBox_iff (distinguishedRadicand j)
+    (fun s : relevantRadicands j => alpha s.1) ha0 ha1 n]
+  constructor
+  · rintro ⟨hjhit, hmiss⟩
+    have hnpos : 0 < n := by
+      by_contra hn
+      have hnzero : n = 0 := Nat.eq_zero_of_not_pos hn
+      subst n
+      norm_num at hjhit
+      linarith [ha1 (distinguishedRadicand j)]
+    refine ⟨hnpos, (isValue_iff_coordinateConditions n j hj).2 ?_⟩
+    refine ⟨by simpa [distinguishedRadicand] using hjhit, ?_⟩
+    intro s hs hcoord
+    let sr : relevantRadicands j :=
+      ⟨s, mem_relevantRadicands.mpr (Or.inr (mem_squarefreeBelow.mp hs))⟩
+    have hne : sr ≠ distinguishedRadicand j := by
+      intro h
+      have : s = j := congrArg Subtype.val h
+      exact (mem_squarefreeBelow.mp hs).2.1.ne this
+    exact hmiss sr hne (by simpa [sr] using hcoord)
+  · rintro ⟨hnpos, hvalue⟩
+    obtain ⟨hjhit, hsmall⟩ := (isValue_iff_coordinateConditions n j hj).1 hvalue
+    refine ⟨by simpa [distinguishedRadicand] using hjhit, ?_⟩
+    intro s hne hcoord
+    have hsne : s.1 ≠ j := by
+      intro h
+      apply hne
+      apply Subtype.ext
+      simpa [distinguishedRadicand] using h
+    have hsbelow : s.1 ∈ squarefreeBelow j := by
+      rcases mem_relevantRadicands.mp s.2 with hs | hs
+      · exact (hsne hs).elim
+      · exact mem_squarefreeBelow.mpr hs
+    exact hsmall s.1 hsbelow (by simpa using hcoord)
+
+/-- The subtype product over all relevant radicands except `j` is the advertised product over
+`squarefreeBelow j`. -/
+theorem product_erase_distinguished (j : ℕ) :
+    ∏ s ∈ (Finset.univ.erase (distinguishedRadicand j)), (1 - alpha s.1) =
+      ∏ s ∈ squarefreeBelow j, (1 - alpha s) := by
+  classical
+  refine Finset.prod_bij (fun s _ => s.1) ?_ ?_ ?_ ?_
+  · intro s hs
+    have hne : s ≠ distinguishedRadicand j := Finset.ne_of_mem_erase hs
+    rcases mem_relevantRadicands.mp s.2 with hsj | hsj
+    · exfalso
+      apply hne
+      apply Subtype.ext
+      simpa [distinguishedRadicand] using hsj
+    · exact mem_squarefreeBelow.mpr hsj
+  · intro a ha b hb hab
+    exact Subtype.ext hab
+  · intro s hs
+    let sr : relevantRadicands j :=
+      ⟨s, mem_relevantRadicands.mpr (Or.inr (mem_squarefreeBelow.mp hs))⟩
+    have hne : sr ≠ distinguishedRadicand j := by
+      intro h
+      have : s = j := congrArg Subtype.val h
+      exact (mem_squarefreeBelow.mp hs).2.1.ne this
+    exact ⟨sr, Finset.mem_erase.mpr ⟨hne, Finset.mem_univ sr⟩, rfl⟩
+  · intro s hs
+    rfl
+
+/-- Axiom-free proof candidate for Peter Kagey's Problem 13 / OEIS A261865. -/
+theorem density_formula_solution (j : ℕ) (hj : 2 ≤ j) (hsq : Squarefree j) :
+    {n : ℕ | 0 < n ∧ IsValue n j}.HasDensity (predictedDensity j) := by
+  classical
+  have hge : ∀ s ∈ relevantRadicands j, 2 ≤ s := by
+    intro s hs
+    rcases mem_relevantRadicands.mp hs with rfl | hs
+    · exact hj
+    · exact hs.1
+  have hsqR : ∀ s ∈ relevantRadicands j, Squarefree s := by
+    intro s hs
+    rcases mem_relevantRadicands.mp hs with rfl | hs
+    · exact hsq
+    · exact hs.2.2
+  have ha0 : ∀ s : relevantRadicands j, 0 < alpha s.1 :=
+    fun s => alpha_pos_of_two_le (hge s.1 s.2)
+  have ha1 : ∀ s : relevantRadicands j, alpha s.1 < 1 :=
+    fun s => alpha_lt_one_of_two_le (hge s.1 s.2)
+  have hrel : UnitAddTorus.NoIntegerRelation
+      (fun s : relevantRadicands j => alpha s.1) :=
+    noIntegerRelation_alpha (relevantRadicands j) hge hsqR
+  have hgeneric := UnitAddTorus.hasDensity_terminalBox
+    (distinguishedRadicand j) (fun s : relevantRadicands j => alpha s.1) ha0 ha1 hrel
+  have hevent :
+      {n : ℕ | n • (fun s : relevantRadicands j => (alpha s.1 : UnitAddCircle)) ∈
+        UnitAddTorus.terminalBox (distinguishedRadicand j)
+          (fun s : relevantRadicands j => alpha s.1)} =
+      {n : ℕ | 0 < n ∧ IsValue n j} := by
+    ext n
+    exact orbit_mem_terminalBox_iff n j hj
+  rw [hevent] at hgeneric
+  convert hgeneric using 1
+  rw [predictedDensity, product_erase_distinguished]
+  rfl
+
+end OeisA261865
diff --git a/FormalConjectures/OEIS/A261865Base.lean b/FormalConjectures/OEIS/A261865Base.lean
new file mode 100644
index 0000000000..655153d177
--- /dev/null
+++ b/FormalConjectures/OEIS/A261865Base.lean
@@ -0,0 +1,296 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddTorus
+public import FormalConjecturesForMathlib.NumberTheory.SquarefreeRadicals
+
+@[expose] public section
+
+/-!
+# OEIS A261865 / Peter Kagey's Problem 13: definitions and reductions
+-/
+
+open Filter
+open scoped BigOperators Topology
+
+namespace OeisA261865
+
+/-- A positive integer multiple of `√k` lies strictly in `(n, n + 1)`. -/
+def Hits (k n : ℕ) : Prop :=
+  ∃ m : ℕ, 0 < m ∧
+    (n : ℝ) < (m : ℝ) * Real.sqrt (k : ℝ) ∧
+      (m : ℝ) * Real.sqrt (k : ℝ) < (n : ℝ) + 1
+
+/-- `k` is the least positive radicand that hits the interval `(n, n + 1)`. -/
+def IsValue (n k : ℕ) : Prop :=
+  0 < k ∧ Hits k n ∧ ∀ r : ℕ, 0 < r → r < k → ¬ Hits r n
+
+/-- The rotation parameter `1 / √s`. -/
+noncomputable def alpha (s : ℕ) : ℝ :=
+  1 / Real.sqrt (s : ℝ)
+
+/-- The fractional-part condition corresponding to `Hits s n`. -/
+def CoordinateHit (s n : ℕ) : Prop :=
+  1 - alpha s < Int.fract ((n : ℝ) * alpha s)
+
+/-- The next positive integer after a nonnegative real `x` lies below `x + a`
+exactly when the fractional part of `x` is greater than `1 - a`. -/
+theorem exists_nat_between_iff_fract {x a : ℝ} (hx : 0 ≤ x) :
+    (∃ m : ℕ, 0 < m ∧ x < (m : ℝ) ∧ (m : ℝ) < x + a) ↔
+      1 - a < Int.fract x := by
+  constructor
+  · rintro ⟨m, _hmpos, hxm, hmx⟩
+    have hfloor_lt : ⌊x⌋ < (m : ℤ) :=
+      Int.floor_lt.mpr (by simpa using hxm)
+    have hnext_le : ⌊x⌋ + 1 ≤ (m : ℤ) := by omega
+    have hnext_le_real : ((⌊x⌋ + 1 : ℤ) : ℝ) ≤ (m : ℝ) := by
+      exact_mod_cast hnext_le
+    have hnext_lt : (⌊x⌋ : ℝ) + 1 < x + a := by
+      exact lt_of_le_of_lt (by simpa using hnext_le_real) hmx
+    have hdecomp := Int.floor_add_fract x
+    linarith
+  · intro hfract
+    have hfloor_nonneg : 0 ≤ ⌊x⌋ := Int.floor_nonneg.mpr hx
+    let m : ℕ := ⌊x⌋.toNat + 1
+    have hmcast : (m : ℝ) = (⌊x⌋ : ℝ) + 1 := by
+      norm_num [m]
+      exact_mod_cast Int.toNat_of_nonneg hfloor_nonneg
+    refine ⟨m, by simp [m], ?_, ?_⟩
+    · rw [hmcast]
+      exact Int.lt_floor_add_one x
+    · rw [hmcast]
+      have hdecomp := Int.floor_add_fract x
+      linarith
+
+/-- The interval-hitting predicate is exactly an irrational-rotation interval. -/
+theorem hits_iff_coordinateHit (s n : ℕ) (hs : 2 ≤ s) :
+    Hits s n ↔ CoordinateHit s n := by
+  have hs_real_pos : (0 : ℝ) < (s : ℝ) := by positivity
+  have hsqrt_pos : (0 : ℝ) < Real.sqrt (s : ℝ) := Real.sqrt_pos.2 hs_real_pos
+  have hx : 0 ≤ (n : ℝ) / Real.sqrt (s : ℝ) :=
+    div_nonneg (by positivity) hsqrt_pos.le
+  constructor
+  · rintro ⟨m, hmpos, hleft, hright⟩
+    have hleft' : (n : ℝ) / Real.sqrt (s : ℝ) < (m : ℝ) :=
+      (div_lt_iff₀ hsqrt_pos).2 hleft
+    have hright' : (m : ℝ) <
+        (n : ℝ) / Real.sqrt (s : ℝ) + 1 / Real.sqrt (s : ℝ) := by
+      have := (lt_div_iff₀ hsqrt_pos).2 hright
+      convert this using 1 <;> ring
+    have hfract := (exists_nat_between_iff_fract hx).mp
+      ⟨m, hmpos, hleft', hright'⟩
+    simpa [CoordinateHit, alpha, div_eq_mul_inv] using hfract
+  · intro hcoord
+    have hfract :
+        1 - 1 / Real.sqrt (s : ℝ) <
+          Int.fract ((n : ℝ) / Real.sqrt (s : ℝ)) := by
+      simpa [CoordinateHit, alpha, div_eq_mul_inv] using hcoord
+    obtain ⟨m, hmpos, hleft, hright⟩ :=
+      (exists_nat_between_iff_fract hx).mpr hfract
+    refine ⟨m, hmpos, (div_lt_iff₀ hsqrt_pos).mp hleft, ?_⟩
+    apply (lt_div_iff₀ hsqrt_pos).mp
+    convert hright using 1 <;> ring
+
+/-- The radicand `1` never hits an open unit interval between consecutive integers. -/
+theorem not_hits_one (n : ℕ) : ¬ Hits 1 n := by
+  rintro ⟨m, _hm, hleft, hright⟩
+  have hnm : n < m := by
+    exact_mod_cast (by simpa using hleft)
+  have hright' : (m : ℝ) < (n : ℝ) + 1 := by simpa using hright
+  have hmn : m ≤ n := by
+    by_contra h
+    have hle : n + 1 ≤ m := by omega
+    have hle' : (n : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast hle
+    linarith
+  omega
+
+/-- Removing a positive square factor from a radicand preserves the hitting property. -/
+theorem hits_square_mul_imp (c s n : ℕ) (hc : 0 < c) :
+    Hits (c ^ 2 * s) n → Hits s n := by
+  rintro ⟨m, hm, hleft, hright⟩
+  have hsqrt :
+      Real.sqrt ((c ^ 2 * s : ℕ) : ℝ) =
+        (c : ℝ) * Real.sqrt (s : ℝ) := by
+    rw [Nat.cast_mul, Nat.cast_pow, Real.sqrt_mul (sq_nonneg (c : ℝ))]
+    rw [Real.sqrt_sq (Nat.cast_nonneg c)]
+  refine ⟨m * c, Nat.mul_pos hm hc, ?_, ?_⟩
+  · calc
+      (n : ℝ) < (m : ℝ) * ((c : ℝ) * Real.sqrt (s : ℝ)) := by
+        rw [← hsqrt]
+        exact hleft
+      _ = ((m * c : ℕ) : ℝ) * Real.sqrt (s : ℝ) := by
+        push_cast
+        ring
+  · calc
+      ((m * c : ℕ) : ℝ) * Real.sqrt (s : ℝ) =
+          (m : ℝ) * ((c : ℝ) * Real.sqrt (s : ℝ)) := by
+            push_cast
+            ring
+      _ < (n : ℝ) + 1 := by
+        rw [← hsqrt]
+        exact hright
+
+/-- Every hit descends to a hit by a positive squarefree radicand no larger than the original. -/
+theorem exists_squarefree_hit_le (r n : ℕ) (hr : 0 < r) (hhit : Hits r n) :
+    ∃ s : ℕ, 0 < s ∧ s ≤ r ∧ Squarefree s ∧ Hits s n := by
+  induction r using Nat.strong_induction_on with
+  | h r ih =>
+      by_cases hsq : Squarefree r
+      · exact ⟨r, hr, le_rfl, hsq, hhit⟩
+      · rcases e : r.minSqFac with _ | d
+        · exact (hsq (Nat.squarefree_iff_minSqFac.mpr e)).elim
+        · have hdprime : d.Prime := Nat.minSqFac_prime e
+          obtain ⟨s, hrs⟩ := Nat.minSqFac_dvd e
+          have hdpos : 0 < d := hdprime.pos
+          have hspos : 0 < s := by
+            apply Nat.pos_of_ne_zero
+            intro hs0
+            have hr0 : r = 0 := by simpa [hs0] using hrs
+            omega
+          have hslt : s < r := by
+            rw [hrs]
+            have hdd : 1 < d * d := by nlinarith [hdprime.two_le]
+            simpa using Nat.mul_lt_mul_of_pos_right hdd hspos
+          have hhit_s : Hits s n := by
+            apply hits_square_mul_imp d s n hdpos
+            simpa [pow_two, hrs] using hhit
+          obtain ⟨t, htpos, htle, htsq, hthit⟩ := ih s hslt hspos hhit_s
+          exact ⟨t, htpos, htle.trans hslt.le, htsq, hthit⟩
+
+/-- The squarefree integers in `[2, j)`. -/
+noncomputable def squarefreeBelow (j : ℕ) : Finset ℕ := by
+  classical
+  exact (Finset.Ico 2 j).filter Squarefree
+
+@[simp] theorem mem_squarefreeBelow {j s : ℕ} :
+    s ∈ squarefreeBelow j ↔ 2 ≤ s ∧ s < j ∧ Squarefree s := by
+  classical
+  simp [squarefreeBelow, and_assoc]
+
+/-- The squarefree radicands relevant to the value `j`, including `j` itself. -/
+noncomputable def relevantRadicands (j : ℕ) : Finset ℕ :=
+  insert j (squarefreeBelow j)
+
+@[simp] theorem mem_relevantRadicands {j s : ℕ} :
+    s ∈ relevantRadicands j ↔ s = j ∨ (2 ≤ s ∧ s < j ∧ Squarefree s) := by
+  classical
+  simp [relevantRadicands]
+
+/-- `j` is the least successful radicand exactly when it hits and every smaller squarefree
+radicand at least two misses. -/
+theorem isValue_iff_squarefree_competitors (n j : ℕ) (hj : 2 ≤ j) :
+    IsValue n j ↔
+      Hits j n ∧ ∀ s ∈ squarefreeBelow j, ¬ Hits s n := by
+  constructor
+  · rintro ⟨_hjpos, hjhit, hminimal⟩
+    refine ⟨hjhit, ?_⟩
+    intro s hs
+    have hs' := mem_squarefreeBelow.mp hs
+    exact hminimal s (lt_of_lt_of_le Nat.zero_lt_two hs'.1) hs'.2.1
+  · rintro ⟨hjhit, hsmall⟩
+    refine ⟨lt_of_lt_of_le Nat.zero_lt_two hj, hjhit, ?_⟩
+    intro r hrpos hrj hrhit
+    obtain ⟨s, hspos, hsr, hssq, hshit⟩ := exists_squarefree_hit_le r n hrpos hrhit
+    have hsne : s ≠ 1 := by
+      intro hs1
+      subst s
+      exact not_hits_one n hshit
+    have hsge : 2 ≤ s := by omega
+    have hslt : s < j := lt_of_le_of_lt hsr hrj
+    exact hsmall s (mem_squarefreeBelow.mpr ⟨hsge, hslt, hssq⟩) hshit
+
+/-- Fractional-part version of `isValue_iff_squarefree_competitors`. -/
+theorem isValue_iff_coordinateConditions (n j : ℕ) (hj : 2 ≤ j) :
+    IsValue n j ↔
+      CoordinateHit j n ∧ ∀ s ∈ squarefreeBelow j, ¬ CoordinateHit s n := by
+  rw [isValue_iff_squarefree_competitors n j hj, hits_iff_coordinateHit j n hj]
+  constructor
+  · rintro ⟨hjhit, hsmall⟩
+    refine ⟨hjhit, ?_⟩
+    intro s hs hscoord
+    have hsge := (mem_squarefreeBelow.mp hs).1
+    exact hsmall s hs ((hits_iff_coordinateHit s n hsge).mpr hscoord)
+  · rintro ⟨hjhit, hsmall⟩
+    refine ⟨hjhit, ?_⟩
+    intro s hs hshit
+    have hsge := (mem_squarefreeBelow.mp hs).1
+    exact hsmall s hs ((hits_iff_coordinateHit s n hsge).mp hshit)
+
+/-- Adjoin the rational coordinate `1` to a finite family of radicands. -/
+def radicandWithOne {S : Finset ℕ} : Option S → ℕ
+  | none => 1
+  | some s => s.1
+
+/-- Reciprocal radicals indexed by distinct squarefree integers at least two have no integer
+relation modulo `1`. -/
+theorem noIntegerRelation_alpha (S : Finset ℕ)
+    (hge : ∀ s ∈ S, 2 ≤ s) (hsq : ∀ s ∈ S, Squarefree s) :
+    UnitAddTorus.NoIntegerRelation (fun s : S => alpha s.1) := by
+  let r : Option S → ℕ := radicandWithOne
+  have hr_sq : ∀ o, Squarefree (r o) := by
+    intro o
+    cases o with
+    | none => simp [r, radicandWithOne]
+    | some s => simpa [r, radicandWithOne] using hsq s.1 s.2
+  have hr_inj : Function.Injective r := by
+    intro o₁ o₂ h
+    cases o₁ with
+    | none =>
+        cases o₂ with
+        | none => rfl
+        | some s =>
+            exfalso
+            have := hge s.1 s.2
+            simp [r, radicandWithOne] at h
+            omega
+    | some s =>
+        cases o₂ with
+        | none =>
+            exfalso
+            have := hge s.1 s.2
+            simp [r, radicandWithOne] at h
+            omega
+        | some t =>
+            apply congrArg some
+            apply Subtype.ext
+            simpa [r, radicandWithOne] using h
+  have hli := Real.linearIndependent_inv_sqrt_squarefree r hr_sq hr_inj
+  intro k hk
+  obtain ⟨z, hz⟩ := hk
+  let c : Option S → ℚ
+    | none => -(z : ℚ)
+    | some s => (k s : ℚ)
+  have hsum :
+      ∑ o, c o • (1 / Real.sqrt (r o : ℝ)) =
+        ∑ o, (0 : ℚ) • (1 / Real.sqrt (r o : ℝ)) := by
+    rw [Fintype.sum_option]
+    simp only [c, r, radicandWithOne, Nat.cast_one, Real.sqrt_one, div_one,
+      Rat.smul_def, Rat.cast_neg, Rat.cast_intCast, neg_mul, mul_one,
+      zero_smul, Finset.sum_const_zero]
+    change -(z : ℝ) + ∑ s : S, (k s : ℝ) * alpha s.1 = 0
+    linarith
+  have hc := (Fintype.linearIndependent_iffₛ.mp hli c (fun _ => 0) hsum)
+  funext s
+  have hs := hc (some s)
+  exact_mod_cast (by simpa [c] using hs)
+
+/-- The density predicted for the value `j` in OEIS A261865. -/
+noncomputable def predictedDensity (j : ℕ) : ℝ :=
+  alpha j * ∏ s ∈ squarefreeBelow j, (1 - alpha s)
+
+end OeisA261865
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/EmpiricalProbability.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/EmpiricalProbability.lean
new file mode 100644
index 0000000000..0d33922423
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/EmpiricalProbability.lean
@@ -0,0 +1,107 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddTorus
+public import Mathlib.MeasureTheory.Measure.Portmanteau
+
+@[expose] public section
+
+/-!
+# Empirical probability measures on a finite torus
+
+This file packages the measure-theoretic bridge used after Weyl's criterion.
+The empirical measure of the first `N + 1` points of a sequence is a genuine
+probability measure, and convergence of all continuous empirical averages
+implies weak convergence of these empirical measures.
+-/
+
+noncomputable section
+
+open Filter MeasureTheory Set Topology
+open scoped BigOperators ENNReal NNReal Topology
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- The uniform empirical probability measure on `Y 0, ..., Y N`. -/
+def empiricalProbability (Y : ℕ → UnitAddTorus d) (N : ℕ) :
+    ProbabilityMeasure (UnitAddTorus d) :=
+  ⟨((N + 1 : ℕ) : ℝ≥0∞)⁻¹ •
+      ∑ n ∈ Finset.range (N + 1), Measure.dirac (Y n), by
+    rw [isProbabilityMeasure_iff]
+    simp [Measure.smul_apply, ENNReal.inv_mul_cancel]⟩
+
+/-- Integrating against the empirical probability measure is the finite
+arithmetic average over the orbit segment. -/
+theorem integral_empiricalProbability (Y : ℕ → UnitAddTorus d) (N : ℕ)
+    (F : C(UnitAddTorus d, ℂ)) :
+    ∫ x, F x ∂(empiricalProbability Y N : Measure (UnitAddTorus d)) =
+      (∑ n ∈ Finset.range (N + 1), F (Y n)) / (N + 1) := by
+  classical
+  rw [empiricalProbability, integral_smul_measure]
+  rw [integral_finset_sum_measure]
+  · simp only [integral_dirac]
+    simp [div_eq_mul_inv, smul_eq_mul, mul_comm]
+  · intro n hn
+    exact integrable_dirac (by simp)
+
+/-- The mass assigned by the empirical probability measure to a measurable
+set is its relative frequency in the orbit segment. -/
+theorem empiricalProbability_apply (Y : ℕ → UnitAddTorus d) (N : ℕ)
+    {s : Set (UnitAddTorus d)} (hs : MeasurableSet s) :
+    (empiricalProbability Y N : Measure (UnitAddTorus d)) s =
+      (((Finset.range (N + 1)).filter fun n => Y n ∈ s).card : ℝ≥0∞) /
+        (N + 1) := by
+  classical
+  simp [empiricalProbability, Measure.smul_apply, hs, div_eq_mul_inv]
+
+/-- If every continuous empirical average converges to its Haar integral,
+then the empirical probability measures converge weakly to Haar measure. -/
+theorem tendsto_empiricalProbability_of_tendsto_average
+    (Y : ℕ → UnitAddTorus d)
+    (havg : ∀ F : C(UnitAddTorus d, ℂ),
+      Tendsto
+        (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / N)
+        atTop
+        (𝓝 (∫ x, F x))) :
+    Tendsto (empiricalProbability Y) atTop
+      (𝓝 (⟨volume, inferInstance⟩ : ProbabilityMeasure (UnitAddTorus d))) := by
+  rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ]
+  intro f
+  let F : C(UnitAddTorus d, ℂ) :=
+    (ContinuousMap.equivBoundedOfCompact (UnitAddTorus d) ℂ).symm f
+  have hsucc : Tendsto (fun N : ℕ => N + 1) atTop atTop := by
+    refine tendsto_atTop.2 fun b => ⟨b, ?_⟩
+    intro a ha
+    exact ha.trans (Nat.le_add_right a 1)
+  have h := (havg F).comp hsucc
+  simpa [integral_empiricalProbability, F] using h
+
+/-- The empirical probability measures of a torus rotation with no integer
+relation converge weakly to Haar probability measure. -/
+theorem tendsto_empiricalProbability_rotation
+    (a : d → ℝ) (ha : NoIntegerRelation a) :
+    Tendsto
+      (empiricalProbability
+        (fun n => n • (fun i => (a i : UnitAddCircle))))
+      atTop
+      (𝓝 (⟨volume, inferInstance⟩ : ProbabilityMeasure (UnitAddTorus d))) :=
+  tendsto_empiricalProbability_of_tendsto_average _
+    (tendsto_average_rotation a ha)
+
+end UnitAddTorus
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/TerminalBox.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/TerminalBox.lean
new file mode 100644
index 0000000000..78fcfcc407
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/TerminalBox.lean
@@ -0,0 +1,172 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddTorus
+public import FormalConjecturesForMathlib.MeasureTheory.Group.UnitAddCircleArc
+public import FormalConjecturesForMathlib.MeasureTheory.Probability.Empirical
+public import FormalConjecturesForMathlib.MeasureTheory.Probability.PiContinuitySet
+
+@[expose] public section
+
+open Filter Set MeasureTheory
+open scoped Topology BigOperators ENNReal NNReal
+
+noncomputable section
+
+namespace UnitAddTorus
+
+variable {ι : Type*} [Fintype ι]
+
+/-- The coordinate event saying that the distinguished coordinate hits its terminal arc and every
+other coordinate misses its terminal arc. -/
+def terminalCoordinateSet [DecidableEq ι] (j : ι) (a : ι → ℝ) (i : ι) :
+    Set UnitAddCircle :=
+  if i = j then UnitAddCircle.terminalArc (a i)
+  else (UnitAddCircle.terminalArc (a i))ᶜ
+
+/-- The corresponding rectangle in the finite unit torus. -/
+def terminalBox [DecidableEq ι] (j : ι) (a : ι → ℝ) : Set (UnitAddTorus ι) :=
+  Set.pi univ (terminalCoordinateSet j a)
+
+/-- Orbit membership in the terminal box is exactly one hit and all other misses. -/
+theorem nsmul_mem_terminalBox_iff [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1) (n : ℕ) :
+    n • (fun i => (a i : UnitAddCircle)) ∈ terminalBox j a ↔
+      (1 - a j < Int.fract ((n : ℝ) * a j) ∧
+        ∀ i, i ≠ j → ¬(1 - a i < Int.fract ((n : ℝ) * a i))) := by
+  classical
+  simp only [terminalBox, Set.mem_pi, Set.mem_univ, forall_true_left,
+    terminalCoordinateSet, Pi.smul_apply]
+  constructor
+  · intro h
+    refine ⟨?_, ?_⟩
+    · have hj := h j
+      simp only [if_pos rfl] at hj
+      exact (UnitAddCircle.nsmul_mem_terminalArc_iff (ha0 j) (ha1 j) n).mp hj
+    · intro i hij hi
+      have hmiss := h i
+      simp only [if_neg hij] at hmiss
+      exact hmiss ((UnitAddCircle.nsmul_mem_terminalArc_iff (ha0 i) (ha1 i) n).mpr hi)
+  · rintro ⟨hj, hother⟩ i
+    by_cases hij : i = j
+    · subst i
+      simp only [if_pos rfl]
+      exact (UnitAddCircle.nsmul_mem_terminalArc_iff (ha0 j) (ha1 j) n).mpr hj
+    · simp only [if_neg hij, Set.mem_compl_iff]
+      intro hi
+      exact hother i hij ((UnitAddCircle.nsmul_mem_terminalArc_iff (ha0 i) (ha1 i) n).mp hi)
+
+/-- The terminal box is measurable. -/
+theorem measurableSet_terminalBox [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) : MeasurableSet (terminalBox j a) := by
+  apply MeasurableSet.univ_pi
+  intro i
+  by_cases h : i = j
+  · simp [terminalCoordinateSet, h, UnitAddCircle.measurableSet_terminalArc]
+  · simp [terminalCoordinateSet, h, UnitAddCircle.measurableSet_terminalArc]
+
+/-- Every coordinate set of the terminal box has null frontier. -/
+theorem volume_frontier_terminalCoordinateSet [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1) (i : ι) :
+    volume (frontier (terminalCoordinateSet j a i)) = 0 := by
+  by_cases h : i = j
+  · subst i
+    simpa [terminalCoordinateSet] using
+      UnitAddCircle.volume_frontier_terminalArc (ha0 j) (ha1 j)
+  · simpa [terminalCoordinateSet, h] using
+      UnitAddCircle.volume_frontier_terminalArc_compl (ha0 i) (ha1 i)
+
+/-- The terminal box is a continuity set for Haar probability measure. -/
+theorem volume_frontier_terminalBox [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1) :
+    volume (frontier (terminalBox j a)) = 0 := by
+  exact measure_frontier_pi_eq_zero (fun _ : ι => (volume : Measure UnitAddCircle))
+    (terminalCoordinateSet j a) (volume_frontier_terminalCoordinateSet j a ha0 ha1)
+
+/-- Haar mass of a terminal coordinate event. -/
+theorem volume_terminalCoordinateSet [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1) (i : ι) :
+    volume (terminalCoordinateSet j a i) =
+      ENNReal.ofReal (if i = j then a i else 1 - a i) := by
+  by_cases h : i = j
+  · subst i
+    simpa [terminalCoordinateSet] using
+      UnitAddCircle.volume_terminalArc (ha0 j) (ha1 j)
+  · simpa [terminalCoordinateSet, h] using
+      UnitAddCircle.volume_terminalArc_compl (ha0 i) (ha1 i)
+
+/-- Haar mass of the terminal box. -/
+theorem volume_terminalBox [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1) :
+    volume (terminalBox j a) =
+      ENNReal.ofReal (a j * ∏ i ∈ (Finset.univ.erase j), (1 - a i)) := by
+  rw [show (volume : Measure (UnitAddTorus ι)) =
+      Measure.pi (fun _ : ι => (volume : Measure UnitAddCircle)) by rfl]
+  rw [terminalBox, Measure.pi_pi]
+  simp_rw [volume_terminalCoordinateSet j a ha0 ha1]
+  rw [← ENNReal.ofReal_prod_of_nonneg]
+  · congr 1
+    calc
+      (∏ i, if i = j then a i else 1 - a i) =
+          (if j = j then a j else 1 - a j) *
+            ∏ i ∈ Finset.univ.erase j, (if i = j then a i else 1 - a i) := by
+        exact (Finset.mul_prod_erase Finset.univ
+          (fun i => if i = j then a i else 1 - a i) (Finset.mem_univ j)).symm
+      _ = a j * ∏ i ∈ Finset.univ.erase j, (1 - a i) := by
+        simp only [if_pos rfl]
+        apply congrArg (fun x => a j * x)
+        apply Finset.prod_congr rfl
+        intro i hi
+        have hij : i ≠ j := (Finset.mem_erase.mp hi).1
+        simp [hij]
+  · intro i hi
+    split_ifs
+    · exact (ha0 i).le
+    · exact sub_nonneg.mpr (ha1 i).le
+
+/-- The terminal-box orbit event has the expected natural density. -/
+theorem hasDensity_terminalBox [DecidableEq ι]
+    (j : ι) (a : ι → ℝ) (ha0 : ∀ i, 0 < a i) (ha1 : ∀ i, a i < 1)
+    (hrel : NoIntegerRelation a) :
+    {n : ℕ | n • (fun i => (a i : UnitAddCircle)) ∈ terminalBox j a}.HasDensity
+      (a j * ∏ i ∈ (Finset.univ.erase j), (1 - a i)) := by
+  let μ : ProbabilityMeasure (UnitAddTorus ι) := ⟨volume, inferInstance⟩
+  have havg : ∀ F : C(UnitAddTorus ι, ℂ),
+      Tendsto
+        (fun N : ℕ =>
+          (∑ n ∈ Finset.range N, F (n • (fun i => (a i : UnitAddCircle)))) / (N : ℂ))
+        atTop
+        (𝓝 (∫ x, F x ∂(μ : Measure (UnitAddTorus ι)))) := by
+    simpa [μ] using tendsto_average_rotation a hrel
+  have hd := MeasureTheory.hasDensity_of_tendsto_average
+    (Y := fun n => n • (fun i => (a i : UnitAddCircle))) μ havg
+    (measurableSet_terminalBox j a) (by
+      change (volume (frontier (terminalBox j a))).toNNReal = 0
+      rw [volume_frontier_terminalBox j a ha0 ha1]
+      rfl)
+    {n : ℕ | n • (fun i => (a i : UnitAddCircle)) ∈ terminalBox j a} (fun _ => Iff.rfl)
+  convert hd using 1
+  change a j * ∏ i ∈ Finset.univ.erase j, (1 - a i) =
+    (volume (terminalBox j a)).toReal
+  have hnonneg : 0 ≤ a j * ∏ i ∈ Finset.univ.erase j, (1 - a i) := by
+    apply mul_nonneg (ha0 j).le
+    apply Finset.prod_nonneg
+    intro i hi
+    exact sub_nonneg.mpr (ha1 i).le
+  rw [volume_terminalBox j a ha0 ha1, ENNReal.toReal_ofReal hnonneg]
+
+end UnitAddTorus
\ No newline at end of file
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArc.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArc.lean
new file mode 100644
index 0000000000..292decb2c7
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArc.lean
@@ -0,0 +1,147 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+
+@[expose] public section
+
+/-!
+# Short terminal arcs on the unit additive circle
+
+For `0 < a < 1`, the arc represented by the real interval `(1-a, 1)` is open,
+its endpoint closure is represented by `[1-a, 1]`, and both have normalized
+Haar measure `a`.
+-/
+
+noncomputable section
+
+open MeasureTheory Set Topology
+open scoped ENNReal NNReal Topology
+
+namespace UnitAddCircle
+
+/-- The open terminal arc of length `a` in `ℝ / ℤ`. -/
+def openArc (a : ℝ) : Set UnitAddCircle :=
+  ((↑) : ℝ → UnitAddCircle) '' Ioo (1 - a) 1
+
+/-- The closed endpoint hull of `openArc a`. -/
+def closedArc (a : ℝ) : Set UnitAddCircle :=
+  ((↑) : ℝ → UnitAddCircle) '' Icc (1 - a) 1
+
+private theorem coe_eq_coe_iff_of_mem_Ioc {x y : ℝ}
+    (hx : x ∈ Ioc (0 : ℝ) 1) (hy : y ∈ Ioc (0 : ℝ) 1) :
+    (x : UnitAddCircle) = (y : UnitAddCircle) ↔ x = y := by
+  constructor
+  · intro h
+    have h' := congrArg (AddCircle.equivIoc (1 : ℝ) 0) h
+    rw [AddCircle.equivIoc_coe_eq hx, AddCircle.equivIoc_coe_eq hy] at h'
+    exact congrArg Subtype.val h'
+  · rintro rfl
+    rfl
+
+private theorem coe_fract (x : ℝ) :
+    ((Int.fract x : ℝ) : UnitAddCircle) = (x : UnitAddCircle) := by
+  apply (AddCircle.equivIco (1 : ℝ) 0).injective
+  apply Subtype.ext
+  rw [AddCircle.equivIco_coe_eq (Int.fract_mem x)]
+  simpa using AddCircle.coe_equivIco_mk_apply (p := (1 : ℝ)) x
+
+/-- `openArc a` is open. -/
+theorem isOpen_openArc (a : ℝ) : IsOpen (openArc a) :=
+  QuotientAddGroup.isOpenMap_coe isOpen_Ioo
+
+/-- `closedArc a` is closed. -/
+theorem isClosed_closedArc (a : ℝ) : IsClosed (closedArc a) :=
+  (isCompact_Icc.image (AddCircle.continuous_mk' (1 : ℝ))).isClosed
+
+/-- The open arc is contained in its endpoint closure. -/
+theorem openArc_subset_closedArc (a : ℝ) : openArc a ⊆ closedArc a :=
+  image_mono Ioo_subset_Icc_self
+
+/-- Membership of a real point in the terminal arc is exactly the corresponding
+fractional-part inequality. -/
+theorem coe_mem_openArc_iff {a x : ℝ} (ha : a < 1) :
+    ((x : UnitAddCircle) ∈ openArc a) ↔ 1 - a < Int.fract x := by
+  constructor
+  · rintro ⟨y, hy, hxy⟩
+    have hyIco : y ∈ Ico (0 : ℝ) 1 :=
+      ⟨(sub_nonneg.mpr ha.le).trans hy.1.le, hy.2⟩
+    have hfrIco : Int.fract x ∈ Ico (0 : ℝ) 1 := Int.fract_mem x
+    have hyfr : y = Int.fract x :=
+      (AddCircle.coe_eq_coe_iff_of_mem_Ico hyIco hfrIco).mp
+        (hxy.trans (coe_fract x).symm)
+    simpa [hyfr] using hy.1
+  · intro hx
+    exact ⟨Int.fract x, ⟨hx, Int.fract_lt_one x⟩, coe_fract x⟩
+
+private theorem preimage_openArc_inter_Ioc {a : ℝ} (ha : a < 1) :
+    ((↑) : ℝ → UnitAddCircle) ⁻¹' openArc a ∩ Ioc 0 1 = Ioo (1 - a) 1 := by
+  ext x
+  constructor
+  · rintro ⟨⟨y, hy, hxy⟩, hx⟩
+    have hyIoc : y ∈ Ioc (0 : ℝ) 1 :=
+      ⟨(sub_pos.mpr ha).trans hy.1, hy.2.le⟩
+    have hxy' : y = x :=
+      (coe_eq_coe_iff_of_mem_Ioc hyIoc hx).mp hxy
+    simpa [hxy'] using hy
+  · intro hx
+    refine ⟨⟨x, hx, rfl⟩, ?_⟩
+    exact ⟨(sub_pos.mpr ha).trans hx.1, hx.2.le⟩
+
+private theorem preimage_closedArc_inter_Ioc {a : ℝ} (ha : a < 1) :
+    ((↑) : ℝ → UnitAddCircle) ⁻¹' closedArc a ∩ Ioc 0 1 = Icc (1 - a) 1 := by
+  ext x
+  constructor
+  · rintro ⟨⟨y, hy, hxy⟩, hx⟩
+    have hyIoc : y ∈ Ioc (0 : ℝ) 1 :=
+      ⟨(sub_pos.mpr ha).trans_le hy.1, hy.2⟩
+    have hxy' : y = x :=
+      (coe_eq_coe_iff_of_mem_Ioc hyIoc hx).mp hxy
+    simpa [hxy'] using hy
+  · intro hx
+    refine ⟨⟨x, hx, rfl⟩, ?_⟩
+    exact ⟨(sub_pos.mpr ha).trans_le hx.1, hx.2⟩
+
+/-- The open terminal arc has Haar measure `a`. -/
+theorem volume_openArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    volume (openArc a) = ENNReal.ofReal a := by
+  rw [AddCircle.add_projection_respects_measure (1 : ℝ) 0
+    (isOpen_openArc a).measurableSet]
+  rw [preimage_openArc_inter_Ioc ha1, Real.volume_Ioo]
+  congr 1
+  ring
+
+/-- Adding the two endpoints does not change the Haar measure. -/
+theorem volume_closedArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    volume (closedArc a) = ENNReal.ofReal a := by
+  rw [AddCircle.add_projection_respects_measure (1 : ℝ) 0
+    (isClosed_closedArc a).measurableSet]
+  rw [preimage_closedArc_inter_Ioc ha1, Real.volume_Icc]
+  congr 1
+  ring
+
+/-- The two endpoint conventions are equal almost everywhere. -/
+theorem openArc_ae_eq_closedArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    openArc a =ᵐ[volume] closedArc a := by
+  apply EventuallyLE.antisymm (openArc_subset_closedArc a).eventuallyLE
+  rw [ae_le_set]
+  exact measure_mono_null (diff_subset_iff.mpr (openArc_subset_closedArc a)) <| by
+    rw [measure_diff (isOpen_openArc a).measurableSet (measure_ne_top _ _),
+      volume_closedArc ha0 ha1, volume_openArc ha0 ha1]
+    simp
+
+end UnitAddCircle
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArcReal.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArcReal.lean
new file mode 100644
index 0000000000..01040f796f
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddCircleArcReal.lean
@@ -0,0 +1,56 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddCircleArc
+public import Mathlib.MeasureTheory.Measure.Real
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Set Topology
+open scoped ENNReal NNReal Topology
+
+namespace UnitAddCircle
+
+/-- Real Haar measure of the open terminal arc. -/
+theorem volumeReal_openArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    (volume : Measure UnitAddCircle).real (openArc a) = a := by
+  rw [Measure.real, volume_openArc ha0 ha1, ENNReal.toReal_ofReal ha0]
+
+/-- Real Haar measure of the closed terminal arc. -/
+theorem volumeReal_closedArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    (volume : Measure UnitAddCircle).real (closedArc a) = a := by
+  rw [Measure.real, volume_closedArc ha0 ha1, ENNReal.toReal_ofReal ha0]
+
+/-- Real Haar measure of the complement of the open terminal arc. -/
+theorem volumeReal_compl_openArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    (volume : Measure UnitAddCircle).real (openArc a)ᶜ = 1 - a := by
+  have h := measureReal_add_measureReal_compl
+    (μ := (volume : Measure UnitAddCircle)) (isOpen_openArc a).measurableSet
+  rw [volumeReal_openArc ha0 ha1, probReal_univ] at h
+  linarith
+
+/-- Real Haar measure of the complement of the closed terminal arc. -/
+theorem volumeReal_compl_closedArc {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) :
+    (volume : Measure UnitAddCircle).real (closedArc a)ᶜ = 1 - a := by
+  have h := measureReal_add_measureReal_compl
+    (μ := (volume : Measure UnitAddCircle)) (isClosed_closedArc a).measurableSet
+  rw [volumeReal_closedArc ha0 ha1, probReal_univ] at h
+  linarith
+
+end UnitAddCircle
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean
new file mode 100644
index 0000000000..a357e268a7
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean
@@ -0,0 +1,279 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Analysis.Fourier.AddCircleMulti
+public import Mathlib.Algebra.Field.GeomSum
+public import Mathlib.Analysis.SpecificLimits.Normed
+
+@[expose] public section
+
+/-!
+# A continuous Weyl criterion on a finite-dimensional unit torus
+
+Mathlib proves that the multivariate Fourier monomials have dense complex
+linear span in the continuous functions on `UnitAddTorus d`.  This file
+packages the standard consequence needed for equidistribution arguments:
+convergence of the empirical averages of every Fourier monomial implies
+convergence of the empirical averages of every continuous function.
+-/
+
+open Filter MeasureTheory Topology
+open scoped Topology
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- The standard Haar volume on `UnitAddCircle = AddCircle 1` has total mass one. -/
+instance unitAddCircleVolume_isProbabilityMeasure :
+    IsProbabilityMeasure (volume : Measure UnitAddCircle) :=
+  IsProbabilityMeasure.mk (by
+    simpa using (AddCircle.measure_univ (T := (1 : ℝ))))
+
+/-- On a unit torus, the standard product volume is the product of the probability-normalized
+Haar measures used by Mathlib's Fourier basis. -/
+lemma volume_eq_fourierVolume :
+    (volume : Measure (UnitAddTorus d)) =
+      Measure.pi (fun _ : d => AddCircle.haarAddCircle) := by
+  change Measure.pi (fun _ : d => (volume : Measure UnitAddCircle)) =
+    Measure.pi (fun _ : d => AddCircle.haarAddCircle)
+  apply congrArg (fun μ : d → Measure UnitAddCircle => Measure.pi μ)
+  funext i
+  simpa using (AddCircle.volume_eq_smul_haarAddCircle (T := (1 : ℝ)))
+
+/--
+**Continuous Weyl criterion on a finite unit torus.**
+
+If the empirical averages along `Y` converge to the `μ`-integral for every
+multivariate Fourier monomial, then they converge to the `μ`-integral for
+every continuous complex-valued function.  The proof extends convergence
+from the linear span of the monomials to its uniform closure, which is all of
+`C(UnitAddTorus d, ℂ)` by `span_mFourier_closure_eq_top`.
+-/
+theorem tendsto_average_of_tendsto_mFourier
+    (Y : ℕ → UnitAddTorus d) (μ : Measure (UnitAddTorus d))
+    [IsProbabilityMeasure μ]
+    (hfou : ∀ k : d → ℤ,
+      Tendsto
+        (fun N : ℕ => (∑ n ∈ Finset.range N, mFourier k (Y n)) / N)
+        atTop
+        (𝓝 (∫ x, mFourier k x ∂μ))) :
+    ∀ F : C(UnitAddTorus d, ℂ),
+      Tendsto
+        (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / N)
+        atTop
+        (𝓝 (∫ x, F x ∂μ)) := by
+  have hint : ∀ g : C(UnitAddTorus d, ℂ), Integrable g μ := fun g =>
+    g.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)
+  have hspan : ∀ g ∈ Submodule.span ℂ (Set.range (mFourier (d := d))),
+      Tendsto
+        (fun N : ℕ => (∑ n ∈ Finset.range N, g (Y n)) / N)
+        atTop
+        (𝓝 (∫ x, g x ∂μ)) := by
+    intro g hg
+    induction hg using Submodule.span_induction with
+    | mem g hgmem =>
+        obtain ⟨k, rfl⟩ := hgmem
+        exact hfou k
+    | zero =>
+        simp only [ContinuousMap.zero_apply, Finset.sum_const_zero, zero_div, integral_zero]
+        exact tendsto_const_nhds
+    | add g₁ g₂ _ _ ih₁ ih₂ =>
+        simp only [ContinuousMap.add_apply, Finset.sum_add_distrib, add_div,
+          integral_add (hint g₁) (hint g₂)]
+        exact ih₁.add ih₂
+    | smul c g _ ih =>
+        simp only [ContinuousMap.smul_apply, smul_eq_mul, ← Finset.mul_sum, mul_div_assoc,
+          integral_const_mul]
+        exact ih.const_mul c
+  intro F
+  rw [Metric.tendsto_atTop]
+  intro ε hε
+  have hF : F ∈ closure (Submodule.span ℂ (Set.range (mFourier (d := d))) : Set _) := by
+    rw [← Submodule.topologicalClosure_coe, span_mFourier_closure_eq_top,
+      Submodule.top_coe]
+    exact Set.mem_univ F
+  obtain ⟨p, hp, hdist⟩ := Metric.mem_closure_iff.mp hF (ε / 3) (by positivity)
+  rw [dist_eq_norm] at hdist
+  obtain ⟨N₀, hN₀⟩ :=
+    (Metric.tendsto_atTop.mp (hspan p hp)) (ε / 3) (by positivity)
+  refine ⟨N₀, fun N hN => ?_⟩
+  have hbound : ∀ z : UnitAddTorus d, ‖F z - p z‖ ≤ ‖F - p‖ := fun z => by
+    simpa using (F - p).norm_coe_le_norm z
+  have h1 :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+          (∑ n ∈ Finset.range N, p (Y n)) / N‖ ≤ ‖F - p‖ := by
+    rw [div_sub_div_same, ← Finset.sum_sub_distrib, norm_div, Complex.norm_natCast]
+    rcases Nat.eq_zero_or_pos N with h | h
+    · simp [h]
+    · rw [div_le_iff₀ (by exact_mod_cast h)]
+      calc
+        ‖∑ n ∈ Finset.range N, (F (Y n) - p (Y n))‖
+            ≤ ∑ n ∈ Finset.range N, ‖F (Y n) - p (Y n)‖ := norm_sum_le _ _
+        _ ≤ ∑ _n ∈ Finset.range N, ‖F - p‖ :=
+          Finset.sum_le_sum (fun n _ => hbound _)
+        _ = ‖F - p‖ * N := by
+          rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
+  have h2 : ‖(∫ x, p x ∂μ) - ∫ x, F x ∂μ‖ ≤ ‖F - p‖ := by
+    rw [← integral_sub (hint p) (hint F)]
+    calc
+      ‖∫ x, (p x - F x) ∂μ‖ ≤ ∫ x, ‖p x - F x‖ ∂μ :=
+        norm_integral_le_integral_norm _
+      _ ≤ ∫ _x, ‖F - p‖ ∂μ := by
+        refine integral_mono_of_nonneg
+          (by filter_upwards with z using norm_nonneg (p z - F z))
+          (integrable_const _) ?_
+        filter_upwards with z
+        rw [norm_sub_rev]
+        exact hbound z
+      _ = ‖F - p‖ := by simp
+  have hN0' := hN₀ N hN
+  rw [dist_eq_norm] at hN0' ⊢
+  have htri :
+      ‖(∑ n ∈ Finset.range N, F (Y n)) / N - ∫ x, F x ∂μ‖ ≤
+        ‖(∑ n ∈ Finset.range N, F (Y n)) / N -
+            (∑ n ∈ Finset.range N, p (Y n)) / N‖ +
+          ‖(∑ n ∈ Finset.range N, p (Y n)) / N - ∫ x, p x ∂μ‖ +
+          ‖(∫ x, p x ∂μ) - ∫ x, F x ∂μ‖ := by
+    have heq :
+        (∑ n ∈ Finset.range N, F (Y n)) / N - ∫ x, F x ∂μ =
+          ((∑ n ∈ Finset.range N, F (Y n)) / N -
+              (∑ n ∈ Finset.range N, p (Y n)) / N) +
+            ((∑ n ∈ Finset.range N, p (Y n)) / N - ∫ x, p x ∂μ) +
+            ((∫ x, p x ∂μ) - ∫ x, F x ∂μ) := by ring
+    rw [heq]
+    exact norm_add₃_le
+  linarith [htri, h1, h2, hN0', hdist]
+
+/-- There is no nontrivial integer relation among `a` and `1`. -/
+def NoIntegerRelation (a : d → ℝ) : Prop :=
+  ∀ k : d → ℤ, (∃ z : ℤ, ∑ i, (k i : ℝ) * a i = z) → k = 0
+
+/-- A multivariate Fourier monomial turns addition on the torus into multiplication. -/
+lemma mFourier_add_point (k : d → ℤ) (x y : UnitAddTorus d) :
+    mFourier k (x + y) = mFourier k x * mFourier k y := by
+  simp only [mFourier, ContinuousMap.coe_mk, Pi.add_apply, fourier_apply, smul_add,
+    AddCircle.toCircle_add, Circle.coe_mul, Finset.prod_mul_distrib]
+
+/-- A Fourier monomial along a rotation orbit is a geometric progression. -/
+lemma mFourier_nsmul (k : d → ℤ) (x : UnitAddTorus d) (n : ℕ) :
+    mFourier k (n • x) = (mFourier k x) ^ n := by
+  induction n with
+  | zero => simp [mFourier, fourier_apply]
+  | succ n ih =>
+      rw [succ_nsmul, mFourier_add_point, ih, pow_succ]
+
+/-- A Fourier monomial is the canonical circle character evaluated on the corresponding
+integer linear combination of the coordinates. -/
+lemma mFourier_eq_toCircle_sum (k : d → ℤ) (x : UnitAddTorus d) :
+    mFourier k x =
+      ((AddCircle.toCircle (∑ i, k i • x i) : Circle) : ℂ) := by
+  classical
+  simp only [mFourier, ContinuousMap.coe_mk, fourier_apply]
+  let s : Finset d := Finset.univ
+  change (∏ i ∈ s, ((AddCircle.toCircle (k i • x i) : Circle) : ℂ)) =
+    ((AddCircle.toCircle (∑ i ∈ s, k i • x i) : Circle) : ℂ)
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert a s ha ih =>
+      rw [Finset.prod_insert ha, Finset.sum_insert ha, AddCircle.toCircle_add,
+        Circle.coe_mul, ih]
+
+/-- Under `NoIntegerRelation`, every nonconstant Fourier monomial is nontrivial on the
+rotation vector. -/
+lemma mFourier_coe_ne_one {a : d → ℝ} (ha : NoIntegerRelation a)
+    {k : d → ℤ} (hk : k ≠ 0) :
+    mFourier k (fun i => (a i : UnitAddCircle)) ≠ 1 := by
+  intro h
+  have hcirc :
+      AddCircle.toCircle (∑ i, k i • (a i : UnitAddCircle)) = (1 : Circle) := by
+    apply Subtype.ext
+    simpa [mFourier_eq_toCircle_sum] using h
+  have hzero : (∑ i, k i • (a i : UnitAddCircle)) = 0 := by
+    apply AddCircle.injective_toCircle one_ne_zero
+    simpa using hcirc
+  have hzero' : ((∑ i, (k i : ℝ) * a i : ℝ) : UnitAddCircle) = 0 := by
+    simpa [zsmul_eq_mul] using hzero
+  obtain ⟨z, hz⟩ := (AddCircle.coe_eq_zero_iff (1 : ℝ)).mp hzero'
+  apply hk
+  apply ha k
+  exact ⟨z, by simpa [zsmul_eq_mul] using hz.symm⟩
+
+/-- The Haar integral of a torus Fourier monomial is `1` at frequency zero and `0`
+otherwise. -/
+lemma integral_mFourier (k : d → ℤ) :
+    ∫ x : UnitAddTorus d, mFourier k x = if k = 0 then 1 else 0 := by
+  rw [volume_eq_fourierVolume (d := d)]
+  letI : MeasureSpace UnitAddCircle := ⟨AddCircle.haarAddCircle⟩
+  change (∫ x : UnitAddTorus d, mFourier k x) = if k = 0 then 1 else 0
+  have h := (orthonormal_iff_ite.mp (orthonormal_mFourier (d := d))) (0 : d → ℤ) k
+  simpa only [ContinuousMap.inner_toLp, mFourier_zero, ContinuousMap.one_apply,
+    map_one, one_mul, mul_one, Pi.zero_apply, neg_zero, zero_add, eq_comm] using h
+
+/-- The Cesàro averages of a nontrivial unit-modulus geometric progression tend to zero. -/
+lemma tendsto_geom_average_zero {z : ℂ} (hz : z ≠ 1) (hnorm : ‖z‖ = 1) :
+    Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, z ^ n) / N) atTop (𝓝 0) := by
+  have hbound : ∀ N : ℕ,
+      ‖(∑ n ∈ Finset.range N, z ^ n) / N‖ ≤
+        (2 / ‖z - 1‖) / (N : ℝ) := by
+    intro N
+    rw [geom_sum_eq hz, norm_div, norm_div, Complex.norm_natCast]
+    by_cases hN : N = 0
+    · simp [hN]
+    have hden : 0 < ‖z - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hz)
+    have hNpos : (0 : ℝ) < N := by exact_mod_cast Nat.pos_of_ne_zero hN
+    apply div_le_div_of_nonneg_right _ hNpos.le
+    apply div_le_div_of_nonneg_right _ hden.le
+    calc
+      ‖z ^ N - 1‖ ≤ ‖z ^ N‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _
+      _ = 2 := by norm_num [norm_pow, hnorm]
+  refine squeeze_zero_norm hbound ?_
+  exact tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop
+
+/-- Weyl equidistribution for a torus rotation whose coordinates, together with `1`,
+have no nontrivial integer relation. -/
+theorem tendsto_average_rotation
+    (a : d → ℝ) (ha : NoIntegerRelation a) :
+    ∀ F : C(UnitAddTorus d, ℂ),
+      Tendsto
+        (fun N : ℕ =>
+          (∑ n ∈ Finset.range N, F (n • (fun i => (a i : UnitAddCircle)))) / N)
+        atTop
+        (𝓝 (∫ x, F x)) := by
+  apply tendsto_average_of_tendsto_mFourier
+    (Y := fun n => n • (fun i => (a i : UnitAddCircle))) volume
+  intro k
+  by_cases hk : k = 0
+  · subst k
+    have heq :
+        (fun N : ℕ =>
+          (∑ n ∈ Finset.range N,
+            mFourier (0 : d → ℤ) (n • (fun i => (a i : UnitAddCircle)))) / N) =ᶠ[atTop]
+          fun _ => (1 : ℂ) := by
+      filter_upwards [eventually_gt_atTop 0] with N hN
+      simp [mFourier_zero, hN.ne']
+    simpa [integral_mFourier] using tendsto_const_nhds.congr' heq.symm
+  · have hz : mFourier k (fun i => (a i : UnitAddCircle)) ≠ 1 :=
+      mFourier_coe_ne_one ha hk
+    have hnorm : ‖mFourier k (fun i => (a i : UnitAddCircle))‖ = 1 := by
+      simp only [mFourier, fourier_apply, ContinuousMap.coe_mk, norm_prod,
+        Circle.norm_coe, Finset.prod_const_one]
+    have hgeom := tendsto_geom_average_zero hz hnorm
+    rw [integral_mFourier, if_neg hk]
+    simpa only [mFourier_nsmul] using hgeom
+
+end UnitAddTorus
\ No newline at end of file
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangle.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangle.lean
new file mode 100644
index 0000000000..2432476bb2
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangle.lean
@@ -0,0 +1,71 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddCircleArc
+public import Mathlib.MeasureTheory.Constructions.Pi
+
+@[expose] public section
+
+/-!
+# Rectangles in a finite unit torus
+
+A coordinate rectangle in a finite product is open or closed when every side
+is, and its product Haar measure is the product of the side measures.
+-/
+
+noncomputable section
+
+open MeasureTheory Set Topology
+open scoped BigOperators ENNReal NNReal Topology
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- The coordinate rectangle with side `B i` in coordinate `i`. -/
+def rectangle (B : d → Set UnitAddCircle) : Set (UnitAddTorus d) :=
+  Set.pi Set.univ B
+
+private theorem rectangle_eq_iInter (B : d → Set UnitAddCircle) :
+    rectangle B = ⋂ i, (fun x : UnitAddTorus d => x i) ⁻¹' B i := by
+  ext x
+  simp [rectangle]
+
+/-- A finite product of open sides is open. -/
+theorem isOpen_rectangle {B : d → Set UnitAddCircle} (hB : ∀ i, IsOpen (B i)) :
+    IsOpen (rectangle B) := by
+  rw [rectangle_eq_iInter]
+  exact isOpen_iInter_of_finite fun i => (hB i).preimage (continuous_apply i)
+
+/-- A finite product of closed sides is closed. -/
+theorem isClosed_rectangle {B : d → Set UnitAddCircle} (hB : ∀ i, IsClosed (B i)) :
+    IsClosed (rectangle B) := by
+  rw [rectangle_eq_iInter]
+  exact isClosed_iInter fun i => (hB i).preimage (continuous_apply i)
+
+/-- Coordinatewise inclusion gives inclusion of rectangles. -/
+theorem rectangle_mono {A B : d → Set UnitAddCircle} (h : ∀ i, A i ⊆ B i) :
+    rectangle A ⊆ rectangle B :=
+  Set.pi_mono fun i _ => h i
+
+/-- Haar measure of a finite torus rectangle is the product of the side measures. -/
+theorem volume_rectangle (B : d → Set UnitAddCircle) :
+    volume (rectangle B) = ∏ i, volume (B i) := by
+  simpa [rectangle] using
+    (Measure.pi_pi (fun _ : d => (volume : Measure UnitAddCircle)) B)
+
+end UnitAddTorus
diff --git a/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangleReal.lean b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangleReal.lean
new file mode 100644
index 0000000000..bccf9f9d70
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorusRectangleReal.lean
@@ -0,0 +1,41 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Analysis.Equidistribution.UnitAddTorusRectangle
+public import Mathlib.MeasureTheory.Measure.Real
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Set Topology
+open scoped BigOperators ENNReal NNReal Topology
+
+namespace UnitAddTorus
+
+variable {d : Type*} [Fintype d]
+
+/-- Real Haar measure of a finite torus rectangle is the product of the real
+Haar measures of its sides. -/
+theorem volumeReal_rectangle (B : d → Set UnitAddCircle) :
+    (volume : Measure (UnitAddTorus d)).real (rectangle B) =
+      ∏ i, (volume : Measure UnitAddCircle).real (B i) := by
+  rw [Measure.real, volume_rectangle]
+  rw [ENNReal.toReal_prod]
+  rfl
+
+end UnitAddTorus
diff --git a/FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean b/FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean
new file mode 100644
index 0000000000..4d2ffacc8d
--- /dev/null
+++ b/FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean
@@ -0,0 +1,145 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.MeasureTheory.Group.AddCircle
+public import Mathlib.Analysis.Normed.Group.AddCircle
+
+@[expose] public section
+
+open Set Filter MeasureTheory
+open scoped Topology ENNReal
+
+noncomputable section
+
+namespace UnitAddCircle
+
+/-- The arc with fractional representatives in `(1-a,1)`. -/
+def terminalArc (a : ℝ) : Set UnitAddCircle :=
+  Metric.ball ((1 - a / 2 : ℝ) : UnitAddCircle) (a / 2)
+
+/-- The preimage of a ball under the real quotient map is the union of its integer translates. -/
+theorem coe_preimage_ball_eq_iUnion (x ε : ℝ) :
+    ((↑) : ℝ → UnitAddCircle) ⁻¹' Metric.ball (x : UnitAddCircle) ε =
+      ⋃ z : ℤ, Metric.ball (x + z) ε := by
+  ext y
+  simp only [Metric.mem_ball, Set.mem_preimage, Set.mem_iUnion, Real.dist_eq,
+    dist_eq_norm, ← QuotientAddGroup.mk_sub, UnitAddCircle.norm_eq]
+  constructor
+  · intro h
+    refine ⟨round (y - x), ?_⟩
+    simpa [sub_sub, add_comm, add_left_comm, add_assoc] using h
+  · rintro ⟨z, hz⟩
+    have hmin := round_le (y - x) z
+    exact hmin.trans_lt (by simpa [sub_sub, add_comm, add_left_comm, add_assoc] using hz)
+
+/-- Membership in the terminal metric arc is exactly a strict fractional-coordinate inequality. -/
+theorem coe_mem_terminalArc_iff {a t : ℝ} (ha0 : 0 < a) (ha1 : a < 1)
+    (ht : t ∈ Set.Ico (0 : ℝ) 1) :
+    ((t : ℝ) : UnitAddCircle) ∈ terminalArc a ↔ 1 - a < t := by
+  change t ∈ ((↑) : ℝ → UnitAddCircle) ⁻¹'
+    Metric.ball ((1 - a / 2 : ℝ) : UnitAddCircle) (a / 2) ↔ _
+  rw [coe_preimage_ball_eq_iUnion]
+  simp only [Set.mem_iUnion, Metric.mem_ball, Real.dist_eq]
+  constructor
+  · rintro ⟨z, hz⟩
+    obtain ⟨hzl, hzu⟩ := abs_lt.mp hz
+    by_cases hzero : z = 0
+    · subst z
+      norm_num at hzl hzu
+      linarith
+    · rcases lt_or_gt_of_ne hzero with hzneg | hzpos
+      · have hzle : (z : ℝ) ≤ -1 := by exact_mod_cast (show z ≤ -1 by omega)
+        linarith [ht.1]
+      · have hzone : (1 : ℝ) ≤ z := by exact_mod_cast (show (1 : ℤ) ≤ z by omega)
+        linarith [ht.2]
+  · intro h
+    refine ⟨0, ?_⟩
+    rw [Int.cast_zero, add_zero, abs_lt]
+    constructor <;> linarith [ht.2]
+
+/-- Fractional representatives are unchanged by passing to `UnitAddCircle`. -/
+theorem coe_fract_eq (x : ℝ) :
+    ((x : ℝ) : UnitAddCircle) = ((Int.fract x : ℝ) : UnitAddCircle) := by
+  rw [← Int.floor_add_fract x]
+  simp
+
+/-- A rotation point lies in the terminal arc precisely when its fractional part lies in the
+corresponding terminal interval. -/
+theorem nsmul_mem_terminalArc_iff {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) (n : ℕ) :
+    n • (a : UnitAddCircle) ∈ terminalArc a ↔
+      1 - a < Int.fract ((n : ℝ) * a) := by
+  have hfract : Int.fract ((n : ℝ) * a) ∈ Set.Ico (0 : ℝ) 1 :=
+    ⟨Int.fract_nonneg _, Int.fract_lt_one _⟩
+  rw [show n • (a : UnitAddCircle) = (((n : ℝ) * a : ℝ) : UnitAddCircle) by
+    simp [nsmul_eq_mul]]
+  rw [coe_fract_eq]
+  exact coe_mem_terminalArc_iff ha0 ha1 hfract
+
+/-- Spheres in the additive circle have Haar measure zero. -/
+theorem volume_sphere_eq_zero {c r : ℝ} (_hr0 : 0 ≤ r) (_hr : r < 1 / 2) :
+    volume (Metric.sphere (c : UnitAddCircle) r) = 0 := by
+  rw [← ae_eq_empty]
+  filter_upwards [AddCircle.closedBall_ae_eq_ball
+    (x := (c : UnitAddCircle)) (ε := r)] with y hy
+  apply propext
+  constructor
+  · intro hysphere
+    have hclosed : y ∈ Metric.closedBall (c : UnitAddCircle) r :=
+      Metric.mem_closedBall.mpr (Metric.mem_sphere.mp hysphere).le
+    have hball : y ∈ Metric.ball (c : UnitAddCircle) r := hy.mp hclosed
+    exact (Metric.mem_ball.mp hball).ne (Metric.mem_sphere.mp hysphere)
+  · intro hyempty
+    exact hyempty.elim
+
+/-- The terminal arc has length `a`. -/
+theorem volume_terminalArc {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    volume (terminalArc a) = ENNReal.ofReal a := by
+  calc
+    volume (terminalArc a) =
+        volume (Metric.closedBall ((1 - a / 2 : ℝ) : UnitAddCircle) (a / 2)) := by
+          exact measure_congr (AddCircle.closedBall_ae_eq_ball
+            (x := ((1 - a / 2 : ℝ) : UnitAddCircle)) (ε := a / 2)).symm
+    _ = ENNReal.ofReal a := by
+      rw [AddCircle.volume_closedBall]
+      congr 1
+      rw [min_eq_right]
+      · ring
+      · linarith
+
+/-- The terminal arc is measurable. -/
+theorem measurableSet_terminalArc (a : ℝ) : MeasurableSet (terminalArc a) :=
+  Metric.isOpen_ball.measurableSet
+
+/-- The terminal arc has null frontier. -/
+theorem volume_frontier_terminalArc {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    volume (frontier (terminalArc a)) = 0 := by
+  apply measure_mono_null Metric.frontier_ball_subset_sphere
+  exact volume_sphere_eq_zero (by positivity) (by linarith)
+
+/-- The complement of a terminal arc has null frontier as well. -/
+theorem volume_frontier_terminalArc_compl {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    volume (frontier (terminalArc a)ᶜ) = 0 := by
+  simpa using volume_frontier_terminalArc ha0 ha1
+
+/-- The complement of a terminal arc has length `1-a`. -/
+theorem volume_terminalArc_compl {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    volume (terminalArc a)ᶜ = ENNReal.ofReal (1 - a) := by
+  rw [measure_compl (measurableSet_terminalArc a) (measure_ne_top _ _)]
+  rw [AddCircle.measure_univ, volume_terminalArc ha0 ha1]
+  norm_num [ENNReal.ofReal_sub 1 ha0.le]
+
+end UnitAddCircle
diff --git a/FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean b/FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean
new file mode 100644
index 0000000000..3b7e5d9aff
--- /dev/null
+++ b/FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean
@@ -0,0 +1,177 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.Portmanteau
+public import Mathlib.Probability.Distributions.Uniform
+public import Mathlib.Probability.ProbabilityMassFunction.Integrals
+public import FormalConjecturesForMathlib.Data.Set.Density
+
+@[expose] public section
+
+open Filter MeasureTheory Set Topology
+open scoped ENNReal NNReal Topology BigOperators Classical
+
+noncomputable section
+
+namespace MeasureTheory
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+theorem empiricalRange_nonempty_of_ne_zero {N : ℕ} (hN : N ≠ 0) :
+    (Finset.range N).Nonempty :=
+  ⟨0, Finset.mem_range.mpr (Nat.pos_of_ne_zero hN)⟩
+
+/-- The empirical probability measure of the first `N` values of a sequence.
+At `N = 0` we use a harmless Dirac measure. -/
+def empiricalProbabilityMeasure (Y : ℕ → Ω) (N : ℕ) : ProbabilityMeasure Ω := by
+  classical
+  by_cases hN : N = 0
+  · exact ⟨Measure.dirac (Y 0), Measure.dirac.isProbabilityMeasure⟩
+  · let p : PMF ℕ := PMF.uniformOfFinset (Finset.range N) (empiricalRange_nonempty_of_ne_zero hN)
+    let ν : ProbabilityMeasure ℕ := ⟨p.toMeasure, inferInstance⟩
+    exact ProbabilityMeasure.map ν (measurable_of_countable Y).aemeasurable
+
+lemma empiricalProbabilityMeasure_ne_zero (Y : ℕ → Ω) {N : ℕ} (hN : N ≠ 0) :
+    empiricalProbabilityMeasure Y N =
+      ProbabilityMeasure.map
+        (⟨(PMF.uniformOfFinset (Finset.range N)
+            (empiricalRange_nonempty_of_ne_zero hN)).toMeasure,
+          inferInstance⟩ : ProbabilityMeasure ℕ)
+        (measurable_of_countable Y).aemeasurable := by
+  simp [empiricalProbabilityMeasure, hN, empiricalRange_nonempty_of_ne_zero]
+
+variable [PseudoMetricSpace Ω] [BorelSpace Ω]
+
+/-- Integration against the empirical measure is the corresponding finite average. -/
+theorem integral_empiricalProbabilityMeasure
+    (Y : ℕ → Ω) {N : ℕ} (hN : N ≠ 0) (f : BoundedContinuousFunction Ω ℂ) :
+    ∫ x, f x ∂(empiricalProbabilityMeasure Y N : Measure Ω) =
+      (∑ n ∈ Finset.range N, f (Y n)) / (N : ℂ) := by
+  classical
+  rw [empiricalProbabilityMeasure_ne_zero Y hN]
+  let p : PMF ℕ := PMF.uniformOfFinset (Finset.range N) (empiricalRange_nonempty_of_ne_zero hN)
+  have hY : Measurable Y := measurable_of_countable Y
+  rw [ProbabilityMeasure.toMeasure_map]
+  rw [integral_map hY.aemeasurable f.continuous.aestronglyMeasurable]
+  change (∫ n : ℕ, f (Y n) ∂p.toMeasure) = _
+  have hfint : Integrable (fun n => f (Y n)) p.toMeasure := by
+    have hc : Integrable (fun _ : ℕ => (‖f‖ : ℂ)) p.toMeasure := integrable_const _
+    refine hc.mono ?_ ?_
+    · exact (measurable_of_countable (fun n => f (Y n))).aestronglyMeasurable
+    · exact Filter.Eventually.of_forall fun n => by
+        simpa using f.norm_coe_le_norm (Y n)
+  rw [PMF.integral_eq_tsum p (fun n => f (Y n)) hfint]
+  rw [tsum_eq_sum (s := Finset.range N)]
+  · calc
+      (∑ n ∈ Finset.range N, (p n).toReal • f (Y n)) =
+          ∑ n ∈ Finset.range N, ((N : ℝ)⁻¹ : ℝ) • f (Y n) := by
+            apply Finset.sum_congr rfl
+            intro n hn
+            simp [p, PMF.uniformOfFinset_apply, hn, hN]
+      _ = ((N : ℝ)⁻¹ : ℝ) • ∑ n ∈ Finset.range N, f (Y n) := by
+            rw [Finset.smul_sum]
+      _ = (∑ n ∈ Finset.range N, f (Y n)) / (N : ℂ) := by
+            rw [RCLike.real_smul_eq_coe_mul]
+            push_cast
+            field_simp [hN]
+  · intro n hn
+    simp [p, PMF.uniformOfFinset_apply, hn]
+
+/-- The mass of a measurable set under an empirical measure is its finite frequency. -/
+theorem empiricalProbabilityMeasure_apply (Y : ℕ → Ω) {N : ℕ} (hN : N ≠ 0)
+    {A : Set Ω} (hA : MeasurableSet A) :
+    empiricalProbabilityMeasure Y N A =
+      (((Finset.range N).filter fun n => Y n ∈ A).card : ℝ≥0) / N := by
+  classical
+  rw [empiricalProbabilityMeasure_ne_zero Y hN]
+  rw [ProbabilityMeasure.map_apply]
+  · change (((PMF.uniformOfFinset (Finset.range N)
+        (empiricalRange_nonempty_of_ne_zero hN)).toMeasure
+          (Y ⁻¹' A)).toNNReal) = _
+    rw [PMF.toMeasure_uniformOfFinset_apply]
+    · norm_num [ENNReal.toNNReal_div, Finset.filter_filter, and_comm]
+    · exact (measurable_of_countable Y) hA
+  · exact hA
+
+variable [CompactSpace Ω]
+
+/-- Continuous-test-function convergence of finite orbit averages gives weak convergence of the
+empirical probability measures. -/
+theorem tendsto_empiricalProbabilityMeasure
+    (Y : ℕ → Ω) (μ : ProbabilityMeasure Ω)
+    (havg : ∀ F : C(Ω, ℂ),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / (N : ℂ))
+        atTop (𝓝 (∫ x, F x ∂(μ : Measure Ω)))) :
+    Tendsto (empiricalProbabilityMeasure Y) atTop (𝓝 μ) := by
+  rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ]
+  intro f
+  have h := havg ⟨f, f.continuous⟩
+  apply h.congr'
+  filter_upwards [eventually_ne_atTop 0] with N hN
+  exact (integral_empiricalProbabilityMeasure Y hN f).symm
+
+/-- The finite frequency of a continuity set converges to its limiting probability. -/
+theorem tendsto_frequency_of_null_frontier
+    (Y : ℕ → Ω) (μ : ProbabilityMeasure Ω)
+    (havg : ∀ F : C(Ω, ℂ),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / (N : ℂ))
+        atTop (𝓝 (∫ x, F x ∂(μ : Measure Ω))))
+    {A : Set Ω} (hA : MeasurableSet A) (hfront : μ (frontier A) = 0) :
+    Tendsto
+      (fun N : ℕ =>
+        (((Finset.range N).filter fun n => Y n ∈ A).card : ℝ) / N)
+      atTop (𝓝 ((μ A : ℝ≥0) : ℝ)) := by
+  classical
+  have hweak := tendsto_empiricalProbabilityMeasure Y μ havg
+  have hport := ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto hweak hfront
+  have hcoe := (NNReal.continuous_coe.tendsto (μ A)).comp hport
+  apply hcoe.congr'
+  filter_upwards [eventually_ne_atTop 0] with N hN
+  simp only [Function.comp_apply]
+  rw [empiricalProbabilityMeasure_apply Y hN hA]
+  norm_num [NNReal.coe_div]
+
+/-- A continuity-set frequency theorem expressed in the `Set.HasDensity` API. -/
+theorem hasDensity_of_tendsto_average
+    (Y : ℕ → Ω) (μ : ProbabilityMeasure Ω)
+    (havg : ∀ F : C(Ω, ℂ),
+      Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, F (Y n)) / (N : ℂ))
+        atTop (𝓝 (∫ x, F x ∂(μ : Measure Ω))))
+    {A : Set Ω} (hA : MeasurableSet A) (hfront : μ (frontier A) = 0)
+    (S : Set ℕ) (hS : ∀ n, n ∈ S ↔ Y n ∈ A) :
+    S.HasDensity ((μ A : ℝ≥0) : ℝ) := by
+  classical
+  have hfreq := tendsto_frequency_of_null_frontier Y μ havg hA hfront
+  change Tendsto
+    (fun N : ℕ => (((S ∩ Set.univ) ∩ Set.Iio N).ncard : ℝ) /
+      ((Set.univ ∩ Set.Iio N).ncard : ℝ))
+    atTop (𝓝 ((μ A : ℝ≥0) : ℝ))
+  apply hfreq.congr'
+  filter_upwards with N
+  have hfinite : ((S ∩ Set.univ) ∩ Set.Iio N).Finite :=
+    (Set.finite_Iio N).subset Set.inter_subset_right
+  have hcard :
+      ((S ∩ Set.univ) ∩ Set.Iio N).ncard =
+        ((Finset.range N).filter fun n => Y n ∈ A).card := by
+    rw [Set.ncard_eq_toFinset_card _ hfinite]
+    congr 1
+    ext n
+    simp [hS, and_comm]
+  rw [hcard]
+  simp
+
+end MeasureTheory
diff --git a/FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean b/FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean
new file mode 100644
index 0000000000..35f7cb8698
--- /dev/null
+++ b/FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean
@@ -0,0 +1,105 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.FiniteMeasurePi
+
+@[expose] public section
+
+open Set Topology MeasureTheory
+open scoped Topology BigOperators
+
+noncomputable section
+
+namespace Set
+
+variable {ι : Type*} [Fintype ι]
+variable {α : Type*} [TopologicalSpace α]
+
+private theorem mem_interior_of_mem_notMem_frontier {A : Set α} {x : α}
+    (hx : x ∈ A) (hfront : x ∉ frontier A) : x ∈ interior A := by
+  by_contra hxint
+  apply hfront
+  rw [frontier]
+  exact ⟨subset_closure hx, hxint⟩
+
+/-- The frontier of a finite product rectangle is contained in the union of the coordinate
+frontiers. -/
+theorem frontier_pi_subset_iUnion (A : ι → Set α) :
+    frontier (Set.pi univ A) ⊆
+      ⋃ i, (fun x : ι → α => x i) ⁻¹' frontier (A i) := by
+  classical
+  intro x hx
+  by_contra hnot
+  have hcoord : ∀ i, x i ∉ frontier (A i) := by
+    simpa only [Set.mem_iUnion, Set.mem_preimage, not_exists] using hnot
+  by_cases hxA : x ∈ Set.pi univ A
+  · have hxint : x ∈ interior (Set.pi univ A) := by
+      let U : Set (ι → α) := Set.pi univ (fun i => interior (A i))
+      have hUopen : IsOpen U := isOpen_set_pi finite_univ (fun i _ => isOpen_interior)
+      have hxU : x ∈ U := by
+        intro i _
+        exact mem_interior_of_mem_notMem_frontier (hxA i trivial) (hcoord i)
+      have hUsub : U ⊆ Set.pi univ A := by
+        intro y hy i _
+        exact interior_subset (hy i trivial)
+      exact interior_maximal hUsub hUopen hxU
+    rw [frontier] at hx
+    exact hx.2 hxint
+  · have hex : ∃ i, x i ∉ A i := by
+      simpa only [Set.mem_pi, Set.mem_univ, forall_true_left, not_forall] using hxA
+    obtain ⟨i, hi⟩ := hex
+    let V : Set (ι → α) := (fun y => y i) ⁻¹' interior (A i)ᶜ
+    have hVopen : IsOpen V := isOpen_interior.preimage (continuous_apply i)
+    have hxV : x ∈ V := by
+      exact mem_interior_of_mem_notMem_frontier
+        (show x i ∈ (A i)ᶜ by simpa) (by simpa using hcoord i)
+    have hVsub : V ⊆ (Set.pi univ A)ᶜ := by
+      intro y hy hyA
+      exact (interior_subset hy) (hyA i trivial)
+    have hxcompint : x ∈ interior (Set.pi univ A)ᶜ :=
+      interior_maximal hVsub hVopen hxV
+    have hnotfront : x ∉ frontier (Set.pi univ A)ᶜ := by
+      intro hfront
+      rw [frontier] at hfront
+      exact hfront.2 hxcompint
+    exact hnotfront (by simpa using hx)
+
+end Set
+
+namespace MeasureTheory
+
+variable {ι : Type*} [Fintype ι]
+variable {α : Type*} [MeasurableSpace α] [TopologicalSpace α]
+
+/-- A finite product of coordinate continuity sets is a continuity set for the product measure. -/
+theorem measure_frontier_pi_eq_zero
+    (μ : ι → Measure α) [∀ i, IsProbabilityMeasure (μ i)]
+    (A : ι → Set α) (hnull : ∀ i, μ i (frontier (A i)) = 0) :
+    Measure.pi μ (frontier (Set.pi univ A)) = 0 := by
+  classical
+  apply measure_mono_null (Set.frontier_pi_subset_iUnion A)
+  apply measure_iUnion_null
+  intro i
+  have heq :
+      (fun x : ι → α => x i) ⁻¹' frontier (A i) =
+        Set.pi univ (fun j => if j = i then frontier (A j) else univ) := by
+    ext x
+    simp [Set.mem_pi]
+  rw [heq, Measure.pi_pi, Finset.prod_eq_zero_iff]
+  exact ⟨i, Finset.mem_univ i, by simp [hnull i]⟩
+
+end MeasureTheory
diff --git a/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean b/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean
new file mode 100644
index 0000000000..1fda3cedb2
--- /dev/null
+++ b/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean
@@ -0,0 +1,170 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib
+
+@[expose] public section
+
+noncomputable section
+
+open scoped Classical
+open Polynomial Module
+
+namespace Nat
+
+/-- The product of two squarefree natural numbers is a square only when they are equal. -/
+theorem eq_of_squarefree_of_isSquare_mul {a b : ℕ} (ha : Squarefree a) (hb : Squarefree b)
+    (hab : IsSquare (a * b)) : a = b := by
+  apply (Squarefree.ext_iff ha hb).2
+  intro p hp
+  obtain ⟨c, hc⟩ := hab
+  have hfac : a.factorization p + b.factorization p = 2 * c.factorization p := by
+    calc
+      a.factorization p + b.factorization p = (a * b).factorization p := by
+        have h := congrArg (fun f : ℕ →₀ ℕ => f p)
+          (factorization_mul ha.ne_zero hb.ne_zero).symm
+        simpa using h
+      _ = (c ^ 2).factorization p := by
+        simpa [pow_two, hc]
+      _ = 2 * c.factorization p := by simp [factorization_pow]
+  constructor
+  · intro hpa
+    have hfa : a.factorization p = 1 := factorization_eq_one_of_squarefree ha hp hpa
+    have hfb_le : b.factorization p ≤ 1 := hb.natFactorization_le_one p
+    have hfb : b.factorization p = 1 := by omega
+    exact (hp.dvd_iff_one_le_factorization hb.ne_zero).2 (by omega)
+  · intro hpb
+    have hfb : b.factorization p = 1 := factorization_eq_one_of_squarefree hb hp hpb
+    have hfa_le : a.factorization p ≤ 1 := ha.natFactorization_le_one p
+    have hfa : a.factorization p = 1 := by omega
+    exact (hp.dvd_iff_one_le_factorization ha.ne_zero).2 (by omega)
+
+end Nat
+
+namespace Real
+
+/-- In a number field, a non-rational element whose square is rational has trace zero. -/
+theorem trace_eq_zero_of_sq_ratCast {K : Type*} [Field K] [NumberField K] {x : K} {r : ℚ}
+    (hx2 : x ^ 2 = algebraMap ℚ K r) (hx : x ∉ (algebraMap ℚ K).range) :
+    Algebra.trace ℚ K x = 0 := by
+  have hmonic : (X ^ 2 - C r).Monic := Polynomial.monic_X_pow_sub_C r (by norm_num)
+  have haeval : aeval x (X ^ 2 - C r : ℚ[X]) = 0 := by simp [hx2]
+  have hdvd : minpoly ℚ x ∣ (X ^ 2 - C r) := minpoly.dvd ℚ x haeval
+  have hint : IsIntegral ℚ x := Algebra.IsIntegral.isIntegral x
+  have hne : (X ^ 2 - C r : ℚ[X]) ≠ 0 := Polynomial.X_pow_sub_C_ne_zero (by norm_num) r
+  have hdeg2 : (minpoly ℚ x).natDegree = 2 := by
+    have hle : (minpoly ℚ x).natDegree ≤ 2 := by
+      have := Polynomial.natDegree_le_of_dvd hdvd hne
+      simpa [Polynomial.natDegree_X_pow_sub_C] using this
+    have hge : 2 ≤ (minpoly ℚ x).natDegree := by
+      by_contra h
+      push_neg at h
+      interval_cases hh : (minpoly ℚ x).natDegree
+      · exact (minpoly.natDegree_pos hint).ne' hh
+      · exact hx (minpoly.natDegree_eq_one_iff.mp hh)
+    omega
+  have heq_rev : X ^ 2 - C r = minpoly ℚ x :=
+    Polynomial.eq_of_monic_of_dvd_of_natDegree_le
+      (p := minpoly ℚ x) (q := X ^ 2 - C r)
+      (minpoly.monic hint) hmonic hdvd
+      (by rw [hdeg2, Polynomial.natDegree_X_pow_sub_C])
+  have heq : minpoly ℚ x = X ^ 2 - C r := heq_rev.symm
+  rw [trace_eq_finrank_mul_minpoly_nextCoeff, heq]
+  have hnc : (X ^ 2 - C r : ℚ[X]).nextCoeff = 0 := by
+    rw [Polynomial.nextCoeff_of_natDegree_pos
+      (by rw [Polynomial.natDegree_X_pow_sub_C]; norm_num)]
+    simp [Polynomial.coeff_X_pow]
+  rw [hnc]
+  simp
+
+/-- Square roots of an injective finite family of squarefree natural numbers are
+linearly independent over the rationals. -/
+theorem linearIndependent_sqrt_squarefree {ι : Type*} [Fintype ι]
+    (s : ι → ℕ) (hs : ∀ i, Squarefree (s i)) (hinj : Function.Injective s) :
+    LinearIndependent ℚ (fun i => Real.sqrt (s i)) := by
+  let K : IntermediateField ℚ ℝ :=
+    IntermediateField.adjoin ℚ (Set.range fun i => Real.sqrt (s i))
+  have hfd : FiniteDimensional ℚ K := by
+    refine IntermediateField.finiteDimensional_adjoin ?_
+    rintro x ⟨i, rfl⟩
+    refine ⟨Polynomial.X ^ 2 - Polynomial.C (s i : ℚ),
+      Polynomial.monic_X_pow_sub_C _ two_ne_zero, ?_⟩
+    norm_num [← Polynomial.C_pow]
+  letI : NumberField K :=
+    { to_charZero := inferInstance
+      to_finiteDimensional := hfd }
+  let root (i : ι) : K :=
+    ⟨Real.sqrt (s i), IntermediateField.subset_adjoin ℚ _ ⟨i, rfl⟩⟩
+  have hroot_sq (i : ι) : (root i) ^ 2 = algebraMap ℚ K (s i : ℚ) := by
+    apply Subtype.ext
+    change (Real.sqrt (s i : ℝ)) ^ 2 = (s i : ℝ)
+    exact Real.sq_sqrt (Nat.cast_nonneg _)
+  have hmul_sq (i j : ι) : (root i * root j) ^ 2 = algebraMap ℚ K ((s i * s j : ℕ) : ℚ) := by
+    rw [mul_pow, hroot_sq, hroot_sq, ← map_mul]
+    norm_cast
+  have hmul_not_range {i j : ι} (hij : i ≠ j) :
+      root i * root j ∉ (algebraMap ℚ K).range := by
+    intro h
+    obtain ⟨q, hq⟩ := h
+    have hsq_rat : IsSquare (((s i * s j : ℕ) : ℚ)) := by
+      refine ⟨q, ?_⟩
+      apply (algebraMap ℚ K).injective
+      calc
+        algebraMap ℚ K (((s i * s j : ℕ) : ℚ)) = (root i * root j) ^ 2 :=
+          (hmul_sq i j).symm
+        _ = (algebraMap ℚ K q) ^ 2 := by rw [← hq]
+        _ = algebraMap ℚ K (q * q) := by rw [map_mul, pow_two]
+    have hsq_nat : IsSquare (s i * s j) := by
+      rwa [Rat.isSquare_natCast_iff] at hsq_rat
+    exact hij (hinj (Nat.eq_of_squarefree_of_isSquare_mul (hs i) (hs j) hsq_nat))
+  have htrace_mul_of_ne {i j : ι} (hij : i ≠ j) :
+      Algebra.trace ℚ K (root i * root j) = 0 :=
+    trace_eq_zero_of_sq_ratCast (hmul_sq i j) (hmul_not_range hij)
+  have htrace_self (i : ι) :
+      Algebra.trace ℚ K (root i * root i) = (finrank ℚ K : ℚ) * s i := by
+    convert congr_arg (fun x : K => Algebra.trace ℚ K x) (hroot_sq i) using 1
+    · rw [sq]
+    · rw [Algebra.trace_algebraMap]
+      norm_num [Algebra.smul_def]
+  have htraceMatrix :
+      Algebra.traceMatrix ℚ root = Matrix.diagonal (fun i => (finrank ℚ K : ℚ) * s i) := by
+    ext i j
+    by_cases h : i = j
+    · subst j
+      simp [Algebra.traceMatrix_apply, Algebra.traceForm_apply, htrace_self]
+    · simp [Algebra.traceMatrix_apply, Algebra.traceForm_apply, h,
+        htrace_mul_of_ne h]
+  have hdiscr : Algebra.discr ℚ root ≠ 0 := by
+    rw [Algebra.discr_def, htraceMatrix]
+    simp only [Matrix.det_diagonal]
+    exact Finset.prod_ne_zero_iff.mpr fun i _ =>
+      mul_ne_zero (Nat.cast_ne_zero.mpr (ne_of_gt Module.finrank_pos))
+        (Nat.cast_ne_zero.mpr (hs i).ne_zero)
+  have hrootK : LinearIndependent ℚ root := by
+    by_contra h
+    exact hdiscr (Algebra.discr_zero_of_not_linearIndependent ℚ h)
+  let inc : K →ₗ[ℚ] ℝ :=
+    { toFun := fun x => x.1
+      map_add' := fun _ _ => rfl
+      map_smul' := fun _ _ => rfl }
+  have hinc : LinearMap.ker inc = ⊥ := by
+    ext x
+    simp [inc]
+  have himage := hrootK.map' inc hinc
+  simpa [Function.comp_def, root, inc] using himage
+
+end Real
\ No newline at end of file
diff --git a/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean b/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean
new file mode 100644
index 0000000000..ec07c44b80
--- /dev/null
+++ b/FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean
@@ -0,0 +1,45 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.NumberTheory.SquarefreeRadical
+
+@[expose] public section
+
+noncomputable section
+
+namespace Real
+
+/-- Reciprocal square roots of an injective finite family of squarefree naturals are
+linearly independent over the rationals. -/
+theorem linearIndependent_inv_sqrt_squarefree {ι : Type*} [Fintype ι]
+    (s : ι → ℕ) (hs : ∀ i, Squarefree (s i)) (hinj : Function.Injective s) :
+    LinearIndependent ℚ (fun i => 1 / Real.sqrt (s i)) := by
+  have h := linearIndependent_sqrt_squarefree s hs hinj
+  let u : ι → ℚˣ := fun i =>
+    Units.mk0 ((s i : ℚ)⁻¹) (inv_ne_zero (by exact_mod_cast (hs i).ne_zero))
+  have hu := h.units_smul u
+  convert hu using 1
+  funext i
+  have hpos : (0 : ℝ) < s i := by exact_mod_cast (Nat.pos_of_ne_zero (hs i).ne_zero)
+  have hsqrt : Real.sqrt (s i) ≠ 0 := (Real.sqrt_pos.2 hpos).ne'
+  change 1 / Real.sqrt (s i) =
+    (((((s i : ℚ)⁻¹ : ℚ) : ℝ)) * Real.sqrt (s i))
+  rw [Rat.cast_inv, Rat.cast_natCast]
+  field_simp [hsqrt]
+  exact (Real.sq_sqrt hpos.le).symm
+
+end Real