Grace/Cumulus/Set/Ordinal/Omega.g17

Open in Workbench Download source

Imports

ArithmeticLaws · Nat.Foundation

Declarations

Source

1-- Arithmetic at ω, the first limit ordinal: finite ordinals are absorbed2-- on the left, so addition, multiplication, and exponentiation are not3-- commutative4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Set.Ordinal.Omega10import ArithmeticLaws11import Nat.Foundation1213-- Finite ordinals are closed under the three operations.1415theorem ordinalAdd.natural (n m : Nat)16  shows Nat(ordinalAdd(n, m))17proof18  induction m19  | zero =>20    have nOrdinal := Ordinal.natural at n21    have base := ordinalAdd.zero at n22    rw base23    assumption24  | succ(k) using ih =>25    have nOrdinal := Ordinal.natural at n26    have kOrdinal := Ordinal.natural at k27    have shape := next.natural at k28    rw [shape, ordinalAdd.next]29    have back := next.natural at ordinalAdd(n, k)30    rw ← back31    exact Naturals.constructor.succ with ih3233theorem ordinalMul.natural (n m : Nat)34  shows Nat(ordinalMul(n, m))35proof36  induction m37  | zero =>38    have nOrdinal := Ordinal.natural at n39    have base := ordinalMul.zero at n40    rw [base, ← nat.zero]41    exact Naturals.constructor.zero42  | succ(k) using ih =>43    have nOrdinal := Ordinal.natural at n44    have kOrdinal := Ordinal.natural at k45    have shape := next.natural at k46    rw [shape, ordinalMul.next]47    exact ordinalAdd.natural at ordinalMul(n, k), n4849theorem ordinalPow.natural (n m : Nat)50  shows Nat(ordinalPow(n, m))51proof52  induction m53  | zero =>54    have nOrdinal := Ordinal.natural at n55    have base := ordinalPow.zero at n56    rw base57    exact Naturals.constructor.succ with Naturals.constructor.zero58  | succ(k) using ih =>59    have nOrdinal := Ordinal.natural at n60    have kOrdinal := Ordinal.natural at k61    have shape := next.natural at k62    rw [shape, ordinalPow.next]63    exact ordinalMul.natural at ordinalPow(n, k), n6465-- Addition: every finite ordinal is absorbed by ω on the left.6667theorem ordinalAdd.natural_omega (n : Nat)68  shows ordinalAdd(n, ω) = ω69proof70  have nOrdinal := Ordinal.natural at n71  have limit := Limit.omega72  have ωOrdinal := Ordinal.omega73  apply Subset.antisymmetric74  . intros x hx75    obtain ⟨m, hm, hxm⟩ :=76      ordinalAdd.limit_membership.forward at x, n, ω with limit, hx77    have mNat := nat.omega.backward with hm78    have sumNat := ordinalAdd.natural at n, m79    have sumIn := nat.omega.forward with sumNat80    have included := Ordinal.member_subset with ωOrdinal, sumIn81    exact included with x, hxm82  . intros m hm83    have mNat := nat.omega.backward with hm84    have mOrdinal := Ordinal.natural at m85    have included := ordinalAdd.subset_right at n, m with mOrdinal86    have sumOrdinal := ordinalAdd.ordinal at n, m with mOrdinal87    have bound := Ordinal.subset_bound with mOrdinal, sumOrdinal, included88    apply ordinalAdd.limit_membership.backward at m, n, ω with limit89    witness next(m)90    constructor91    . exact limit.right.right with m, hm92    . rw ordinalAdd.next93      exact bound9495theorem ordinalAdd.one_omega96  shows 1 + ω = ω97proof98  exact ordinalAdd.natural_omega at 199100theorem ordinalAdd.not_commutative101  shows 1 + ω ≠ ω + 1102proof103  intro equal104  have ωOrdinal := Ordinal.omega105  rw [ordinalAdd.one_omega, ordinalAdd.one] at equal106  have self := next.contains at ω107  rw ← equal at self108  exact Ordinal.not_member_self with self109110-- Multiplication: every positive finite ordinal is absorbed by ω on the left.111112theorem ordinalMul.natural_omega (n : Nat)113  requires positive : ∅ ∈ n114  shows ordinalMul(n, ω) = ω115proof116  have nOrdinal := Ordinal.natural at n117  have limit := Limit.omega118  have ωOrdinal := Ordinal.omega119  apply Subset.antisymmetric120  . intros x hx121    obtain ⟨m, hm, hxm⟩ :=122      ordinalMul.limit_membership.forward at x, n, ω with limit, hx123    have mNat := nat.omega.backward with hm124    have productNat := ordinalMul.natural at n, m125    have productIn := nat.omega.forward with productNat126    have included := Ordinal.member_subset with ωOrdinal, productIn127    exact included with x, hxm128  . intros m hm129    have mNat := nat.omega.backward with hm130    have mOrdinal := Ordinal.natural at m131    have nextOrdinal := Ordinal.next with mOrdinal132    have included := ordinalMul.subset_right at n, next(m)133      with positive, nextOrdinal134    apply ordinalMul.limit_membership.backward at m, n, ω with limit135    witness next(m)136    constructor137    . exact limit.right.right with m, hm138    . exact included with m, (next.contains at m)139140theorem ordinalMul.two (α : Ordinal)141  shows α * 2 = α + α142proof143  have two : 2 = next(1) by simp [next.natural]144  rw [two, ordinalMul.next, ordinalMul.one]145  rfl146147theorem ordinalMul.two_omega148  shows 2 * ω = ω149proof150  have positive : ∅ ∈ 2151    apply membership.two.backward152    left153    symm154    exact nat.zero155  exact ordinalMul.natural_omega at 2 with positive156157theorem ordinalMul.not_commutative158  shows 2 * ω ≠ ω * 2159proof160  intro equal161  have ωOrdinal := Ordinal.omega162  rw [ordinalMul.two_omega, ordinalMul.two] at equal163  have limit := Limit.omega164  have zeroIn := Ordinal.zero_member with limit.right.left165  have grows := ordinalAdd.member_right at ω, ω with zeroIn166  rw ← equal at grows167  exact Ordinal.not_member_self with grows168169-- Exponentiation: every finite base above one is absorbed by ω.170171theorem ordinalPow.natural_omega (n : Nat)172  requires above : 1 ∈ n173  shows ordinalPow(n, ω) = ω174proof175  have nOrdinal := Ordinal.natural at n176  have limit := Limit.omega177  have ωOrdinal := Ordinal.omega178  apply Subset.antisymmetric179  . intros x hx180    obtain ⟨m, hm, hxm⟩ :=181      ordinalPow.limit_membership.forward at x, n, ω with limit, hx182    have mNat := nat.omega.backward with hm183    have powerNat := ordinalPow.natural at n, m184    have powerIn := nat.omega.forward with powerNat185    have included := Ordinal.member_subset with ωOrdinal, powerIn186    exact included with x, hxm187  . intros m hm188    have mNat := nat.omega.backward with hm189    have mOrdinal := Ordinal.natural at m190    have nextOrdinal := Ordinal.next with mOrdinal191    have included := ordinalPow.subset_right at n, next(m)192      with above, nextOrdinal193    apply ordinalPow.limit_membership.backward at m, n, ω with limit194    witness next(m)195    constructor196    . exact limit.right.right with m, hm197    . exact included with m, (next.contains at m)198199theorem ordinalPow.two_omega200  shows 2 ^ ω = ω201proof202  have above : 1 ∈ 2203    apply membership.two.backward204    right205    rfl206  exact ordinalPow.natural_omega at 2 with above207208theorem ordinalPow.not_commutative209  shows 2 ^ ω ≠ ω ^ 2210proof211  intro equal212  have ωOrdinal := Ordinal.omega213  have two : 2 = next(1) by simp [next.natural]214  rw [ordinalPow.two_omega, two, ordinalPow.next, ordinalPow.one] at equal215  have limit := Limit.omega216  have zeroIn := Ordinal.zero_member with limit.right.left217  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero218  have oneIn := nat.omega.forward with oneNat219  have grows := ordinalMul.member_right at ω, ω with zeroIn, oneIn220  rw ← equal at grows221  exact Ordinal.not_member_self with grows222