Grace/Cumulus/Complex/PowerArithmetic.g17

Open in Workbench Download source

Imports

SquareDirections · Nat.Parity

Declarations

• complexImaginaryUnit def
• complexImaginaryUnit.member theorem derivation
• natural.double_successor theorem derivation
• complexImaginaryUnit.square theorem derivation
• complexPower.one theorem derivation
• complexPower.square theorem derivation
• complexPower.negative_one_odd theorem derivation
• complexImaginaryUnit.twice theorem derivation
• complexImaginaryUnit.negative_twice theorem derivation
• complexPower.imaginary_odd theorem derivation

Source

1-- Power identities used by parity-based direction separation.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Complex.PowerArithmetic8import SquareDirections9import Nat.Parity1011def complexImaginaryUnit : Set := (realZero, realOne)1213theorem complexImaginaryUnit.member14  shows complexImaginaryUnit ∈ complexCarrier15proof16  unfold complexImaginaryUnit17  exact complexCarrier.pair with *1819theorem natural.double_successor (n : Nat)20  shows add(succ(n), succ(n)) = succ(succ(add(n, n)))21proof22  ring2324section Complexes25notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)2627theorem complexImaginaryUnit.square28  shows ℂ[complexImaginaryUnit * complexImaginaryUnit] = ℂ[-1]29proof30  unfold complexImaginaryUnit31  unfold complexOne32  simp [complexMul.pair, complexNeg.pair, realMulValue.zero_left, realMulValue.zero_right, realMulValue.one_left, realAddValue.zero_left, realAddValue.zero_right, realNegValue.zero]3334theorem complexPower.one (n : Nat)35  shows (ℂ[1]) ^ n = ℂ[1]36proof37  induction n38  | zero =>39    rw monoidPow.zero40    rfl41  | succ(k) using ih =>42    rw [monoidPow.succ, ih]43    have ring := complexes.comm_ring44    ring4546theorem complexPower.square (z : Set) (n : Nat)47  requires member : z ∈ ℂ48  shows z ^ (Grace.Core.Nat.Rec.add(n, n)) = (ℂ[z * z]) ^ n49proof50  induction n51  | zero =>52    rw [Grace.Core.Nat.Rec.add, monoidPow.zero, monoidPow.zero]53    rfl54  | succ(k) using ih =>55    have ring := complexes.comm_ring56    have ordinary := IsCommRing.ring with ring57    have monoid := IsRing.multiplicative with ordinary58    have square := IsRing.mul_closed with ordinary, member, member59    have power := monoidPow.closed at ℂ, complexMul, complexOne, ℂ[z * z], k with *60    rw [natural.double_successor, monoidPow.succ, monoidPow.succ, ih, monoidPow.succ]61    ring6263theorem complexPower.negative_one_odd (n : Nat)64  shows (ℂ[-1]) ^ (succ(Grace.Core.Nat.Rec.add(n, n))) = ℂ[-1]65proof66  induction n67  | zero =>68    rw [Grace.Core.Nat.Rec.add, monoidPow.succ, monoidPow.zero]69    have ring := complexes.comm_ring70    ring71  | succ(k) using ih =>72    rw [natural.double_successor, monoidPow.succ, monoidPow.succ, ih]73    have ring := complexes.comm_ring74    ring7576theorem complexImaginaryUnit.twice (z : Set)77  requires member : z ∈ ℂ78  shows ℂ[complexImaginaryUnit * (complexImaginaryUnit * z)] = ℂ[-z]79proof80  have ring := complexes.comm_ring81  have iIn := complexImaginaryUnit.member82  have regroup : ℂ[complexImaginaryUnit * (complexImaginaryUnit * z)] = ℂ[(complexImaginaryUnit * complexImaginaryUnit) * z]83    ring84  rw [regroup, complexImaginaryUnit.square]85  ring8687theorem complexImaginaryUnit.negative_twice (z : Set)88  requires member : z ∈ ℂ89  shows ℂ[(-complexImaginaryUnit) * ((-complexImaginaryUnit) * z)] = ℂ[-z]90proof91  have ring := complexes.comm_ring92  have iIn := complexImaginaryUnit.member93  have regroup : ℂ[(-complexImaginaryUnit) * ((-complexImaginaryUnit) * z)] = ℂ[complexImaginaryUnit * (complexImaginaryUnit * z)]94    ring95  rw regroup96  exact complexImaginaryUnit.twice with *9798theorem complexPower.imaginary_odd (n : Nat)99  shows (complexImaginaryUnit ^ (succ(Grace.Core.Nat.Rec.add(n, n))) = complexImaginaryUnit ∧ (ℂ[-complexImaginaryUnit]) ^ (succ(Grace.Core.Nat.Rec.add(n, n))) = ℂ[-complexImaginaryUnit]) ∨100    (complexImaginaryUnit ^ (succ(Grace.Core.Nat.Rec.add(n, n))) = ℂ[-complexImaginaryUnit] ∧ (ℂ[-complexImaginaryUnit]) ^ (succ(Grace.Core.Nat.Rec.add(n, n))) = complexImaginaryUnit)101proof102  induction n103  | zero =>104    left105    constructor106    . rw [Grace.Core.Nat.Rec.add, monoidPow.succ, monoidPow.zero]107      have ring := complexes.comm_ring108      have iIn := complexImaginaryUnit.member109      ring110    . rw [Grace.Core.Nat.Rec.add, monoidPow.succ, monoidPow.zero]111      have ring := complexes.comm_ring112      have iIn := complexImaginaryUnit.member113      ring114  | succ(k) using ih =>115    have ring := complexes.comm_ring116    have ordinary := IsCommRing.ring with ring117    have iIn := complexImaginaryUnit.member118    have niIn := IsRing.neg_closed with ordinary, iIn119    cases ih with first | second120    . right121      constructor122      . rw [natural.double_successor, monoidPow.succ, monoidPow.succ, first.left]123        exact complexImaginaryUnit.twice with *124      . rw [natural.double_successor, monoidPow.succ, monoidPow.succ, first.right, complexImaginaryUnit.negative_twice]125        ring126    . left127      constructor128      . rw [natural.double_successor, monoidPow.succ, monoidPow.succ, second.left, complexImaginaryUnit.twice]129        ring130      . rw [natural.double_successor, monoidPow.succ, monoidPow.succ, second.right]131        exact complexImaginaryUnit.negative_twice with *132133end Complexes134