SURREALS: Surreal Numbers: A Study of Square Roots

:: Surreal Numbers: A Study of Square Roots
:: by Karol P\kak
::
:: Received April 10, 2025
:: Copyright (c) 2025 Association of Mizar Users

definition

let x be object ;

func NonNegativePart x -> pair set means :Def1: :: SURREALS:def 1
for o being object holds
( ( o in L_ it implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ it ) & ( o in R_ it implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ it ) );

proof end;

proof end;

end;

:: deftheorem Def1 defines NonNegativePart SURREALS:def 1 :

registration

let x be object ;

cluster (NonNegativePart x) `1 -> surreal-membered for set ;

proof end;

cluster (NonNegativePart x) `2 -> surreal-membered for set ;

proof end;

end;

theorem Th1: :: SURREALS:1

for o being object holds
( L_ (NonNegativePart o) c= L_ o & R_ (NonNegativePart o) c= R_ o )

proof end;

registration

let x be Surreal;

cluster NonNegativePart x -> pair surreal ;

proof end;

end;

theorem Th2: :: SURREALS:2

for o being object
for x being Surreal holds
( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) )

proof end;

theorem Th3: :: SURREALS:3

for x being Surreal holds born (NonNegativePart x) c= born x

proof end;

theorem Th4: :: SURREALS:4

for x being Surreal st 0_No <= x holds
0_No <= NonNegativePart x

proof end;

theorem :: SURREALS:5

for x being Surreal st 0_No <= x holds
NonNegativePart x == x

proof end;

definition

let lamb be object ;
let X, Y be set ;

func sqrt (lamb,X,Y) -> surreal-membered set means :Def2: :: SURREALS:def 2
for o being object holds
( o in it iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) );

proof end;

proof end;

end;

:: deftheorem Def2 defines sqrt SURREALS:def 2 :

definition

let x0 be pair object ;
let x be object ;

func transitions_of (x0,x) -> Function means :Def3: :: SURREALS:def 3
( dom it = NAT & it . 0 = x0 & ( for n being Nat holds
( it . n is pair & (it . (n + 1)) `1 = (L_ (it . n)) \/ (sqrt (x,(L_ (it . n)),(R_ (it . n)))) & (it . (n + 1)) `2 = ((R_ (it . n)) \/ (sqrt (x,(L_ (it . n)),(L_ (it . n))))) \/ (sqrt (x,(R_ (it . n)),(R_ (it . n)))) ) ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines transitions_of SURREALS:def 3 :

definition

let x0 be pair object ;
let x be object ;

func sqrtL (x0,x) -> Function means :Def4: :: SURREALS:def 4
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x0,x)) . k) `1 ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines sqrtL SURREALS:def 4 :

definition

let x0 be pair object ;
let x be object ;

func sqrtR (x0,x) -> Function means :Def5: :: SURREALS:def 5
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x0,x)) . k) `2 ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines sqrtR SURREALS:def 5 :

theorem Th6: :: SURREALS:6

for o being object
for p being pair object holds
( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p )

proof end;

theorem Th7: :: SURREALS:7

for n, m being Nat
for o being object
for p being pair object st n <= m holds
( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m )

proof end;

theorem Th8: :: SURREALS:8

for n being Nat
for o being object
for p being pair object holds
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )

proof end;

theorem Th9: :: SURREALS:9

for n being Nat
for o being object
for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( (sqrtL (p,o)) . n is surreal-membered & (sqrtR (p,o)) . n is surreal-membered )

proof end;

theorem Th10: :: SURREALS:10

for o being object
for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( Union (sqrtL (p,o)) is surreal-membered & Union (sqrtR (p,o)) is surreal-membered )

proof end;

theorem Th11: :: SURREALS:11

for o being object
for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
sqrt (o,X1,Y1) c= sqrt (o,X2,Y2)

proof end;

theorem :: SURREALS:12

for o being object
for p being pair object holds Union (sqrtL (p,o)) = (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))

proof end;

theorem :: SURREALS:13

for o being object
for p being pair object holds Union (sqrtR (p,o)) = ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))

proof end;

definition

let A be Ordinal;

func No_sqrt_op A -> ManySortedSet of Day A means :Def6: :: SURREALS:def 6
ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def6 defines No_sqrt_op SURREALS:def 6 :

theorem Th14: :: SURREALS:14

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_sqrt_op A = S . A

proof end;

definition

let o be object ;
assume A1: o is Surreal ;

func sqrt o -> set means :Def7: :: SURREALS:def 7
for x being Surreal st x = o holds
it = (No_sqrt_op (born x)) . x;

proof end;

proof end;

end;

:: deftheorem Def7 defines sqrt SURREALS:def 7 :

definition

let x be Surreal;

:: original: sqrt
redefine func sqrt x -> set equals :: SURREALS:def 8
(No_sqrt_op (born x)) . x;

coherence ;
compatibility by Def7;

end;

:: deftheorem defines sqrt SURREALS:def 8 :

definition

let x be object ;

func sqrt_0 x -> pair set means :Def9: :: SURREALS:def 9
for o being object holds
( ( o in L_ it implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ it ) & ( o in R_ it implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ it ) );

proof end;

proof end;

end;

:: deftheorem Def9 defines sqrt_0 SURREALS:def 9 :

theorem Th15: :: SURREALS:15

for x being Surreal holds sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))]

proof end;

theorem :: SURREALS:16

for o being object
for p being pair object st Union (sqrtL (p,o)) = {} holds
L_ p = {}

proof end;

theorem Th17: :: SURREALS:17

for x1, x2, y, z being Surreal st not x2 == 0_No & y = x1 * (x2 ") holds
( ( y * y < z implies x1 * x1 < z * (x2 * x2) ) & ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) )

proof end;

Lm1: for x, y, z being Surreal holds z * ((x + y) * (x + y)) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x)))

proof end;

Lm2: for x, y, z being Surreal holds ((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == (x - (y * y)) * (x - (z * z))

proof end;

theorem Th18: :: SURREALS:18

for o being object
for x being Surreal st x <= 0_No holds
Union (sqrtL ((sqrt_0 x),o)) = {}

proof end;

theorem Th19: :: SURREALS:19

for x, y being Surreal st 0_No <= x holds
( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal )

proof end;

theorem Th20: :: SURREALS:20

for x being Surreal st x <= 0_No holds
sqrt x is surreal

proof end;

registration

let x be Surreal;

cluster sqrt x -> surreal ;

proof end;

end;

registration

let x be Surreal;

cluster sqrt_0 x -> pair surreal ;

proof end;

end;

theorem Th21: :: SURREALS:21

for x being Surreal st 0_No <= x holds
( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by Th19;

theorem :: SURREALS:22

for x being Surreal st 0_No == x holds
sqrt x == 0_No by Th19;

theorem :: SURREALS:23

for x, y being Surreal st 0_No <= x holds
( ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) ) by Th19;

theorem :: SURREALS:24

for x being Surreal st x < 0_No & ( for y being Surreal st y in R_ x holds
y < 0_No ) holds
sqrt x = 0_No

proof end;

theorem Th25: :: SURREALS:25

for x being Surreal st ( for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ) holds
sqrt x = sqrt_0 x

proof end;

registration

reduce sqrt 0_No to 0_No ;

proof end;

reduce sqrt 1_No to 1_No ;

proof end;

reduce sqrt (- 1_No) to - 1_No;

proof end;

end;

theorem :: SURREALS:26

for x, y being Surreal st 0_No <= x & x <= y holds
sqrt x <= sqrt y

proof end;

theorem Th27: :: SURREALS:27

for x, y being Surreal st 0_No <= x & x < y holds
sqrt x < sqrt y

proof end;

theorem Th28: :: SURREALS:28

for x, y being Surreal st 0_No <= x & x == y * y & not y == sqrt x holds
y == - (sqrt x)

proof end;

registration

let x be positive Surreal;

cluster sqrt x -> positive ;

proof end;

end;

theorem Th29: :: SURREALS:29

for x being Surreal st 0_No <= x holds
sqrt (x * x) == x

proof end;

theorem :: SURREALS:30

for x being Surreal st 0_No < x holds
(sqrt x) " == sqrt (x ")

proof end;

theorem Th31: :: SURREALS:31

for x being Surreal st 0_No < x holds
ex y being Surreal st
( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )

proof end;

theorem :: SURREALS:32

ex x, y being Surreal st
( x == y & y < 0_No & sqrt x < sqrt y )

proof end;