The proof
Source
Main.lean · 28608 lines · 1.4 MB
Showing the first 500 of 28608 lines. The whole file is 1.4 MB; download it to read the rest.
/-
THIRD-PARTY SOURCE, LICENSE, AND MODIFICATION NOTICE
This file incorporates adapted source from Prime Number Theorem and More
(PrimeNumberTheoremAnd), a collaborative project organized by Alex Kontorovich
and Terence Tao, with contributions by the project's contributors.
Upstream repository: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
Upstream revision: a5154676af9aa3095150ee410cdda80555aa0642
Project citation: Alex Kontorovich and Terence Tao, Prime Number Theorem and More,
version 0.1.0, project launched January 9, 2024; see upstream CITATION.cff.
Adapted files, relative to the upstream PrimeNumberTheoremAnd directory:
Wiener.lean
Fourier.lean
Sobolev.lean
SmoothExistence.lean
Mathlib/Analysis/Asymptotics/Asymptotics.lean
Mathlib/Algebra/Notation/Support.lean
MODIFICATIONS: These files were ported from Lean 4.32.2 to Lean 4.33.1 and the
pinned Mathlib version; unused declarations and Architect/blueprint metadata were
removed; declaration attributes, options, and instance registrations were replaced
with ordinary definitions and closed concrete local dictionaries where needed;
imports were supplied by the trusted wrapper and the retained source was flattened
into this single file. The upstream authors are credited for that reused material,
not represented as authors or endorsers of this Erdos 653 submission.
The copied and adapted upstream material is distributed under Apache License 2.0.
The complete upstream license follows.
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
1. Definitions.
"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.
"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.
"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.
"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.
"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.
"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.
"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).
"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.
"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."
"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.
2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.
3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.
4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:
(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and
(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and
(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and
(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.
You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.
5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.
6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.
7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.
8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.
9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.
END OF TERMS AND CONDITIONS
APPENDIX: How to apply the Apache License to your work.
To apply the Apache License to your work, attach the following
boilerplate notice, with the fields enclosed by brackets "[]"
replaced with your own identifying information. (Don't include
the brackets!) The text should be enclosed in the appropriate
comment syntax for the file format. We also recommend that a
file or class name and description of purpose be included on the
same "printed page" as the copyright notice for easier
identification within third-party archives.
Copyright [yyyy] [name of copyright owner]
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
http://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.
-/
end Bounty
-- Source: DistanceCounts/Core.lean
section BodyFile000
/-! Positive pinned-distance counts and the epsilon formulation used by the construction. -/
noncomputable section
namespace DistanceCounts
/-- The genuine Euclidean plane, not the maximum-norm product `ℝ × ℝ`. -/
abbrev Point := EuclideanSpace ℝ (Fin 2)
/-- Distinct positive distances from a pin to the other points of a finite set. -/
def distanceValues (X : Finset Point) (p : Point) : Finset ℝ := by
classical
exact (X.erase p).image (fun q => dist p q)
/-- The number of distance values, rather than the number of neighbours. -/
def pinnedCount (X : Finset Point) (p : Point) : ℕ :=
(distanceValues X p).card
/-- The set of distinct pinned-distance counts occurring in a configuration. -/
def countSpectrum (X : Finset Point) : Finset ℕ := by
classical
exact X.image (pinnedCount X)
/-- The cardinality maximized in the question. -/
def diversity (X : Finset Point) : ℕ :=
(countSpectrum X).card
/-- The epsilon formulation of the question, exactly as stated by the user. -/
def Erdos653 : Prop :=
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ X : Finset Point, X.card = n ∧ (1 - ε) * (n : ℝ) ≤ (diversity X : ℝ)
/-- Coordinate formula useful for algebraic control-point calculations. -/
def sqDist (p q : Point) : ℝ :=
(p 0 - q 0) ^ 2 + (p 1 - q 1) ^ 2
end DistanceCounts
end
end BodyFile000
-- Source: DistanceCounts/GaussianNorm.lean
section BodyFile001
/-! Inert-prime residues and exact denominators of rational squared distances. -/
noncomputable section
namespace DistanceCounts.GaussianNorm
/-- The actual Gaussian residue class, not a coordinatewise surrogate. -/
def residue (p : ℕ) (z : GaussianInt) :
GaussianInt ⧸ Ideal.span ({(p : GaussianInt)} : Set GaussianInt) :=
Ideal.Quotient.mk _ z
/-- Being nonzero modulo a rational integer is exactly Gaussian nondivisibility. -/
theorem residue_ne_zero_iff (p : ℕ) (z : GaussianInt) :
residue p z ≠ 0 ↔ ¬(p : GaussianInt) ∣ z := by
simp only [residue, ne_eq, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
/-- Adding an integer-grid difference to `z/q` preserves every residue at a
prime factor of `q`. This is the arithmetic uniformity over pins in §3.3. -/
theorem residue_add_denominator_mul (p q : ℕ) (hpq : p ∣ q) (z w : GaussianInt) :
residue p (z + (q : GaussianInt) * w) = residue p z := by
apply Ideal.Quotient.eq.2
apply Ideal.mem_span_singleton.2
have hcast : (p : GaussianInt) ∣ (q : GaussianInt) := by
obtain ⟨k, hk⟩ := hpq
exact ⟨(k : GaussianInt), by exact_mod_cast hk⟩
simpa only [add_sub_cancel_left] using dvd_mul_of_dvd_left hcast w
/-- An inert rational prime divides a Gaussian norm precisely when it divides
its Gaussian argument. The forward implication uses primality and conjugation. -/
theorem inert_dvd_norm_iff (p : ℕ) (hp : p.Prime) (hp3 : p % 4 = 3)
(z : GaussianInt) : (p : ℤ) ∣ z.norm ↔ (p : GaussianInt) ∣ z := by
have hprime : Prime (p : GaussianInt) :=
@GaussianInt.prime_of_nat_prime_of_mod_four_eq_three p ⟨hp⟩ hp3
constructor
· intro h
have hc : (p : GaussianInt) ∣ (z.norm : GaussianInt) := by
simpa only [Int.cast_natCast] using
(Zsqrtd.intCast_dvd_intCast (p : ℤ) z.norm).2 h
rw [Zsqrtd.norm_eq_mul_conj] at hc
rcases hprime.dvd_or_dvd hc with hz | hz
· exact hz
· obtain ⟨w, hw⟩ := hz
refine ⟨star w, ?_⟩
simpa [mul_comm] using congrArg star hw
· intro h
apply (Zsqrtd.intCast_dvd_intCast (p : ℤ) z.norm).1
change (p : GaussianInt) ∣ (z.norm : GaussianInt)
rw [Zsqrtd.norm_eq_mul_conj]
exact dvd_mul_of_dvd_left h (star z)
/-- The natural-valued norm version used by rational reduction. -/
theorem inert_dvd_natNorm_iff (p : ℕ) (hp : p.Prime) (hp3 : p % 4 = 3)
(z : GaussianInt) : p ∣ z.norm.natAbs ↔ (p : GaussianInt) ∣ z := by
rw [← Int.natCast_dvd, inert_dvd_norm_iff p hp hp3 z]
/-- An inverse modulo an inert prime forces a nonzero Gaussian residue. -/
theorem not_dvd_of_inverse_residue (p : ℕ) (hp : p.Prime) (hp3 : p % 4 = 3)
(z w : GaussianInt) (hw : (p : GaussianInt) ∣ z * w - 1) :
¬(p : GaussianInt) ∣ z := by
intro hz
have hprime : Prime (p : GaussianInt) :=
@GaussianInt.prime_of_nat_prime_of_mod_four_eq_three p ⟨hp⟩ hp3
exact hprime.not_dvd_one ((dvd_sub_right (dvd_mul_of_dvd_left hz w)).1 hw)
/-- A unit in the quotient ring provides the required inverse congruence. -/
theorem not_dvd_of_isUnit_residue (p : ℕ) (hp : p.Prime) (hp3 : p % 4 = 3)
(z : GaussianInt) (hz : IsUnit (residue p z)) : ¬(p : GaussianInt) ∣ z := by
obtain ⟨u, hu⟩ := hz.exists_right_inv
obtain ⟨w, hw⟩ := Ideal.Quotient.mk_surjective u
have hzw : residue p (z * w) = 1 := by
change Ideal.Quotient.mk _ (z * w) = 1
rw [map_mul, hw]
exact hu
apply not_dvd_of_inverse_residue p hp hp3 z w
exact Ideal.mem_span_singleton.1
((Ideal.Quotient.mk_eq_one_iff_sub_mem (z * w)).1 hzw)
/-- Coprimality follows from the nonzero residues at all inert prime factors.
No squarefreeness is needed for this particular implication. -/
theorem coprime_norm_of_inert_factors (z : GaussianInt) (q : ℕ)
(h : ∀ p, p.Prime → p ∣ q → p % 4 = 3 ∧ ¬(p : GaussianInt) ∣ z) :
Nat.Coprime z.norm.natAbs q := by
apply Nat.Coprime.symm
apply Nat.coprime_of_dvd
intro p hp hpq hpn
exact (h p hp hpq).2 ((inert_dvd_natNorm_iff p hp (h p hp hpq).1 z).1 hpn)
/-- The squarefree denominator setting: a finite set of distinct inert primes. -/
theorem coprime_norm_prime_product (S : Finset ℕ) (z : GaussianInt)
(hprime : ∀ p ∈ S, p.Prime) (hinert : ∀ p ∈ S, p % 4 = 3)
(hres : ∀ p ∈ S, ¬(p : GaussianInt) ∣ z) :
Nat.Coprime z.norm.natAbs (∏ p ∈ S, p) := by
apply Nat.Coprime.prod_right
intro p hp
apply Nat.Coprime.symm
apply (hprime p hp).coprime_iff_not_dvd.2
intro hpn
exact hres p hp ((inert_dvd_natNorm_iff p (hprime p hp) (hinert p hp) z).1 hpn)
/-- Nonzero residue classes are a sufficient input to the product lemma. -/
theorem coprime_norm_prime_product_of_nonzero (S : Finset ℕ) (z : GaussianInt)
(hprime : ∀ p ∈ S, p.Prime) (hinert : ∀ p ∈ S, p % 4 = 3)
(hres : ∀ p ∈ S, residue p z ≠ 0) :
Nat.Coprime z.norm.natAbs (∏ p ∈ S, p) :=
coprime_norm_prime_product S z hprime hinert
(fun p hp => (residue_ne_zero_iff p z).1 (hres p hp))
/-- Unit residue classes give the same exact coprimality conclusion. -/
theorem coprime_norm_prime_product_of_units (S : Finset ℕ) (z : GaussianInt)
(hprime : ∀ p ∈ S, p.Prime) (hinert : ∀ p ∈ S, p % 4 = 3)
(hres : ∀ p ∈ S, IsUnit (residue p z)) :
Nat.Coprime z.norm.natAbs (∏ p ∈ S, p) :=
coprime_norm_prime_product S z hprime hinert
(fun p hp => not_dvd_of_isUnit_residue p (hprime p hp) (hinert p hp) z (hres p hp))
/-- The squared length of a Gaussian rational vector with denominator `q`. -/
def normQuotient (z : GaussianInt) (q : ℕ) : ℚ :=
(z.norm : ℚ) / (q : ℚ) ^ 2
/-- The displayed denominator is already reduced; this includes the integral
case `q = 1` and does not require the numerator to be positive. -/
theorem normQuotient_den (z : GaussianInt) (q : ℕ) (hq : 0 < q)
(hcop : Nat.Coprime z.norm.natAbs q) : (normQuotient z q).den = q ^ 2 := by
have hcop2 : Nat.Coprime z.norm.natAbs ((q ^ 2 : ℕ) : ℤ).natAbs := by
simpa only [Int.natAbs_natCast] using hcop.pow_right 2
have hden := Rat.den_div_eq_of_coprime
(a := z.norm) (b := ((q ^ 2 : ℕ) : ℤ)) (by positivity) hcop2
have heq : normQuotient z q = Rat.divInt z.norm ((q ^ 2 : ℕ) : ℤ) := by
simp only [normQuotient, Rat.divInt_eq_div, Int.cast_natCast, Nat.cast_pow, Int.cast_pow]
rw [heq]
exact_mod_cast hden
/-- Every numerator in the prescribed residue class has the same exact
squared denominator, regardless of the integer-grid displacement. -/
theorem normQuotient_den_prime_product_add_mul (S : Finset ℕ) (z w : GaussianInt)
(hprime : ∀ p ∈ S, p.Prime) (hinert : ∀ p ∈ S, p % 4 = 3)
(hres : ∀ p ∈ S, residue p z ≠ 0) :
(normQuotient (z + ((∏ p ∈ S, p : ℕ) : GaussianInt) * w)
(∏ p ∈ S, p)).den = (∏ p ∈ S, p) ^ 2 := by
apply normQuotient_den
· exact Finset.prod_pos (fun p hp => (hprime p hp).pos)
· apply coprime_norm_prime_product_of_nonzero S _ hprime hinert
intro p hp
rw [residue_add_denominator_mul p (∏ p ∈ S, p)
(Finset.dvd_prod_of_mem (fun p : ℕ => p) hp)]
exact hres p hp
/-- Equality of reduced squared lengths forces equality of their positive
Gaussian-rational denominators. -/
theorem denominator_eq_of_normQuotient_eq (z w : GaussianInt) (q r : ℕ)
(hq : 0 < q) (hr : 0 < r)
(hz : Nat.Coprime z.norm.natAbs q) (hw : Nat.Coprime w.norm.natAbs r)
(h : normQuotient z q = normQuotient w r) : q = r := by
have hd := congrArg Rat.den h
rw [normQuotient_den z q hq hz, normQuotient_den w r hr hw] at hd
nlinarith
/-- Passing to the real plane cannot identify different rational squared lengths. -/
theorem normQuotient_cast_eq_iff (z w : GaussianInt) (q r : ℕ) :
(normQuotient z q : ℝ) = (normQuotient w r : ℝ) ↔
normQuotient z q = normQuotient w r := by
constructor <;> intro h <;> exact_mod_cast h
/-- Distinct positive denominators have disjoint real squared-length palettes. -/
theorem normQuotient_real_ne (z w : GaussianInt) (q r : ℕ)
(hq : 0 < q) (hr : 0 < r) (hqr : q ≠ r)
(hz : Nat.Coprime z.norm.natAbs q) (hw : Nat.Coprime w.norm.natAbs r) :
(normQuotient z q : ℝ) ≠ (normQuotient w r : ℝ) := by
intro h
exact hqr (denominator_eq_of_normQuotient_eq z w q r hq hr hz hw
((normQuotient_cast_eq_iff z w q r).1 h))
/-- The full real palette at a fixed reduced denominator. -/
def squaredPalette (q : ℕ) : Set ℝ :=
{d | ∃ z : GaussianInt, Nat.Coprime z.norm.natAbs q ∧ d = (normQuotient z q : ℝ)}
theorem squaredPalette_disjoint (q r : ℕ) (hq : 0 < q) (hr : 0 < r) (hqr : q ≠ r) :
Disjoint (squaredPalette q) (squaredPalette r) := by
apply Set.disjoint_left.2
rintro d ⟨z, hz, hdz⟩ ⟨w, hw, hdw⟩
exact normQuotient_real_ne z w q r hq hr hqr hz hw (hdz.symm.trans hdw)
/-- Distinct sets of prime factors really give different product denominators. -/
theorem prime_product_ne (S T : Finset ℕ)
(hS : ∀ p ∈ S, p.Prime) (hT : ∀ p ∈ T, p.Prime) (hne : S ≠ T) :
(∏ p ∈ S, p) ≠ ∏ p ∈ T, p := by
intro h
apply hne
have hf := congrArg Nat.primeFactors h
simpa only [Nat.primeFactors_prod hS, Nat.primeFactors_prod hT] using hf
/-- The exact denominator-prime-set separation invoked in Proof.md §4.1. -/
theorem prime_product_squaredPalette_disjoint (S T : Finset ℕ)
(hS : ∀ p ∈ S, p.Prime) (hT : ∀ p ∈ T, p.Prime) (hne : S ≠ T) :
Disjoint (squaredPalette (∏ p ∈ S, p)) (squaredPalette (∏ p ∈ T, p)) := by
apply squaredPalette_disjoint
· exact Finset.prod_pos (fun p hp => (hS p hp).pos)
· exact Finset.prod_pos (fun p hp => (hT p hp).pos)
· exact prime_product_ne S T hS hT hne
/-- Coordinate differences of the form `z/q` have the rational norm quotient
as their genuine Euclidean squared-distance formula. -/
theorem sqDist_eq_normQuotient (a b : DistanceCounts.Point) (z : GaussianInt) (q : ℕ)
(hre : a 0 - b 0 = (z.re : ℝ) / q)
(him : a 1 - b 1 = (z.im : ℝ) / q) :
DistanceCounts.sqDist a b = (normQuotient z q : ℝ) := by
simp only [DistanceCounts.sqDist, hre, him, normQuotient, Rat.cast_div,
Rat.cast_intCast, Rat.cast_pow, Rat.cast_natCast, div_pow]
rw [← add_div]
congr 1
simp only [Zsqrtd.norm, Int.cast_sub, Int.cast_mul, Int.cast_neg, Int.cast_one]
ring
end DistanceCounts.GaussianNorm
end
end BodyFile001
-- Source: DistanceCounts/OffsetSeparation.lean
Provenance