The proof
Erdős problem 96
If points in form a convex polygon then there are many pairs which are distance apart.Source
Main.lean · 2338 lines · 103.0 kB
/-!
# Superlinearly many unit distances in convex position
Authors: Liam Kruer <[email protected]>
Jensen Kohlmeyer <[email protected]>
OpenAI Codex provided substantial assistance with the mathematical exploration,
construction, proofs, formalization, verification, and manuscript preparation.
The authors are responsible for the content.
Complete proof declarations for the supplied counterexample target.
The task provides the imports and enclosing Bounty namespace.
-/
open _root_.Erdos96
/- ## Angle -/
section OriginalAngle
/- Calculus of the angle subtended by a unit chord at the origin. -/
namespace Proof
noncomputable def chordCos (r s : ℝ) : ℝ := (r ^ 2 + s ^ 2 - 1) / (2 * r * s)
noncomputable def chordCosLeft (r s : ℝ) : ℝ := (r ^ 2 - s ^ 2 + 1) / (2 * r ^ 2 * s)
noncomputable def chordCosMixed (r s : ℝ) : ℝ := -(r ^ 2 + s ^ 2 + 1) / (2 * r ^ 2 * s ^ 2)
noncomputable def chordAngle (r s : ℝ) : ℝ := Real.arccos (chordCos r s)
theorem chordCos_comm (r s : ℝ) : chordCos r s = chordCos s r := by
unfold chordCos
congr 1 <;> ring
theorem hasDerivAt_chordCos_left {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
HasDerivAt (fun x => chordCos x s) (chordCosLeft r s) r := by
have hnum := (((hasDerivAt_id r).pow 2).add_const (s ^ 2)).sub_const 1
have hden := ((hasDerivAt_id r).const_mul 2).mul_const s
convert! hnum.div hden (mul_ne_zero (mul_ne_zero two_ne_zero hr) hs) using 1
dsimp only [id_eq, Pi.pow_apply]
unfold chordCosLeft
field_simp [hr, hs]
ring
theorem hasDerivAt_chordCos_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
HasDerivAt (chordCos r) (chordCosLeft s r) s := by
simpa only [chordCos_comm] using hasDerivAt_chordCos_left hs hr
theorem hasDerivAt_chordCosLeft_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
HasDerivAt (chordCosLeft r) (chordCosMixed r s) s := by
have hnum := (((hasDerivAt_id s).pow 2).const_sub (r ^ 2)).add_const 1
have hden := (hasDerivAt_id s).const_mul (2 * r ^ 2)
convert! hnum.div hden (mul_ne_zero (mul_ne_zero two_ne_zero (pow_ne_zero 2 hr)) hs) using 1
dsimp only [id_eq, Pi.pow_apply]
unfold chordCosMixed
field_simp [hr, hs]
ring
theorem chordCos_mixed_identity {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
-(chordCosMixed r s * (1 - chordCos r s ^ 2) +
chordCos r s * chordCosLeft r s * chordCosLeft s r) = 1 / (r ^ 2 * s ^ 2) := by
unfold chordCosMixed chordCos chordCosLeft
field_simp [hr, hs]
ring
noncomputable def chordAngleLeft (r s : ℝ) : ℝ :=
-chordCosLeft r s / Real.sqrt (1 - chordCos r s ^ 2)
theorem chord_discriminant_pos {r s : ℝ}
(hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
0 < 1 - chordCos r s ^ 2 := by
nlinarith
theorem hasDerivAt_chordAngle_left {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
(hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
HasDerivAt (fun x => chordAngle x s) (chordAngleLeft r s) r := by
convert! (Real.hasDerivAt_arccos (ne_of_gt hl) (ne_of_lt hu)).comp r
(hasDerivAt_chordCos_left hr hs) using 1
unfold chordAngleLeft
ring
theorem hasDerivAt_chordAngleLeft_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
(hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
HasDerivAt (chordAngleLeft r)
(1 / (r ^ 2 * s ^ 2 * Real.sqrt (1 - chordCos r s ^ 2) ^ 3)) s := by
have hq := chord_discriminant_pos hl hu
have hsqrt : Real.sqrt (1 - chordCos r s ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hq)
have hsquare := Real.sq_sqrt hq.le
have hnum := (hasDerivAt_chordCosLeft_right hr hs).neg
have hden := (((hasDerivAt_chordCos_right hr hs).pow 2).const_sub 1).sqrt (ne_of_gt hq)
convert! hnum.div hden hsqrt using 1
have hid := chordCos_mixed_identity hr hs
dsimp only [id_eq, Pi.pow_apply, Pi.neg_apply, Nat.cast_ofNat, Nat.reduceSub, pow_one, one_mul, mul_one]
field_simp [hr, hs, hsqrt] at hid ⊢
rw [hsquare]
linear_combination -hid
theorem chordAngle_mixed_positive {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
(hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
0 < deriv (chordAngleLeft r) s := by
rw [(hasDerivAt_chordAngleLeft_right hr hs hl hu).deriv]
have := Real.sqrt_pos.mpr (chord_discriminant_pos hl hu)
positivity
end Proof
end OriginalAngle
/- ## GenericAngles -/
section OriginalGenericAngles
/- Local separation of finite linear combinations of edge angles. -/
namespace Proof
open Set Filter
open scoped Topology
def ChordFeasible (r s : ℝ) : Prop :=
r ≠ 0 ∧ s ≠ 0 ∧ -1 < chordCos r s ∧ chordCos r s < 1
theorem chordAngle_rectangle_strict {a b c d : ℝ} (hab : a < b) (hcd : c < d)
(hf : ∀ x ∈ Icc a b, ∀ y ∈ Icc c d, ChordFeasible x y) :
0 < chordAngle b d - chordAngle a d - chordAngle b c + chordAngle a c := by
have hm : ∀ x ∈ Icc a b, chordAngleLeft x c < chordAngleLeft x d := by
intro x hx
have hmono : StrictMonoOn (chordAngleLeft x) (Icc c d) := by
apply strictMonoOn_of_deriv_pos (convex_Icc c d)
· intro y hy
obtain ⟨hr, hs, hl, hu⟩ := hf x hx y hy
exact (hasDerivAt_chordAngleLeft_right hr hs hl hu).continuousAt.continuousWithinAt
· intro y hy
obtain ⟨hr, hs, hl, hu⟩ := hf x hx y (interior_subset hy)
exact chordAngle_mixed_positive hr hs hl hu
exact hmono ⟨le_rfl, hcd.le⟩ ⟨hcd.le, le_rfl⟩ hcd
have hder : ∀ x ∈ Icc a b,
HasDerivAt (fun t => chordAngle t d - chordAngle t c)
(chordAngleLeft x d - chordAngleLeft x c) x := by
intro x hx
obtain ⟨hrd, hsd, hld, hud⟩ := hf x hx d ⟨hcd.le, le_rfl⟩
obtain ⟨hrc, hsc, hlc, huc⟩ := hf x hx c ⟨le_rfl, hcd.le⟩
exact (hasDerivAt_chordAngle_left hrd hsd hld hud).sub
(hasDerivAt_chordAngle_left hrc hsc hlc huc)
have hmono : StrictMonoOn (fun t => chordAngle t d - chordAngle t c) (Icc a b) := by
apply strictMonoOn_of_deriv_pos (convex_Icc a b)
· intro x hx
exact (hder x hx).continuousAt.continuousWithinAt
· intro x hx
rw [(hder x (interior_subset hx)).deriv]
exact sub_pos.mpr (hm x (interior_subset hx))
have hh := hmono ⟨le_rfl, hab.le⟩ ⟨hab.le, le_rfl⟩ hab
linarith
noncomputable def matrixSum {L P : Type*} [Fintype L] [Fintype P]
(f : L → P → ℝ → ℝ → ℝ) (r : L → ℝ) (s : P → ℝ) : ℝ :=
∑ i, ∑ j, f i j (r i) (s j)
theorem matrix_rectangle {L P : Type*} [Fintype L] [Fintype P]
[DecidableEq L] [DecidableEq P] (f : L → P → ℝ → ℝ → ℝ)
(r : L → ℝ) (s : P → ℝ) (i : L) (j : P) (x y : ℝ) :
matrixSum f (Function.update r i x) (Function.update s j y) -
matrixSum f r (Function.update s j y) -
matrixSum f (Function.update r i x) s + matrixSum f r s =
f i j x y - f i j (r i) y - f i j x (s j) + f i j (r i) (s j) := by
let g := fun a b => f a b (Function.update r i x a) (Function.update s j y b) -
f a b (r a) (Function.update s j y b) -
f a b (Function.update r i x a) (s b) + f a b (r a) (s b)
have he : matrixSum f (Function.update r i x) (Function.update s j y) -
matrixSum f r (Function.update s j y) -
matrixSum f (Function.update r i x) s + matrixSum f r s = ∑ a, ∑ b, g a b := by
simp only [matrixSum, g, Finset.sum_add_distrib, Finset.sum_sub_distrib]
rw [he, Finset.sum_eq_single i]
· rw [Finset.sum_eq_single j]
· simp [g]
· intro b _ hbj
simp [g, Function.update_of_ne hbj]
· simp
· intro a _ hai
apply Finset.sum_eq_zero
intro b _
simp [g, Function.update_of_ne hai]
· simp
theorem finite_avoidance {X K Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] [Zero Y]
(f : K → X → Y) (U : Set X) (hU : IsOpen U) (hne : U.Nonempty)
(hc : ∀ k, ContinuousOn (f k) U)
(hnc : ∀ k, ∀ V : Set X, V ⊆ U → IsOpen V → V.Nonempty → ∃ x ∈ V, f k x ≠ 0)
(s : Finset K) : ∃ x ∈ U, ∀ k ∈ s, f k x ≠ 0 := by
classical
suffices ∃ V : Set X, V ⊆ U ∧ IsOpen V ∧ V.Nonempty ∧
∀ x ∈ V, ∀ k ∈ s, f k x ≠ 0 by
obtain ⟨V, hVU, hVo, ⟨x, hx⟩, hv⟩ := this
exact ⟨x, hVU hx, hv x hx⟩
induction s using Finset.induction_on with
| empty => exact ⟨U, subset_rfl, hU, hne, by simp⟩
| @insert k s hks ih =>
obtain ⟨V, hVU, hVo, hVne, hV⟩ := ih
obtain ⟨x, hx, hkx⟩ := hnc k V hVU hVo hVne
refine ⟨V ∩ (f k) ⁻¹' ({0}ᶜ), inter_subset_left.trans hVU,
(hc k |>.mono hVU).isOpen_inter_preimage hVo isClosed_singleton.isOpen_compl,
⟨x, hx, hkx⟩, ?_⟩
intro y hy j hj
rcases Finset.mem_insert.mp hj with rfl | hj
· exact hy.2
· exact hV y hy.1 j hj
theorem coordinate_rectangle {L P : Type*} [DecidableEq L] [DecidableEq P]
{U : Set ((L → ℝ) × (P → ℝ))} (hU : IsOpen U) {z : (L → ℝ) × (P → ℝ)}
(hz : z ∈ U) (i : L) (j : P) :
∃ b d : ℝ, z.1 i < b ∧ z.2 j < d ∧
∀ x ∈ Icc (z.1 i) b, ∀ y ∈ Icc (z.2 j) d,
(Function.update z.1 i x, Function.update z.2 j y) ∈ U := by
let F := fun xy : ℝ × ℝ => (Function.update z.1 i xy.1, Function.update z.2 j xy.2)
have hF : Continuous F := by unfold F; fun_prop
have hmem : (z.1 i, z.2 j) ∈ F ⁻¹' U := by simpa [F] using hz
obtain ⟨A, hA, B, hB, hAB⟩ := mem_nhds_prod_iff.mp ((hU.preimage hF).mem_nhds hmem)
obtain ⟨a, b, hab, hAsub⟩ := mem_nhds_iff_exists_Ioo_subset.mp hA
obtain ⟨c, d, hcd, hBsub⟩ := mem_nhds_iff_exists_Ioo_subset.mp hB
refine ⟨(z.1 i + b) / 2, (z.2 j + d) / 2, by linarith [hab.2], by linarith [hcd.2], ?_⟩
intro x hx y hy
change (x, y) ∈ F ⁻¹' U
apply hAB
constructor
· apply hAsub
constructor <;> linarith [hab.1, hab.2, hx.1, hx.2]
· apply hBsub
constructor <;> linarith [hcd.1, hcd.2, hy.1, hy.2]
theorem angle_sum_not_constant {L P : Type*} [Fintype L] [Fintype P]
[DecidableEq L] [DecidableEq P] (c : L → P → ℝ) (i : L) (j : P) (hc : c i j ≠ 0)
(U : Set ((L → ℝ) × (P → ℝ))) (hU : IsOpen U) (hne : U.Nonempty)
(hf : ∀ z ∈ U, ChordFeasible (z.1 i) (z.2 j)) (k : ℝ) :
∃ z ∈ U, matrixSum (fun a b x y => c a b * chordAngle x y) z.1 z.2 ≠ k := by
by_contra hnone
push Not at hnone
obtain ⟨z, hz⟩ := hne
obtain ⟨b, d, hb, hd, hrect⟩ := coordinate_rectangle hU hz i j
have hfeas : ∀ x ∈ Icc (z.1 i) b, ∀ y ∈ Icc (z.2 j) d, ChordFeasible x y := by
intro x hx y hy
simpa using hf _ (hrect x hx y hy)
have hpositive := chordAngle_rectangle_strict hb hd hfeas
have h00 := hnone z hz
have h11 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ d ⟨hd.le, le_rfl⟩)
have h01 := hnone _ (hrect (z.1 i) ⟨le_rfl, hb.le⟩ d ⟨hd.le, le_rfl⟩)
have h10 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ (z.2 j) ⟨le_rfl, hd.le⟩)
simp only [Function.update_eq_self] at h01 h10
have hid := matrix_rectangle (fun a b x y => c a b * chordAngle x y) z.1 z.2 i j b d
rw [h00, h11, h01, h10] at hid
have hzero : c i j * (chordAngle b d - chordAngle (z.1 i) d -
chordAngle b (z.2 j) + chordAngle (z.1 i) (z.2 j)) = 0 := by linear_combination -hid
exact (mul_ne_zero hc (ne_of_gt hpositive)) hzero
theorem weighted_angles_continuousAt {L P : Type*} [Fintype L] [Fintype P]
(c : L → P → ℝ) (z : (L → ℝ) × (P → ℝ))
(hr : ∀ i, z.1 i ≠ 0) (hs : ∀ j, z.2 j ≠ 0) :
ContinuousAt (fun u => matrixSum (fun i j x y => c i j * chordAngle x y) u.1 u.2) z := by
unfold matrixSum chordAngle chordCos
fun_prop (disch := aesop)
theorem finite_angle_avoidance {L P K : Type*} [Fintype L] [Fintype P]
[DecidableEq L] [DecidableEq P]
(c : K → L → P → ℝ) (offset : K → ℝ) (U : Set ((L → ℝ) × (P → ℝ)))
(hU : IsOpen U) (hne : U.Nonempty)
(hnz : ∀ z ∈ U, (∀ i, z.1 i ≠ 0) ∧ (∀ j, z.2 j ≠ 0))
(hc : ∀ k, ∃ i j, c k i j ≠ 0)
(hfeas : ∀ k i j, c k i j ≠ 0 → ∀ z ∈ U, ChordFeasible (z.1 i) (z.2 j))
(s : Finset K) : ∃ z ∈ U, ∀ k ∈ s,
matrixSum (fun i j x y => c k i j * chordAngle x y) z.1 z.2 ≠ offset k := by
let f := fun (k : K) (z : (L → ℝ) × (P → ℝ)) =>
matrixSum (fun i j x y => c k i j * chordAngle x y) z.1 z.2 - offset k
have hcont : ∀ k, ContinuousOn (f k) U := by
intro k z hz
exact ((weighted_angles_continuousAt (c k) z (hnz z hz).1 (hnz z hz).2).sub
continuousAt_const).continuousWithinAt
have hnc : ∀ k, ∀ V : Set ((L → ℝ) × (P → ℝ)),
V ⊆ U → IsOpen V → V.Nonempty → ∃ z ∈ V, f k z ≠ 0 := by
intro k V hVU hVo hVne
obtain ⟨i, j, hij⟩ := hc k
obtain ⟨z, hz, hh⟩ := angle_sum_not_constant (c k) i j hij V hVo hVne
(fun z hz => hfeas k i j hij z (hVU hz)) (offset k)
exact ⟨z, hz, sub_ne_zero.mpr hh⟩
obtain ⟨z, hz, hh⟩ := finite_avoidance f U hU hne hcont hnc s
exact ⟨z, hz, fun k hk => sub_ne_zero.mp (hh k hk)⟩
end Proof
end OriginalGenericAngles
/- ## SeedAlgebra -/
section OriginalSeedAlgebra
/- Polynomial identities for the two classes of incidence seeds. -/
namespace Proof
noncomputable section
def lineC (x t : ℝ) : ℝ := x ^ 2 + t / 2
def pointD (x t : ℝ) : ℝ := -x ^ 2 + t / 2
def lineSeed (ε x t : ℝ) : ℂ := ⟨ε * x, -1 / 2 + ε ^ 2 * lineC x t⟩
def pointSeed (ε x t : ℝ) : ℂ := ⟨-ε * x, 1 / 2 + ε ^ 2 * pointD x t⟩
def support (a b : ℂ) : ℝ := a.re * (b.re - a.re) + a.im * (b.im - a.im)
theorem line_support_identity (ε x t y u : ℝ) :
support (lineSeed ε x t) (lineSeed ε y u) =
ε ^ 2 * (-(y - x) ^ 2 / 2 - (u - t) / 4) +
ε ^ 4 * lineC x t * (lineC y u - lineC x t) := by
simp only [support, lineSeed, lineC]
ring
theorem point_support_identity (ε x t y u : ℝ) :
support (pointSeed ε x t) (pointSeed ε y u) =
ε ^ 2 * (-(y - x) ^ 2 / 2 + (u - t) / 4) +
ε ^ 4 * pointD x t * (pointD y u - pointD x t) := by
simp only [support, pointSeed, pointD]
ring
theorem line_normSq (ε x t : ℝ) :
Complex.normSq (lineSeed ε x t) =
1 / 4 - ε ^ 2 * t / 2 + ε ^ 4 * (lineC x t) ^ 2 := by
simp only [Complex.normSq_apply, lineSeed, lineC]
ring
theorem point_normSq (ε x t : ℝ) :
Complex.normSq (pointSeed ε x t) =
1 / 4 + ε ^ 2 * t / 2 + ε ^ 4 * (pointD x t) ^ 2 := by
simp only [Complex.normSq_apply, pointSeed, pointD]
ring
theorem incidence_distance_identity (ε x t y u : ℝ)
(h : u - t = (y - x) ^ 2) :
Complex.normSq (pointSeed ε y u - lineSeed ε x t) =
1 + ε ^ 4 * (pointD y u - lineC x t) ^ 2 := by
simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im,
pointSeed, lineSeed, pointD, lineC]
linear_combination ε ^ 2 * h
theorem signed_digit_margin {x t : ℝ}
(h : |t| < (50 / 27 : ℝ) * x ^ 2) :
-x ^ 2 / 2 - t / 4 < -x ^ 2 / 27 ∧
-x ^ 2 / 2 + t / 4 < -x ^ 2 / 27 := by
rcases abs_lt.mp h with ⟨hl, hu⟩
constructor <;> linarith
end
end Proof
end OriginalSeedAlgebra
/- ## RadialGeometry -/
section OriginalRadialGeometry
/- Strict radial support, rotations, and their convexity consequences. -/
namespace Proof
open scoped InnerProductSpace
theorem support_eq_inner (a b : ℂ) : support a b = ⟪a, b - a⟫_ℝ := by
simp only [support, Complex.inner, Complex.mul_re, Complex.sub_re,
Complex.sub_im, Complex.conj_re, Complex.conj_im]
ring
theorem support_eq_normSq (a b : ℂ) :
2 * support a b = Complex.normSq b - Complex.normSq a - Complex.normSq (b - a) := by
simp only [support, Complex.normSq_apply, Complex.sub_re, Complex.sub_im]
ring
theorem support_negative_of_equal_norm {a b : ℂ} (hne : a ≠ b)
(hnorm : ‖a‖ = ‖b‖) : support a b < 0 := by
have heq : Complex.normSq a = Complex.normSq b := by
simpa only [Complex.normSq_eq_norm_sq] using congrArg (fun r : ℝ => r ^ 2) hnorm
have hp : 0 < Complex.normSq (b - a) := Complex.normSq_pos.mpr (sub_ne_zero.mpr hne.symm)
have := support_eq_normSq a b
linarith
theorem convexIndependent_of_support {ι : Type*} (p : ι → ℂ)
(h : ∀ i j, i ≠ j → support (p i) (p j) < 0) : ConvexIndependent ℝ p := by
intro s i hi
by_contra hnot
have hs : p '' s ⊆ {z : ℂ | ⟪p i, z⟫_ℝ < ⟪p i, p i⟫_ℝ} := by
rintro z ⟨j, hj, rfl⟩
have hij : i ≠ j := fun he => hnot (he.symm ▸ hj)
have hh := h i j hij
rw [support_eq_inner, inner_sub_right] at hh
exact sub_neg.mp hh
have hc : Convex ℝ {z : ℂ | ⟪p i, z⟫_ℝ < ⟪p i, p i⟫_ℝ} :=
convex_halfSpace_lt ((innerₗ ℂ) (p i)).isLinear _
have hz := (convexHull_min hs hc) hi
exact lt_irrefl _ (show ⟪p i, p i⟫_ℝ < ⟪p i, p i⟫_ℝ from hz)
theorem support_mul (a b w : ℂ) :
support (a * w) (b * w) = Complex.normSq w * support a b := by
simp only [support, Complex.mul_re, Complex.mul_im, Complex.normSq_apply]
ring
theorem norm_subset_prod {ι : Type*} (s : Finset ι) (w : ι → ℂ)
(hw : ∀ i ∈ s, ‖w i‖ = 1) : ‖∏ i ∈ s, w i‖ = 1 := by
rw [norm_prod]
exact Finset.prod_eq_one hw
theorem norm_prod_sub_one_le {ι : Type*} (s : Finset ι) (w : ι → ℂ)
(hw : ∀ i ∈ s, ‖w i‖ = 1) :
‖(∏ i ∈ s, w i) - 1‖ ≤ ∑ i ∈ s, ‖w i - 1‖ := by
classical
induction s using Finset.induction_on with
| empty => simp
| @insert i s hi ih =>
rw [Finset.prod_insert hi, Finset.sum_insert hi]
have hwi := hw i (Finset.mem_insert_self i s)
have hws : ∀ j ∈ s, ‖w j‖ = 1 := fun j hj => hw j (Finset.mem_insert_of_mem hj)
calc
‖w i * (∏ j ∈ s, w j) - 1‖ =
‖w i * ((∏ j ∈ s, w j) - 1) + (w i - 1)‖ := by congr 1; ring
_ ≤ ‖w i * ((∏ j ∈ s, w j) - 1)‖ + ‖w i - 1‖ := norm_add_le _ _
_ = ‖(∏ j ∈ s, w j) - 1‖ + ‖w i - 1‖ := by rw [norm_mul, hwi, one_mul]
_ ≤ ‖w i - 1‖ + ∑ j ∈ s, ‖w j - 1‖ := by linarith [ih hws]
theorem support_change_same_norm (a b a' b' : ℂ) (hn : ‖a'‖ = ‖a‖) :
|support a' b' - support a b| ≤
‖a' - a‖ * ‖b'‖ + ‖a‖ * ‖b' - b‖ := by
have he : support a' b' - support a b =
⟪a' - a, b'⟫_ℝ + ⟪a, b' - b⟫_ℝ := by
simp only [support_eq_inner, inner_sub_left, inner_sub_right,
real_inner_self_eq_norm_sq, hn]
ring
rw [he]
exact (abs_add_le _ _).trans (add_le_add (abs_real_inner_le_norm _ _) (abs_real_inner_le_norm _ _))
theorem rotated_support_bound {a b u v : ℂ} {H : ℝ}
(ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
(hU : ‖u - 1‖ ≤ H) (hV : ‖v - 1‖ ≤ H) :
support (a * u) (b * v) ≤ support a b + 2 * H := by
have hH : 0 ≤ H := (norm_nonneg _).trans hU
have hau : ‖a * u‖ = ‖a‖ := by rw [norm_mul, hu, mul_one]
have hbv : ‖b * v‖ = ‖b‖ := by rw [norm_mul, hv, mul_one]
have hdiffa : ‖a * u - a‖ ≤ H := by
rw [← mul_sub_one, norm_mul]
exact (mul_le_mul ha hU (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
have hdiffb : ‖b * v - b‖ ≤ H := by
rw [← mul_sub_one, norm_mul]
exact (mul_le_mul hb hV (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
have hh := support_change_same_norm a b (a * u) (b * v) hau
rw [hbv] at hh
have h1 : ‖a * u - a‖ * ‖b‖ ≤ H := by
exact (mul_le_mul hdiffa hb (norm_nonneg _) hH).trans_eq (mul_one H)
have h2 : ‖a‖ * ‖b * v - b‖ ≤ H := by
exact (mul_le_mul ha hdiffb (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
have := le_abs_self (support (a * u) (b * v) - support a b)
linarith
end Proof
end OriginalRadialGeometry
/- ## Amplification -/
section OriginalAmplification
/- Amplification by products of unit complex numbers. -/
namespace Proof
noncomputable section
def subsetProduct {E : Type*} (w : E → ℂ) (S : Finset E) : ℂ := ∏ e ∈ S, w e
def rotatedCopy {I E : Type*} (b : I → ℂ) (w : E → ℂ) (x : I × Finset E) : ℂ :=
b x.1 * subsetProduct w x.2
theorem subsetProduct_norm {E : Type*} (w : E → ℂ) (hw : ∀ e, ‖w e‖ = 1)
(S : Finset E) : ‖subsetProduct w S‖ = 1 :=
norm_subset_prod S w (fun e _ => hw e)
theorem subsetProduct_close {E : Type*} [Fintype E] (w : E → ℂ)
(hw : ∀ e, ‖w e‖ = 1) (S : Finset E) :
‖subsetProduct w S - 1‖ ≤ ∑ e, ‖w e - 1‖ := by
classical
refine (norm_prod_sub_one_le S w (fun e _ => hw e)).trans ?_
exact Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ S)
(fun e _ _ => norm_nonneg (w e - 1))
theorem rotatedCopy_injective {I E : Type*} (b : I → ℂ) (w : E → ℂ)
(hb : ∀ i, b i ≠ 0) (hn : Function.Injective (fun i => ‖b i‖))
(hw : ∀ e, ‖w e‖ = 1) (hprod : Function.Injective (subsetProduct w)) :
Function.Injective (rotatedCopy b w) := by
rintro ⟨i, S⟩ ⟨j, T⟩ he
have hnorm := congrArg norm he
simp only [rotatedCopy, norm_mul, subsetProduct_norm w hw, mul_one] at hnorm
have hij := hn hnorm
subst j
have hST := hprod (mul_left_cancel₀ (hb i) he)
exact Prod.ext rfl hST
theorem rotatedCopy_convexIndependent {I E : Type*} [Fintype E]
(b : I → ℂ) (w : E → ℂ) (hb : ∀ i, b i ≠ 0)
(hn : Function.Injective (fun i => ‖b i‖)) (hb1 : ∀ i, ‖b i‖ ≤ 1)
(hw : ∀ e, ‖w e‖ = 1) (hprod : Function.Injective (subsetProduct w))
(hsupport : ∀ i j, i ≠ j → support (b i) (b j) < -2 * ∑ e, ‖w e - 1‖) :
ConvexIndependent ℝ (rotatedCopy b w) := by
apply convexIndependent_of_support
rintro ⟨i, S⟩ ⟨j, T⟩ hne
by_cases hij : i = j
· subst j
apply support_negative_of_equal_norm
· exact fun h => hne (rotatedCopy_injective b w hb hn hw hprod h)
· simp only [rotatedCopy, norm_mul, subsetProduct_norm w hw]
· have hbound := rotated_support_bound (hb1 i) (hb1 j)
(subsetProduct_norm w hw S) (subsetProduct_norm w hw T)
(subsetProduct_close w hw S) (subsetProduct_close w hw T)
dsimp [rotatedCopy]
linarith [hsupport i j hij]
theorem rotatedCopy_unit_edge {I E : Type*} [DecidableEq E]
(b : I → ℂ) (w : E → ℂ) (hw : ∀ e, ‖w e‖ = 1)
(i j : I) (e : E) (he : ‖b i - b j * w e‖ = 1)
(S : Finset E) (hS : e ∉ S) :
dist (rotatedCopy b w (i, S)) (rotatedCopy b w (j, insert e S)) = 1 := by
simp only [rotatedCopy, subsetProduct, Finset.prod_insert hS, dist_eq_norm]
rw [show b i * (∏ f ∈ S, w f) - b j * (w e * ∏ f ∈ S, w f) =
(b i - b j * w e) * ∏ f ∈ S, w f by ring]
rw [norm_mul, he, norm_subset_prod S w (fun f _ => hw f), one_mul]
end
end Proof
end OriginalAmplification
/- ## GenericRotations -/
section OriginalGenericRotations
/- Distinct subset products of correction rotations in every feasible open radius set. -/
namespace Proof
open Set Filter
open scoped Topology
noncomputable section
def edgeAngleSum {L P E : Type*} [Fintype E] (l : E → L) (p : E → P)
(a : E → ℝ) (z : (L → ℝ) × (P → ℝ)) : ℝ :=
∑ e, a e * chordAngle (z.1 (l e)) (z.2 (p e))
theorem edge_angle_rectangle {L P E : Type*} [Fintype E]
[DecidableEq L] [DecidableEq P] [DecidableEq E]
(l : E → L) (p : E → P) (hij : Function.Injective (fun e => (l e, p e)))
(a : E → ℝ) (r : L → ℝ) (s : P → ℝ) (e : E) (x y : ℝ) :
edgeAngleSum l p a (Function.update r (l e) x, Function.update s (p e) y) -
edgeAngleSum l p a (r, Function.update s (p e) y) -
edgeAngleSum l p a (Function.update r (l e) x, s) + edgeAngleSum l p a (r, s) =
a e * (chordAngle x y - chordAngle (r (l e)) y - chordAngle x (s (p e)) +
chordAngle (r (l e)) (s (p e))) := by
let g := fun f => a f * (chordAngle (Function.update r (l e) x (l f)) (Function.update s (p e) y (p f)) -
chordAngle (r (l f)) (Function.update s (p e) y (p f)) -
chordAngle (Function.update r (l e) x (l f)) (s (p f)) + chordAngle (r (l f)) (s (p f)))
have he : edgeAngleSum l p a (Function.update r (l e) x, Function.update s (p e) y) -
edgeAngleSum l p a (r, Function.update s (p e) y) -
edgeAngleSum l p a (Function.update r (l e) x, s) + edgeAngleSum l p a (r, s) = ∑ f, g f := by
simp only [g, edgeAngleSum, mul_add, mul_sub, Finset.sum_add_distrib, Finset.sum_sub_distrib]
rw [he, Finset.sum_eq_single e]
· simp [g]
· intro f _ hfe
by_cases hl : l f = l e
· have hp : p f ≠ p e := fun hh => hfe (hij (Prod.ext hl hh))
simp [g, Function.update_of_ne hp]
· simp [g, Function.update_of_ne hl]
· simp
theorem edge_angle_sum_not_constant {L P E : Type*} [Fintype E]
[DecidableEq L] [DecidableEq P] [DecidableEq E]
(l : E → L) (p : E → P) (hij : Function.Injective (fun e => (l e, p e)))
(a : E → ℝ) (e : E) (ha : a e ≠ 0)
(U : Set ((L → ℝ) × (P → ℝ))) (hU : IsOpen U) (hne : U.Nonempty)
(hf : ∀ z ∈ U, ChordFeasible (z.1 (l e)) (z.2 (p e))) (k : ℝ) :
∃ z ∈ U, edgeAngleSum l p a z ≠ k := by
by_contra hnone
push Not at hnone
obtain ⟨z, hz⟩ := hne
obtain ⟨b, d, hb, hd, hrect⟩ := coordinate_rectangle hU hz (l e) (p e)
have hfeas : ∀ x ∈ Icc (z.1 (l e)) b, ∀ y ∈ Icc (z.2 (p e)) d, ChordFeasible x y := by
intro x hx y hy
simpa using hf _ (hrect x hx y hy)
have hpositive := chordAngle_rectangle_strict hb hd hfeas
have h00 := hnone z hz
have h11 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ d ⟨hd.le, le_rfl⟩)
have h01 := hnone _ (hrect (z.1 (l e)) ⟨le_rfl, hb.le⟩ d ⟨hd.le, le_rfl⟩)
have h10 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ (z.2 (p e)) ⟨le_rfl, hd.le⟩)
simp only [Function.update_eq_self] at h01 h10
have hid := edge_angle_rectangle l p hij a z.1 z.2 e b d
rw [h00, h11, h01, h10] at hid
have hzero : a e * (chordAngle b d - chordAngle (z.1 (l e)) d -
chordAngle b (z.2 (p e)) + chordAngle (z.1 (l e)) (z.2 (p e))) = 0 := by linarith
exact mul_ne_zero ha (ne_of_gt hpositive) hzero
theorem edge_angles_continuousAt {L P E : Type*} [Fintype E]
(l : E → L) (p : E → P) (a : E → ℝ) (z : (L → ℝ) × (P → ℝ))
(hr : ∀ i, z.1 i ≠ 0) (hs : ∀ j, z.2 j ≠ 0) : ContinuousAt (edgeAngleSum l p a) z := by
unfold edgeAngleSum chordAngle chordCos
fun_prop (disch := aesop)
def subsetDifference {E : Type*} [DecidableEq E] (S T : Finset E) (e : E) : ℝ :=
(if e ∈ S then 1 else 0) - (if e ∈ T then 1 else 0)
theorem subsetDifference_sum {E : Type*} [Fintype E] [DecidableEq E]
(S T : Finset E) (f : E → ℝ) :
∑ e, subsetDifference S T e * f e = (∑ e ∈ S, f e) - ∑ e ∈ T, f e := by
simp [subsetDifference, sub_mul, ite_mul, Finset.sum_sub_distrib]
theorem subsetDifference_nonzero {E : Type*} [DecidableEq E]
{S T : Finset E} (hne : S ≠ T) : ∃ e, subsetDifference S T e ≠ 0 := by
by_contra hh
push Not at hh
apply hne
ext e
have he := hh e
by_cases hS : e ∈ S <;> by_cases hT : e ∈ T <;> simp_all [subsetDifference]
def phaseRotations {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(z : (L → ℝ) × (P → ℝ)) (e : E) : ℂ :=
Complex.exp (((θ e - chordAngle (z.1 (l e)) (z.2 (p e)) : ℝ) : ℂ) * Complex.I)
theorem phaseRotations_norm {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(z : (L → ℝ) × (P → ℝ)) (e : E) : ‖phaseRotations l p θ z e‖ = 1 := by
exact Complex.norm_exp_ofReal_mul_I _
theorem exp_phase_small_injective {x y : ℝ} (hsmall : |x - y| < Real.pi)
(he : Complex.exp ((x : ℂ) * Complex.I) = Complex.exp ((y : ℂ) * Complex.I)) : x = y := by
have hexp : Complex.exp (((x - y : ℝ) : ℂ) * Complex.I) = Complex.exp 0 := by
rw [Complex.ofReal_sub, sub_mul, Complex.exp_sub, he, div_self (Complex.exp_ne_zero _), Complex.exp_zero]
have hxy := abs_lt.mp hsmall
have hh := Complex.exp_inj_of_neg_pi_lt_of_le_pi
(x := ((x - y : ℝ) : ℂ) * Complex.I) (y := 0)
(by simpa using hxy.1) (by simpa using hxy.2.le)
(by simpa using neg_neg_of_pos Real.pi_pos) (by simpa using Real.pi_pos.le) hexp
have := congrArg Complex.im hh
exact sub_eq_zero.mp (by simpa using this)
theorem subsetProduct_phase {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(z : (L → ℝ) × (P → ℝ)) (S : Finset E) :
subsetProduct (phaseRotations l p θ z) S =
Complex.exp (((∑ e ∈ S, (θ e - chordAngle (z.1 (l e)) (z.2 (p e))) : ℝ) : ℂ) * Complex.I) := by
unfold subsetProduct phaseRotations
rw [← Complex.exp_sum]
congr 1
simp [Complex.ofReal_sum, Finset.sum_sub_distrib, sub_mul, Finset.sum_mul]
def relationPhase {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(S T : Finset E) (z : (L → ℝ) × (P → ℝ)) : ℝ :=
(∑ e ∈ S, (θ e - chordAngle (z.1 (l e)) (z.2 (p e)))) -
∑ e ∈ T, (θ e - chordAngle (z.1 (l e)) (z.2 (p e)))
theorem relationPhase_eq {L P E : Type*} [Fintype E] [DecidableEq E]
(l : E → L) (p : E → P) (θ : E → ℝ) (S T : Finset E) (z : (L → ℝ) × (P → ℝ)) :
relationPhase l p θ S T z =
(∑ e, subsetDifference S T e * θ e) - edgeAngleSum l p (subsetDifference S T) z := by
unfold relationPhase edgeAngleSum
rw [← Finset.sum_sub_distrib, ← subsetDifference_sum S T]
apply Finset.sum_congr rfl
intro e _
ring
theorem relationPhase_exp {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(S T : Finset E) (z : (L → ℝ) × (P → ℝ))
(he : subsetProduct (phaseRotations l p θ z) S = subsetProduct (phaseRotations l p θ z) T) :
Complex.exp (((relationPhase l p θ S T z : ℝ) : ℂ) * Complex.I) = 1 := by
unfold relationPhase
rw [Complex.ofReal_sub, sub_mul, Complex.exp_sub,
← subsetProduct_phase l p θ z S, ← subsetProduct_phase l p θ z T, he]
apply div_self
rw [subsetProduct_phase]
exact Complex.exp_ne_zero _
theorem phaseRotations_continuousAt {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(z : (L → ℝ) × (P → ℝ)) (hr : ∀ i, z.1 i ≠ 0) (hs : ∀ j, z.2 j ≠ 0) (e : E) :
ContinuousAt (fun u => phaseRotations l p θ u e) z := by
unfold phaseRotations chordAngle chordCos
fun_prop (disch := aesop)
theorem subset_products_separate {L P E : Type*} [Fintype E]
[DecidableEq L] [DecidableEq P] [DecidableEq E]
(l : E → L) (p : E → P) (hij : Function.Injective (fun e => (l e, p e)))
(θ : E → ℝ) (U : Set ((L → ℝ) × (P → ℝ))) (hU : IsOpen U) (hne : U.Nonempty)
(hnz : ∀ z ∈ U, (∀ i, z.1 i ≠ 0) ∧ (∀ j, z.2 j ≠ 0))
(hf : ∀ e, ∀ z ∈ U, ChordFeasible (z.1 (l e)) (z.2 (p e)))
(S T : Finset E) (hST : S ≠ T) :
∃ z ∈ U, subsetProduct (phaseRotations l p θ z) S ≠ subsetProduct (phaseRotations l p θ z) T := by
by_contra hnone
push Not at hnone
obtain ⟨e, he⟩ := subsetDifference_nonzero hST
obtain ⟨z₀, hz₀⟩ := hne
let φ := relationPhase l p θ S T
have hc : ContinuousOn φ U := by
intro z hz
have hh : ContinuousAt (fun u => (∑ e, subsetDifference S T e * θ e) -
edgeAngleSum l p (subsetDifference S T) u) z :=
continuousAt_const.sub (edge_angles_continuousAt l p (subsetDifference S T) z (hnz z hz).1 (hnz z hz).2)
change ContinuousWithinAt φ U z
rw [show φ = fun u => (∑ e, subsetDifference S T e * θ e) -
edgeAngleSum l p (subsetDifference S T) u by funext u; exact relationPhase_eq l p θ S T u]
exact hh.continuousWithinAt
let V := U ∩ (fun z => |φ z - φ z₀|) ⁻¹' Iio Real.pi
have hVo : IsOpen V :=
(hc.sub continuousOn_const).abs.isOpen_inter_preimage hU isOpen_Iio
have hVne : V.Nonempty := ⟨z₀, hz₀, by simpa using Real.pi_pos⟩
have hVU : V ⊆ U := inter_subset_left
have hconstant : ∀ z ∈ V, edgeAngleSum l p (subsetDifference S T) z =
(∑ e, subsetDifference S T e * θ e) - φ z₀ := by
intro z hz
have h1 := relationPhase_exp l p θ S T z (hnone z (hVU hz))
have h0 := relationPhase_exp l p θ S T z₀ (hnone z₀ hz₀)
have hphase : φ z = φ z₀ := exp_phase_small_injective hz.2 (h1.trans h0.symm)
rw [show φ z = (∑ e, subsetDifference S T e * θ e) -
edgeAngleSum l p (subsetDifference S T) z from relationPhase_eq l p θ S T z] at hphase
linarith
obtain ⟨z, hz, hh⟩ := edge_angle_sum_not_constant l p hij (subsetDifference S T) e he V hVo hVne
(fun z hz => hf e z (hVU hz)) ((∑ e, subsetDifference S T e * θ e) - φ z₀)
exact hh (hconstant z hz)
theorem exists_injective_subsetProducts {L P E : Type*} [Fintype E]
[DecidableEq L] [DecidableEq P] [DecidableEq E]
(l : E → L) (p : E → P) (hij : Function.Injective (fun e => (l e, p e)))
(θ : E → ℝ) (U : Set ((L → ℝ) × (P → ℝ))) (hU : IsOpen U) (hne : U.Nonempty)
(hnz : ∀ z ∈ U, (∀ i, z.1 i ≠ 0) ∧ (∀ j, z.2 j ≠ 0))
(hf : ∀ e, ∀ z ∈ U, ChordFeasible (z.1 (l e)) (z.2 (p e))) :
∃ z ∈ U, Function.Injective (subsetProduct (phaseRotations l p θ z)) := by
classical
let K := {st : Finset E × Finset E // st.1 ≠ st.2}
let f := fun (k : K) (z : (L → ℝ) × (P → ℝ)) =>
subsetProduct (phaseRotations l p θ z) k.val.1 - subsetProduct (phaseRotations l p θ z) k.val.2
have hc : ∀ k, ContinuousOn (f k) U := by
intro k z hz
have hrot := phaseRotations_continuousAt l p θ z (hnz z hz).1 (hnz z hz).2
apply ContinuousAt.continuousWithinAt
unfold f subsetProduct
fun_prop
have hnc : ∀ k, ∀ V : Set ((L → ℝ) × (P → ℝ)),
V ⊆ U → IsOpen V → V.Nonempty → ∃ z ∈ V, f k z ≠ 0 := by
intro k V hVU hVo hVne
obtain ⟨z, hz, hh⟩ := subset_products_separate l p hij θ V hVo hVne
(fun z hz => hnz z (hVU hz)) (fun e z hz => hf e z (hVU hz)) k.val.1 k.val.2 k.property
exact ⟨z, hz, sub_ne_zero.mpr hh⟩
obtain ⟨z, hz, hh⟩ := finite_avoidance f U hU hne hc hnc Finset.univ
refine ⟨z, hz, ?_⟩
intro S T heq
by_contra hST
exact hh (⟨(S, T), hST⟩ : K) (Finset.mem_univ _) (sub_eq_zero.mpr heq)
end
end Proof
end OriginalGenericRotations
/- ## CorrectionAlgebra -/
section OriginalCorrectionAlgebra
/- Exact algebraic correction of a fourth-order error in a unit distance. -/
namespace Proof
noncomputable section
def correctionRadicand (ε t M q : ℝ) : ℝ :=
t ^ 2 - ε ^ 2 * M ^ 2 * q - ε ^ 6 * M ^ 4 / 4
def chordNumerator (ε t M : ℝ) (q : ℂ) : ℂ :=
⟨q.re + ε ^ 4 * M ^ 2 / 2, -ε * Real.sqrt (correctionRadicand ε t M q.re)⟩
def correction (ε t M : ℝ) (q : ℂ) : ℂ := chordNumerator ε t M q / q
def correctionCoefficient (ε t M : ℝ) (q : ℂ) : ℂ :=
(⟨ε * M ^ 2 / 2,
M ^ 2 * (q.re + ε ^ 4 * M ^ 2 / 4) /
(Real.sqrt (correctionRadicand ε t M q.re) - t)⟩ : ℂ) / q
theorem chordNumerator_normSq (ε t M : ℝ) (q : ℂ)
(him : q.im = ε * t) (hF : 0 ≤ correctionRadicand ε t M q.re) :
Complex.normSq (chordNumerator ε t M q) = Complex.normSq q := by
have hs := Real.sq_sqrt hF
simp only [chordNumerator, Complex.normSq_apply]
rw [him]
dsimp [correctionRadicand] at hs ⊢
linear_combination ε ^ 2 * hs
theorem correction_norm (ε t M : ℝ) (q : ℂ) (hq : q ≠ 0)
(him : q.im = ε * t) (hF : 0 ≤ correctionRadicand ε t M q.re) :
‖correction ε t M q‖ = 1 := by
have hh : Complex.normSq (correction ε t M q) = 1 := by
rw [correction, Complex.normSq_div, chordNumerator_normSq ε t M q him hF]
exact div_self (ne_of_gt (Complex.normSq_pos.mpr hq))
rw [Complex.normSq_eq_norm_sq] at hh
nlinarith [norm_nonneg (correction ε t M q)]
theorem correction_cubic_identity (ε t M : ℝ) (q : ℂ) (hq : q ≠ 0)
(him : q.im = ε * t) (hF : 0 ≤ correctionRadicand ε t M q.re)
(hden : Real.sqrt (correctionRadicand ε t M q.re) - t ≠ 0) :
correction ε t M q - 1 = (ε : ℂ) ^ 3 * correctionCoefficient ε t M q := by
have hs := Real.sq_sqrt hF
have he : chordNumerator ε t M q - q = (ε : ℂ) ^ 3 *
(⟨ε * M ^ 2 / 2,
M ^ 2 * (q.re + ε ^ 4 * M ^ 2 / 4) /
(Real.sqrt (correctionRadicand ε t M q.re) - t)⟩ : ℂ) := by
apply Complex.ext
· simp only [chordNumerator, Complex.sub_re, Complex.mul_re, ← Complex.ofReal_pow,
Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero]
ring
· simp only [chordNumerator, Complex.sub_im, Complex.mul_im,
← Complex.ofReal_pow, Complex.ofReal_re, Complex.ofReal_im, zero_mul, add_zero]
rw [him]
rw [← mul_div_assoc]
apply (eq_div_iff hden).mpr
dsimp [correctionRadicand] at hs ⊢
linear_combination -ε * hs
unfold correction correctionCoefficient
rw [← div_self hq, ← sub_div, he, mul_div_assoc]
theorem correction_unit_distance (a b : ℂ) (ε t M : ℝ)
(hq : starRingEnd ℂ a * b ≠ 0)
(him : (starRingEnd ℂ a * b).im = ε * t)
(hF : 0 ≤ correctionRadicand ε t M (starRingEnd ℂ a * b).re)
(hdist : Complex.normSq (b - a) = 1 + ε ^ 4 * M ^ 2) :
‖a - b * correction ε t M (starRingEnd ℂ a * b)‖ = 1 := by
let q := starRingEnd ℂ a * b
let w := correction ε t M q
have hw : ‖w‖ = 1 := correction_norm ε t M q hq him hF
have hz : starRingEnd ℂ a * (b * w) = chordNumerator ε t M q := by
change starRingEnd ℂ a * (b * (chordNumerator ε t M q / q)) = _
rw [← mul_assoc]
exact mul_div_cancel₀ _ hq
have hreal : (a * starRingEnd ℂ (b * w)).re = q.re + ε ^ 4 * M ^ 2 / 2 := by
have hh := congrArg Complex.re hz
simp only [Complex.mul_re, Complex.mul_im, Complex.conj_re, Complex.conj_im,
chordNumerator] at hh ⊢
linarith
have hbase : Complex.normSq a + Complex.normSq b - 2 * q.re = 1 + ε ^ 4 * M ^ 2 := by
simpa [Complex.normSq_sub, q, mul_comm, add_comm] using hdist
have hns : Complex.normSq (a - b * w) = 1 := by
rw [Complex.normSq_sub, Complex.normSq_mul, Complex.normSq_eq_norm_sq w, hw, one_pow, mul_one,
hreal]
linarith
rw [Complex.normSq_eq_norm_sq] at hns
nlinarith [norm_nonneg (a - b * w)]
end
end Proof
end OriginalCorrectionAlgebra
/- ## SeedGerms -/
section OriginalSeedGerms
/- Continuous formulas for the small correction rotations at a seed. -/
namespace Proof
open Filter
open scoped Topology
noncomputable section
def seedTangent (ε x t y u : ℝ) : ℝ :=
(x - y) / 2 + ε ^ 2 * (x * pointD y u + y * lineC x t)
def seedProduct (ε x t y u : ℝ) : ℂ :=
starRingEnd ℂ (lineSeed ε x t) * pointSeed ε y u
def seedCoefficient (ε x t y u : ℝ) : ℂ :=
correctionCoefficient ε (seedTangent ε x t y u) (pointD y u - lineC x t)
(seedProduct ε x t y u)
def seedCorrection (ε x t y u : ℝ) : ℂ :=
correction ε (seedTangent ε x t y u) (pointD y u - lineC x t)
(seedProduct ε x t y u)
theorem seedProduct_im (ε x t y u : ℝ) :
(seedProduct ε x t y u).im = ε * seedTangent ε x t y u := by
simp [seedProduct, seedTangent, lineSeed, pointSeed, Complex.mul_im]
ring
theorem seedProduct_zero (x t y u : ℝ) : seedProduct 0 x t y u = (-1 / 4 : ℂ) := by
apply Complex.ext <;> norm_num [seedProduct, lineSeed, pointSeed, Complex.mul_re, Complex.mul_im]
theorem continuous_lineSeed (x t : ℝ) : Continuous (fun ε => lineSeed ε x t) := by
unfold lineSeed
simp only [Complex.mk_eq_add_mul_I]
fun_prop
theorem continuous_pointSeed (x t : ℝ) : Continuous (fun ε => pointSeed ε x t) := by
unfold pointSeed
simp only [Complex.mk_eq_add_mul_I]
fun_prop
theorem continuous_seedProduct (x t y u : ℝ) : Continuous (fun ε => seedProduct ε x t y u) := by
exact ((continuous_lineSeed x t).star).mul (continuous_pointSeed y u)
theorem continuous_seedTangent (x t y u : ℝ) : Continuous (fun ε => seedTangent ε x t y u) := by
unfold seedTangent
fun_prop
theorem seed_radicand_zero (x t y u : ℝ) :
correctionRadicand 0 (seedTangent 0 x t y u) (pointD y u - lineC x t)
(seedProduct 0 x t y u).re = ((x - y) / 2) ^ 2 := by
simp [correctionRadicand, seedTangent]
theorem seed_denominator_pos (x t y u : ℝ) (hxy : x < y) :
0 < Real.sqrt (correctionRadicand 0 (seedTangent 0 x t y u)
(pointD y u - lineC x t) (seedProduct 0 x t y u).re) - seedTangent 0 x t y u := by
rw [seed_radicand_zero]
simp only [seedTangent, zero_pow (by decide : 2 ≠ 0), zero_mul, add_zero]
rw [Real.sqrt_sq_eq_abs, abs_of_neg (by linarith : (x - y) / 2 < 0)]
linarith
theorem continuousAt_seedCoefficient (x t y u : ℝ) (hxy : x < y) :
ContinuousAt (fun ε => seedCoefficient ε x t y u) 0 := by
have hq : seedProduct 0 x t y u ≠ 0 := by rw [seedProduct_zero]; norm_num
have hden := ne_of_gt (seed_denominator_pos x t y u hxy)
have hcq := (continuous_seedProduct x t y u).continuousAt (x := 0)
have hct := (continuous_seedTangent x t y u).continuousAt (x := 0)
unfold seedCoefficient correctionCoefficient
apply ContinuousAt.div _ hcq hq
simp only [Complex.mk_eq_add_mul_I]
have hreal : ContinuousAt (fun ε =>
(pointD y u - lineC x t) ^ 2 *
((seedProduct ε x t y u).re + ε ^ 4 * (pointD y u - lineC x t) ^ 2 / 4) /
(Real.sqrt (correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re) - seedTangent ε x t y u)) 0 := by
apply ContinuousAt.div
· fun_prop
· unfold correctionRadicand
fun_prop
· exact hden
fun_prop
theorem seedCorrection_properties (x t y u : ℝ) (hxy : x < y)
(hinc : u - t = (y - x) ^ 2) :
∀ᶠ ε in 𝓝 (0 : ℝ),
‖seedCorrection ε x t y u‖ = 1 ∧
‖lineSeed ε x t - pointSeed ε y u * seedCorrection ε x t y u‖ = 1 ∧
seedCorrection ε x t y u - 1 = (ε : ℂ) ^ 3 * seedCoefficient ε x t y u := by
have hq : ∀ᶠ ε in 𝓝 (0 : ℝ), seedProduct ε x t y u ≠ 0 :=
(continuous_seedProduct x t y u).continuousAt.eventually_ne (by rw [seedProduct_zero]; norm_num)
have hFcont : Continuous (fun ε => correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re) := by
unfold correctionRadicand
have ht := continuous_seedTangent x t y u
have hq := continuous_seedProduct x t y u
fun_prop
have hF : ∀ᶠ ε in 𝓝 (0 : ℝ), 0 < correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re := by
apply continuousAt_const.eventually_lt hFcont.continuousAt
rw [seed_radicand_zero]
exact sq_pos_of_ne_zero (by linarith)
have hdc : Continuous (fun ε => Real.sqrt (correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re) - seedTangent ε x t y u) :=
hFcont.sqrt.sub (continuous_seedTangent x t y u)
have hd := hdc.continuousAt.eventually_ne (ne_of_gt (seed_denominator_pos x t y u hxy))
filter_upwards [hq, hF, hd] with ε hq hF hd
exact ⟨correction_norm _ _ _ _ hq (seedProduct_im ε x t y u) hF.le,
correction_unit_distance _ _ _ _ _ hq (seedProduct_im ε x t y u) hF.le
(incidence_distance_identity ε x t y u hinc),
correction_cubic_identity _ _ _ _ hq (seedProduct_im ε x t y u) hF.le hd⟩
theorem seedCorrection_im_negative (x t y u : ℝ) (hxy : x < y) :
∀ᶠ ε in 𝓝[>] (0 : ℝ),
(seedProduct ε x t y u * seedCorrection ε x t y u).im < 0 := by
have hq : ∀ᶠ ε in 𝓝 (0 : ℝ), seedProduct ε x t y u ≠ 0 :=
(continuous_seedProduct x t y u).continuousAt.eventually_ne (by rw [seedProduct_zero]; norm_num)
have hFcont : Continuous (fun ε => correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re) := by
unfold correctionRadicand
have ht := continuous_seedTangent x t y u
have hq := continuous_seedProduct x t y u
fun_prop
have hF : ∀ᶠ ε in 𝓝 (0 : ℝ), 0 < correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re := by
apply continuousAt_const.eventually_lt hFcont.continuousAt
rw [seed_radicand_zero]
exact sq_pos_of_ne_zero (by linarith)
filter_upwards [hq.filter_mono nhdsWithin_le_nhds, hF.filter_mono nhdsWithin_le_nhds,
self_mem_nhdsWithin] with ε hq hF (hε : 0 < ε)
change (seedProduct ε x t y u * (chordNumerator ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u) / seedProduct ε x t y u)).im < 0
rw [mul_div_cancel₀ _ hq]
change -ε * Real.sqrt (correctionRadicand ε (seedTangent ε x t y u)
(pointD y u - lineC x t) (seedProduct ε x t y u).re) < 0
exact mul_neg_of_neg_of_pos (neg_neg_of_pos hε) (Real.sqrt_pos.mpr hF)
end
end Proof
end OriginalSeedGerms
/- ## SeedLimits -/
section OriginalSeedLimits
/- Choosing one sufficiently small positive parameter for finitely many seed inequalities. -/
namespace Proof
open Filter
open scoped Topology
noncomputable section
theorem eventually_scaled_ne (a b : ℝ → ℂ) (F : ℝ → ℝ)
(hF : ContinuousAt F 0) (hF0 : F 0 ≠ 0)
(hid : ∀ ε, Complex.normSq (a ε) - Complex.normSq (b ε) = ε ^ 2 * F ε) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), ‖a ε‖ ≠ ‖b ε‖ := by
have he : ∀ᶠ ε in 𝓝[>] (0 : ℝ), F ε ≠ 0 :=
(hF.eventually_ne hF0).filter_mono nhdsWithin_le_nhds
filter_upwards [he, self_mem_nhdsWithin] with ε hFε (hε : 0 < ε)
intro hn
have hs : Complex.normSq (a ε) = Complex.normSq (b ε) := by
simp only [Complex.normSq_eq_norm_sq, hn]
have hz := hid ε
rw [hs, sub_self] at hz
exact mul_ne_zero (pow_ne_zero 2 (ne_of_gt hε)) hFε hz.symm
theorem eventually_scaled_support (a b : ℝ → ℂ) (A F : ℝ → ℝ)
(hF : ContinuousAt F 0) (hF0 : F 0 < 0)
(hid : ∀ ε, support (a ε) (b ε) + ε ^ 3 * A ε = ε ^ 2 * F ε) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), support (a ε) (b ε) < -ε ^ 3 * A ε := by
have he : ∀ᶠ ε in 𝓝[>] (0 : ℝ), F ε < 0 :=
(hF.eventually_lt continuousAt_const hF0).filter_mono nhdsWithin_le_nhds
filter_upwards [he, self_mem_nhdsWithin] with ε hFε (hε : 0 < ε)
have hh : ε ^ 2 * F ε < 0 := mul_neg_of_pos_of_neg (pow_pos hε 2) hFε
linarith [hid ε]
theorem eventually_line_support (x t y u : ℝ) (A : ℝ → ℝ)
(hA : ContinuousAt A 0) (hm : -(y - x) ^ 2 / 2 - (u - t) / 4 < 0) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), support (lineSeed ε x t) (lineSeed ε y u) < -ε ^ 3 * A ε := by
let F := fun ε => -(y - x) ^ 2 / 2 - (u - t) / 4 +
ε ^ 2 * lineC x t * (lineC y u - lineC x t) + ε * A ε
apply eventually_scaled_support _ _ A F
· unfold F; fun_prop
· simpa [F] using hm
· intro ε
rw [line_support_identity]
dsimp [F]
ring
theorem eventually_point_support (x t y u : ℝ) (A : ℝ → ℝ)
(hA : ContinuousAt A 0) (hm : -(y - x) ^ 2 / 2 + (u - t) / 4 < 0) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), support (pointSeed ε x t) (pointSeed ε y u) < -ε ^ 3 * A ε := by
let F := fun ε => -(y - x) ^ 2 / 2 + (u - t) / 4 +
ε ^ 2 * pointD x t * (pointD y u - pointD x t) + ε * A ε
apply eventually_scaled_support _ _ A F
· unfold F; fun_prop
· simpa [F] using hm
· intro ε
rw [point_support_identity]
dsimp [F]
ring
theorem eventually_cross_support (x t y u : ℝ) (A : ℝ → ℝ) (hA : ContinuousAt A 0) :
∀ᶠ ε in 𝓝[>] (0 : ℝ),
support (lineSeed ε x t) (pointSeed ε y u) < -ε ^ 3 * A ε ∧
support (pointSeed ε y u) (lineSeed ε x t) < -ε ^ 3 * A ε := by
have hc₁ : ContinuousAt (fun ε => support (lineSeed ε x t) (pointSeed ε y u) + ε ^ 3 * A ε) 0 := by
unfold support lineSeed pointSeed; fun_prop
have hc₂ : ContinuousAt (fun ε => support (pointSeed ε y u) (lineSeed ε x t) + ε ^ 3 * A ε) 0 := by
unfold support lineSeed pointSeed; fun_prop
have h₁ : ∀ᶠ ε in 𝓝 (0 : ℝ), support (lineSeed ε x t) (pointSeed ε y u) + ε ^ 3 * A ε < 0 :=
hc₁.eventually_lt continuousAt_const (by norm_num [support, lineSeed, pointSeed])
have h₂ : ∀ᶠ ε in 𝓝 (0 : ℝ), support (pointSeed ε y u) (lineSeed ε x t) + ε ^ 3 * A ε < 0 :=
hc₂.eventually_lt continuousAt_const (by norm_num [support, lineSeed, pointSeed])
filter_upwards [h₁.filter_mono nhdsWithin_le_nhds, h₂.filter_mono nhdsWithin_le_nhds] with ε h₁ h₂
constructor <;> linarith
theorem eventually_line_norm_ne (x t y u : ℝ) (htu : t ≠ u) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), ‖lineSeed ε x t‖ ≠ ‖lineSeed ε y u‖ := by
apply eventually_scaled_ne _ _ (fun ε => -(t - u) / 2 + ε ^ 2 * ((lineC x t) ^ 2 - (lineC y u) ^ 2))
· fun_prop
· simp only [zero_pow (by decide : 2 ≠ 0), zero_mul, add_zero]
exact div_ne_zero (neg_ne_zero.mpr (sub_ne_zero.mpr htu)) (by norm_num)
· intro ε
rw [line_normSq, line_normSq]
ring
theorem eventually_point_norm_ne (x t y u : ℝ) (htu : t ≠ u) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), ‖pointSeed ε x t‖ ≠ ‖pointSeed ε y u‖ := by
apply eventually_scaled_ne _ _ (fun ε => (t - u) / 2 + ε ^ 2 * ((pointD x t) ^ 2 - (pointD y u) ^ 2))
· fun_prop
· simp only [zero_pow (by decide : 2 ≠ 0), zero_mul, add_zero]
exact div_ne_zero (sub_ne_zero.mpr htu) (by norm_num)
· intro ε
rw [point_normSq, point_normSq]
ring
theorem eventually_cross_norm_ne (x t y u : ℝ) (ht : 0 < t) (hu : 0 < u) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), ‖lineSeed ε x t‖ ≠ ‖pointSeed ε y u‖ := by
apply eventually_scaled_ne _ _ (fun ε => -(t + u) / 2 + ε ^ 2 * ((lineC x t) ^ 2 - (pointD y u) ^ 2))
· fun_prop
· simp only [zero_pow (by decide : 2 ≠ 0), zero_mul, add_zero]
linarith
· intro ε
rw [line_normSq, point_normSq]
ring
end
end Proof
end OriginalSeedLimits
/- ## Incidence -/
section OriginalIncidence
/- The coordinate incidence graph used in the construction. -/
namespace Proof
abbrev PointLabel (d : ℕ) := Fin d → Fin d
abbrev LineLabel (d : ℕ) := (i : Fin d) × ({j : Fin d // j ≠ i} → Fin d)
abbrev EdgeLabel (d : ℕ) := PointLabel d × Fin d
def edgePoint {d : ℕ} (e : EdgeLabel d) : PointLabel d := e.1
def edgeLine {d : ℕ} (e : EdgeLabel d) : LineLabel d := ⟨e.2, fun j => e.1 j⟩
theorem edge_endpoints_injective (d : ℕ) :
Function.Injective (fun e : EdgeLabel d => (edgeLine e, edgePoint e)) := by
intro e f h
have hpoint : e.1 = f.1 := congrArg Prod.snd h
have hline : e.2 = f.2 := congrArg (fun p => p.1.1) h
exact Prod.ext hpoint hline
theorem pointLabel_card (d : ℕ) : Fintype.card (PointLabel d) = d ^ d := by
simp [PointLabel]
theorem puncturedFin_card {d : ℕ} (i : Fin d) :
Fintype.card {j : Fin d // j ≠ i} = d - 1 := by
simp
theorem lineLabel_card (d : ℕ) : Fintype.card (LineLabel d) = d * d ^ (d - 1) := by
simp [LineLabel, Fintype.card_sigma]
theorem edgeLabel_card (d : ℕ) : Fintype.card (EdgeLabel d) = d ^ (d + 1) := by
simp [EdgeLabel, pow_succ]
theorem vertexLabel_card {d : ℕ} (hd : 1 ≤ d) :
Fintype.card (LineLabel d ⊕ PointLabel d) = 2 * d ^ d := by
rw [Fintype.card_sum, lineLabel_card, pointLabel_card]
have hpow : d * d ^ (d - 1) = d ^ d := by
rw [← pow_succ', Nat.sub_add_cancel hd]
omega
end Proof
end OriginalIncidence
/- ## Digits -/
section OriginalDigits
/- Separation of distinct finite sums of powers of five. -/
namespace Proof
noncomputable section
def digitSum (q : ℝ) (s : Finset ℕ) : ℝ := ∑ i ∈ s, q ^ i
theorem geometric_five (n : ℕ) :
4 * (∑ i ∈ Finset.range n, (5 : ℝ) ^ i) = (5 : ℝ) ^ n - 1 := by
induction n with
| zero => norm_num
| succ n ih => rw [Finset.sum_range_succ, pow_succ]; linarith
theorem geometric_twentyfive (n : ℕ) :
24 * (∑ i ∈ Finset.range n, (25 : ℝ) ^ i) = (25 : ℝ) ^ n - 1 := by
induction n with
| zero => norm_num
| succ n ih => rw [Finset.sum_range_succ, pow_succ]; linarith
theorem dominant_digit_bounds {q : ℝ} (hq : 0 ≤ q) {A B : Finset ℕ} {h : ℕ}
(hdis : Disjoint A B) (hmem : h ∈ A) (hmax : ∀ j ∈ A ∪ B, j ≤ h) :
q ^ h - (∑ i ∈ Finset.range h, q ^ i) ≤ digitSum q A - digitSum q B ∧
digitSum q A - digitSum q B ≤ q ^ h + (∑ i ∈ Finset.range h, q ^ i) := by
have hsubB : B ⊆ Finset.range h := by
intro j hj
have hle := hmax j (Finset.mem_union_right A hj)
have hne : j ≠ h := by
intro he
exact (Finset.disjoint_left.mp hdis hmem) (he ▸ hj)
exact Finset.mem_range.mpr (lt_of_le_of_ne hle hne)
have hsubA : A ⊆ Finset.range (h + 1) := by
intro j hj
exact Finset.mem_range.mpr (Nat.lt_succ_of_le (hmax j (Finset.mem_union_left B hj)))
have hAlo : q ^ h ≤ digitSum q A :=
Finset.single_le_sum (fun j _ => pow_nonneg hq j) hmem
have hBlo : 0 ≤ digitSum q B := Finset.sum_nonneg (fun j _ => pow_nonneg hq j)
have hAhi : digitSum q A ≤ ∑ i ∈ Finset.range (h + 1), q ^ i :=
Finset.sum_le_sum_of_subset_of_nonneg hsubA (fun j _ _ => pow_nonneg hq j)
have hBhi : digitSum q B ≤ ∑ i ∈ Finset.range h, q ^ i :=
Finset.sum_le_sum_of_subset_of_nonneg hsubB (fun j _ _ => pow_nonneg hq j)
rw [Finset.sum_range_succ] at hAhi
constructor <;> linarith
theorem dominant_five_separation {A B : Finset ℕ} {h : ℕ}
(hdis : Disjoint A B) (hmem : h ∈ A) (hmax : ∀ j ∈ A ∪ B, j ≤ h) :
0 < digitSum 5 A - digitSum 5 B ∧
0 < digitSum 25 A - digitSum 25 B ∧
digitSum 25 A - digitSum 25 B <
(50 / 27 : ℝ) * (digitSum 5 A - digitSum 5 B) ^ 2 := by
obtain ⟨h5lo, h5hi⟩ := dominant_digit_bounds (q := 5) (by norm_num) hdis hmem hmax
obtain ⟨h25lo, h25hi⟩ := dominant_digit_bounds (q := 25) (by norm_num) hdis hmem hmax
have g5 := geometric_five h
have g25 := geometric_twentyfive h
have hp5 : 0 < (5 : ℝ) ^ h := by positivity
have hp25 : 0 < (25 : ℝ) ^ h := by positivity
have hx : 3 / 4 * (5 : ℝ) ^ h < digitSum 5 A - digitSum 5 B := by linarith
have ht : digitSum 25 A - digitSum 25 B < 25 / 24 * (25 : ℝ) ^ h := by linarith
have hp : (25 : ℝ) ^ h = ((5 : ℝ) ^ h) ^ 2 := by
rw [← pow_mul, Nat.mul_comm, pow_mul]
norm_num
have hsq := mul_self_lt_mul_self (by positivity : (0 : ℝ) ≤ 3 / 4 * 5 ^ h) hx
refine ⟨by linarith, by linarith, ?_⟩
rw [hp] at ht
nlinarith
theorem digit_separation {s t : Finset ℕ} (hne : s ≠ t) :
digitSum 5 s ≠ digitSum 5 t ∧ digitSum 25 s ≠ digitSum 25 t ∧
|digitSum 25 s - digitSum 25 t| <
(50 / 27 : ℝ) * (digitSum 5 s - digitSum 5 t) ^ 2 := by
let A := s \ t
let B := t \ s
have hdis : Disjoint A B := by
simp only [A, B, Finset.disjoint_left, Finset.mem_sdiff]
aesop
have hneAB : (A ∪ B).Nonempty := by
by_contra hc
have he : A ∪ B = ∅ := Finset.not_nonempty_iff_eq_empty.mp hc
apply hne
ext i
have hi : i ∉ A ∪ B := by rw [he]; simp
simp only [A, B, Finset.mem_union, Finset.mem_sdiff] at hi
tauto
let h := (A ∪ B).max' hneAB
have hh : h ∈ A ∪ B := Finset.max'_mem _ _
have hmax : ∀ j ∈ A ∪ B, j ≤ h := fun j hj => Finset.le_max' _ j hj
have he5 : digitSum 5 s - digitSum 5 t = digitSum 5 A - digitSum 5 B := by
exact (Finset.sum_sdiff_sub_sum_sdiff (s₁ := t) (s₂ := s) (f := fun i => (5 : ℝ) ^ i)).symm
have he25 : digitSum 25 s - digitSum 25 t = digitSum 25 A - digitSum 25 B := by
exact (Finset.sum_sdiff_sub_sum_sdiff (s₁ := t) (s₂ := s) (f := fun i => (25 : ℝ) ^ i)).symm
rcases Finset.mem_union.mp hh with hh | hh
· obtain ⟨hx, ht, hbound⟩ := dominant_five_separation hdis hh hmax
refine ⟨?_, ?_, ?_⟩
· intro he; rw [he, sub_self] at he5; linarith
· intro he; rw [he, sub_self] at he25; linarith
· rw [he5, he25, abs_of_pos ht]; exact hbound
· have hmax' : ∀ j ∈ B ∪ A, j ≤ h := by simpa [Finset.union_comm] using hmax
obtain ⟨hx, ht, hbound⟩ := dominant_five_separation hdis.symm hh hmax'
refine ⟨?_, ?_, ?_⟩
· intro he; rw [he, sub_self] at he5; linarith
· intro he; rw [he, sub_self] at he25; linarith
· rw [he5, he25, abs_of_neg (by linarith : digitSum 25 A - digitSum 25 B < 0)]
nlinarith
end
end Proof
end OriginalDigits
/- ## LabelDigits -/
section OriginalLabelDigits
/- An injective assignment of lacunary digits to coordinate incidence labels. -/
namespace Proof
noncomputable section
def pointCells {d : ℕ} (p : PointLabel d) : Finset (Fin d × Fin d) :=
Finset.univ.image (fun i => (i, p i))
def lineCells {d : ℕ} (l : LineLabel d) : Finset (Fin d × Fin d) :=
Finset.univ.image (fun i : {j : Fin d // j ≠ l.1} => (i.val, l.2 i))
theorem mem_pointCells {d : ℕ} (p : PointLabel d) (i j : Fin d) :
(i, j) ∈ pointCells p ↔ p i = j := by
simp [pointCells]
theorem mem_lineCells {d : ℕ} (l : LineLabel d) (i j : Fin d) :
(i, j) ∈ lineCells l ↔ ∃ h : i ≠ l.1, l.2 ⟨i, h⟩ = j := by
simp [lineCells]
theorem pointCells_injective (d : ℕ) : Function.Injective (@pointCells d) := by
intro p q he
funext i
have hi : (i, p i) ∈ pointCells q := by rw [← he, mem_pointCells]
exact (mem_pointCells q i (p i)).mp hi |>.symm
theorem lineCells_injective (d : ℕ) : Function.Injective (@lineCells d) := by
rintro ⟨i, f⟩ ⟨j, g⟩ he
have hij : i = j := by
by_contra hne
have hj : (i, g ⟨i, hne⟩) ∈ lineCells ⟨j, g⟩ := by
rw [mem_lineCells]
exact ⟨hne, rfl⟩
rw [← he, mem_lineCells] at hj
obtain ⟨hbad, _⟩ := hj
exact hbad rfl
subst j
have hfg : f = g := by
funext k
have hk : (k.val, f k) ∈ lineCells ⟨i, g⟩ := by
rw [← he, mem_lineCells]
exact ⟨k.property, rfl⟩
obtain ⟨_, hh⟩ := (mem_lineCells _ _ _).mp hk
exact hh.symm
subst g
rfl
theorem incidence_cells {d : ℕ} (e : EdgeLabel d) :
pointCells (edgePoint e) = insert (e.2, e.1 e.2) (lineCells (edgeLine e)) := by
ext ⟨i, j⟩
simp only [Finset.mem_insert, mem_pointCells, mem_lineCells, edgePoint, edgeLine,
Prod.mk.injEq]
by_cases hi : i = e.2
· subst i
simp [eq_comm]
· simp [hi]
theorem completing_cell_absent {d : ℕ} (e : EdgeLabel d) :
(e.2, e.1 e.2) ∉ lineCells (edgeLine e) := by
simp [mem_lineCells, edgeLine]
def digitIndex (d : ℕ) : (Fin d × Fin d) ↪ ℕ :=
(Fintype.equivFin (Fin d × Fin d)).toEmbedding.trans ⟨Fin.val, Fin.val_injective⟩
def pointDigits {d : ℕ} (p : PointLabel d) : Finset ℕ := (pointCells p).map (digitIndex d)
def lineDigits {d : ℕ} (l : LineLabel d) : Finset ℕ := (lineCells l).map (digitIndex d)
theorem pointDigits_injective (d : ℕ) : Function.Injective (@pointDigits d) := by
intro p q he
exact pointCells_injective d (Finset.map_injective (digitIndex d) he)
theorem lineDigits_injective (d : ℕ) : Function.Injective (@lineDigits d) := by
intro p q he
exact lineCells_injective d (Finset.map_injective (digitIndex d) he)
def pointX {d : ℕ} (p : PointLabel d) : ℝ := digitSum 5 (pointDigits p)
def lineX {d : ℕ} (l : LineLabel d) : ℝ := digitSum 5 (lineDigits l)
def pointT {d : ℕ} (p : PointLabel d) : ℝ := 1 + digitSum 25 (pointDigits p)
def lineT {d : ℕ} (l : LineLabel d) : ℝ := 1 + digitSum 25 (lineDigits l)
theorem incidence_digit_identity {d : ℕ} (e : EdgeLabel d) :
let z : ℝ := 5 ^ (digitIndex d (e.2, e.1 e.2))
0 < z ∧ pointX (edgePoint e) - lineX (edgeLine e) = z ∧
pointT (edgePoint e) - lineT (edgeLine e) = z ^ 2 := by
have hnew : digitIndex d (e.2, e.1 e.2) ∉ lineDigits (edgeLine e) := by
simp [lineDigits, completing_cell_absent]
have hcells : pointDigits (edgePoint e) =
insert (digitIndex d (e.2, e.1 e.2)) (lineDigits (edgeLine e)) := by
simp only [pointDigits, lineDigits, incidence_cells, Finset.map_insert]
dsimp only
refine ⟨by positivity, ?_, ?_⟩
· simp [pointX, lineX, digitSum, hcells, Finset.sum_insert hnew]
· simp only [pointT, lineT, hcells, digitSum, Finset.sum_insert hnew]
have hp : (25 : ℝ) ^ (digitIndex d (e.2, e.1 e.2)) =
((5 : ℝ) ^ (digitIndex d (e.2, e.1 e.2))) ^ 2 := by
rw [← pow_mul, Nat.mul_comm, pow_mul]
norm_num
linarith
end
end Proof
end OriginalLabelDigits
/- ## SeedPattern -/
section OriginalSeedPattern
/- Abstract hypotheses on a finite incidence pattern and its lacunary realization. -/
namespace Proof
open Filter
open scoped Topology
noncomputable section
structure SeedPattern (L P E : Type*) where
line : E → L
point : E → P
endpoints_injective : Function.Injective (fun e => (line e, point e))
LX : L → ℝ
LT : L → ℝ
PX : P → ℝ
PT : P → ℝ
LT_pos : ∀ l, 0 < LT l
PT_pos : ∀ p, 0 < PT p
LT_injective : Function.Injective LT
PT_injective : Function.Injective PT
line_margin : ∀ l k, l ≠ k → -(LX k - LX l) ^ 2 / 2 - (LT k - LT l) / 4 < 0
point_margin : ∀ p q, p ≠ q → -(PX q - PX p) ^ 2 / 2 + (PT q - PT p) / 4 < 0
edge_positive : ∀ e, LX (line e) < PX (point e)
edge_identity : ∀ e, PT (point e) - LT (line e) = (PX (point e) - LX (line e)) ^ 2
def coordinatePattern (d : ℕ) : SeedPattern (LineLabel d) (PointLabel d) (EdgeLabel d) where
line := edgeLine
point := edgePoint
endpoints_injective := edge_endpoints_injective d
LX := lineX
LT := lineT
PX := pointX
PT := pointT
LT_pos l := by
have hh : 0 ≤ digitSum 25 (lineDigits l) := Finset.sum_nonneg (fun _ _ => by positivity)
dsimp [lineT]; linarith
PT_pos p := by
have hh : 0 ≤ digitSum 25 (pointDigits p) := Finset.sum_nonneg (fun _ _ => by positivity)
dsimp [pointT]; linarith
LT_injective := by
intro l k he
by_contra hne
have hh := (digit_separation ((lineDigits_injective d).ne hne)).2.1
apply hh
dsimp [lineT] at he
linarith
PT_injective := by
intro p q he
by_contra hne
have hh := (digit_separation ((pointDigits_injective d).ne hne)).2.1
apply hh
dsimp [pointT] at he
linarith
line_margin := by
intro l k hne
obtain ⟨hX, _, hsep⟩ := digit_separation ((lineDigits_injective d).ne hne.symm)
have hm := (signed_digit_margin hsep).1
have hsq : 0 < (digitSum 5 (lineDigits k) - digitSum 5 (lineDigits l)) ^ 2 :=
sq_pos_of_ne_zero (sub_ne_zero.mpr hX)
dsimp [lineX, lineT]
have he : 1 + digitSum 25 (lineDigits k) - (1 + digitSum 25 (lineDigits l)) =
digitSum 25 (lineDigits k) - digitSum 25 (lineDigits l) := by ring
rw [he]
linarith
point_margin := by
intro p q hne
obtain ⟨hX, _, hsep⟩ := digit_separation ((pointDigits_injective d).ne hne.symm)
have hm := (signed_digit_margin hsep).2
have hsq : 0 < (digitSum 5 (pointDigits q) - digitSum 5 (pointDigits p)) ^ 2 :=
sq_pos_of_ne_zero (sub_ne_zero.mpr hX)
dsimp [pointX, pointT]
have he : 1 + digitSum 25 (pointDigits q) - (1 + digitSum 25 (pointDigits p)) =
digitSum 25 (pointDigits q) - digitSum 25 (pointDigits p) := by ring
rw [he]
linarith
edge_positive e := by
obtain ⟨hz, hx, ht⟩ := incidence_digit_identity e
linarith
edge_identity e := by
obtain ⟨hz, hx, ht⟩ := incidence_digit_identity e
rw [hx, ht]
def SeedPattern.base {L P E : Type*} (S : SeedPattern L P E) (ε : ℝ) : L ⊕ P → ℂ :=
Sum.elim (fun l => lineSeed ε (S.LX l) (S.LT l)) (fun p => pointSeed ε (S.PX p) (S.PT p))
def SeedPattern.rot {L P E : Type*} (S : SeedPattern L P E) (ε : ℝ) (e : E) : ℂ :=
seedCorrection ε (S.LX (S.line e)) (S.LT (S.line e)) (S.PX (S.point e)) (S.PT (S.point e))
def SeedPattern.coeff {L P E : Type*} (S : SeedPattern L P E) (ε : ℝ) (e : E) : ℂ :=
seedCoefficient ε (S.LX (S.line e)) (S.LT (S.line e)) (S.PX (S.point e)) (S.PT (S.point e))
theorem SeedPattern.coeff_continuous {L P E : Type*} (S : SeedPattern L P E) (e : E) :
ContinuousAt (fun ε => S.coeff ε e) 0 :=
continuousAt_seedCoefficient _ _ _ _ (S.edge_positive e)
end
end Proof
end OriginalSeedPattern
/- ## PreparedSeed -/
section OriginalPreparedSeed
/- Existence of a finite seed with exact unit corrections and a strict support margin. -/
namespace Proof
open Filter
open scoped Topology
noncomputable section
structure PreparedSeed {L P E : Type*} [Fintype E] (l : E → L) (p : E → P) where
base : L ⊕ P → ℂ
rotation : E → ℂ
base_ne_zero : ∀ i, base i ≠ 0
base_norm_lt : ∀ i, ‖base i‖ < 1
radii_injective : Function.Injective (fun i => ‖base i‖)
rotation_norm : ∀ e, ‖rotation e‖ = 1
unit_edge : ∀ e, ‖base (Sum.inl (l e)) - base (Sum.inr (p e)) * rotation e‖ = 1
support_margin : ∀ i j, i ≠ j →
support (base i) (base j) < -2 * ∑ e, ‖rotation e - 1‖
chord_im_negative : ∀ e,
(starRingEnd ℂ (base (Sum.inl (l e))) * base (Sum.inr (p e)) * rotation e).im < 0
theorem SeedPattern.exists_prepared {L P E : Type*} [Fintype L] [Fintype P] [Fintype E]
(S : SeedPattern L P E) : Nonempty (PreparedSeed S.line S.point) := by
let A := fun ε : ℝ => 2 * ∑ e, ‖S.coeff ε e‖
have hcoeff : ∀ e, ContinuousAt (fun ε => S.coeff ε e) 0 := S.coeff_continuous
have hA : ContinuousAt A 0 := by unfold A; fun_prop
have hbase : ∀ i, Continuous (fun ε => S.base ε i) := by
intro i
cases i with
| inl l => exact continuous_lineSeed _ _
| inr p => exact continuous_pointSeed _ _
have hbase0 : ∀ i, ‖S.base 0 i‖ = 1 / 2 := by
intro i
cases i <;> norm_num [SeedPattern.base, lineSeed, pointSeed, Complex.norm_def, Complex.normSq_apply]
have hbounds : ∀ i, ∀ᶠ ε in 𝓝[>] (0 : ℝ), S.base ε i ≠ 0 ∧ ‖S.base ε i‖ < 1 := by
intro i
have hlo : ∀ᶠ ε in 𝓝 (0 : ℝ), 0 < ‖S.base ε i‖ :=
continuousAt_const.eventually_lt (hbase i).norm.continuousAt (by rw [hbase0]; norm_num)
have hhi : ∀ᶠ ε in 𝓝 (0 : ℝ), ‖S.base ε i‖ < 1 :=
(hbase i).norm.continuousAt.eventually_lt continuousAt_const (by rw [hbase0]; norm_num)
filter_upwards [hlo.filter_mono nhdsWithin_le_nhds, hhi.filter_mono nhdsWithin_le_nhds] with ε hlo hhi
exact ⟨norm_pos_iff.mp hlo, hhi⟩
have hnorms : ∀ i j, ∀ᶠ ε in 𝓝[>] (0 : ℝ), i ≠ j → ‖S.base ε i‖ ≠ ‖S.base ε j‖ := by
intro i j
by_cases hij : i = j
· exact Eventually.of_forall (fun _ h => (h hij).elim)
cases i with
| inl l =>
cases j with
| inl k =>
have hk : l ≠ k := fun h => hij (congrArg Sum.inl h)
exact (eventually_line_norm_ne _ _ _ _ (S.LT_injective.ne hk)).mono (fun _ h _ => h)
| inr p =>
exact (eventually_cross_norm_ne _ _ _ _ (S.LT_pos l) (S.PT_pos p)).mono (fun _ h _ => h)
| inr p =>
cases j with
| inl l =>
exact (eventually_cross_norm_ne _ _ _ _ (S.LT_pos l) (S.PT_pos p)).mono (fun _ h _ => h.symm)
| inr q =>
have hq : p ≠ q := fun h => hij (congrArg Sum.inr h)
exact (eventually_point_norm_ne _ _ _ _ (S.PT_injective.ne hq)).mono (fun _ h _ => h)
have hsupports : ∀ i j, ∀ᶠ ε in 𝓝[>] (0 : ℝ),
i ≠ j → support (S.base ε i) (S.base ε j) < -ε ^ 3 * A ε := by
intro i j
by_cases hij : i = j
· exact Eventually.of_forall (fun _ h => (h hij).elim)
cases i with
| inl l =>
cases j with
| inl k =>
have hk : l ≠ k := fun h => hij (congrArg Sum.inl h)
exact (eventually_line_support _ _ _ _ A hA (S.line_margin l k hk)).mono (fun _ h _ => h)
| inr p =>
exact (eventually_cross_support _ _ _ _ A hA).mono (fun _ h _ => h.1)
| inr p =>
cases j with
| inl l =>
exact (eventually_cross_support _ _ _ _ A hA).mono (fun _ h _ => h.2)
| inr q =>
have hq : p ≠ q := fun h => hij (congrArg Sum.inr h)
exact (eventually_point_support _ _ _ _ A hA (S.point_margin p q hq)).mono (fun _ h _ => h)
have hedges : ∀ e, ∀ᶠ ε in 𝓝[>] (0 : ℝ),
‖S.rot ε e‖ = 1 ∧
‖S.base ε (Sum.inl (S.line e)) - S.base ε (Sum.inr (S.point e)) * S.rot ε e‖ = 1 ∧
S.rot ε e - 1 = (ε : ℂ) ^ 3 * S.coeff ε e := fun e =>
(seedCorrection_properties _ _ _ _ (S.edge_positive e) (S.edge_identity e)).filter_mono
nhdsWithin_le_nhds
have him : ∀ e, ∀ᶠ ε in 𝓝[>] (0 : ℝ),
(starRingEnd ℂ (S.base ε (Sum.inl (S.line e))) *
S.base ε (Sum.inr (S.point e)) * S.rot ε e).im < 0 := fun e =>
seedCorrection_im_negative _ _ _ _ (S.edge_positive e)
have hbAll : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ∀ i, S.base ε i ≠ 0 ∧ ‖S.base ε i‖ < 1 := by
simpa only [eventually_all] using hbounds
have hnAll : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ∀ i j, i ≠ j → ‖S.base ε i‖ ≠ ‖S.base ε j‖ := by
simpa only [eventually_all] using hnorms
have hsAll : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ∀ i j, i ≠ j →
support (S.base ε i) (S.base ε j) < -ε ^ 3 * A ε := by
simpa only [eventually_all] using hsupports
have heAll : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ∀ e,
‖S.rot ε e‖ = 1 ∧
‖S.base ε (Sum.inl (S.line e)) - S.base ε (Sum.inr (S.point e)) * S.rot ε e‖ = 1 ∧
S.rot ε e - 1 = (ε : ℂ) ^ 3 * S.coeff ε e := by
simpa only [eventually_all] using hedges
have hiAll : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ∀ e,
(starRingEnd ℂ (S.base ε (Sum.inl (S.line e))) *
S.base ε (Sum.inr (S.point e)) * S.rot ε e).im < 0 := by
simpa only [eventually_all] using him
have hall := hbAll.and (hnAll.and (hsAll.and (heAll.and (hiAll.and self_mem_nhdsWithin))))
obtain ⟨ε, hb, hn, hs, he, hi, hε⟩ := hall.exists
have hε : 0 < ε := hε
have hsum : 2 * ∑ e, ‖S.rot ε e - 1‖ = ε ^ 3 * A ε := by
simp_rw [fun e => (he e).2.2, norm_mul, norm_pow, Complex.norm_real, Real.norm_eq_abs,
abs_of_pos hε]
rw [← Finset.mul_sum]
dsimp [A]
ring
refine ⟨{
base := S.base ε
rotation := S.rot ε
base_ne_zero := fun i => (hb i).1
base_norm_lt := fun i => (hb i).2
radii_injective := fun i j hh => by_contra fun hij => hn i j hij hh
rotation_norm := fun e => (he e).1
unit_edge := fun e => (he e).2.1
support_margin := ?_
chord_im_negative := hi }⟩
intro i j hij
have hh := hs i j hij
linarith [hsum]
end
end Proof
end OriginalPreparedSeed
/- ## PhaseGeometry -/
section OriginalPhaseGeometry
/- Unit chords and radial changes with the directions held fixed. -/
namespace Proof
noncomputable section
def unitChord (r s : ℝ) : ℂ := Complex.exp (((-chordAngle r s : ℝ) : ℂ) * Complex.I)
theorem unitChord_norm (r s : ℝ) : ‖unitChord r s‖ = 1 := Complex.norm_exp_ofReal_mul_I _
theorem unitChord_re {r s : ℝ} (hf : ChordFeasible r s) : (unitChord r s).re = chordCos r s := by
simp [unitChord, Complex.exp_re, chordAngle, Real.cos_arccos hf.2.2.1.le hf.2.2.2.le]
theorem unitChord_im (r s : ℝ) : (unitChord r s).im = -Real.sqrt (1 - chordCos r s ^ 2) := by
simp [unitChord, Complex.exp_im, chordAngle, Real.sin_arccos]
theorem unitChord_im_neg {r s : ℝ} (hf : ChordFeasible r s) : (unitChord r s).im < 0 := by
rw [unitChord_im]
exact neg_neg_of_pos (Real.sqrt_pos.mpr (chord_discriminant_pos hf.2.2.1 hf.2.2.2))
theorem unitChord_distance {r s : ℝ} (hf : ChordFeasible r s) :
‖(r : ℂ) - (s : ℂ) * unitChord r s‖ = 1 := by
have hs : Complex.normSq ((r : ℂ) - (s : ℂ) * unitChord r s) = 1 := by
rw [Complex.normSq_sub, Complex.normSq_mul, Complex.normSq_eq_norm_sq (unitChord r s),
unitChord_norm, one_pow, mul_one]
simp only [Complex.normSq_ofReal, Complex.mul_re, Complex.ofReal_re,
Complex.ofReal_im, zero_mul, sub_zero, Complex.conj_re, unitChord_re hf]
unfold chordCos
field_simp [hf.1, hf.2.1]
ring
rw [Complex.normSq_eq_norm_sq] at hs
nlinarith [norm_nonneg ((r : ℂ) - (s : ℂ) * unitChord r s)]
theorem normSq_sub_mul (a b w : ℂ) :
Complex.normSq (a - b * w) = Complex.normSq a + Complex.normSq b * Complex.normSq w -
2 * (starRingEnd ℂ a * b * w).re := by
simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im, Complex.mul_re,
Complex.mul_im, Complex.conj_re, Complex.conj_im]
ring
theorem lower_half_unique {z w : ℂ} (hn : ‖z‖ = ‖w‖) (hr : z.re = w.re)
(hz : z.im < 0) (hw : w.im < 0) : z = w := by
have hsq : Complex.normSq z = Complex.normSq w := by
simp only [Complex.normSq_eq_norm_sq, hn]
apply Complex.ext hr
simp only [Complex.normSq_apply] at hsq
rw [hr] at hsq
nlinarith
theorem corrected_chord {a b w : ℂ} (ha : a ≠ 0) (hb : b ≠ 0) (hw : ‖w‖ = 1)
(he : ‖a - b * w‖ = 1) (him : (starRingEnd ℂ a * b * w).im < 0) :
ChordFeasible ‖a‖ ‖b‖ ∧
starRingEnd ℂ a * b * w = ((‖a‖ * ‖b‖ : ℝ) : ℂ) * unitChord ‖a‖ ‖b‖ := by
let q := starRingEnd ℂ a * b * w
have hr : 0 < ‖a‖ := norm_pos_iff.mpr ha
have hs : 0 < ‖b‖ := norm_pos_iff.mpr hb
have hprod : 0 < ‖a‖ * ‖b‖ := mul_pos hr hs
have hqnorm : ‖q‖ = ‖a‖ * ‖b‖ := by simp [q, hw]
have hqnormSq : q.re ^ 2 + q.im ^ 2 = (‖a‖ * ‖b‖) ^ 2 := by
have h := Complex.normSq_eq_norm_sq q
rw [hqnorm] at h
simpa [Complex.normSq_apply, pow_two] using h
have hqre : q.re = (‖a‖ ^ 2 + ‖b‖ ^ 2 - 1) / 2 := by
have h := normSq_sub_mul a b w
simp only [Complex.normSq_eq_norm_sq, he, hw, one_pow, mul_one] at h
change _ = _ - 2 * q.re at h
linarith
have hratio : q.re / (‖a‖ * ‖b‖) = chordCos ‖a‖ ‖b‖ := by
rw [hqre]
unfold chordCos
ring
have hqim : q.im < 0 := him
have hsqim : 0 < q.im ^ 2 := sq_pos_of_ne_zero (ne_of_lt hqim)
have hlo : -(‖a‖ * ‖b‖) < q.re := by nlinarith
have hhi : q.re < ‖a‖ * ‖b‖ := by nlinarith
have hf : ChordFeasible ‖a‖ ‖b‖ := by
refine ⟨ne_of_gt hr, ne_of_gt hs, ?_, ?_⟩
· rw [← hratio]
exact (lt_div_iff₀ hprod).mpr (by linarith)
· rw [← hratio]
exact (div_lt_iff₀ hprod).mpr (by linarith)
refine ⟨hf, ?_⟩
apply lower_half_unique
· calc
‖q‖ = ‖a‖ * ‖b‖ := hqnorm
_ = ‖((‖a‖ * ‖b‖ : ℝ) : ℂ) * unitChord ‖a‖ ‖b‖‖ := by
rw [norm_mul, unitChord_norm, Complex.norm_of_nonneg hprod.le, mul_one]
· calc
q.re = (‖a‖ * ‖b‖) * chordCos ‖a‖ ‖b‖ := by rw [← hratio]; field_simp
_ = (((‖a‖ * ‖b‖ : ℝ) : ℂ) * unitChord ‖a‖ ‖b‖).re := by simp [unitChord_re hf]
· exact him
· simpa only [Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, zero_mul, zero_add, add_zero] using
mul_neg_of_pos_of_neg hprod (unitChord_im_neg hf)
def radialBase {I : Type*} (b : I → ℂ) (r : I → ℝ) (i : I) : ℂ :=
(r i : ℂ) * (b i / (‖b i‖ : ℂ))
theorem radialBase_at_norm {I : Type*} (b : I → ℂ) (hb : ∀ i, b i ≠ 0) :
radialBase b (fun i => ‖b i‖) = b := by
funext i
exact mul_div_cancel₀ _ (Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr (hb i)))
theorem normalized_norm {b : ℂ} (hb : b ≠ 0) : ‖b / (‖b‖ : ℂ)‖ = 1 := by
rw [norm_div, Complex.norm_of_nonneg (norm_nonneg _)]
exact div_self (norm_ne_zero_iff.mpr hb)
theorem radialBase_norm {I : Type*} (b : I → ℂ) (hb : ∀ i, b i ≠ 0)
(r : I → ℝ) (hr : ∀ i, 0 ≤ r i) (i : I) : ‖radialBase b r i‖ = r i := by
rw [radialBase, norm_mul, normalized_norm (hb i), mul_one, Complex.norm_of_nonneg (hr i)]
def directionRatio (a b : ℂ) : ℂ := (a / (‖a‖ : ℂ)) / (b / (‖b‖ : ℂ))
theorem directionRatio_norm {a b : ℂ} (ha : a ≠ 0) (hb : b ≠ 0) : ‖directionRatio a b‖ = 1 := by
rw [directionRatio, norm_div, normalized_norm ha, normalized_norm hb, div_self (by norm_num : (1 : ℝ) ≠ 0)]
theorem directionRatio_cancel {a b : ℂ} (ha : a ≠ 0) (hb : b ≠ 0) :
starRingEnd ℂ a * b * directionRatio a b = ((‖a‖ * ‖b‖ : ℝ) : ℂ) := by
have hra : (‖a‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr ha)
have hrb : (‖b‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr hb)
have hnorm : starRingEnd ℂ a * a = (‖a‖ : ℂ) ^ 2 := by
rw [← Complex.normSq_eq_conj_mul_self, Complex.normSq_eq_norm_sq, Complex.ofReal_pow]
unfold directionRatio
calc
starRingEnd ℂ a * b * ((a / (‖a‖ : ℂ)) / (b / (‖b‖ : ℂ))) =
(starRingEnd ℂ a * a) * (‖b‖ : ℂ) / (‖a‖ : ℂ) := by field_simp [hra, hrb, hb]
_ = ((‖a‖ * ‖b‖ : ℝ) : ℂ) := by rw [hnorm, Complex.ofReal_mul]; field_simp [hra]
theorem phaseRotations_factor {L P E : Type*} (l : E → L) (p : E → P) (θ : E → ℝ)
(σ : E → ℂ) (hσ : ∀ e, Complex.exp ((θ e : ℂ) * Complex.I) = σ e)
(z : (L → ℝ) × (P → ℝ)) (e : E) :
phaseRotations l p θ z e = σ e * unitChord (z.1 (l e)) (z.2 (p e)) := by
simp only [phaseRotations, unitChord, Complex.ofReal_sub, Complex.ofReal_neg, sub_mul, neg_mul,
Complex.exp_sub, Complex.exp_neg, hσ, div_eq_mul_inv]
theorem radial_unit_distance {a b : ℂ} (ha : a ≠ 0) (hb : b ≠ 0)
{r s : ℝ} (hf : ChordFeasible r s) :
‖(r : ℂ) * (a / (‖a‖ : ℂ)) - (s : ℂ) * (b / (‖b‖ : ℂ)) *
(directionRatio a b * unitChord r s)‖ = 1 := by
have hbn : b / (‖b‖ : ℂ) ≠ 0 :=
div_ne_zero hb (Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr hb))
have hra : (‖a‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr ha)
have hrb : (‖b‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr hb)
have he : (r : ℂ) * (a / (‖a‖ : ℂ)) - (s : ℂ) * (b / (‖b‖ : ℂ)) *
(directionRatio a b * unitChord r s) =
(a / (‖a‖ : ℂ)) * ((r : ℂ) - (s : ℂ) * unitChord r s) := by
unfold directionRatio
field_simp [hbn, hra, hrb, hb]
rw [he, norm_mul, normalized_norm ha, unitChord_distance hf, one_mul]
def PreparedSeed.angles {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (e : E) : ℝ :=
Complex.arg (directionRatio (Q.base (Sum.inl (l e))) (Q.base (Sum.inr (p e))))
def PreparedSeed.radii {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) : (L → ℝ) × (P → ℝ) :=
(fun i => ‖Q.base (Sum.inl i)‖, fun j => ‖Q.base (Sum.inr j)‖)
theorem PreparedSeed.angles_exp {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (e : E) :
Complex.exp ((Q.angles e : ℂ) * Complex.I) =
directionRatio (Q.base (Sum.inl (l e))) (Q.base (Sum.inr (p e))) := by
have hnorm := directionRatio_norm (Q.base_ne_zero (Sum.inl (l e))) (Q.base_ne_zero (Sum.inr (p e)))
have hh := Complex.norm_mul_exp_arg_mul_I (directionRatio (Q.base (Sum.inl (l e))) (Q.base (Sum.inr (p e))))
simpa only [PreparedSeed.angles, hnorm, Complex.ofReal_one, one_mul] using hh
theorem PreparedSeed.feasible {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (e : E) : ChordFeasible (Q.radii.1 (l e)) (Q.radii.2 (p e)) :=
(corrected_chord (Q.base_ne_zero _) (Q.base_ne_zero _) (Q.rotation_norm e)
(Q.unit_edge e) (Q.chord_im_negative e)).1
theorem PreparedSeed.phase_at_radii {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) : phaseRotations l p Q.angles Q.radii = Q.rotation := by
funext e
have ha := Q.base_ne_zero (Sum.inl (l e))
have hb := Q.base_ne_zero (Sum.inr (p e))
have he := (corrected_chord ha hb (Q.rotation_norm e) (Q.unit_edge e) (Q.chord_im_negative e)).2
apply mul_left_cancel₀ (mul_ne_zero ((map_ne_zero (starRingEnd ℂ)).mpr ha) hb)
rw [phaseRotations_factor l p Q.angles _ Q.angles_exp, ← mul_assoc, directionRatio_cancel ha hb]
exact he.symm
end
end Proof
end OriginalPhaseGeometry
/- ## Perturbation -/
section OriginalPerturbation
/- A simultaneous radius perturbation preserving support and separating every subset product. -/
namespace Proof
open Set Filter
open scoped Topology
noncomputable section
def joinedRadii {L P : Type*} (z : (L → ℝ) × (P → ℝ)) : L ⊕ P → ℝ := Sum.elim z.1 z.2
def PreparedSeed.varBase {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (z : (L → ℝ) × (P → ℝ)) : L ⊕ P → ℂ := radialBase Q.base (joinedRadii z)
theorem PreparedSeed.varBase_at_radii {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) : Q.varBase Q.radii = Q.base := by
have hh : joinedRadii Q.radii = fun i => ‖Q.base i‖ := by funext i; cases i <;> rfl
unfold PreparedSeed.varBase
rw [hh]
exact radialBase_at_norm Q.base Q.base_ne_zero
theorem PreparedSeed.varBase_continuous {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (i : L ⊕ P) : Continuous (fun z => Q.varBase z i) := by
cases i <;> simp only [PreparedSeed.varBase, radialBase, joinedRadii, Sum.elim_inl, Sum.elim_inr] <;> fun_prop
theorem joinedRadii_continuous {L P : Type*} (i : L ⊕ P) :
Continuous (fun z : (L → ℝ) × (P → ℝ) => joinedRadii z i) := by
cases i <;> simp only [joinedRadii, Sum.elim_inl, Sum.elim_inr] <;> fun_prop
theorem PreparedSeed.varBase_unit_edge {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (z : (L → ℝ) × (P → ℝ)) (e : E)
(hf : ChordFeasible (z.1 (l e)) (z.2 (p e))) :
‖Q.varBase z (Sum.inl (l e)) - Q.varBase z (Sum.inr (p e)) * phaseRotations l p Q.angles z e‖ = 1 := by
rw [phaseRotations_factor l p Q.angles _ Q.angles_exp]
exact radial_unit_distance (Q.base_ne_zero _) (Q.base_ne_zero _) hf
structure SeparatedSeed {L P E : Type*} [Fintype E] (l : E → L) (p : E → P) where
base : L ⊕ P → ℂ
rotation : E → ℂ
base_ne_zero : ∀ i, base i ≠ 0
base_norm_lt : ∀ i, ‖base i‖ < 1
radii_injective : Function.Injective (fun i => ‖base i‖)
rotation_norm : ∀ e, ‖rotation e‖ = 1
unit_edge : ∀ e, ‖base (Sum.inl (l e)) - base (Sum.inr (p e)) * rotation e‖ = 1
support_margin : ∀ i j, i ≠ j → support (base i) (base j) < -2 * ∑ e, ‖rotation e - 1‖
products_injective : Function.Injective (subsetProduct rotation)
def GoodRadii {L P E : Type*} [Fintype E] {l : E → L} {p : E → P}
(Q : PreparedSeed l p) (z : (L → ℝ) × (P → ℝ)) : Prop :=
(∀ i, 0 < joinedRadii z i) ∧ (∀ i, ‖Q.varBase z i‖ < 1) ∧
Function.Injective (joinedRadii z) ∧
(∀ e, ChordFeasible (z.1 (l e)) (z.2 (p e))) ∧
∀ i j, i ≠ j → support (Q.varBase z i) (Q.varBase z j) <
-2 * ∑ e, ‖phaseRotations l p Q.angles z e - 1‖
theorem PreparedSeed.goodRadii_nhds {L P E : Type*} [Fintype L] [Fintype P] [Fintype E]
{l : E → L} {p : E → P} (Q : PreparedSeed l p) :
∀ᶠ z in 𝓝 Q.radii, GoodRadii Q z := by
have hjoined : ∀ i, joinedRadii Q.radii i = ‖Q.base i‖ := by intro i; cases i <;> rfl
have hr : ∀ i, Q.radii.1 i ≠ 0 := fun i => norm_ne_zero_iff.mpr (Q.base_ne_zero _)
have hs : ∀ j, Q.radii.2 j ≠ 0 := fun j => norm_ne_zero_iff.mpr (Q.base_ne_zero _)
have hrot : ∀ e, ContinuousAt (fun z => phaseRotations l p Q.angles z e) Q.radii :=
phaseRotations_continuousAt l p Q.angles Q.radii hr hs
have hbase : ∀ i, ContinuousAt (fun z => Q.varBase z i) Q.radii :=
fun i => (Q.varBase_continuous i).continuousAt
have hpos : ∀ i, ∀ᶠ z in 𝓝 Q.radii, 0 < joinedRadii z i := by
intro i
apply continuousAt_const.eventually_lt (joinedRadii_continuous i).continuousAt
rw [hjoined]
exact norm_pos_iff.mpr (Q.base_ne_zero i)
have hnorm : ∀ i, ∀ᶠ z in 𝓝 Q.radii, ‖Q.varBase z i‖ < 1 := by
intro i
apply (hbase i).norm.eventually_lt continuousAt_const
rw [Q.varBase_at_radii]
exact Q.base_norm_lt i
have hinj : ∀ i j, ∀ᶠ z in 𝓝 Q.radii, i ≠ j → joinedRadii z i ≠ joinedRadii z j := by
intro i j
by_cases hij : i = j
· exact Eventually.of_forall (fun _ h => (h hij).elim)
have hdiff : ContinuousAt (fun z => joinedRadii z i - joinedRadii z j) Q.radii :=
(joinedRadii_continuous i).continuousAt.sub (joinedRadii_continuous j).continuousAt
have hdiff0 : joinedRadii Q.radii i - joinedRadii Q.radii j ≠ 0 := by
rw [hjoined, hjoined]
exact sub_ne_zero.mpr (Q.radii_injective.ne hij)
exact (hdiff.eventually_ne hdiff0).mono (fun _ hh _ => sub_ne_zero.mp hh)
have hfeas : ∀ e, ∀ᶠ z in 𝓝 Q.radii, ChordFeasible (z.1 (l e)) (z.2 (p e)) := by
intro e
have hcos : ContinuousAt (fun z : (L → ℝ) × (P → ℝ) => chordCos (z.1 (l e)) (z.2 (p e))) Q.radii := by
unfold chordCos
fun_prop (disch := aesop)
have hl : ∀ᶠ z in 𝓝 Q.radii, -1 < chordCos (z.1 (l e)) (z.2 (p e)) :=
continuousAt_const.eventually_lt hcos (Q.feasible e).2.2.1
have hu : ∀ᶠ z in 𝓝 Q.radii, chordCos (z.1 (l e)) (z.2 (p e)) < 1 :=
hcos.eventually_lt continuousAt_const (Q.feasible e).2.2.2
filter_upwards [hpos (Sum.inl (l e)), hpos (Sum.inr (p e)), hl, hu] with z hr hs hl hu
exact ⟨ne_of_gt hr, ne_of_gt hs, hl, hu⟩
have hmargin : ∀ i j, ∀ᶠ z in 𝓝 Q.radii, i ≠ j →
support (Q.varBase z i) (Q.varBase z j) < -2 * ∑ e, ‖phaseRotations l p Q.angles z e - 1‖ := by
intro i j
by_cases hij : i = j
· exact Eventually.of_forall (fun _ h => (h hij).elim)
have hc : ContinuousAt (fun z => support (Q.varBase z i) (Q.varBase z j) +
2 * ∑ e, ‖phaseRotations l p Q.angles z e - 1‖) Q.radii := by
have hri := Complex.continuous_re.continuousAt.comp (hbase i)
have hrj := Complex.continuous_re.continuousAt.comp (hbase j)
have hii := Complex.continuous_im.continuousAt.comp (hbase i)
have hij := Complex.continuous_im.continuousAt.comp (hbase j)
unfold support
exact ((hri.mul (hrj.sub hri)).add (hii.mul (hij.sub hii))).add
(continuousAt_const.mul
(tendsto_finsetSum Finset.univ (fun e _ =>
((hrot e).sub continuousAt_const).norm)))
have hvalue : support (Q.varBase Q.radii i) (Q.varBase Q.radii j) +
2 * ∑ e, ‖phaseRotations l p Q.angles Q.radii e - 1‖ < 0 := by
rw [Q.varBase_at_radii, Q.phase_at_radii]
linarith [Q.support_margin i j hij]
exact (hc.eventually_lt continuousAt_const hvalue).mono (fun _ hh _ => by linarith)
have hposAll : ∀ᶠ z in 𝓝 Q.radii, ∀ i, 0 < joinedRadii z i := by simpa only [eventually_all] using hpos
have hnAll : ∀ᶠ z in 𝓝 Q.radii, ∀ i, ‖Q.varBase z i‖ < 1 := by simpa only [eventually_all] using hnorm
have hiAll : ∀ᶠ z in 𝓝 Q.radii, ∀ i j, i ≠ j → joinedRadii z i ≠ joinedRadii z j := by
simpa only [eventually_all] using hinj
have hfAll : ∀ᶠ z in 𝓝 Q.radii, ∀ e, ChordFeasible (z.1 (l e)) (z.2 (p e)) := by
simpa only [eventually_all] using hfeas
have hmAll : ∀ᶠ z in 𝓝 Q.radii, ∀ i j, i ≠ j →
support (Q.varBase z i) (Q.varBase z j) < -2 * ∑ e, ‖phaseRotations l p Q.angles z e - 1‖ := by
simpa only [eventually_all] using hmargin
filter_upwards [hposAll, hnAll, hiAll, hfAll, hmAll] with z hp hn hi hf hm
exact ⟨hp, hn, fun i j h => by_contra (fun hij => hi i j hij h), hf, hm⟩
theorem PreparedSeed.exists_separated {L P E : Type*} [Fintype L] [Fintype P] [Fintype E]
{l : E → L} {p : E → P} (Q : PreparedSeed l p)
(hij : Function.Injective (fun e => (l e, p e))) : Nonempty (SeparatedSeed l p) := by
classical
obtain ⟨U, hUgood, hU, hz₀⟩ := mem_nhds_iff.mp Q.goodRadii_nhds
have hne : U.Nonempty := ⟨Q.radii, hz₀⟩
have hnz : ∀ z ∈ U, (∀ i, z.1 i ≠ 0) ∧ (∀ j, z.2 j ≠ 0) := by
intro z hz
exact ⟨fun i => ne_of_gt ((hUgood hz).1 (Sum.inl i)), fun j => ne_of_gt ((hUgood hz).1 (Sum.inr j))⟩
obtain ⟨z, hz, hprod⟩ := exists_injective_subsetProducts l p hij Q.angles U hU hne hnz
(fun e z hz => (hUgood hz).2.2.2.1 e)
obtain ⟨hpos, hnorm, hinj, hfeas, hmargin⟩ := hUgood hz
have hrnorm : ∀ i, ‖Q.varBase z i‖ = joinedRadii z i :=
radialBase_norm Q.base Q.base_ne_zero (joinedRadii z) (fun i => (hpos i).le)
refine ⟨{
base := Q.varBase z
rotation := phaseRotations l p Q.angles z
base_ne_zero := fun i => norm_pos_iff.mp (by rw [hrnorm]; exact hpos i)
base_norm_lt := hnorm
radii_injective := ?_
rotation_norm := phaseRotations_norm l p Q.angles z
unit_edge := fun e => Q.varBase_unit_edge z e (hfeas e)
support_margin := hmargin
products_injective := hprod }⟩
intro i j hh
dsimp only at hh
rw [hrnorm, hrnorm] at hh
exact hinj hh
end
end Proof
end OriginalPerturbation
/- ## Counting -/
section OriginalCounting
/- Exact vertex counts and a lower bound for unordered unit pairs. -/
namespace Proof
noncomputable section
def pairDistance {X : Type*} [MetricSpace X] (p : Sym2 X) : ℝ :=
Sym2.lift ⟨dist, fun a b => dist_comm a b⟩ p
def unitPairs {X : Type*} [MetricSpace X] (P : Finset X) : Finset (Sym2 X) := by
classical
exact P.sym2.filter (fun p => pairDistance p = 1)
def rotatedSet {I E : Type*} [Fintype I] [Fintype E] (b : I → ℂ) (w : E → ℂ) : Finset ℂ := by
classical
exact Finset.univ.image (rotatedCopy b w)
theorem mem_rotatedSet {I E : Type*} [Fintype I] [Fintype E]
(b : I → ℂ) (w : E → ℂ) (x : I × Finset E) :
rotatedCopy b w x ∈ rotatedSet b w := by
classical
exact Finset.mem_image.mpr ⟨x, Finset.mem_univ _, rfl⟩
theorem rotatedSet_card {I E : Type*} [Fintype I] [Fintype E]
(b : I → ℂ) (w : E → ℂ) (hinj : Function.Injective (rotatedCopy b w)) :
(rotatedSet b w).card = Fintype.card I * 2 ^ Fintype.card E := by
classical
rw [rotatedSet, Finset.card_image_of_injective _ hinj]
simp
theorem rotatedSet_convexIndependent {I E : Type*} [Fintype I] [Fintype E]
(b : I → ℂ) (w : E → ℂ) (hc : ConvexIndependent ℝ (rotatedCopy b w)) :
ConvexIndependent ℝ (fun z : ↥(rotatedSet b w : Set ℂ) => (z : ℂ)) := by
have he : (rotatedSet b w : Set ℂ) = Set.range (rotatedCopy b w) := by
classical
simp [rotatedSet]
rw [he]
exact hc.range
abbrev LiftedEdge (E : Type*) := (e : E) × {S : Finset E // e ∉ S}
theorem subsets_avoiding_card {E : Type*} [Fintype E] [DecidableEq E] (e : E) :
Fintype.card {S : Finset E // e ∉ S} = 2 ^ (Fintype.card E - 1) := by
rw [Fintype.card_of_subtype ((Finset.univ.erase e).powerset)
(fun S => by simp [Finset.mem_powerset, Finset.subset_erase])]
simp
theorem liftedEdge_card {E : Type*} [Fintype E] [DecidableEq E] :
Fintype.card (LiftedEdge E) = Fintype.card E * 2 ^ (Fintype.card E - 1) := by
simp only [LiftedEdge, Fintype.card_sigma, subsets_avoiding_card,
Finset.sum_const, Finset.card_univ, smul_eq_mul]
def liftedPair {L P E : Type*} [DecidableEq E]
(l : E → L) (p : E → P) (b : L ⊕ P → ℂ) (w : E → ℂ) (x : LiftedEdge E) : Sym2 ℂ :=
s(rotatedCopy b w (Sum.inl (l x.1), x.2.val),
rotatedCopy b w (Sum.inr (p x.1), insert x.1 x.2.val))
theorem liftedPair_injective {L P E : Type*} [DecidableEq E]
(l : E → L) (p : E → P) (b : L ⊕ P → ℂ) (w : E → ℂ)
(he : Function.Injective (fun e => (l e, p e)))
(hinj : Function.Injective (rotatedCopy b w)) :
Function.Injective (liftedPair l p b w) := by
rintro ⟨e, S⟩ ⟨f, T⟩ hh
simp only [liftedPair, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hh
rcases hh with ⟨hl, hp⟩ | ⟨hl, hp⟩
· have hl := hinj hl
have hp := hinj hp
have hlf : l e = l f := Sum.inl.inj (congrArg Prod.fst hl)
have hpf : p e = p f := Sum.inr.inj (congrArg Prod.fst hp)
have hef := he (Prod.ext hlf hpf)
subst f
have hST : S = T := Subtype.ext (congrArg Prod.snd hl)
subst T
rfl
· have hbad := congrArg Prod.fst (hinj hl)
cases hbad
theorem liftedPair_mem_unitPairs {L P E : Type*}
[Fintype L] [Fintype P] [Fintype E] [DecidableEq E]
(l : E → L) (p : E → P) (b : L ⊕ P → ℂ) (w : E → ℂ)
(hw : ∀ e, ‖w e‖ = 1)
(hedge : ∀ e, ‖b (Sum.inl (l e)) - b (Sum.inr (p e)) * w e‖ = 1)
(x : LiftedEdge E) : liftedPair l p b w x ∈ unitPairs (rotatedSet b w) := by
classical
apply Finset.mem_filter.mpr
constructor
· apply Finset.mk_mem_sym2_iff.mpr
exact ⟨mem_rotatedSet b w _, mem_rotatedSet b w _⟩
· exact rotatedCopy_unit_edge b w hw _ _ x.1 (hedge x.1) x.2.val x.2.property
theorem amplification_unitPairs_bound {L P E : Type*}
[Fintype L] [Fintype P] [Fintype E] [DecidableEq E]
(l : E → L) (p : E → P) (b : L ⊕ P → ℂ) (w : E → ℂ)
(he : Function.Injective (fun e => (l e, p e)))
(hinj : Function.Injective (rotatedCopy b w)) (hw : ∀ e, ‖w e‖ = 1)
(hedge : ∀ e, ‖b (Sum.inl (l e)) - b (Sum.inr (p e)) * w e‖ = 1) :
Fintype.card E * 2 ^ (Fintype.card E - 1) ≤ (unitPairs (rotatedSet b w)).card := by
let f : LiftedEdge E → unitPairs (rotatedSet b w) := fun x =>
⟨liftedPair l p b w x, liftedPair_mem_unitPairs l p b w hw hedge x⟩
have hf : Function.Injective f := fun x y h =>
liftedPair_injective l p b w he hinj (congrArg Subtype.val h)
have hc := Fintype.card_le_of_injective f hf
simpa only [liftedEdge_card, Fintype.card_coe] using hc
end
end Proof
end OriginalCounting
/- ## Counterexample -/
section OriginalCounterexample
/- Convex configurations with an unbounded ratio of unit distances to vertices. -/
namespace Proof
noncomputable section
def constructionSize (d : ℕ) : ℕ := 2 * d ^ d * 2 ^ (d ^ (d + 1))
theorem convex_unit_counterexample (d : ℕ) (hd : 2 ≤ d) :
∃ P : Finset ℂ,
ConvexIndependent ℝ (fun z : ↥(P : Set ℂ) => (z : ℂ)) ∧
P.card = constructionSize d ∧ d * P.card ≤ 4 * (unitPairs P).card := by
classical
obtain ⟨Q⟩ := (coordinatePattern d).exists_prepared
obtain ⟨R⟩ := Q.exists_separated (coordinatePattern d).endpoints_injective
let P := rotatedSet R.base R.rotation
have hinj := rotatedCopy_injective R.base R.rotation R.base_ne_zero R.radii_injective
R.rotation_norm R.products_injective
have hconv := rotatedCopy_convexIndependent R.base R.rotation R.base_ne_zero R.radii_injective
(fun i => (R.base_norm_lt i).le) R.rotation_norm R.products_injective R.support_margin
have hcard := rotatedSet_card R.base R.rotation hinj
have hcount := amplification_unitPairs_bound (coordinatePattern d).line (coordinatePattern d).point
R.base R.rotation (coordinatePattern d).endpoints_injective hinj R.rotation_norm R.unit_edge
refine ⟨P, rotatedSet_convexIndependent R.base R.rotation hconv, ?_, ?_⟩
· simpa [P, vertexLabel_card (by omega : 1 ≤ d), edgeLabel_card, constructionSize,
pow_succ] using hcard
· have hm : 1 ≤ Fintype.card (EdgeLabel d) := by
rw [edgeLabel_card]
exact Nat.one_le_iff_ne_zero.mpr (pow_ne_zero _ (by omega))
have hpow : 2 ^ Fintype.card (EdgeLabel d) = 2 * 2 ^ (Fintype.card (EdgeLabel d) - 1) := by
rw [← pow_succ', Nat.sub_add_cancel hm]
have hid : d * P.card = 4 * (Fintype.card (EdgeLabel d) * 2 ^ (Fintype.card (EdgeLabel d) - 1)) := by
dsimp [P]
rw [hcard, vertexLabel_card (by omega : 1 ≤ d), hpow, edgeLabel_card, pow_succ]
ring
rw [hid]
exact Nat.mul_le_mul_left 4 hcount
theorem constructionSize_pos {d : ℕ} (hd : 1 ≤ d) : 0 < constructionSize d := by
unfold constructionSize
positivity
theorem convex_unit_ratios_unbounded (C : ℝ) :
∃ P : Finset ℂ, ConvexIndependent ℝ (fun z : ↥(P : Set ℂ) => (z : ℂ)) ∧
C * (P.card : ℝ) < ((unitPairs P).card : ℝ) := by
obtain ⟨n, hn⟩ := exists_nat_gt (4 * C)
obtain ⟨P, hconv, hcard, hcount⟩ := convex_unit_counterexample (n + 2) (by omega)
have hP : (0 : ℝ) < P.card := by exact_mod_cast (hcard ▸ constructionSize_pos (by omega : 1 ≤ n + 2))
have hcountR : ((n + 2 : ℕ) : ℝ) * P.card ≤ 4 * (unitPairs P).card := by exact_mod_cast hcount
have hdR : 4 * C < ((n + 2 : ℕ) : ℝ) := by push_cast; linarith
refine ⟨P, hconv, ?_⟩
nlinarith [mul_pos (sub_pos.mpr hdR) hP]
end
end Proof
end OriginalCounterexample
/- ## PlaneBridge -/
section OriginalPlaneBridge
/- Transfer from the complex plane to the literal Euclidean-plane definitions. -/
namespace Proof
noncomputable section
open scoped EuclideanGeometry
def complexToPlane : ℂ ≃ₗᵢ[ℝ] ℝ² := Complex.orthonormalBasisOneI.repr
theorem pairDistance_eq_out {X : Type*} [MetricSpace X] (p : Sym2 X) :
pairDistance p = dist p.out.1 p.out.2 := by
have hp : s(p.out.1, p.out.2) = p := by rw [Sym2.mk, p.out_eq]
conv_lhs => rw [← hp]
rfl
theorem unitDistNum_eq_card_unitPairs {X : Type*} [MetricSpace X] (P : Finset X) :
unitDistNum P = (unitPairs P).card := by
classical
simp only [unitDistNum, unitPairs, pairDistance_eq_out]
theorem pairDistance_map_isometry {X Y : Type*} [MetricSpace X] [MetricSpace Y]
(f : X → Y) (hf : Isometry f) (p : Sym2 X) :
pairDistance (Sym2.map f p) = pairDistance p := by
refine Sym2.inductionOn p ?_
intro a b
exact hf.dist_eq a b
theorem unitPairs_image_isometry {X Y : Type*} [MetricSpace X] [MetricSpace Y] [DecidableEq Y]
(f : X → Y) (hf : Isometry f) (P : Finset X) :
unitPairs (P.image f) = (unitPairs P).image (Sym2.map f) := by
classical
rw [unitPairs, Finset.sym2_image, Finset.filter_image]
congr 1
ext p
simp only [Finset.mem_filter, pairDistance_map_isometry f hf, unitPairs]
theorem unitPairs_card_image_isometry {X Y : Type*} [MetricSpace X] [MetricSpace Y] [DecidableEq Y]
(f : X → Y) (hf : Isometry f) (P : Finset X) :
(unitPairs (P.image f)).card = (unitPairs P).card := by
classical
rw [unitPairs_image_isometry f hf, Finset.card_image_of_injective _
(Sym2.map.injective hf.injective)]
theorem convexIndependent_linearMap {I V W : Type*}
[AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W]
(f : V →ₗ[ℝ] W) (hf : Function.Injective f) (p : I → V)
(hp : ConvexIndependent ℝ p) : ConvexIndependent ℝ (f ∘ p) := by
intro S i hi
apply hp S i
have himg : (f ∘ p) '' S = f '' (p '' S) := (Set.image_image f p S).symm
rw [himg, ← f.image_convexHull] at hi
obtain ⟨x, hx, hxi⟩ := hi
have heq : x = p i := hf hxi
simpa only [heq] using hx
theorem convexIndep_image_complexToPlane (P : Finset ℂ)
(hp : ConvexIndependent ℝ (fun z : ↥(P : Set ℂ) => (z : ℂ))) :
EuclideanGeometry.ConvexIndep (P.image complexToPlane) := by
classical
apply convexIndependent_set_iff_notMem_convexHull_sdiff.mp
have hc := convexIndependent_linearMap complexToPlane.toLinearEquiv.toLinearMap
complexToPlane.injective (fun z : ↥(P : Set ℂ) => (z : ℂ)) hp
have hrange : (P.image complexToPlane : Set ℝ²) =
Set.range (fun z : ↥(P : Set ℂ) => complexToPlane (z : ℂ)) := by
ext y
simp
rw [hrange]
exact hc.range
theorem convexUnitDistanceCounts_bddAbove (n : ℕ) :
BddAbove (convexUnitDistanceCounts n) := by
classical
refine ⟨(n + 1).choose 2, ?_⟩
rintro _ ⟨P, hP, _, rfl⟩
rw [unitDistNum_eq_card_unitPairs]
calc
(unitPairs P).card ≤ P.sym2.card := Finset.card_filter_le _ _
_ = (n + 1).choose 2 := by rw [Finset.card_sym2, hP]
theorem unitDistNum_le_max (P : Finset ℝ²) (hP : EuclideanGeometry.ConvexIndep P) :
unitDistNum P ≤ maxConvexUnitDistances P.card := by
apply le_csSup (convexUnitDistanceCounts_bddAbove P.card)
exact ⟨P, rfl, hP, rfl⟩
end
end Proof
end OriginalPlaneBridge
/- ## Problem -/
section OriginalProblem
/-
The negation of Erdős problem 96, with the Euclidean-plane, convexity,
unordered-pair-count, and supremum definitions of Formal Conjectures.
-/
namespace Proof
noncomputable section
open Filter EuclideanGeometry
open scoped EuclideanGeometry
theorem constructionSize_ge_dimension {d : ℕ} (hd : 1 ≤ d) :
d ≤ constructionSize d := by
have hpow : 1 ≤ 2 ^ (d ^ (d + 1)) := Nat.one_le_iff_ne_zero.mpr (by positivity)
calc
d ≤ d ^ d := le_self_pow hd (by omega)
_ ≤ 2 * d ^ d := by omega
_ ≤ constructionSize d := by
simpa only [constructionSize, mul_one] using Nat.mul_le_mul_left (2 * d ^ d) hpow
/-- The explicit family in the literal Euclidean plane. -/
theorem plane_counterexample (d : ℕ) (hd : 2 ≤ d) :
∃ points : Finset ℝ²,
ConvexIndep points ∧ points.card = constructionSize d ∧
d * points.card ≤ 4 * unitDistNum points := by
classical
obtain ⟨P, hconv, hcard, hcount⟩ := convex_unit_counterexample d hd
let points := P.image complexToPlane
have hcard' : points.card = P.card :=
Finset.card_image_of_injective _ complexToPlane.injective
have hunit : unitDistNum points = (unitPairs P).card := by
rw [unitDistNum_eq_card_unitPairs]
exact unitPairs_card_image_isometry complexToPlane complexToPlane.isometry P
refine ⟨points, convexIndep_image_complexToPlane P hconv, hcard'.trans hcard, ?_⟩
rw [hcard', hunit]
exact hcount
/-- Counterexamples occur past every cardinality threshold and every proposed linear bound. -/
theorem large_convex_counterexample (C : ℝ) (N₀ : ℕ) :
∃ points : Finset ℝ²,
N₀ ≤ points.card ∧ ConvexIndep points ∧
C * (points.card : ℝ) < (unitDistNum points : ℝ) := by
obtain ⟨n, hn⟩ := exists_nat_gt (4 * C)
let d := n + N₀ + 2
have hd : 2 ≤ d := by dsimp [d]; omega
obtain ⟨P, hconv, hcard, hcount⟩ := plane_counterexample d hd
have hsize : N₀ ≤ P.card := by
rw [hcard]
exact le_trans (by dsimp [d]; omega) (constructionSize_ge_dimension (by omega))
have hP : (0 : ℝ) < P.card := by
have hh : 0 < P.card := by rw [hcard]; exact constructionSize_pos (by omega)
exact_mod_cast hh
have hcountR : (d : ℝ) * P.card ≤ 4 * unitDistNum P := by exact_mod_cast hcount
have hdR : 4 * C < (d : ℝ) := by dsimp [d]; push_cast; linarith
refine ⟨P, hsize, hconv, ?_⟩
nlinarith [mul_pos (sub_pos.mpr hdR) hP]
/-- The maximum number of unit distances in a convex n-gon is not O(n). -/
theorem erdos_96_false :
¬ ((fun n => (maxConvexUnitDistances n : ℝ)) =O[atTop] fun n => (n : ℝ)) := by
intro h
obtain ⟨C, hC⟩ := h.bound
obtain ⟨N₀, hN₀⟩ := eventually_atTop.mp hC
obtain ⟨P, hlarge, hconv, hcount⟩ := large_convex_counterexample C N₀
have hupper := hN₀ P.card hlarge
have hmax : (unitDistNum P : ℝ) ≤ (maxConvexUnitDistances P.card : ℝ) := by
exact_mod_cast unitDistNum_le_max P hconv
simp only [Real.norm_natCast] at hupper
linarith
end
end Proof
end OriginalProblem
/-- The negation of the exact proposition in the supplied task. -/
theorem target : ¬ (fcTypeOfName% "Erdos96.erdos_96") := by
intro h
exact Proof.erdos_96_false (h.mp True.intro)
Provenance
- Proof SHA-256
- sha256:d445f7ec23d57a36ea4402c11eb8cc65fd6fd18ca1d6192e17f41cc359ea308c
- Solver
- JenW1N
- Attribution
- conjectures.io