Grace/Cumulus/Geometry/Absorption/Separation.g17

Open in Workbench Download source

Imports

Order · TurnRotation · Real.Uncountable

Declarations

Source

1-- Separating a countable set from itself by a turn about the z-axis: for2-- a countable D ⊆ S² off the z-axis, all but countably many t have3-- turn(t)ⁿ(D) ∩ D = ∅ for every n ≥ 1, because turn(t)ⁿ · d = e forces the4-- point of turn(t) to be an n-th root of a complex number determined by5-- d and e, and the reals are uncountable6-- 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.Separation12import Order13import TurnRotation14import Real.Uncountable1516-- The complex point (v(0), v(1)) of a vector of ℝ³.17def vectorPoint (v : Set) : Set := (v(0), v(1))1819theorem vectorPoint.graph (v : Set)20  shows vectorPoint(v) = (v(0), v(1))21proof22  simp [vectorPoint]2324theorem vectorPoint.complex (v : Set)25  requires vector : v : 3 → ℝ26  shows vectorPoint(v) ∈ complexCarrier27proof28  have zeroIn : 0 ∈ 3 by typecheck29  have oneIn : 1 ∈ 3 by typecheck30  have first := FunctionBetween.apply_closed with vector, zeroIn31  have second := FunctionBetween.apply_closed with vector, oneIn32  rw vectorPoint.graph33  exact complexCarrier.pair at v(0), v(1) with *3435-- The remaining entries of a plane turn.36theorem planeTurn.entry01 (a b : Real)37  shows planeTurn(a, b)[0, 1] = -b38proof39  rw [planeTurn.graph, matrix3of.entry01]40  rfl4142theorem planeTurn.entry02 (a b : Real)43  shows planeTurn(a, b)[0, 2] = (0:R)44proof45  rw [planeTurn.graph, matrix3of.entry02]46  rfl4748theorem planeTurn.entry11 (a b : Real)49  shows planeTurn(a, b)[1, 1] = a50proof51  rw [planeTurn.graph, matrix3of.entry11]52  rfl5354theorem planeTurn.entry12 (a b : Real)55  shows planeTurn(a, b)[1, 2] = (0:R)56proof57  rw [planeTurn.graph, matrix3of.entry12]58  rfl5960-- A plane turn acts on the complex point of a vector by multiplication.61theorem planeTurnOf.vector_point (z v : Set)62  requires member : z ∈ complexCarrier63  requires vector : v : 3 → ℝ64  shows vectorPoint(planeTurnOf(z) · v) = complexMul(z, vectorPoint(v))65proof66  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member67  have zeroIn : 0 ∈ 3 by typecheck68  have oneIn : 1 ∈ 3 by typecheck69  have twoIn : 2 ∈ 3 by typecheck70  have v0 := FunctionBetween.apply_closed with vector, zeroIn71  have v1 := FunctionBetween.apply_closed with vector, oneIn72  have v2 := FunctionBetween.apply_closed with vector, twoIn73  have matrix : planeTurn(a, b) : realRing ^ 3 × 3 := planeTurn.matrix with *74  have first := matrixVector.entry at planeTurn(a, b), v, 0 with *75  have second := matrixVector.entry at planeTurn(a, b), v, 1 with *76  rw [planeTurn.entry00, planeTurn.entry01, planeTurn.entry02] at first77  rw [planeTurn.entry10, planeTurn.entry11, planeTurn.entry12] at second78  have product := complexMul.pair at a, b, v(0), v(1) with *79  have horizontal : a * (v(0):R) + (-b) * (v(1):R) + (0:R) * (v(2):R) =80      a * (v(0):R) + -(b * (v(1):R))81    ring82  have vertical : b * (v(0):R) + a * (v(1):R) + (0:R) * (v(2):R) =83      a * (v(1):R) + b * (v(0):R)84    ring85  rw [shape, planeTurnOf.pair, vectorPoint.graph, vectorPoint.graph, product,86    first, second, horizontal, vertical]87  rfl8889-- The parameters t with turn(t)ⁿ · d = e.90def turnBad (n : Nat, d e : Set) : Set :=91  { t ∈ ℝ | matrixPow3(turn(t), n) · d = e }9293theorem turnBad.subset (n : Nat) (d e : Set)94  shows turnBad(n, d, e) ⊆ ℝ95proof96  intros t ht97  have data := turnBad.membership.forward with ht98  exact data.left99100section Complexes101notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)102103-- Solving W · p = r when p has the inverse q.104theorem complex.solve_left (W p q r : Set)105  requires wIn : W ∈ complexCarrier106  requires pIn : p ∈ complexCarrier107  requires qIn : q ∈ complexCarrier108  requires rIn : r ∈ complexCarrier109  requires inverse : complexMul(p, q) = complexOne110  requires equation : complexMul(W, p) = r111  shows W = complexMul(r, q)112proof113  have ring := complexes.comm_ring114  have unit : ℂ[W * (p * q)] = W115    rw inverse116    ring117  have regroup : ℂ[W * (p * q)] = ℂ[(W * p) * q]118    ring119  rw [← unit, regroup, equation]120  rfl121122end Complexes123124-- For n ≥ 1 and d off the z-axis, finitely many t have turn(t)ⁿ · d = e.125theorem turnBad.finite (k : Nat) (d e : Set)126  requires vectorD : d : 3 → ℝ127  requires vectorE : e : 3 → ℝ128  requires offAxis : vectorPoint(d) ≠ complexZero129  shows Finite(turnBad(k + 1, d, e))130proof131  have field := complexes.is_field132  have ring := complexes.comm_ring133  have ordinary := IsCommRing.ring with ring134  have monoid := IsRing.multiplicative with ordinary135  have pointD := vectorPoint.complex at d with vectorD136  have pointE := vectorPoint.complex at e with vectorE137  obtain ⟨commRing, nontrivial, inverses⟩ := field138  obtain ⟨q, inverse⟩ := inverses with vectorPoint(d), pointD, offAxis139  obtain ⟨pIn, qIn, leftLaw, rightLaw⟩ := inverse140  have targetIn := IsRing.mul_closed with ordinary, pointE, qIn141  have injective := turnPoint.injective142  have rootsFinite := complexPowerRoots.finite at complexMul(vectorPoint(e), q), k143    with targetIn144  have preimageFinite := Finite.preimage with injective, rootsFinite145  have bounded : turnBad(k + 1, d, e) ⊆ functionPreimage(turnPoint, ℝ, complexPowerRoots(complexMul(vectorPoint(e), q), k))146    intros t ht147    obtain ⟨real, moved⟩ := turnBad.membership.forward with ht148    have pointIn : turnPoint(t) ∈ complexCarrier :=149      FunctionBetween.apply_closed with turnPoint.function, real150    have powerIn := monoidPow.closed at complexCarrier, complexMul, complexOne,151      turnPoint(t), k + 1 with monoid, pointIn152    have shape := turn.planeTurnOf at t153    have matrixPower := planeTurnOf.pow at turnPoint(t), k + 1 with pointIn154    rw [shape, matrixPower] at moved155    have law := planeTurnOf.vector_point with powerIn, vectorD156    rw moved at law157    symm at law158    have rootEquation := complex.solve_left with powerIn, pIn, qIn, pointE, rightLaw, law159    have succForm : k + 1 = succ(k) := add.right_one at k160    rw succForm at rootEquation161    have inRoots := complexPowerRoots.contains with pointIn, targetIn, rootEquation162    exact functionPreimage.membership.backward with ⟨real, inRoots⟩163  exact Finite.subset with preimageFinite, bounded164165-- The family of these sets over the indices (n, (d, e)), and their union.166defgraph turnBadFamily (D : Set) (p ∈ ℕ × (D × D)) : 𝒫(ℝ) :=167  turnBad(succ(fst(p)), fst(snd(p)), snd(snd(p)))168proof169  obtain ⟨bound, n, hn, q, hq, shape⟩ := product.membership.forward with member170  have natural := omega.natural with hn171  have natSucc : Nat(succ(n)) by typecheck172  rw [shape, fst.pair, snd.pair]173  have subset := turnBad.subset at succ(n), fst(q), snd(q) with natSucc174  exact powerset.membership_iff.backward with subset175176def turnBadSet (D : Set) : Set :=177  ⋃(functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)))178179theorem turnBadSet.graph (D : Set)180  shows turnBadSet(D) = ⋃(functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)))181proof182  simp [turnBadSet]183184theorem turnBadSet.contains (D t : Set) (n : Nat) (d e : Set)185  requires hd : d ∈ D186  requires he : e ∈ D187  requires member : t ∈ turnBad(n + 1, d, e)188  shows t ∈ turnBadSet(D)189proof190  have function := turnBadFamily.function at D191  have pairIn := product.pair at d, e, D, D with *192  have nIn : n ∈ ℕ by typecheck193  have indexIn := product.pair at n, (d, e), ℕ, D × D with *194  have value := turnBadFamily.value at D, (n, (d, e)) with *195  have succForm : n + 1 = succ(n) := add.right_one at n196  rw [fst.pair, snd.pair, fst.pair, snd.pair] at value197  have familyMember : turnBadFamily(D)((n, (d, e))) ∈ functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)) :=198    functionImage.value with function, indexIn199  rw value at familyMember200  rw succForm at member201  rw turnBadSet.graph202  exact union.contains with familyMember, member203204theorem turnBadSet.countable (D : Set)205  requires countable : Countable(D)206  requires subset : D ⊆ S²207  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero208  shows Countable(turnBadSet(D))209proof210  have function := turnBadFamily.function at D211  have pairs := Countable.product with countable, countable212  have index := Countable.product with naturals.countable, pairs213  have members : ∀ p ∈ ℕ × (D × D), Countable(turnBadFamily(D)(p))214    intros p hp215    obtain ⟨bound, n, hn, q, hq, shape⟩ := product.membership.forward with hp216    obtain ⟨boundQ, d, hd, e, he, shapeQ⟩ := product.membership.forward with hq217    have natural := omega.natural with hn218    have value := turnBadFamily.value at D, p with *219    rw [value, shape, shapeQ, fst.pair, snd.pair, fst.pair, snd.pair]220    have vectorD := S².function with (subset with d, hd)221    have vectorE := S².function with (subset with e, he)222    have away := offAxis with d, hd223    have finite := turnBad.finite at n, d, e with vectorD, vectorE, away224    have succForm : n + 1 = succ(n) := add.right_one at n225    rw succForm at finite226    exact Countable.of_finite with finite227  rw turnBadSet.graph228  exact Countable.indexed_union with function, index, members229230-- Some real parameter lies outside the countable bad set.231theorem turnBadSet.exists_outside (D : Set)232  requires countable : Countable(D)233  requires subset : D ⊆ S²234  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero235  shows ∃ t ∈ ℝ, ¬(t ∈ turnBadSet(D))236proof237  have badCountable := turnBadSet.countable with countable, subset, offAxis238  have uncountable := reals.uncountable239  unfold Uncountable at uncountable240  by_contra241  rename this => none242  have cover : ℝ ⊆ turnBadSet(D)243    intros t ht244    by_contra245    apply none246    exact ⟨t, ht, this⟩247  have realsCountable := Countable.subset with badCountable, cover248  exact uncountable with realsCountable249