OrdinalPairs.lean

1import BFPP.OrdinalIndex2import Mathlib.SetTheory.Ordinal.Principal34/-! # Pairing coordinates below a limit ordinal -/56namespace BFPP78set_option autoImplicit false9open Set Order1011universe u1213theorem ordinal_two_mul_limit (tau : Ordinal.{u}) (htau : IsSuccLimit tau) : 2 * tau = tau :=14  Ordinal.mul_omega0_dvd (by norm_num) (by simpa using Ordinal.natCast_lt_omega0 2)15    (Ordinal.isSuccPrelimit_iff_omega0_dvd.mp htau.isSuccPrelimit)1617theorem ordinal_mod_two_cases (a : Ordinal.{u}) : a % 2 = 0 ∨ a % 2 = 1 := by18  have h := Ordinal.mod_lt a (by norm_num : (2 : Ordinal.{u}) ≠ 0)19  have hle : a % 2 ≤ 1 := Order.le_of_lt_succ (by simpa using h)20  rcases hle.lt_or_eq with hlt | heq21  · exact Or.inl (Order.lt_one_iff.mp hlt)22  · exact Or.inr heq2324variable (κ : Ordinal.{u}) [hκ : Fact (IsSuccLimit κ)]2526noncomputable def evenIndex (i : OrdinalIndex κ) : OrdinalIndex κ :=27  ⟨2 * i.val, by28    have h : 2 * i.val < 2 * κ :=29      (Ordinal.isNormal_mul_right (by norm_num : (0 : Ordinal.{u}) < 2)).strictMono i.property30    exact h.trans_eq (ordinal_two_mul_limit κ hκ.out)⟩3132noncomputable def oddIndex (i : OrdinalIndex κ) : OrdinalIndex κ :=33  ⟨2 * i.val + 1, hκ.out.succ_lt (evenIndex κ i).property⟩3435noncomputable def halfIndex (i : OrdinalIndex κ) : OrdinalIndex κ :=36  ⟨i.val / 2, (Ordinal.lt_mul_iff_div_lt (by norm_num : (2 : Ordinal.{u}) ≠ 0)).mp37    (by rw [ordinal_two_mul_limit κ hκ.out]; exact i.property)⟩3839@[simp] theorem half_evenIndex (i : OrdinalIndex κ) : halfIndex κ (evenIndex κ i) = i := by40  apply Subtype.ext41  exact Ordinal.mul_div_cancel i.val (by norm_num)4243@[simp] theorem half_oddIndex (i : OrdinalIndex κ) : halfIndex κ (oddIndex κ i) = i := by44  apply Subtype.ext45  change (2 * i.val + 1) / 2 = i.val46  rw [Ordinal.mul_add_div i.val (by norm_num)]47  norm_num [Ordinal.div_eq_zero_of_lt]4849@[simp] theorem evenIndex_mod (i : OrdinalIndex κ) : (evenIndex κ i).val % 2 = 0 :=50  Ordinal.mul_mod _ _5152@[simp] theorem oddIndex_mod (i : OrdinalIndex κ) : (oddIndex κ i).val % 2 = 1 := by53  change (2 * i.val + 1) % 2 = 154  rw [Ordinal.mul_add_mod_self]55  exact Ordinal.mod_eq_of_lt (by norm_num)5657theorem index_eq_even_or_odd (i : OrdinalIndex κ) :58    i = evenIndex κ (halfIndex κ i) ∨ i = oddIndex κ (halfIndex κ i) := by59  rcases ordinal_mod_two_cases i.val with h | h60  · left61    apply Subtype.ext62    change i.val = 2 * (i.val / 2)63    simpa only [h, add_zero] using (Ordinal.div_add_mod i.val 2).symm64  · right65    apply Subtype.ext66    change i.val = 2 * (i.val / 2) + 167    simpa only [h] using (Ordinal.div_add_mod i.val 2).symm6869@[simp] theorem evenIndex_bot : evenIndex κ ⊥ = ⊥ := by70  apply Subtype.ext71  change (2 : Ordinal.{u}) * 0 = 072  simp7374theorem evenIndex_strictMono : StrictMono (evenIndex κ) := by75  intro i j hij76  exact (Ordinal.isNormal_mul_right (by norm_num : (0 : Ordinal.{u}) < 2)).strictMono hij7778theorem oddIndex_strictMono : StrictMono (oddIndex κ) := by79  intro i j hij80  change 2 * i.val + 1 < 2 * j.val + 181  exact Order.succ_lt_succ (show 2 * i.val < 2 * j.val from evenIndex_strictMono κ hij)8283end BFPP

SHA-256