Grace/Cumulus/Set/Ordinal/ArithmeticLaws.g17

Open in Workbench Download source

Imports

Monotone

Declarations

Source

1-- The laws of ordinal arithmetic: associativity of addition and2-- multiplication, left distributivity, and the two power laws, each by3-- transfinite induction on the right argument4-- 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.ArithmeticLaws10import Monotone1112theorem ordinalAdd.associative (α β : Ordinal, γ : Set)13  shows γ ∈ Ordinal → (α + β) + γ = α + (β + γ)14proof15  induction γ using membership16  intros current ih hCurrent17  have βOrdinal : β ∈ Ordinal by assumption18  have sumOrdinal := ordinalAdd.ordinal at α, β with βOrdinal19  have cases := Ordinal.cases with hCurrent20  cases cases with zero | rest21  . rw zero22    rw ← nat.zero23    have first := ordinalAdd.zero at α + β24    have second := ordinalAdd.zero at β25    rw [first, second]26    rfl27  . cases rest with successor | limit28    . obtain ⟨δ, hδ, shape⟩ := successor29      rw ← shape30      have δOrdinal := Ordinal.member with hCurrent, hδ31      have step := ih with hδ, δOrdinal32      have innerOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal33      have first := ordinalAdd.next at α + β, δ34      have second := ordinalAdd.next at β, δ35      have third := ordinalAdd.next at α, β + δ36      rw [first, second, third, step]37      rfl38    . have innerLimit := ordinalAdd.limit_right at β, current with limit39      have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent40      apply Subset.antisymmetric41      . intros x hx42        obtain ⟨δ, hδ, hxδ⟩ :=43          ordinalAdd.limit_membership.forward at x, α + β, current44            with limit, hx45        have δOrdinal := Ordinal.member with hCurrent, hδ46        have step := ih with hδ, δOrdinal47        rw step at hxδ48        apply ordinalAdd.limit_membership.backward at x, α, β + current49          with innerLimit50        witness β + δ51        constructor52        . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ53        . exact hxδ54      . intros x hx55        obtain ⟨ε, hε, hxε⟩ :=56          ordinalAdd.limit_membership.forward at x, α, β + current57            with innerLimit, hx58        obtain ⟨δ, hδ, hεδ⟩ :=59          ordinalAdd.limit_membership.forward at ε, β, current with limit, hε60        have δOrdinal := Ordinal.member with hCurrent, hδ61        have stageOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal62        have εOrdinal := Ordinal.member with stageOrdinal, hεδ63        have grows := ordinalAdd.monotone at α, ε, β + δ with stageOrdinal, hεδ64        have sumStage := ordinalAdd.ordinal at α, β + δ with stageOrdinal65        have included := Ordinal.member_subset with sumStage, grows66        have step := ih with hδ, δOrdinal67        apply ordinalAdd.limit_membership.backward at x, α + β, current68          with limit69        witness δ70        constructor71        . exact hδ72        . rw step73          exact included with x, hxε7475theorem ordinalMul.distributive (α β : Ordinal, γ : Set)76  shows γ ∈ Ordinal → α * (β + γ) = α * β + α * γ77proof78  induction γ using membership79  intros current ih hCurrent80  have αOrdinal : α ∈ Ordinal by assumption81  have βOrdinal : β ∈ Ordinal by assumption82  have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal83  have cases := Ordinal.cases with hCurrent84  cases cases with zero | rest85  . rw zero86    rw ← nat.zero87    have first := ordinalAdd.zero at β88    have second := ordinalMul.zero at α89    have third := ordinalAdd.zero at α * β90    rw nat.zero at third91    rw [first, second, third]92    rfl93  . cases rest with successor | limit94    . obtain ⟨δ, hδ, shape⟩ := successor95      rw ← shape96      have δOrdinal := Ordinal.member with hCurrent, hδ97      have step := ih with hδ, δOrdinal98      have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal99      have stageOrdinal := ordinalMul.ordinal at α, δ with δOrdinal100      have first := ordinalAdd.next at β, δ101      have second := ordinalMul.next at α, β + δ102      have third := ordinalMul.next at α, δ103      have fourth := ordinalAdd.associative at α * β, α * δ, α with αOrdinal104      rw [first, second, step, third, fourth]105      rfl106    . have zeroCases := Ordinal.trichotomy at ∅ with Ordinal.empty, α, αOrdinal107      cases zeroCases with positive | rest2108      . have innerLimit := ordinalAdd.limit_right at β, current with limit109        have productLimit := ordinalMul.limit_right at α, current110          with positive, limit111        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent112        have productCurrent := ordinalMul.ordinal at α, current with hCurrent113        apply Subset.antisymmetric114        . intros x hx115          obtain ⟨ε, hε, hxε⟩ :=116            ordinalMul.limit_membership.forward at x, α, β + current117              with innerLimit, hx118          obtain ⟨δ, hδ, hεδ⟩ :=119            ordinalAdd.limit_membership.forward at ε, β, current with limit, hε120          have δOrdinal := Ordinal.member with hCurrent, hδ121          have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal122          have εOrdinal := Ordinal.member with sumOrdinal, hεδ123          have included := ordinalMul.subset_monotone at α, ε, β + δ124            with sumOrdinal, hεδ125          have step := ih with hδ, δOrdinal126          have inStage : x ∈ α * (β + δ) := included with x, hxε127          rw step at inStage128          apply ordinalAdd.limit_membership.backward at x, α * β, α * current129            with productLimit130          witness α * δ131          constructor132          . exact ordinalMul.monotone at α, δ, current133            with positive, hCurrent, hδ134          . exact inStage135        . intros x hx136          obtain ⟨ε, hε, hxε⟩ :=137            ordinalAdd.limit_membership.forward at x, α * β, α * current138              with productLimit, hx139          obtain ⟨δ, hδ, hεδ⟩ :=140            ordinalMul.limit_membership.forward at ε, α, current with limit, hε141          have δOrdinal := Ordinal.member with hCurrent, hδ142          have stageOrdinal := ordinalMul.ordinal at α, δ with δOrdinal143          have εOrdinal := Ordinal.member with stageOrdinal, hεδ144          have grows := ordinalAdd.monotone at α * β, ε, α * δ145            with stageOrdinal, hεδ146          have sumStage := ordinalAdd.ordinal at α * β, α * δ with stageOrdinal147          have included := Ordinal.member_subset with sumStage, grows148          have step := ih with hδ, δOrdinal149          apply ordinalMul.limit_membership.backward at x, α, β + current150            with innerLimit151          witness β + δ152          constructor153          . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ154          . rw step155            exact included with x, hxε156      . cases rest2 with equal | below157        . rw ← nat.zero at equal158          rw ← equal159          have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent160          have first := ordinalMul.zero_left at β + current with innerOrdinal161          have second := ordinalMul.zero_left at β with βOrdinal162          have third := ordinalMul.zero_left at current with hCurrent163          rw [first, second, third]164          symm165          exact ordinalAdd.zero at 0166        . exfalso167          exact set.empty with below168169theorem ordinalMul.associative (α β : Ordinal, γ : Set)170  shows γ ∈ Ordinal → (α * β) * γ = α * (β * γ)171proof172  induction γ using membership173  intros current ih hCurrent174  have αOrdinal : α ∈ Ordinal by assumption175  have βOrdinal : β ∈ Ordinal by assumption176  have productOrdinal := ordinalMul.ordinal at α, β with βOrdinal177  have cases := Ordinal.cases with hCurrent178  cases cases with zero | rest179  . rw zero180    rw ← nat.zero181    have first := ordinalMul.zero at α * β182    have second := ordinalMul.zero at β183    have third := ordinalMul.zero at α184    rw nat.zero at third185    rw [first, second, third]186    rfl187  . cases rest with successor | limit188    . obtain ⟨δ, hδ, shape⟩ := successor189      rw ← shape190      have δOrdinal := Ordinal.member with hCurrent, hδ191      have step := ih with hδ, δOrdinal192      have innerOrdinal := ordinalMul.ordinal at β, δ with δOrdinal193      have first := ordinalMul.next at α * β, δ194      have second := ordinalMul.next at β, δ195      have third := ordinalMul.distributive at α, β * δ, β with βOrdinal196      rw [first, step, second, third]197      rfl198    . have zeroCases := Ordinal.trichotomy at ∅ with Ordinal.empty, β, βOrdinal199      cases zeroCases with positive | rest2200      . have innerLimit := ordinalMul.limit_right at β, current201          with positive, limit202        have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent203        apply Subset.antisymmetric204        . intros x hx205          obtain ⟨δ, hδ, hxδ⟩ :=206            ordinalMul.limit_membership.forward at x, α * β, current207              with limit, hx208          have δOrdinal := Ordinal.member with hCurrent, hδ209          have step := ih with hδ, δOrdinal210          rw step at hxδ211          apply ordinalMul.limit_membership.backward at x, α, β * current212            with innerLimit213          witness β * δ214          constructor215          . exact ordinalMul.monotone at β, δ, current216            with positive, hCurrent, hδ217          . exact hxδ218        . intros x hx219          obtain ⟨ε, hε, hxε⟩ :=220            ordinalMul.limit_membership.forward at x, α, β * current221              with innerLimit, hx222          obtain ⟨δ, hδ, hεδ⟩ :=223            ordinalMul.limit_membership.forward at ε, β, current with limit, hε224          have δOrdinal := Ordinal.member with hCurrent, hδ225          have stageOrdinal := ordinalMul.ordinal at β, δ with δOrdinal226          have εOrdinal := Ordinal.member with stageOrdinal, hεδ227          have included := ordinalMul.subset_monotone at α, ε, β * δ228            with stageOrdinal, hεδ229          have step := ih with hδ, δOrdinal230          apply ordinalMul.limit_membership.backward at x, α * β, current231            with limit232          witness δ233          constructor234          . exact hδ235          . rw step236            exact included with x, hxε237      . cases rest2 with equal | below238        . rw ← nat.zero at equal239          rw ← equal240          have first : α * 0 = 0241            rw ordinalMul.zero242            symm243            exact nat.zero244          have second := ordinalMul.zero_left at current with hCurrent245          rw [first, second, first]246          rfl247        . exfalso248          exact set.empty with below249250-- Powers251252theorem ordinalPow.one_left (β : Set)253  shows β ∈ Ordinal → ordinalPow(1, β) = 1254proof255  induction β using membership256  intros current ih hCurrent257  have oneOrdinal := Ordinal.natural at 1258  have cases := Ordinal.cases with hCurrent259  cases cases with zero | rest260  . rw zero261    have base := ordinalPow.zero at 1262    rw nat.zero at base263    exact base264  . cases rest with successor | limit265    . obtain ⟨γ, hγ, shape⟩ := successor266      rw ← shape267      have γOrdinal := Ordinal.member with hCurrent, hγ268      have step := ih with hγ, γOrdinal269      rw [ordinalPow.next, step]270      exact ordinalMul.one at 1271    . apply Subset.antisymmetric272      . intros x hx273        obtain ⟨stage, hStage, hxStage⟩ :=274          ordinalPow.limit_membership.forward at x, 1, current with limit, hx275        have step := ih with hStage, (Ordinal.member with hCurrent, hStage)276        rw step at hxStage277        exact hxStage278      . intros x hx279        apply ordinalPow.limit_membership.backward at x, 1, current with limit280        witness ∅281        constructor282        . exact Ordinal.zero_member with limit.right.left283        . have base := ordinalPow.zero at 1284          rw nat.zero at base285          rw base286          exact hx287288-- A positive ordinal is one or lies above one.289theorem Ordinal.one_or_above_one (α : Ordinal)290  requires positive : ∅ ∈ α291  shows α = 1 ∨ 1 ∈ α292proof293  have αOrdinal : α ∈ Ordinal by assumption294  have oneOrdinal := Ordinal.natural at 1295  have cases := Ordinal.trichotomy at α with αOrdinal, 1, oneOrdinal296  cases cases with below | rest297  . exfalso298    have one : 1 = next(0) by simp [next.natural]299    rw one at below300    simp [next.membership] at below301    cases below with inZero | isZero302    . rw nat.zero at inZero303      exact set.empty with inZero304    . rw isZero at positive305      rw nat.zero at positive306      exact set.empty with positive307  . cases rest with equal | above308    . left309      exact equal310    . right311      exact above312313theorem ordinalPow.add (α β : Ordinal, γ : Set)314  requires positive : ∅ ∈ α315  shows γ ∈ Ordinal → α ^ (β + γ) = α ^ β * α ^ γ316proof317  induction γ using membership318  intros current ih hCurrent319  have αOrdinal : α ∈ Ordinal by assumption320  have βOrdinal : β ∈ Ordinal by assumption321  have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal322  have cases := Ordinal.cases with hCurrent323  cases cases with zero | rest324  . rw zero325    rw ← nat.zero326    have first := ordinalAdd.zero at β327    have second := ordinalPow.zero at α328    have third := ordinalMul.one at α ^ β329    rw [first, second, third]330    rfl331  . cases rest with successor | limit332    . obtain ⟨δ, hδ, shape⟩ := successor333      rw ← shape334      have δOrdinal := Ordinal.member with hCurrent, hδ335      have step := ih with hδ, δOrdinal336      have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal337      have stageOrdinal := ordinalPow.ordinal at α, δ with δOrdinal338      have first := ordinalAdd.next at β, δ339      have second := ordinalPow.next at α, β + δ340      have third := ordinalPow.next at α, δ341      have fourth := ordinalMul.associative at α ^ β, α ^ δ, α with αOrdinal342      rw [first, second, step, third, fourth]343      rfl344    . have oneCases := Ordinal.one_or_above_one with positive345      cases oneCases with one | above346      . rw one347        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent348        have first := ordinalPow.one_left at β + current with innerOrdinal349        have second := ordinalPow.one_left at β with βOrdinal350        have third := ordinalPow.one_left at current with hCurrent351        rw [first, second, third]352        symm353        exact ordinalMul.one at 1354      . have innerLimit := ordinalAdd.limit_right at β, current with limit355        have powerLimit := ordinalPow.limit_right at α, current356          with above, limit357        have innerOrdinal := ordinalAdd.ordinal at β, current with hCurrent358        have powerCurrent := ordinalPow.ordinal at α, current with hCurrent359        apply Subset.antisymmetric360        . intros x hx361          obtain ⟨ε, hε, hxε⟩ :=362            ordinalPow.limit_membership.forward at x, α, β + current363              with innerLimit, hx364          obtain ⟨δ, hδ, hεδ⟩ :=365            ordinalAdd.limit_membership.forward at ε, β, current with limit, hε366          have δOrdinal := Ordinal.member with hCurrent, hδ367          have sumOrdinal := ordinalAdd.ordinal at β, δ with δOrdinal368          have εOrdinal := Ordinal.member with sumOrdinal, hεδ369          have included := ordinalPow.subset_monotone at α, ε, β + δ370            with positive, sumOrdinal, hεδ371          have step := ih with hδ, δOrdinal372          have inStage : x ∈ α ^ (β + δ) := included with x, hxε373          rw step at inStage374          apply ordinalMul.limit_membership.backward at x, α ^ β, α ^ current375            with powerLimit376          witness α ^ δ377          constructor378          . exact ordinalPow.monotone at α, δ, current with above, hCurrent, hδ379          . exact inStage380        . intros x hx381          obtain ⟨ε, hε, hxε⟩ :=382            ordinalMul.limit_membership.forward at x, α ^ β, α ^ current383              with powerLimit, hx384          obtain ⟨δ, hδ, hεδ⟩ :=385            ordinalPow.limit_membership.forward at ε, α, current with limit, hε386          have δOrdinal := Ordinal.member with hCurrent, hδ387          have stageOrdinal := ordinalPow.ordinal at α, δ with δOrdinal388          have εOrdinal := Ordinal.member with stageOrdinal, hεδ389          have included := ordinalMul.subset_monotone at α ^ β, ε, α ^ δ390            with stageOrdinal, hεδ391          have step := ih with hδ, δOrdinal392          apply ordinalPow.limit_membership.backward at x, α, β + current393            with innerLimit394          witness β + δ395          constructor396          . exact ordinalAdd.monotone at β, δ, current with hCurrent, hδ397          . rw step398            exact included with x, hxε399400theorem ordinalPow.mul (α β : Ordinal, γ : Set)401  requires positive : ∅ ∈ α402  shows γ ∈ Ordinal → (α ^ β) ^ γ = α ^ (β * γ)403proof404  induction γ using membership405  intros current ih hCurrent406  have αOrdinal : α ∈ Ordinal by assumption407  have βOrdinal : β ∈ Ordinal by assumption408  have powerOrdinal := ordinalPow.ordinal at α, β with βOrdinal409  have cases := Ordinal.cases with hCurrent410  cases cases with zero | rest411  . rw zero412    rw ← nat.zero413    have first := ordinalPow.zero at α ^ β414    have second := ordinalMul.zero at β415    have third := ordinalPow.zero at α416    rw nat.zero at third417    rw [first, second, third]418    rfl419  . cases rest with successor | limit420    . obtain ⟨δ, hδ, shape⟩ := successor421      rw ← shape422      have δOrdinal := Ordinal.member with hCurrent, hδ423      have step := ih with hδ, δOrdinal424      have innerOrdinal := ordinalMul.ordinal at β, δ with δOrdinal425      have first := ordinalPow.next at α ^ β, δ426      have second := ordinalMul.next at β, δ427      have third := ordinalPow.add at α, β * δ, β with positive, βOrdinal428      rw [first, step, second, third]429      rfl430    . have oneCases := Ordinal.one_or_above_one with positive431      cases oneCases with one | above432      . rw one433        have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent434        have first := ordinalPow.one_left at β with βOrdinal435        have second := ordinalPow.one_left at current with hCurrent436        have third := ordinalPow.one_left at β * current with innerOrdinal437        rw [first, second, third]438        rfl439      . have zeroCases := Ordinal.trichotomy at ∅440        with Ordinal.empty, β, βOrdinal441        cases zeroCases with βPositive | rest2442        . have innerLimit := ordinalMul.limit_right at β, current443            with βPositive, limit444          have innerOrdinal := ordinalMul.ordinal at β, current with hCurrent445          apply Subset.antisymmetric446          . intros x hx447            obtain ⟨δ, hδ, hxδ⟩ :=448              ordinalPow.limit_membership.forward at x, α ^ β, current449                with limit, hx450            have δOrdinal := Ordinal.member with hCurrent, hδ451            have step := ih with hδ, δOrdinal452            rw step at hxδ453            apply ordinalPow.limit_membership.backward at x, α, β * current454              with innerLimit455            witness β * δ456            constructor457            . exact ordinalMul.monotone at β, δ, current458                with βPositive, hCurrent, hδ459            . exact hxδ460          . intros x hx461            obtain ⟨ε, hε, hxε⟩ :=462              ordinalPow.limit_membership.forward at x, α, β * current463                with innerLimit, hx464            obtain ⟨δ, hδ, hεδ⟩ :=465              ordinalMul.limit_membership.forward at ε, β, current466                with limit, hε467            have δOrdinal := Ordinal.member with hCurrent, hδ468            have stageOrdinal := ordinalMul.ordinal at β, δ with δOrdinal469            have εOrdinal := Ordinal.member with stageOrdinal, hεδ470            have included := ordinalPow.subset_monotone at α, ε, β * δ471              with positive, stageOrdinal, hεδ472            have step := ih with hδ, δOrdinal473            apply ordinalPow.limit_membership.backward at x, α ^ β, current474              with limit475            witness δ476            constructor477            . exact hδ478            . rw step479              exact included with x, hxε480        . cases rest2 with equal | below481          . rw ← nat.zero at equal482            rw ← equal483            have first := ordinalPow.zero at α484            have second := ordinalMul.zero_left at current with hCurrent485            have third := ordinalPow.one_left at current with hCurrent486            rw [first, second, third, first]487            rfl488          . exfalso489            exact set.empty with below490