Mathlib.Topology.Space­Filling­Curve

theorem exists_grayPath_between_adjacent_vertices (d : ℕ) (hd : 0 < d) (u v : Fin d → Bool) (huv : FaceAdjacentVertex u v) : ∃ path : Fin (2 ^ d) → Fin d → Bool, Bijective path ∧ (∀ k l : Fin (2 ^ d), l.val = k.val + 1 → FaceAdjacentVertex (path k) (path l)) ∧ path 0 = u ∧ path (rev 0) = v := by obtain ⟨i, hdiff, hsame⟩ := huv obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : d ≠ 0) let top : Fin (n + 1) := ⟨n, by omega⟩ let σ : Perm (Fin (n + 1)) := Equiv.swap i top let path : Fin (2 ^ (n + 1)) → Fin (n + 1) → Bool := fun k j => u j ^^ grayBit k.val (σ j).val refine ⟨path, ?_, ?_, ?_, ?_⟩ · apply (Fintype.bijective_iff_injective_and_card _).2 constructor · intro k l hkl apply (grayBits_bijective (n + 1)).1 funext j have h := congrFun hkl (σ j) simp only [path, σ, Equiv.swap_apply_self] at h exact Bool.xor_right_inj.mp h · simp · intro k l hkl obtain ⟨j, hj, hother⟩ := grayBit_adjacent (n + 1) k.val (by simpa only [← hkl] using l.isLt) refine ⟨σ.symm j, ?_, ?_⟩ · simp only [path, Equiv.apply_symm_apply, hkl] intro he exact hj (Bool.xor_right_inj.mp he) · intro a ha have hneq : σ a ≠ j := by intro h apply ha apply σ.injective exact h.trans (σ.apply_symm_apply j).symm have heq := hother (σ a) hneq simpa only [path, hkl] using congrArg (fun b => u a ^^ b) heq · funext j simp [path, grayBit, reflectedGray] · funext j have hlast : (rev (0 : Fin (2 ^ (n + 1)))).val = 2 ^ (n + 1) - 1 := by simp [rev] simp only [path] rw [hlast, grayBit_last n (σ j).val (σ j).isLt] by_cases hj : j = i · subst j simp only [σ, Equiv.swap_apply_left, top, Fin.val_mk, decide_true, Bool.xor_true] cases hu : u i <;> cases hv : v i <;> simp_all · have hσ : σ j ≠ top := by intro h apply hj apply σ.injective exact h.trans (Equiv.swap_apply_left i top).symm have hne : (σ j).val ≠ n := by intro h apply hσ exact Fin.ext h simp [hne, hsame j hj]

theorem exists_adjacent_child_gate (d : ℕ) (hd : 2 ≤ d) (u v : Fin d → ℕ) (huv : FaceAdjacentGrid u v) (a : Fin d → Bool) : ∃ b c : Fin d → Bool, FaceAdjacentVertex a b ∧ FaceAdjacentGrid (childGridCoord u b) (childGridCoord v c) := by classical obtain ⟨i, hi, hsame⟩ := huv have : Nontrivial (Fin d) := Fin.nontrivial_iff_two_le.mpr hd obtain ⟨j, hji⟩ := exists_ne i have hij : i ≠ j := Ne.symm hji rcases hi with hforward | hbackward · by_cases hai : a i = true · let b : Fin d → Bool := fun k => if k = j then !a k else a k let c : Fin d → Bool := fun k => if k = i then false else b k refine ⟨b, c, ?_, ?_⟩ · unfold FaceAdjacentVertex refine ⟨j, ?_, ?_⟩ · simp [b] · intro k hk simp [b, hk] · unfold FaceAdjacentGrid refine ⟨i, ?_, ?_⟩ · simp [childGridCoord, b, c, hij, hai] omega · intro k hk simp [childGridCoord, b, c, hk, hsame k hk] · let b : Fin d → Bool := fun k => if k = i then true else a k let c : Fin d → Bool := fun k => if k = i then false else b k refine ⟨b, c, ?_, ?_⟩ · unfold FaceAdjacentVertex refine ⟨i, ?_, ?_⟩ · simp [b, hai] · intro k hk simp [b, hk] · unfold FaceAdjacentGrid refine ⟨i, ?_, ?_⟩ · simp [childGridCoord, b, c] omega · intro k hk simp [childGridCoord, b, c, hk, hsame k hk] · by_cases hai : a i = false · let b : Fin d → Bool := fun k => if k = j then !a k else a k let c : Fin d → Bool := fun k => if k = i then true else b k refine ⟨b, c, ?_, ?_⟩ · unfold FaceAdjacentVertex refine ⟨j, ?_, ?_⟩ · simp [b] · intro k hk simp [b, hk] · unfold FaceAdjacentGrid refine ⟨i, ?_, ?_⟩ · simp [childGridCoord, b, c, hij, hai] omega · intro k hk simp [childGridCoord, b, c, hk, hsame k hk] · let b : Fin d → Bool := fun k => if k = i then false else a k let c : Fin d → Bool := fun k => if k = i then true else b k refine ⟨b, c, ?_, ?_⟩ · unfold FaceAdjacentVertex refine ⟨i, ?_, ?_⟩ · simp [b, hai] · intro k hk simp [b, hk] · unfold FaceAdjacentGrid refine ⟨i, ?_, ?_⟩ · simp [childGridCoord, b, c] omega · intro k hk simp [childGridCoord, b, c, hk, hsame k hk]

theorem exists_finiteDyadicTraversal (d n : ℕ) (hd : 0 < d) : Nonempty (FiniteDyadicTraversal d n) := by by_cases h1 : d = 1 · subst d exact exists_finiteDyadicTraversal_one n · have hd2 : 2 ≤ d := by omega induction n with | zero => exact exists_finiteDyadicTraversal_zero d | succ n ih => obtain ⟨T⟩ := ih exact exists_finiteDyadicTraversal_succ d n hd2 T

theorem exists_localizedCubeMap_of_traversal (d : ℕ) (T : DyadicTraversal d) : Nonempty (LocalizedCubeMap d T) := by let H : ℝ → Fin d → ℝ := fun t => if ht : t ∈ Icc (0 : ℝ) 1 then choose (dyadicCellFiber_nonempty T t ht) else fun _ => 0 refine ⟨{ toFun := H, localizes := ?_ }⟩ intro n k t ht have hpos : (0 : ℝ) < (2 ^ (d * n) : ℝ) := by positivity have hkle : ((k.val : ℝ) + 1) ≤ (2 ^ (d * n) : ℝ) := by exact_mod_cast (succ_le_of_lt k.isLt) have htu : t ∈ Icc (0 : ℝ) 1 := by change (k.val : ℝ) / (2 ^ (d * n) : ℝ) ≤ t ∧ t ≤ ((k.val : ℝ) + 1) / (2 ^ (d * n) : ℝ) at ht constructor · exact (by positivity : 0 ≤ (k.val : ℝ) / (2 ^ (d * n) : ℝ)).trans ht.1 · exact ht.2.trans ((div_le_iff₀ hpos).2 (by simpa using hkle)) have hf := Classical.choose_spec (dyadicCellFiber_nonempty T t htu) change dyadicCubeCell T n k (H t) dsimp [H] rw [dif_pos htu] exact hf n k ht

theorem grayBit_adjacent (d k : ℕ) (hk : k + 1 < 2 ^ d) : ∃ i : Fin d, grayBit k i.val ≠ grayBit (k + 1) i.val ∧ ∀ j : Fin d, j ≠ i → grayBit k j.val = grayBit (k + 1) j.val := by have hall : ∀ k : ℕ, ∃ i : ℕ, grayBit k i ≠ grayBit (k + 1) i ∧ ∀ j : ℕ, j ≠ i → grayBit k j = grayBit (k + 1) j := by intro m induction m using Nat.strong_induction_on with | h m ih => rcases Nat.mod_two_eq_zero_or_one m with h | h · have hm : m = 2 * (m / 2) := by omega refine ⟨0, ?_, ?_⟩ · simpa only [← hm] using grayBit_even_odd_zero (m / 2) · intro j hj obtain ⟨a, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj simpa only [← hm, Nat.succ_eq_add_one] using grayBit_even_odd_succ (m / 2) a · have hm : m = 2 * (m / 2) + 1 := by omega let n := m / 2 have hn : n < m := by dsimp [n]; omega obtain ⟨i, hi, hother⟩ := ih n hn refine ⟨i + 1, ?_, ?_⟩ · rw [hm, show 2 * n + 1 + 1 = 2 * (n + 1) by omega, grayBit_odd_succ, grayBit_even_succ] exact hi · intro j hj cases j with | zero => rw [hm, show 2 * (m / 2) + 1 + 1 = 2 * (n + 1) by dsimp [n] omega] exact grayBit_odd_even_zero n | succ a => have ha : a ≠ i := by omega rw [hm, show 2 * n + 1 + 1 = 2 * (n + 1) by omega, grayBit_odd_succ, grayBit_even_succ] exact hother a ha obtain ⟨i, hi, hother⟩ := hall k have hbound : i < d := by by_contra h have hki : grayBit k i = false := by change (Nat.xor k (k / 2)).testBit i = false apply Nat.testBit_lt_two_pow rw [Nat.xor_eq] exact lt_of_lt_of_le (Nat.xor_lt_two_pow (lt_of_succ_lt hk) (Nat.lt_of_le_of_lt (Nat.div_le_self k 2) (lt_of_succ_lt hk))) (Nat.pow_le_pow_right (by omega : 0 < 2) (Nat.le_of_not_gt h)) have hsi : grayBit (k + 1) i = false := by change (Nat.xor (k + 1) ((k + 1) / 2)).testBit i = false apply Nat.testBit_lt_two_pow rw [Nat.xor_eq] exact lt_of_lt_of_le (Nat.xor_lt_two_pow hk (Nat.lt_of_le_of_lt (Nat.div_le_self (k + 1) 2) hk)) (Nat.pow_le_pow_right (by omega : 0 < 2) (Nat.le_of_not_gt h)) exact hi (hki.trans hsi.symm) refine ⟨⟨i, hbound⟩, hi, ?_⟩ intro j hj exact hother j.val (by intro heq; apply hj; exact Fin.ext heq)

theorem exists_pairing_gap_le_one (N : ℕ) (hN : Even N) (hN2 : 2 ≤ N) (t : Fin N → ℝ) (ht : ∀ i, t i ∈ Icc (0 : ℝ) 1) : ∃ M : PerfectPairing N, (∑ j : Fin (N / 2), |t (M.edge j).1 - t (M.edge j).2|) ≤ 1 := by have htwo : N / 2 * 2 = N := by have hd : 2 ∣ N := hN.two_dvd omega let e : Fin (N / 2) × Fin 2 ≃ Fin N := finProdFinEquiv.trans (finCongr htwo) let σ := Tuple.sort t let u : Fin N → ℝ := t ∘ σ have hu : Monotone u := Tuple.monotone_sort t let M : PerfectPairing N := { edge := fun j => (σ (e (j, 0)), σ (e (j, 1))) distinct := by intro j h have he := σ.injective h have he' := e.injective he exact (Fin.zero_ne_one : (0 : Fin 2) ≠ 1) (congrArg snd he') covers := by intro i obtain ⟨⟨j, k⟩, hjk⟩ := e.surjective (σ.symm i) refine ⟨j, ?_, ?_⟩ · fin_cases k · left; exact (σ.apply_symm_apply i).symm.trans (congrArg σ hjk.symm) · right; exact (σ.apply_symm_apply i).symm.trans (congrArg σ hjk.symm) · intro j' hj' rcases hj' with hj' | hj' · have h : e (j, k) = e (j', 0) := by calc _ = σ.symm i := hjk _ = σ.symm (σ (e (j', 0))) := congrArg σ.symm hj' _ = _ := σ.symm_apply_apply _ exact (congrArg fst (e.injective h)).symm · have h : e (j, k) = e (j', 1) := by calc _ = σ.symm i := hjk _ = σ.symm (σ (e (j', 1))) := congrArg σ.symm hj' _ = _ := σ.symm_apply_apply _ exact (congrArg fst (e.injective h)).symm } refine ⟨M, ?_⟩ have heval (j : Fin (N / 2)) (k : Fin 2) : (e (j, k)).val = 2 * j.val + k.val := by simp [e, finCongr_apply, finProdFinEquiv_apply_val] omega let v : ℕ → ℝ := fun i => if hi : i < N then u ⟨i, hi⟩ else 1 have hv (i : Fin N) : v i.val = u i := by simp [v] have hgap (j : Fin (N / 2)) : |t (M.edge j).1 - t (M.edge j).2| = v (2 * j.val + 1) - v (2 * j.val) := by have hle : e (j, 0) ≤ e (j, 1) := by apply Fin.le_iff_val_le_val.mpr simp [heval] have hmono := hu hle change u (e (j, 0)) ≤ u (e (j, 1)) at hmono have hval0 : (e (j, 0)).val = 2 * j.val := by simpa using heval j 0 have hval1 : (e (j, 1)).val = 2 * j.val + 1 := by simpa using heval j 1 change |u (e (j, 0)) - u (e (j, 1))| = _ rw [abs_sub_comm, abs_of_nonneg (sub_nonneg.mpr hmono)] rw [← hv, ← hv, hval0, hval1] let g : ℕ → ℝ := fun i => v (i + 1) - v i let s : Finset ℕ := Finset.univ.image (fun j : Fin (N / 2) => 2 * j.val) have hinj : Injective (fun j : Fin (N / 2) => 2 * j.val) := by intro j k h apply Fin.ext change 2 * j.val = 2 * k.val at h omega have hsubset : s ⊆ range (N - 1) := by intro i hi obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi simp only [Finset.mem_range] have := j.isLt omega have hgnonneg (i : ℕ) (hi : i ∈ range (N - 1)) : 0 ≤ g i := by have hi' : i < N - 1 := Finset.mem_range.mp hi have hi0 : i < N := by omega have hi1 : i + 1 < N := by omega change 0 ≤ v (i + 1) - v i simp only [v, dif_pos hi0, dif_pos hi1] have hidx : (⟨i, hi0⟩ : Fin N) ≤ ⟨i + 1, hi1⟩ := by apply Fin.le_iff_val_le_val.mpr change i ≤ i + 1 omega exact sub_nonneg.mpr (hu hidx) have hsumgap : (∑ j : Fin (N / 2), |t (M.edge j).1 - t (M.edge j).2|) = ∑ i ∈ s, g i := by rw [Finset.sum_image (by intro j _ k _ h; exact hinj h)] apply Finset.sum_congr rfl intro j hj simpa [g] using hgap j have hsumle : (∑ i ∈ s, g i) ≤ ∑ i ∈ range (N - 1), g i := Finset.sum_le_sum_of_subset_of_nonneg hsubset (by intro i hi _ exact hgnonneg i hi) have htel : (∑ i ∈ range (N - 1), g i) = v (N - 1) - v 0 := Finset.sum_range_sub v (N - 1) have hlast : v (N - 1) ≤ 1 := by have hi : N - 1 < N := by omega simpa [v, hi, u] using (ht (σ ⟨N - 1, hi⟩)).2 have hfirst : 0 ≤ v 0 := by have hi : 0 < N := by omega simpa [v, hi, u] using (ht (σ ⟨0, hi⟩)).1 rw [hsumgap] linarith [hsumle, htel]

theorem exists_compatible_child_paths (d n : ℕ) (hd : 2 ≤ d) (parent : Fin (2 ^ (d * n)) → Fin d → ℕ) (hadj : ∀ k l : Fin (2 ^ (d * n)), l.val = k.val + 1 → FaceAdjacentGrid (parent k) (parent l)) : ∃ path : Fin (2 ^ (d * n)) → Fin (2 ^ d) → Fin d → Bool, (∀ k, Bijective (path k)) ∧ (∀ k : Fin (2 ^ (d * n)), ∀ a b : Fin (2 ^ d), b.val = a.val + 1 → FaceAdjacentVertex (path k a) (path k b)) ∧ (∀ k l : Fin (2 ^ (d * n)), l.val = k.val + 1 → FaceAdjacentGrid (childGridCoord (parent k) (path k (rev 0))) (childGridCoord (parent l) (path l 0))) := by classical obtain ⟨entry, exit, _, hgate, hbridge⟩ := exists_compatible_child_gates d n hd parent hadj (fun _ => false) have hpaths : ∀ k : Fin (2 ^ (d * n)), ∃ p : Fin (2 ^ d) → Fin d → Bool, Bijective p ∧ (∀ a b : Fin (2 ^ d), b.val = a.val + 1 → FaceAdjacentVertex (p a) (p b)) ∧ p 0 = entry k ∧ p (rev 0) = exit k := by intro k exact exists_grayPath_between_adjacent_vertices d (by omega) (entry k) (exit k) (hgate k) choose path hpath using hpaths refine ⟨path, (fun k => (hpath k).1), (fun k a b hab => (hpath k).2.1 a b hab), ?_⟩ intro k l hkl rw [(hpath k).2.2.2, (hpath l).2.2.1] exact hbridge k l hkl

theorem DyadicTraversal.cubeCell_cover {d : ℕ} (T : DyadicTraversal d) (n : ℕ) (x : Fin d → ℝ) (hx : InUnitCube x) : ∃ k : Fin (2 ^ (d * n)), dyadicCubeCell T n k x := by -- For each coordinate, clip `⌊2^n * x i⌋₊` to `2^n - 1`. -- The resulting grid tuple contains x, including coordinates equal to 1. -- Use `(T.bijective n).2` to obtain its traversal index. let q : ℕ := 2 ^ n have hq : 0 < q := by dsimp [q]; positivity have hqR : (0 : ℝ) < q := by exact_mod_cast hq let a : Fin d → Fin q := fun i => ⟨min ⌊(q : ℝ) * x i⌋₊ (q - 1), lt_of_le_of_lt (Nat.min_le_right _ _) (sub_lt hq (by omega))⟩ have ha (i : Fin d) : (a i).val / (q : ℝ) ≤ x i ∧ x i ≤ ((a i).val + 1) / (q : ℝ) := by have hxi := hx i have hx0 : (0 : ℝ) ≤ x i := hxi.1 have hx1 : x i ≤ 1 := hxi.2 have hprod0 : (0 : ℝ) ≤ (q : ℝ) * x i := mul_nonneg hqR.le hx0 have hprodle : (q : ℝ) * x i ≤ q := by nlinarith have hfloorle : ⌊(q : ℝ) * x i⌋₊ ≤ q := Nat.floor_le_of_le hprodle by_cases hf : ⌊(q : ℝ) * x i⌋₊ < q · have hamin : (a i).val = ⌊(q : ℝ) * x i⌋₊ := by simp [a, Nat.min_eq_left (by omega : ⌊(q : ℝ) * x i⌋₊ ≤ q - 1)] have hlower := Nat.floor_le hprod0 have hupper := Nat.lt_floor_add_one ((q : ℝ) * x i) rw [hamin] constructor · apply (div_le_iff₀ hqR).2 nlinarith · apply (le_div_iff₀ hqR).2 nlinarith · have heq : ⌊(q : ℝ) * x i⌋₊ = q := by omega have hlower := Nat.floor_le hprod0 have hx_eq : x i = 1 := by rw [heq] at hlower; nlinarith have hamin : (a i).val = q - 1 := by simp [a, heq] rw [hamin, hx_eq] constructor · apply (div_le_iff₀ hqR).2 have : q - 1 < q := sub_lt hq (by omega) simpa only [one_mul] using (show ((q - 1 : ℕ) : ℝ) ≤ (q : ℝ) by exact_mod_cast (le_of_lt this)) · have hsub : q - 1 + 1 = q := Nat.sub_add_cancel (by omega) rw [show ((q - 1 : ℕ) : ℝ) + 1 = (q : ℝ) by exact_mod_cast hsub] exact le_of_eq (div_self hqR.ne').symm have ha' : ∀ i, x i ∈ Icc (((a i).val : ℝ) / (2 ^ n : ℝ)) ((((a i).val : ℝ) + 1) / (2 ^ n : ℝ)) := by intro i simpa [q] using ha i obtain ⟨k, hk⟩ := (T.bijective n).2 a refine ⟨k, ?_⟩ intro i simpa [dyadicCubeCell, hk] using ha' i

theorem DyadicTraversal.exists_parameter_for_cubePoint {d : ℕ} (T : DyadicTraversal d) (x : Fin d → ℝ) (hx : InUnitCube x) : ∃ t : ℝ, t ∈ Icc (0 : ℝ) 1 ∧ ∀ n : ℕ, ∃ k : Fin (2 ^ (d * n)), t ∈ dyadicTimeCell d n k ∧ dyadicCubeCell T n k x := by classical let F : ℕ → Set ℝ := fun n => ⋃ k : Fin (2 ^ (d * n)), if dyadicCubeCell T n k x then dyadicTimeCell d n k else ∅ have hclosed (n : ℕ) : IsClosed (F n) := by dsimp [F] apply isClosed_iUnion_of_finite intro k split · exact isClosed_Icc · exact isClosed_empty have hnonempty (n : ℕ) : (F n).Nonempty := by obtain ⟨k, hk⟩ := T.cubeCell_cover n x hx refine ⟨(k.val : ℝ) / (2 ^ (d * n) : ℝ), ?_⟩ change _ ∈ ⋃ k : Fin (2 ^ (d * n)), if dyadicCubeCell T n k x then dyadicTimeCell d n k else ∅ apply Set.mem_iUnion.mpr refine ⟨k, ?_⟩ simp only [if_pos hk, dyadicTimeCell, Set.mem_Icc] constructor · exact le_rfl · apply div_le_div_of_nonneg_right (by norm_num) (by positivity) have hstep (n : ℕ) : F (n + 1) ⊆ F n := by intro t ht obtain ⟨l, hl⟩ := Set.mem_iUnion.mp ht have hxl : dyadicCubeCell T (n + 1) l x := by by_contra h simp [h] at hl have htl : t ∈ dyadicTimeCell d (n + 1) l := by simpa [hxl] using hl have hpow : 2 ^ (d * (n + 1)) = 2 ^ (d * n) * 2 ^ d := by simp [mul_add, pow_add] let k : Fin (2 ^ (d * n)) := ⟨l.val / 2 ^ d, (Nat.div_lt_iff_lt_mul (by positivity : 0 < 2 ^ d)).2 (by rw [← hpow]; exact l.isLt)⟩ have hparent : l.val / 2 ^ d = k.val := rfl have hxk := dyadicCubeCell_parent' T k l hparent x hxl change t ∈ ⋃ k : Fin (2 ^ (d * n)), if dyadicCubeCell T n k x then dyadicTimeCell d n k else ∅ apply Set.mem_iUnion.mpr refine ⟨k, ?_⟩ simpa [hxk] using dyadicTimeCell_parent k l hparent htl have hsubset : F 0 ⊆ Icc (0 : ℝ) 1 := by intro t ht obtain ⟨k, hk⟩ := Set.mem_iUnion.mp ht have htk : t ∈ dyadicTimeCell d 0 k := by by_cases h : dyadicCubeCell T 0 k x · simpa [F, h] using hk · simp [h] at hk have hk0 : k.val = 0 := by have hklt := k.isLt simp only [mul_zero, pow_zero] at hklt omega simpa [dyadicTimeCell, hk0] using htk have hcompact : IsCompact (F 0) := isCompact_Icc.of_isClosed_subset (hclosed 0) hsubset obtain ⟨t, ht⟩ := IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed F hstep hnonempty hcompact hclosed refine ⟨t, hsubset ((Set.mem_iInter.mp ht) 0), ?_⟩ intro n obtain ⟨k, hk⟩ := Set.mem_iUnion.mp ((Set.mem_iInter.mp ht) n) by_cases hxk : dyadicCubeCell T n k x · exact ⟨k, by simpa [F, hxk] using hk, hxk⟩ · simp [hxk] at hk

theorem sqEuclideanDist_le_of_neighboring_cubeCells {d n : ℕ} (T : DyadicTraversal d) (k l : Fin (2 ^ (d * n))) (hkl : k.val ≤ l.val + 1 ∧ l.val ≤ k.val + 1) (x y : Fin d → ℝ) (hx : dyadicCubeCell T n k x) (hy : dyadicCubeCell T n l y) : sqEuclideanDist x y ≤ 4 * (d : ℝ) * ((1 : ℝ) / (2 : ℝ) ^ n) ^ 2 := by -- Split into equal cells or either orientation of consecutive indices. -- In every coordinate the two cell points differ by at most two widths. -- For consecutive indices, `T.adjacent` says that one grid coordinate -- changes by one and all the rest agree. From `hx i` and `hy i`, multiply -- interval endpoints by the positive denominator `2^n` to get -- `|x i - y i| ≤ 2 / 2^n`; the equal-index case has the same bound. -- Bound each squared summand, then sum over `Fin d` and simplify its card. have hgrid (i : Fin d) : (T.cell n k i).val ≤ (T.cell n l i).val + 1 ∧ (T.cell n l i).val ≤ (T.cell n k i).val + 1 := by by_cases heq : k = l · subst l exact ⟨by omega, by omega⟩ · have hcases : l.val = k.val + 1 ∨ k.val = l.val + 1 := by have hne : k.val ≠ l.val := fun h => heq (Fin.ext h) omega rcases hcases with hnext | hprev · obtain ⟨j, hj, hs⟩ := T.adjacent n k l hnext by_cases hij : i = j · subst i rcases hj with h | h <;> omega · rw [hs i hij] exact ⟨by omega, by omega⟩ · obtain ⟨j, hj, hs⟩ := T.adjacent n l k hprev by_cases hij : i = j · subst i rcases hj with h | h <;> omega · rw [hs i hij] exact ⟨by omega, by omega⟩ have hq : (0 : ℝ) < (2 : ℝ) ^ n := by positivity have hcoord (i : Fin d) : -(2 / (2 : ℝ) ^ n) ≤ x i - y i ∧ x i - y i ≤ 2 / (2 : ℝ) ^ n := by obtain ⟨hxl, hxu⟩ := hx i obtain ⟨hyl, hyu⟩ := hy i obtain ⟨hkl', hlk'⟩ := hgrid i have hkl'' : ((T.cell n k i).val : ℝ) ≤ (T.cell n l i).val + 1 := by exact_mod_cast hkl' have hlk'' : ((T.cell n l i).val : ℝ) ≤ (T.cell n k i).val + 1 := by exact_mod_cast hlk' have hxl' := (div_le_iff₀ hq).mp hxl have hxu' := (le_div_iff₀ hq).mp hxu have hyl' := (div_le_iff₀ hq).mp hyl have hyu' := (le_div_iff₀ hq).mp hyu have hleft : y i - x i ≤ 2 / (2 : ℝ) ^ n := (le_div_iff₀ hq).2 (by nlinarith) have hright : x i - y i ≤ 2 / (2 : ℝ) ^ n := (le_div_iff₀ hq).2 (by nlinarith) constructor <;> linarith calc sqEuclideanDist x y = ∑ i : Fin d, (x i - y i) ^ 2 := rfl _ ≤ ∑ _i : Fin d, (2 / (2 : ℝ) ^ n) ^ 2 := by apply Finset.sum_le_sum intro i _ exact sq_le_sq' (hcoord i).1 (hcoord i).2 _ = 4 * (d : ℝ) * ((1 : ℝ) / (2 : ℝ) ^ n) ^ 2 := by simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] ring

theorem LocalizedCubeMap.modulus {d : ℕ} {T : DyadicTraversal d} (H : LocalizedCubeMap d T) (hd : 2 ≤ d) {s t : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) (ht : t ∈ Icc (0 : ℝ) 1) : sqEuclideanDist (H.toFun s) (H.toFun t) ≤ 16 * (d : ℝ) * |s - t| ^ ((2 : ℝ) / d) := by -- Separate `s = t`. Otherwise use `exists_dyadicScale` on `|s-t|`, -- `exists_neighboring_timeCells` at that scale, then localize both values. -- Combine `sqEuclideanDist_le_of_neighboring_cubeCells` with -- `dyadicScale_sq_bound` and multiply by `4*d`. -- For a zero gap, rewrite the distance as a sum of zero squares. For a -- positive gap, the scale upper bound supplies `hgap` for time proximity; -- both resulting memberships feed `H.localizes` at the same level. -- `hs` and `ht` give `|s-t| ≤ 1`. At a positive gap, take the scale -- `n` and neighboring indices `k,l`; the cube estimate is `4*d*w_n²`, -- while the lower scale inequality gives `w_n² ≤ 4*gap^(2/d)`. by_cases heq : s = t · subst t simp [sqEuclideanDist] <;> positivity · have hδ : 0 < |s - t| := abs_pos.mpr (sub_ne_zero.mpr heq) have hδ1 : |s - t| ≤ 1 := by apply abs_le.mpr constructor <;> have := hs.1 <;> have := hs.2 <;> have := ht.1 <;> have := ht.2 <;> linarith obtain ⟨n, hnlow, hnup⟩ := exists_dyadicScale d (by omega) hδ hδ1 obtain ⟨k, l, hsk, htl, hkl, hlk⟩ := exists_neighboring_timeCells d n hs ht hnup have hcube := sqEuclideanDist_le_of_neighboring_cubeCells T k l ⟨hkl, hlk⟩ (H.toFun s) (H.toFun t) (H.localizes n k s hsk) (H.localizes n l t htl) have hscale := dyadicScale_sq_bound d n (by omega) hnlow have hdR : (0 : ℝ) ≤ d := by exact_mod_cast (zero_le d) nlinarith [mul_le_mul_of_nonneg_left hscale (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4) hdR)]

theorem dyadicScale_sq_bound (d n : ℕ) (hd : 0 < d) {δ : ℝ} (hδ : (1 : ℝ) / (2 : ℝ) ^ (d * (n + 1)) ≤ δ) : ((1 : ℝ) / (2 : ℝ) ^ n) ^ 2 ≤ 4 * δ ^ ((2 : ℝ) / d) := by have ha : 0 ≤ ((1 : ℝ) / 2 ^ (n + 1)) := by positivity have hw : (1 : ℝ) / 2 ^ (d * (n + 1)) = ((1 : ℝ) / 2 ^ (n + 1)) ^ d := by simp [one_div, inv_pow, ← pow_mul, mul_comm d (n + 1)] have hp : 0 ≤ (2 : ℝ) / d := by positivity have hr := Real.rpow_le_rpow (by positivity : 0 ≤ (1 : ℝ) / 2 ^ (d * (n + 1))) hδ hp rw [hw] at hr have hpow : (((1 : ℝ) / 2 ^ (n + 1)) ^ d) ^ ((2 : ℝ) / d) = ((1 : ℝ) / 2 ^ (n + 1)) ^ 2 := by rw [show (2 : ℝ) / d = (d : ℝ)⁻¹ * 2 by ring, Real.rpow_mul (pow_nonneg ha d), Real.pow_rpow_inv_natCast ha (Nat.ne_of_gt hd)] exact Real.rpow_natCast _ 2 rw [hpow] at hr have halg : ((1 : ℝ) / 2 ^ n) ^ 2 = 4 * ((1 : ℝ) / 2 ^ (n + 1)) ^ 2 := by rw [pow_succ] have h2n : (2 : ℝ) ^ n ≠ 0 := by positivity field_simp ring rw [halg] exact mul_le_mul_of_nonneg_left hr (by norm_num)

theorem exists_compatible_child_gates (d n : ℕ) (hd : 2 ≤ d) (parent : Fin (2 ^ (d * n)) → Fin d → ℕ) (hadj : ∀ k l : Fin (2 ^ (d * n)), l.val = k.val + 1 → FaceAdjacentGrid (parent k) (parent l)) (first : Fin d → Bool) : ∃ entry exit : Fin (2 ^ (d * n)) → Fin d → Bool, entry 0 = first ∧ (∀ k, FaceAdjacentVertex (entry k) (exit k)) ∧ (∀ k l : Fin (2 ^ (d * n)), l.val = k.val + 1 → FaceAdjacentGrid (childGridCoord (parent k) (exit k)) (childGridCoord (parent l) (entry l))) := by classical let m := 2 ^ (d * n) let step (k : ℕ) (a : Fin d → Bool) : {bc : (Fin d → Bool) × (Fin d → Bool) // FaceAdjacentVertex a bc.1 ∧ (∀ h : k + 1 < m, FaceAdjacentGrid (childGridCoord (parent (Fin.ofNat m k)) bc.1) (childGridCoord (parent (Fin.ofNat m (k + 1))) bc.2))} := by by_cases h : k + 1 < m · have hk : k < m := by omega have hvals : (Fin.ofNat m (k + 1)).val = (Fin.ofNat m k).val + 1 := by simp [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt hk] have hex : ∃ bc : (Fin d → Bool) × (Fin d → Bool), FaceAdjacentVertex a bc.1 ∧ FaceAdjacentGrid (childGridCoord (parent (Fin.ofNat m k)) bc.1) (childGridCoord (parent (Fin.ofNat m (k + 1))) bc.2) := by obtain ⟨b, c, hab, hbc⟩ := exists_adjacent_child_gate d hd (parent (Fin.ofNat m k)) (parent (Fin.ofNat m (k + 1))) (hadj _ _ hvals) a exact ⟨(b, c), hab, hbc⟩ let bc := choose hex exact ⟨bc, (Classical.choose_spec hex).1, fun _ => (Classical.choose_spec hex).2⟩ · let i : Fin d := ⟨0, by omega⟩ let b : Fin d → Bool := fun j => if j = i then !a j else a j refine ⟨(b, a), ?_, ?_⟩ · unfold FaceAdjacentVertex refine ⟨i, ?_, ?_⟩ · simp [b] · intro j hj simp [b, hj] · intro h' omega let entryNat : ℕ → Fin d → Bool := Nat.rec first (fun k a => (step k a).1.2) let entry : Fin m → Fin d → Bool := fun k => entryNat k.val let exit : Fin m → Fin d → Bool := fun k => (step k.val (entryNat k.val)).1.1 refine ⟨entry, exit, ?_, ?_, ?_⟩ · simp [entry, entryNat] · intro k exact (step k.val (entryNat k.val)).2.1 · intro k l hkl have hk : k.val + 1 < m := by omega have hnext : entryNat l.val = (step k.val (entryNat k.val)).1.2 := by rw [hkl] have hkfin : Fin.ofNat m k.val = k := by apply Fin.ext simp have hlfin : Fin.ofNat m (k.val + 1) = l := by apply Fin.ext simp [Nat.mod_eq_of_lt hk, hkl] simpa only [entry, exit, hkfin, hlfin, hnext] using (step k.val (entryNat k.val)).2.2 hk

theorem grayBits_bijective (d : ℕ) : Bijective (fun k : Fin (2 ^ d) => fun i : Fin d => grayBit k.val i.val) := by apply (Fintype.bijective_iff_injective_and_card _).2 constructor · intro x y hxy have hbit (n i : ℕ) : grayBit n i = (n.testBit i ^^ n.testBit (i + 1)) := by simp only [grayBit, reflectedGray, Nat.xor_eq, Nat.testBit_xor, Nat.testBit_div_two] have hdown : ∀ j : ℕ, j ≤ d → x.val.testBit (d - j) = y.val.testBit (d - j) := by intro j induction j with | zero => intro _ have hx : x.val.testBit d = false := Nat.testBit_lt_two_pow x.isLt have hy : y.val.testBit d = false := Nat.testBit_lt_two_pow y.isLt simp [hx, hy] | succ j ih => intro hj have hj' : j ≤ d := by omega let i := d - (j + 1) have hi : i < d := by dsimp [i]; omega have his : i + 1 = d - j := by dsimp [i]; omega have hg := congrFun hxy ⟨i, hi⟩ change grayBit x.val i = grayBit y.val i at hg rw [hbit, hbit, his, ih hj'] at hg exact Bool.xor_left_inj.mp hg apply Fin.ext apply Nat.eq_of_testBit_eq intro i by_cases hi : i < d · simpa only [Nat.sub_sub_self (le_of_lt hi)] using hdown (d - i) (sub_le d i) · have hx : x.val.testBit i = false := Nat.testBit_lt_two_pow (lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (by omega : 0 < 2) (by omega : d ≤ i))) have hy : y.val.testBit i = false := Nat.testBit_lt_two_pow (lt_of_lt_of_le y.isLt (Nat.pow_le_pow_right (by omega : 0 < 2) (by omega : d ≤ i))) simp [hx, hy] · simp

theorem exists_child_grid_order (d n : ℕ) (hd : 2 ≤ d) (parent : Fin (2 ^ (d * n)) → Fin d → Fin (2 ^ n)) (hbij : Bijective parent) (hadj : ∀ k l : Fin (2 ^ (d * n)), l.val = k.val + 1 → FaceAdjacentGrid (fun i => (parent k i).val) (fun i => (parent l i).val)) : ∃ child : Fin (2 ^ (d * (n + 1))) → Fin d → Fin (2 ^ (n + 1)), Bijective child ∧ (∀ k l : Fin (2 ^ (d * (n + 1))), l.val = k.val + 1 → FaceAdjacentGrid (fun i => (child k i).val) (fun i => (child l i).val)) ∧ (∀ (k : Fin (2 ^ (d * n))) (l : Fin (2 ^ (d * (n + 1)))), l.val / 2 ^ d = k.val → ∀ i : Fin d, (child l i).val / 2 = (parent k i).val) := by classical let P := 2 ^ (d * n) let B := 2 ^ d let T := 2 ^ (d * (n + 1)) have hT : T = P * B := by dsimp [T, P, B] rw [mul_add, mul_one, pow_add] have hB : 0 < B := by dsimp [B]; positivity let e : Fin P × Fin B ≃ Fin T := finProdFinEquiv.trans (finCongr hT.symm) have he (k : Fin P) (a : Fin B) : (e (k, a)).val = B * k.val + a.val := by simp [e, finCongr_apply, finProdFinEquiv_apply_val] omega have hdiv (l : Fin T) : (e.symm l).1.val = l.val / B := by have h := he (e.symm l).1 (e.symm l).2 rw [e.apply_symm_apply] at h have ha := (e.symm l).2.isLt rw [h, Nat.add_comm, Nat.add_mul_div_left _ _ hB, Nat.div_eq_of_lt ha] omega have hmod (l : Fin T) : (e.symm l).2.val = l.val % B := by have h := he (e.symm l).1 (e.symm l).2 rw [e.apply_symm_apply] at h have ha := (e.symm l).2.isLt rw [h, Nat.add_comm, Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt ha] obtain ⟨path, hpbij, hpadj, hpbridge⟩ := exists_compatible_child_paths d n hd (fun k i => (parent k i).val) hadj have hcoord (k : Fin P) (a : Fin B) (i : Fin d) : childGridCoord (fun i => (parent k i).val) (path k a) i < 2 ^ (n + 1) := by have hk := (parent k i).isLt dsimp [childGridCoord] rw [pow_succ] split <;> omega let child : Fin T → Fin d → Fin (2 ^ (n + 1)) := fun l i => ⟨childGridCoord (fun i => (parent (e.symm l).1 i).val) (path (e.symm l).1 (e.symm l).2) i, hcoord (e.symm l).1 (e.symm l).2 i⟩ have hchild (k : Fin P) (a : Fin B) (i : Fin d) : (child (e (k, a)) i).val = 2 * (parent k i).val + if path k a i then 1 else 0 := by simp [child, childGridCoord] have hnest (l : Fin T) (i : Fin d) : (child l i).val / 2 = (parent (e.symm l).1 i).val := by change (2 * (parent (e.symm l).1 i).val + if path (e.symm l).1 (e.symm l).2 i then 1 else 0) / 2 = _ split <;> omega have hcbij : Bijective child := by constructor · intro l m hlm have hk : (e.symm l).1 = (e.symm m).1 := by apply hbij.1 funext i apply Fin.ext calc (parent (e.symm l).1 i).val = (child l i).val / 2 := (hnest l i).symm _ = (child m i).val / 2 := by rw [hlm] _ = (parent (e.symm m).1 i).val := hnest m i have ha : (e.symm l).2 = (e.symm m).2 := by apply (hpbij (e.symm m).1).1 funext i have hi := congrFun hlm i have hv := congrArg val hi change 2 * (parent (e.symm l).1 i).val + (if path (e.symm l).1 (e.symm l).2 i then 1 else 0) = 2 * (parent (e.symm m).1 i).val + (if path (e.symm m).1 (e.symm m).2 i then 1 else 0) at hv rw [hk] at hv by_cases hb : path (e.symm m).1 (e.symm l).2 i <;> by_cases hc : path (e.symm m).1 (e.symm m).2 i <;> simp [hb, hc] at hv ⊢ apply e.symm.injective exact Prod.ext hk ha · intro y have hybound (i : Fin d) : (y i).val / 2 < 2 ^ n := by have hi := (y i).isLt have hp : 2 ^ (n + 1) = 2 ^ n * 2 := pow_succ 2 n have hi' : (y i).val < 2 ^ n * 2 := hp ▸ hi omega let u : Fin d → Fin (2 ^ n) := fun i => ⟨(y i).val / 2, hybound i⟩ obtain ⟨k, hk⟩ := hbij.2 u let bits : Fin d → Bool := fun i => (y i).val % 2 = 1 obtain ⟨a, ha⟩ := (hpbij k).2 bits refine ⟨e (k, a), ?_⟩ funext i apply Fin.ext rw [hchild] have hv := (y i).val.mod_add_div 2 have hr : (y i).val % 2 < 2 := Nat.mod_lt _ (by omega) have hk' := congrFun hk i have ha' := congrFun ha i have hk'' := congrArg val hk' change (parent k i).val = (y i).val / 2 at hk'' change path k a i = ((y i).val % 2 = 1) at ha' rw [hk'', ha'] by_cases hb : (y i).val % 2 = 1 <;> simp [hb] <;> omega have hcadj (k l : Fin T) (hkl : l.val = k.val + 1) : FaceAdjacentGrid (fun i => (child k i).val) (fun i => (child l i).val) := by let q := (e.symm k).1 let r := (e.symm k).2 let q' := (e.symm l).1 let r' := (e.symm l).2 have hkval : k.val = B * q.val + r.val := by simpa only [q, r, e.apply_symm_apply] using (he q r) have hlval : l.val = B * q'.val + r'.val := by simpa only [q', r', e.apply_symm_apply] using (he q' r') by_cases hsame : q = q' · have hrr : r'.val = r.val + 1 := by have hr := r.isLt have hr' := r'.isLt rw [hsame] at hkval omega obtain ⟨i, hi, hother⟩ := hpadj q r r' hrr refine ⟨i, ?_, ?_⟩ · change (2 * (parent q i).val + if path q r i then 1 else 0) + 1 = (2 * (parent q' i).val + if path q' r' i then 1 else 0) ∨ (2 * (parent q' i).val + if path q' r' i then 1 else 0) + 1 = (2 * (parent q i).val + if path q r i then 1 else 0) rw [← hsame] by_cases hb : path q r i <;> by_cases hc : path q r' i <;> simp [hb, hc] at hi ⊢ · intro j hj change 2 * (parent q j).val + (if path q r j then 1 else 0) = 2 * (parent q' j).val + (if path q' r' j then 1 else 0) rw [← hsame, hother j hj] · have hq : q'.val = q.val + 1 := by have hstep : q'.val = q.val + (if B ∣ k.val + 1 then 1 else 0) := by rw [show q'.val = l.val / B from hdiv l, show q.val = k.val / B from hdiv k, hkl, Nat.succ_div] split_ifs at hstep with hdvd · exact hstep · have hqeq : q = q' := Fin.ext (by omega) exact False.elim (hsame hqeq) have hr : r.val = B - 1 := by have hr := r.isLt have hr' := r'.isLt rw [hq] at hlval simp only [mul_add, mul_one] at hlval omega have hr' : r'.val = 0 := by have hrr := r.isLt have hrr' := r'.isLt rw [hq] at hlval simp only [mul_add, mul_one] at hlval omega have hrfin : r = rev (0 : Fin B) := by apply Fin.ext simpa using hr have hrfin' : r' = 0 := Fin.ext hr' simpa only [child, Fin.val_mk, q, q', r, r', hrfin, hrfin'] using hpbridge q q' hq refine ⟨child, hcbij, hcadj, ?_⟩ intro k l hkl i rw [hnest] have hq : (e.symm l).1 = k := Fin.ext ((hdiv l).trans hkl) rw [hq]

theorem exists_perfectPairing_sqEuclidean_cost_le (d N : ℕ) (hd : 2 ≤ d) (hN : Even N) (hN2 : 2 ≤ N) (x : Fin N → Fin d → ℝ) (hx : ∀ i, InUnitCube (x i)) : ∃ M : PerfectPairing N, (∑ j : Fin (N / 2), sqEuclideanDist (x (M.edge j).1) (x (M.edge j).2)) ≤ 16 * (d : ℝ) * (N : ℝ) ^ (1 - (2 : ℝ) / d) := by obtain ⟨C⟩ := exists_holderCubeCurve d hd let t : Fin N → ℝ := fun i => choose (C.surjectiveOn (x i) (hx i)) have ht (i : Fin N) : t i ∈ Icc (0 : ℝ) 1 := (Classical.choose_spec (C.surjectiveOn (x i) (hx i))).1 have hxt (i : Fin N) : C.toFun (t i) = x i := (Classical.choose_spec (C.surjectiveOn (x i) (hx i))).2 obtain ⟨M, hgap⟩ := exists_pairing_gap_le_one N hN hN2 t ht refine ⟨M, ?_⟩ let p : ℝ := (2 : ℝ) / d have hdpos : (0 : ℝ) < d := by exact_mod_cast (by omega : 0 < d) have hp0 : 0 < p := by dsimp [p]; positivity have hp1 : p ≤ 1 := by dsimp [p] apply (div_le_iff₀ hdpos).2 norm_num exact_mod_cast hd have hq : 0 ≤ 1 - p := by linarith have hm : 0 < N / 2 := by omega have hnonneg (j : Fin (N / 2)) : 0 ≤ |t (M.edge j).1 - t (M.edge j).2| := abs_nonneg _ have hpow := sum_rpow_le_card_rpow hm p hp0 hp1 (fun j => |t (M.edge j).1 - t (M.edge j).2|) hnonneg hgap have hedge (j : Fin (N / 2)) : sqEuclideanDist (x (M.edge j).1) (x (M.edge j).2) ≤ 16 * (d : ℝ) * |t (M.edge j).1 - t (M.edge j).2| ^ p := by rw [← hxt (M.edge j).1, ← hxt (M.edge j).2] exact C.modulus (ht _) (ht _) have hcoeff : 0 ≤ 16 * (d : ℝ) := by positivity have hbase : ((N / 2 : ℕ) : ℝ) ≤ (N : ℝ) := by exact_mod_cast Nat.div_le_self N 2 calc (∑ j : Fin (N / 2), sqEuclideanDist (x (M.edge j).1) (x (M.edge j).2)) ≤ ∑ j : Fin (N / 2), 16 * (d : ℝ) * |t (M.edge j).1 - t (M.edge j).2| ^ p := Finset.sum_le_sum (fun j _ => hedge j) _ = 16 * (d : ℝ) * (∑ j : Fin (N / 2), |t (M.edge j).1 - t (M.edge j).2| ^ p) := by rw [Finset.mul_sum] _ ≤ 16 * (d : ℝ) * ((N / 2 : ℕ) : ℝ) ^ (1 - p) := mul_le_mul_of_nonneg_left hpow hcoeff _ ≤ 16 * (d : ℝ) * (N : ℝ) ^ (1 - p) := mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (by positivity) hbase hq) hcoeff _ = _ := rfl

theorem exists_neighboring_timeCells (d n : ℕ) {s t : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) (ht : t ∈ Icc (0 : ℝ) 1) (hgap : |s - t| ≤ (1 : ℝ) / (2 : ℝ) ^ (d * n)) : ∃ k l : Fin (2 ^ (d * n)), s ∈ dyadicTimeCell d n k ∧ t ∈ dyadicTimeCell d n l ∧ k.val ≤ l.val + 1 ∧ l.val ≤ k.val + 1 := by -- Clamp the floor of `2^(d*n) * s` and `2^(d*n) * t` at the final cell. -- Closed endpoints permit either adjacent index at a subdivision boundary. -- Write `q = 2^(d*n)` (strictly positive). For each `u ∈ [0,1]`, use -- `min ⌊q*u⌋₊ (q-1)`; `Nat.floor_le` and `Nat.lt_floor_add_one` put `u` -- in its closed cell, including `u=1`. Multiplying `hgap` by `q` shows -- `|q*s-q*t| ≤ 1`. The two clamped floors then differ by at most one; -- prove each orientation using `Nat.le_floor` and -- `Nat.floor_le_of_le`, with the final-cell clamp handled by `omega`. let q : ℕ := 2 ^ (d * n) have hq : 0 < q := by dsimp [q]; positivity have hqR : (0 : ℝ) < q := by exact_mod_cast hq let idx (u : ℝ) : Fin q := ⟨min ⌊(q : ℝ) * u⌋₊ (q - 1), lt_of_le_of_lt (Nat.min_le_right _ _) (sub_lt hq (by omega))⟩ have hcell (u : ℝ) (hu : u ∈ Icc (0 : ℝ) 1) : (idx u).val / (q : ℝ) ≤ u ∧ u ≤ ((idx u).val + 1) / (q : ℝ) := by have hprod0 : (0 : ℝ) ≤ (q : ℝ) * u := mul_nonneg hqR.le hu.1 have hprodle : (q : ℝ) * u ≤ q := by nlinarith [hu.2] have hfloorle : ⌊(q : ℝ) * u⌋₊ ≤ q := Nat.floor_le_of_le hprodle by_cases hf : ⌊(q : ℝ) * u⌋₊ < q · have hidx : (idx u).val = ⌊(q : ℝ) * u⌋₊ := by simp [idx, Nat.min_eq_left (by omega : ⌊(q : ℝ) * u⌋₊ ≤ q - 1)] have hlower := Nat.floor_le hprod0 have hupper := Nat.lt_floor_add_one ((q : ℝ) * u) rw [hidx] constructor · apply (div_le_iff₀ hqR).2 nlinarith · apply (le_div_iff₀ hqR).2 nlinarith · have heq : ⌊(q : ℝ) * u⌋₊ = q := by omega have hlower := Nat.floor_le hprod0 have hu_eq : u = 1 := by rw [heq] at hlower; nlinarith have hidx : (idx u).val = q - 1 := by simp [idx, heq] rw [hidx, hu_eq] constructor · apply (div_le_iff₀ hqR).2 simpa only [one_mul] using (show ((q - 1 : ℕ) : ℝ) ≤ (q : ℝ) by exact_mod_cast (sub_le q 1)) · have hsub : q - 1 + 1 = q := Nat.sub_add_cancel (by omega) rw [show ((q - 1 : ℕ) : ℝ) + 1 = (q : ℝ) by exact_mod_cast hsub] exact le_of_eq (div_self hqR.ne').symm have hscaled : |(q : ℝ) * s - (q : ℝ) * t| ≤ 1 := by have hqpow : (q : ℝ) = (2 : ℝ) ^ (d * n) := by simp [q] have hgap' : |s - t| ≤ 1 / (q : ℝ) := by simpa [hqpow] using hgap have hmul := mul_le_mul_of_nonneg_left hgap' hqR.le rw [mul_div_cancel₀ _ hqR.ne'] at hmul calc |(q : ℝ) * s - (q : ℝ) * t| = |(q : ℝ) * (s - t)| := by rw [mul_sub] _ = (q : ℝ) * |s - t| := by rw [abs_mul, abs_of_pos hqR] _ ≤ 1 := hmul have hfloor_close (u v : ℝ) (hu : 0 ≤ u) (hv : 0 ≤ v) (h : u ≤ v + 1) : ⌊u⌋₊ ≤ ⌊v⌋₊ + 1 := by have hvlt := Nat.lt_floor_add_one v have hult : u < ((⌊v⌋₊ + 2 : ℕ) : ℝ) := by push_cast; linarith have hf := (Nat.floor_lt' (by omega : ⌊v⌋₊ + 2 ≠ 0)).2 hult omega have hst : (q : ℝ) * s ≤ (q : ℝ) * t + 1 := by have := (abs_le.mp hscaled).2 linarith have hts : (q : ℝ) * t ≤ (q : ℝ) * s + 1 := by have := (abs_le.mp hscaled).1 linarith have hfs : ⌊(q : ℝ) * s⌋₊ ≤ ⌊(q : ℝ) * t⌋₊ + 1 := hfloor_close _ _ (mul_nonneg hqR.le hs.1) (mul_nonneg hqR.le ht.1) hst have hft : ⌊(q : ℝ) * t⌋₊ ≤ ⌊(q : ℝ) * s⌋₊ + 1 := hfloor_close _ _ (mul_nonneg hqR.le ht.1) (mul_nonneg hqR.le hs.1) hts have hindices : (idx s).val ≤ (idx t).val + 1 ∧ (idx t).val ≤ (idx s).val + 1 := by dsimp [idx] omega refine ⟨⟨(idx s).val, by simpa only [q] using (idx s).isLt⟩, ⟨(idx t).val, by simpa only [q] using (idx t).isLt⟩, ?_, ?_, hindices.1, hindices.2⟩ · simpa only [dyadicTimeCell, Set.mem_Icc, Nat.cast_pow, Nat.cast_ofNat, q] using hcell s hs · simpa only [dyadicTimeCell, Set.mem_Icc, Nat.cast_pow, Nat.cast_ofNat, q] using hcell t ht

theorem exists_coherent_finiteDyadicTraversals (d : ℕ) (hfinite : ∀ n, Nonempty (FiniteDyadicTraversal d n)) : ∃ T : ∀ n, FiniteDyadicTraversal d n, ∀ n, (T (n + 1)).truncate (le_succ n) = T n := by letI (n : ℕ) : Nonempty (FiniteDyadicTraversal d n) := hfinite n letI (n : ℕ) : Finite (FiniteDyadicTraversal d n) := finite_finiteDyadicTraversal d n obtain ⟨T, hT⟩ := exists_seq_forall_proj_of_forall_finite (fun {i j} hij (U : FiniteDyadicTraversal d j) => U.truncate hij) (by intro i U; rfl) (by intro i j k hij hjk U; rfl) (by intro i U; exact Set.toFinite _) exact ⟨T, fun n => hT (le_succ n)⟩