Grace/Cumulus/Geometry/Absorption/Order.g17

Open in Workbench Download source

Imports

Turn · CountableUnion · Roots

Declarations

Source

1-- The order of turn(t): the plane turn by a complex number z, with2-- planeTurnOf(z)ⁿ = planeTurnOf(zⁿ); turn(t) is the plane turn by the point3-- (turnCos(t), turnSin(t)) of the unit circle, so turn(t)ⁿ = 1 forces that4-- point to be an n-th root of unity, of which there are finitely many;5-- hence turn(t) has infinite order for all but countably many t6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Geometry.Absorption.Order12import Turn13import CountableUnion14import Roots1516-- Coordinates of a complex number are real.17instance complexCarrier.fst_real (z : Set)18  requires member : z ∈ complexCarrier19  shows fst(z) ∈ ℝ20proof21  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member22  rw [shape, fst.pair]23  exact aReal2425instance complexCarrier.snd_real (z : Set)26  requires member : z ∈ complexCarrier27  shows snd(z) ∈ ℝ28proof29  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member30  rw [shape, snd.pair]31  exact bReal3233-- The plane turn by a complex number.34def planeTurnOf (z : Set) : Set := planeTurn(fst(z), snd(z))3536theorem planeTurnOf.graph (z : Set)37  shows planeTurnOf(z) = planeTurn(fst(z), snd(z))38proof39  simp [planeTurnOf]4041theorem planeTurnOf.pair (a b : Real)42  shows planeTurnOf((a, b)) = planeTurn(a, b)43proof44  rw [planeTurnOf.graph, fst.pair, snd.pair]45  rfl4647instance planeTurnOf.matrix (z : Set)48  requires member : z ∈ complexCarrier49  shows planeTurnOf(z) : realRing ^ 3 × 350proof51  have first := complexCarrier.fst_real with member52  have second := complexCarrier.snd_real with member53  rw planeTurnOf.graph54  exact planeTurn.matrix with *5556theorem planeTurnOf.one57  shows planeTurnOf(complexOne) = Ring.one(matrixRing(realRing, 3))58proof59  have pair : complexOne = ((1:R), (0:R))60    unfold complexOne61    rfl62  rw [pair, planeTurnOf.pair]63  exact planeTurn.one6465theorem planeTurnOf.mul (z w : Set)66  requires memberZ : z ∈ complexCarrier67  requires memberW : w ∈ complexCarrier68  shows matrixMul3(planeTurnOf(z), planeTurnOf(w)) = planeTurnOf(complexMul(z, w))69proof70  obtain ⟨a, aReal, b, bReal, shapeZ⟩ := complexCarrier.cases with memberZ71  obtain ⟨c, cReal, d, dReal, shapeW⟩ := complexCarrier.cases with memberW72  have product := complexMul.pair at a, b, c, d with *73  have difference : a * c - b * d = a * c + -(b * d)74    ring75  rw [shapeZ, shapeW, planeTurnOf.pair, planeTurnOf.pair, product,76    planeTurnOf.pair, planeTurn.mul, difference]77  rfl7879theorem planeTurnOf.pow (z : Set) (n : Nat)80  requires member : z ∈ complexCarrier81  shows planeTurnOf(z) ^ n = planeTurnOf(monoidPow(complexMul, complexOne, z, n))82proof83  induction n84  | zero =>85    have matrix := planeTurnOf.matrix with member86    rw [matrixPow3.zero, monoidPow.zero, planeTurnOf.one]87    rfl88  | succ(k) using ih =>89    have ring := complexes.comm_ring90    have ordinary := IsCommRing.ring with ring91    have monoid := IsRing.multiplicative with ordinary92    have matrix := planeTurnOf.matrix with member93    have power := monoidPow.closed at complexCarrier, complexMul, complexOne, z, k94      with monoid, member95    have succForm : k + 1 = succ(k) := add.right_one at k96    have typed : Matrix3(planeTurnOf(z)) := Matrix3.of_matrix with matrix97    have step := matrixPow3.succ at planeTurnOf(z), k with typed98    rw succForm at step99    have combine := planeTurnOf.mul with member, power100    rw [step, ih, monoidPow.succ]101    exact combine102103-- A plane turn equal to the identity is the turn by (1, 0).104theorem planeTurn.eq_one (a b : Real)105  requires same : planeTurn(a, b) = Ring.one(matrixRing(realRing, 3))106  shows a = (1:R) ∧ b = (0:R)107proof108  have comm := realRing.comm_ring109  have zeroIn : 0 ∈ 3 by typecheck110  have oneIn : 1 ∈ 3 by typecheck111  have zeroReal : (0:R) ∈ ℝ by typecheck112  have oneReal : (1:R) ∈ ℝ by typecheck113  have entry00 := matrixRing.one_entry at realRing, 3, 0, 0 with *114  have entry10 := matrixRing.one_entry at realRing, 3, 1, 0 with *115  rw [realRing.carrierOf, realRing.zero_eq, realRing.one_eq] at entry00116  rw [realRing.carrierOf, realRing.zero_eq, realRing.one_eq] at entry10117  have equal : (0:N) = (0:N) by rfl118  have different : (1:N) ≠ (0:N)119    intro flipped120    symm at flipped121    exact threeIndex.zero_ne_one with flipped122  have diagonal := singleValue.same at ℝ, realZero, realOne, 0, 0 with *123  have off := singleValue.other at ℝ, realZero, realOne, 0, 1 with *124  have first := planeTurn.entry00 at a, b125  have second := planeTurn.entry10 at a, b126  constructor127  . calc128      a = planeTurn(a, b)[0, 0] := by rw first129      _ = Ring.one(matrixRing(realRing, 3))[0, 0] := by rw same130      _ = (1:R) := by rw [entry00, diagonal]131  . calc132      b = planeTurn(a, b)[1, 0] := by rw second133      _ = Ring.one(matrixRing(realRing, 3))[1, 0] := by rw same134      _ = (0:R) := by rw [entry10, off]135136theorem complexCarrier.eq_one (z : Set)137  requires member : z ∈ complexCarrier138  requires first : fst(z) = (1:R)139  requires second : snd(z) = (0:R)140  shows z = complexOne141proof142  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member143  rw [shape, fst.pair] at first144  rw [shape, snd.pair] at second145  rw [shape, first, second]146  unfold complexOne147  rfl148149-- The point of the unit circle that turn(t) turns by.150defgraph turnPoint (t ∈ ℝ) : complexCarrier := (turnCos(t), turnSin(t))151proof152  have real : Real(t) by typecheck153  exact complexCarrier.pair at turnCos(t), turnSin(t) with *154155theorem turnPoint.injective156  shows InjectiveBetween(turnPoint, ℝ, complexCarrier)157proof158  have function := turnPoint.function159  apply Injective.of_pointwise with function160  intros s hs t ht same161  have valueS := turnPoint.value at s with *162  have valueT := turnPoint.value at t with *163  rw [valueS, valueT] at same164  obtain ⟨cosEqual, sinEqual⟩ := orderedPair.injective with same165  exact turn.injective_of_coordinates with cosEqual, sinEqual166167theorem turn.planeTurnOf (t : Real)168  shows turn(t) = planeTurnOf(turnPoint(t))169proof170  have real : t ∈ ℝ by typecheck171  have value := turnPoint.value at t with *172  rw [value, planeTurnOf.pair, turn.graph]173  rfl174175-- The parameters t with turn(t)ⁿ = 1, for one n and for some n ≥ 1.176def turnOrderSet (n : Nat) : Set :=177  { t ∈ ℝ | matrixPow3(turn(t), n) = Ring.one(matrixRing(realRing, 3)) }178179def turnOrders : Set :=180  { t ∈ ℝ | ∃ n ∈ ℕ, 0 < n ∧ matrixPow3(turn(t), n) = Ring.one(matrixRing(realRing, 3)) }181182theorem turnOrderSet.subset (n : Nat)183  shows turnOrderSet(n) ⊆ ℝ184proof185  intros t ht186  have data := turnOrderSet.membership.forward with ht187  exact data.left188189-- For n ≥ 1 only finitely many t have turn(t)ⁿ = 1: their points are190-- n-th roots of unity, and t ↦ turnPoint(t) is injective.191theorem turnOrderSet.finite (k : Nat)192  shows Finite(turnOrderSet(k + 1))193proof194  have injective := turnPoint.injective195  have rootsFinite := complexUnityRoots.finite at k196  have preimageFinite := Finite.preimage with injective, rootsFinite197  have bounded : turnOrderSet(k + 1) ⊆ functionPreimage(turnPoint, ℝ, complexUnityRoots(k))198    intros t ht199    obtain ⟨real, power⟩ := turnOrderSet.membership.forward with ht200    have typed : Real(t) by typecheck201    have pointIn : turnPoint(t) ∈ complexCarrier :=202      FunctionBetween.apply_closed with turnPoint.function, real203    have shape := turn.planeTurnOf at t204    have matrixPower := planeTurnOf.pow at turnPoint(t), k + 1 with pointIn205    have succForm : k + 1 = succ(k) := add.right_one at k206    rw shape at power207    have unitPower : planeTurnOf(monoidPow(complexMul, complexOne, turnPoint(t), k + 1)) =208        Ring.one(matrixRing(realRing, 3))209      rw ← matrixPower210      exact power211    have ring := complexes.comm_ring212    have ordinary := IsCommRing.ring with ring213    have monoid := IsRing.multiplicative with ordinary214    have powerIn := monoidPow.closed at complexCarrier, complexMul, complexOne,215      turnPoint(t), k + 1 with monoid, pointIn216    have first := complexCarrier.fst_real with powerIn217    have second := complexCarrier.snd_real with powerIn218    rw planeTurnOf.graph at unitPower219    obtain ⟨fstOne, sndZero⟩ := planeTurn.eq_one with unitPower220    have rootOfUnity := complexCarrier.eq_one with powerIn, fstOne, sndZero221    rw succForm at rootOfUnity222    have inRoots := complexUnityRoots.contains with pointIn, rootOfUnity223    exact functionPreimage.membership.backward with ⟨real, inRoots⟩224  exact Finite.subset with preimageFinite, bounded225226-- The family n ↦ turnOrderSet(n + 1), indexed by ℕ.227defgraph turnOrderFamily (n ∈ ℕ) : 𝒫(ℝ) := turnOrderSet(n + 1)228proof229  have subset := turnOrderSet.subset at n + 1230  exact powerset.membership_iff.backward with subset231232-- turn(t) has infinite order for all but countably many t.233theorem turn.infinite_order234  shows Countable(turnOrders)235proof236  have function := turnOrderFamily.function237  have naturals := naturals.countable238  have members : ∀ n ∈ ℕ, Countable(turnOrderFamily(n))239    intros n hn240    have natural := omega.natural with hn241    have value := turnOrderFamily.value at n with *242    have finite := turnOrderSet.finite at n243    rw value244    exact Countable.of_finite with finite245  have unionCountable := Countable.indexed_union with function, naturals, members246  have bounded : turnOrders ⊆ ⋃(functionImage(turnOrderFamily, ℕ, 𝒫(ℝ)))247    intros t ht248    obtain ⟨real, n, hn, positive, power⟩ := turnOrders.membership.forward with ht249    have natural := omega.natural with hn250    have alternatives := natural.zero_or_successor at n with natural251    cases alternatives with zero | successor252    . exfalso253      rw zero at positive254      exact Less.irreflexive with positive255    . obtain ⟨k, naturalK, shape⟩ := successor256      have succForm : k + 1 = succ(k) := add.right_one at k257      have kIn : k ∈ ℕ by typecheck258      have value := turnOrderFamily.value at k with *259      have inSet : t ∈ turnOrderSet(k + 1)260        apply turnOrderSet.membership.backward261        refine ⟨real, ?_⟩262        rw [succForm, ← shape]263        exact power264      have familyMember : turnOrderFamily(k) ∈ functionImage(turnOrderFamily, ℕ, 𝒫(ℝ)) :=265        functionImage.value with function, kIn266      rw value at familyMember267      exact union.contains with familyMember, inSet268  exact Countable.subset with unionCountable, bounded269