Emmy, the Algebra System: Differential Geometry Chapter Eleven
Functional Differential Geometry: Chapter 11
11 Special Relativity
Einsten noticed that Maxwell’s equations were inconsistent with Galilean relativity.
Implementation
(define (make-four-tuple ct space)
(up ct (ref space 0) (ref space 1) (ref space 2)))(define (four-tuple->ct v) (ref v 0))(define (four-tuple->space v)
(up (ref v 1) (ref v 2) (ref v 3)))(define (proper-space-interval four-tuple)
(sqrt (- (square (four-tuple->space four-tuple))
(square (four-tuple->ct four-tuple)))))(define (proper-time-interval four-tuple)
(sqrt (- (square (four-tuple->ct four-tuple))
(square (four-tuple->space four-tuple)))))(define ((general-boost beta) xi-p)
(let ((gamma (expt (- 1 (square beta)) (/ -1 2))))
(let ((factor (/ (- gamma 1) (square beta))))
(let ((xi-p-time (four-tuple->ct xi-p))
(xi-p-space (four-tuple->space xi-p)))
(let ((beta-dot-xi-p (dot-product beta xi-p-space)))
(make-four-tuple
(* gamma (+ xi-p-time beta-dot-xi-p))
(+ (* gamma beta xi-p-time)
xi-p-space
(* factor beta beta-dot-xi-p))))))))(print-expression
(- (proper-space-interval
((general-boost (up 'vx 'vy 'vz))
(make-four-tuple 'ct (up 'x 'y 'z))))
(proper-space-interval
(make-four-tuple 'ct (up 'x 'y 'z)))))
NoteOUT
2026-04-03T18:56:14.108Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ct 2) (expt vx 4)) (* 2 (expt ct 2) (expt vx 2) (expt vy 2)) (* 2 (expt ct 2) (expt vx 2) (expt vz 2)) (* (expt ct 2) (expt vy 4)) (* 2 (expt ct 2) (expt vy 2) (expt vz 2)) (* (expt ct 2) (expt vz 4)) (* -1 (expt vx 4) (expt x 2)) (* -2 (expt vx 3) vy x y) (* -2 (expt vx 3) vz x z) (* -1 (expt vx 2) (expt vy 2) (expt x 2)) (* -1 (expt vx 2) (expt vy 2) (expt y 2)) (* -2 (expt vx 2) vy vz y z) (* -1 (expt vx 2) (expt vz 2) (expt x 2)) (* -1 (expt vx 2) (expt vz 2) (expt z 2)) (* (expt vx 2) (expt y 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* (expt vx 2) (expt z 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -2 vx (expt vy 3) x y) (* -2 vx (expt vy 2) vz x z) (* -2 vx vy (expt vz 2) x y) (* -2 vx vy x y (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -2 vx (expt vz 3) x z) (* -2 vx vz x z (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -1 (expt vy 4) (expt y 2)) (* -2 (expt vy 3) vz y z) (* -1 (expt vy 2) (expt vz 2) (expt y 2)) (* -1 (expt vy 2) (expt vz 2) (expt z 2)) (* (expt vy 2) (expt x 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* (expt vy 2) (expt z 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -2 vy (expt vz 3) y z) (* -2 vy vz y z (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -1 (expt vz 4) (expt z 2)) (* (expt vz 2) (expt x 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* (expt vz 2) (expt y 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* -1 (expt ct 2) (expt vx 2)) (* -1 (expt ct 2) (expt vy 2)) (* -1 (expt ct 2) (expt vz 2)) (* (expt vx 2) (expt x 2)) (* 2 vx vy x y) (* 2 vx vz x z) (* (expt vy 2) (expt y 2)) (* 2 vy vz y z) (* (expt vz 2) (expt z 2)))) in e3
2026-04-03T18:56:14.111Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt vx 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* (expt vy 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)) (* (expt vz 2) (expt (expt (+ (* -1 (expt vx 2)) (* -1 (expt vy 2)) (* -1 (expt vz 2)) 1) 1/2) 2)))) in e3
2026-04-03T18:56:14.140Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* -1 (expt ct 2)) (expt x 2) (expt y 2) (expt z 2))) in c1
2026-04-03T18:56:14.141Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* -1 (expt vx 4)) (* -2 (expt vx 2) (expt vy 2)) (* -2 (expt vx 2) (expt vz 2)) (* -1 (expt vy 4)) (* -2 (expt vy 2) (expt vz 2)) (* -1 (expt vz 4)) (expt vx 2) (expt vy 2) (expt vz 2))) in c1
0(define ((general-boost2 direction v:c) four-tuple-prime)
(let ((delta-ct-prime (four-tuple->ct four-tuple-prime))
(delta-x-prime (four-tuple->space four-tuple-prime)))
(let ((betasq (square v:c)))
(let ((bx (dot-product direction delta-x-prime))
(gamma (/ 1 (sqrt (- 1 betasq)))))
(let ((alpha (- gamma 1)))
(let ((delta-ct
(* gamma (+ delta-ct-prime (* bx v:c))))
(delta-x
(+ (* gamma v:c direction delta-ct-prime)
delta-x-prime
(* alpha direction bx))))
(make-four-tuple delta-ct delta-x)))))))Rotations
(define ((extended-rotation R) xi)
(make-four-tuple
(four-tuple->ct xi)
(R (four-tuple->space xi))))the following calculation does not seem to stop.
(comment
(print-expression
(let-scheme ((beta (up 'bx 'by 'bz))
(xi (make-four-tuple 'ct (up 'x 'y 'z)))
(R (compose
(rotate-x 'theta)
(rotate-y 'phi)
(rotate-z 'psi)))
(R-inverse (compose
(rotate-z (- 'psi))
(rotate-y (- 'phi))
(rotate-x (- 'theta)))))
(- ((general-boost beta) xi)
((compose (extended-rotation R-inverse)
(general-boost (R beta))
(extended-rotation R))
xi))))
:end-comment)Special Relativity Frames
(define ((coordinates->event ancestor-frame this-frame
boost-direction v:c origin)
coords)
((point ancestor-frame)
(make-SR-coordinates ancestor-frame
(+ ((general-boost2 boost-direction v:c) coords)
origin))))(define ((event->coordinates ancestor-frame this-frame
boost-direction v:c origin)
event)
(make-SR-coordinates this-frame
((general-boost2 (- boost-direction) v:c)
(- ((chart ancestor-frame) event) origin))))NOTE: this seems to be the wrong definition, using the default environment
(comment
(define make-SR-frame
(frame-maker coordinates->event event->coordinates)))Velocity Addition Formula
(define home (base-frame-maker 'home 'home))(define A
(e/make-SR-frame 'A home
(up 1 0 0)
'va:c
(make-SR-coordinates home (up 0 0 0 0))))(define B
(e/make-SR-frame 'B A
(up 1 0 0)
'vb:c
(make-SR-coordinates A (up 0 0 0 0))))(print-expression
(let-scheme ((B-origin-home-coords
((chart home)
((point B)
(make-SR-coordinates B (up 'ct 0 0 0))))))
(/ (ref B-origin-home-coords 1)
(ref B-origin-home-coords 0))))(/ (+ va:c vb:c) (+ (* va:c vb:c) 1))(define (add-v:cs va:c vb:c)
(/ (+ va:c vb:c)
(+ 1 (* va:c vb:c))))Twin Paradox
(define start-event
((point home)
(make-SR-coordinates home (up 0 0 0 0))))(define outgoing
(e/make-SR-frame 'outgoing ; for debugging
home ; base frame
(up 1 0 0) ; x direction
(/ 24 25) ; velocity as fraction of c
((chart home)
start-event)))(define traveller-at-turning-point-event
((point home)
(e/make-SR-coordinates home
(up (* 'c 25) (* 25 (/ 24 25) 'c) 0 0))))(print-expression
(- ((chart outgoing) traveller-at-turning-point-event)
((chart outgoing) start-event)))(up (* 7N c) 0 0 0)(print-expression
(- ((chart home) traveller-at-turning-point-event)
((chart home) start-event)))(up (* 25 c) (* 24N c) 0 0)(print-expression
(proper-time-interval
(- ((chart outgoing) traveller-at-turning-point-event)
((chart outgoing) start-event))))
NoteOUT
2026-04-03T18:56:14.185Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? 49N) in e1
2026-04-03T18:56:14.186Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (expt c 2)) in e1
2026-04-03T18:56:14.187Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (= (sqrt (expt c 2)) (expt c 1)) in simsqrt1
(* 7N c)(print-expression
(proper-time-interval
(- ((chart home) traveller-at-turning-point-event)
((chart home) start-event))))(* 7N c)(define halfway-at-home-event
((point home)
(e/make-SR-coordinates home (up (* 'c 25) 0 0 0))))(print-expression
(proper-time-interval
(- ((chart home) halfway-at-home-event)
((chart home) start-event))))
NoteOUT
2026-04-03T18:56:14.195Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? 625) in e1
2026-04-03T18:56:14.196Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (expt c 2)) in e1
(* 25 c)(print-expression
(proper-time-interval
(- ((chart outgoing) halfway-at-home-event)
((chart outgoing) start-event))))(* 25 c)(define home-at-outgoing-turning-point-event
((point outgoing)
(e/make-SR-coordinates
outgoing
(up (* 7 'c) (* 7 (/ -24 25) 'c) 0 0))))(print-expression
(proper-time-interval
(- ((chart home) home-at-outgoing-turning-point-event)
((chart home) start-event))))
NoteOUT
2026-04-03T18:56:14.200Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? 2401/625) in e1
2026-04-03T18:56:14.200Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (expt c 2)) in e1
(* 49/25 c)(define incoming
(e/make-SR-frame 'incoming home
(up -1 0 0) (/ 24 25)
((chart home)
traveller-at-turning-point-event)))(define end-event
((point home)
(e/make-SR-coordinates home (up (* 'c 50) 0 0 0))))(print-expression
(- ((chart incoming) end-event)
(make-SR-coordinates incoming
(up (* 'c 7) 0 0 0))))(up 0 0 0 0)(print-expression
(- ((chart home) end-event)
((chart home)
((point incoming)
(make-SR-coordinates incoming
(up (* 'c 7) 0 0 0))))))(up 0 0 0 0)(print-expression
(+ (proper-time-interval
(- ((chart outgoing) traveller-at-turning-point-event)
((chart outgoing) start-event)))
(proper-time-interval
(- ((chart incoming) end-event)
((chart incoming) traveller-at-turning-point-event)))))(* 14N c)(print-expression
(proper-time-interval
(- ((chart home) end-event)
((chart home) start-event))))
NoteOUT
2026-04-03T18:56:14.209Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? 2500) in e1
2026-04-03T18:56:14.209Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (expt c 2)) in e1
(* 50 c)(define home-at-incoming-turning-point-event
((point incoming)
(e/make-SR-coordinates incoming
(up 0 (* 7 (/ -24 25) 'c) 0 0))))(print-expression
(proper-time-interval
(- ((chart home) end-event)
((chart home) home-at-incoming-turning-point-event))))(* 49/25 c)(repl/scittle-sidebar)