Review Derivation: Physics Derivation Graph

Return to navigation page or list derivations

Review Lorentz transformation

abstract: source: \cite{1999_Tipler_Llewellyn}, page 21; see also https://en.wikipedia.org/wiki/Lorentz_transformation and https://en.wikipedia.org/wiki/Derivations_of_the_Lorentz_transformations
reference:

step	inference rule	input	feed	output	step validity (as per SymPy)
Note about step 1: equation 1-13 on page 21 in \cite{1999_Tipler_Llewellyn}
1	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			4662369843 $x' = \gamma (x - v t)$	no validation is available for declarations
Note about step 2: equation 1-14 on page 21 in \cite{1999_Tipler_Llewellyn}
2	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			2983053062 $x = \gamma (x' + v t')$	no validation is available for declarations
Note about step 3: solve output expr for $t$'
3	0000111556: substitute LHS of expr 1 into expr 2 number of inputs: 2; feeds: 0; outputs: 1 Substitute LHS of Eq.~\ref{eq:#1} into Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2983053062 $x = \gamma (x' + v t')$ 4662369843 $x' = \gamma (x - v t)$		3426941928 $x = \gamma ( \gamma (x - v t) + v t' )$	LHS diff is -pdg0004037 + pdg0005456 RHS diff is pdg0001790(-pdg0001357pdg0001467 - pdg0001357pdg0004989 + pdg0001464 + pdg0001790(pdg0001357*pdg0001467 - pdg0004037))
4	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	3426941928 $x = \gamma ( \gamma (x - v t) + v t' )$		2096918413 $x = \gamma ( \gamma x - \gamma v t + v t' )$	LHS diff is 0 RHS diff is pdg0001790(pdg0001357pdg0004989 - pdg0001790(pdg0001357pdg0001467 - pdg0004037)) - pdg0001790(-pdg0001357pdg0001467pdg0001790 + pdg0001357pdg0004989 + pdg0001790pdg0004037)
5	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	2096918413 $x = \gamma ( \gamma x - \gamma v t + v t' )$		7741202861 $x = \gamma^2 x - \gamma^2 v t + \gamma v t'$	LHS diff is 0 RHS diff is pdg0001357pdg0001467pdg0001790*2 - pdg0001357pdg0001790pdg0004989 - pdg00017902pdg0004037 + pdg0001790(-pdg0001357pdg0001467pdg0001790 + pdg0001357pdg0004989 + pdg0001790pdg0004037)
6	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	7741202861 $x = \gamma^2 x - \gamma^2 v t + \gamma v t'$	7337056406 $\gamma^2 x$	4139999399 $x - \gamma^2 x = - \gamma^2 v t + \gamma v t'$	valid
7	0000111613: factor out X from LHS number of inputs: 1; feeds: 1; outputs: 1 Factor $#1$ from the LHS of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	4139999399 $x - \gamma^2 x = - \gamma^2 v t + \gamma v t'$	3495403335 $x$	9031609275 $x (1 - \gamma^2 ) = - \gamma^2 v t + \gamma v t'$	Not evaluated due to missing term in SymPy
8	0000111530: add X to both sides number of inputs: 1; feeds: 1; outputs: 1 Add $#1$ to both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	9031609275 $x (1 - \gamma^2 ) = - \gamma^2 v t + \gamma v t'$	8014566709 $\gamma^2 v t$	9409776983 $x (1 - \gamma^2 ) + \gamma^2 v t = \gamma v t'$	Not evaluated due to missing term in SymPy
9	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	9409776983 $x (1 - \gamma^2 ) + \gamma^2 v t = \gamma v t'$	2226340358 $\gamma v$	1974334644 $\frac{x (1 - \gamma^2 )}{\gamma v} + \frac{\gamma^2 v t}{\gamma v} = t'$	Not evaluated due to missing term in SymPy
10	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	1974334644 $\frac{x (1 - \gamma^2 )}{\gamma v} + \frac{\gamma^2 v t}{\gamma v} = t'$		8730201316 $\frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t = t'$	Not evaluated due to missing term in SymPy
11	0000111268: swap LHS with RHS number of inputs: 1; feeds: 0; outputs: 1 Swap LHS of Eq.~\ref{eq:#1} with RHS; yields Eq.~\ref{eq:#2}.	8730201316 $\frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t = t'$		5148266645 $t' = \frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t$	Not evaluated due to missing term in SymPy
12	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			4287102261 $x^2 + y^2 + z^2 = c^2 t^2$	no validation is available for declarations
13	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			1201689765 $x'^2 + y'^2 + z'^2 = c^2 t'^2$	no validation is available for declarations
14	0000111104: declare assumption number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an assumption.			7057864873 $y' = y$	no validation is available for declarations
15	0000111104: declare assumption number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an assumption.			8515803375 $z' = z$	no validation is available for declarations
16	0000111797: substitute LHS of four expressions into expression number of inputs: 5; feeds: 0; outputs: 1 Substitute LHS of Eq.~\ref{eq:#1} and LHS of Eq.~\ref{eq:#2} and LHS of Eq.~\ref{eq:#3} and LHS of Eq.~\ref{eq:#4} into Eq.~\ref{eq:#5}; yields Eq.~\ref{eq:#6}.	1201689765 $x'^2 + y'^2 + z'^2 = c^2 t'^2$ 4662369843 $x' = \gamma (x - v t)$ 5148266645 $t' = \frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t$ 7057864873 $y' = y$ 8515803375 $z' = z$		9805063945 $\gamma^2 (x - v t)^2 + y^2 + z^2 = c^2 \gamma^2 \left( t + \frac{ 1 - \gamma^2 }{ \gamma^2 } \frac{x}{v} \right)^2$	recognized infrule but not yet supported
Note about step 17: expanded the squared terms
17	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	9805063945 $\gamma^2 (x - v t)^2 + y^2 + z^2 = c^2 \gamma^2 \left( t + \frac{ 1 - \gamma^2 }{ \gamma^2 } \frac{x}{v} \right)^2$		1935543849 $\gamma^2 x^2 - \gamma^2 2 x v t + \gamma^2 v^2 t^2 + y^2 + z^2 = c^2 \gamma^2 \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x^2}{\gamma^2} + c^2 \gamma^2 2 t \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x}{\gamma} + c^2 \gamma^2 t^2$	LHS diff is 0 RHS diff is pdg0004567*2(-pdg0001357*2pdg0001467*2pdg0001790*4 + 2pdg0001357*2pdg0001467pdg0001790pdg0004037(pdg00017902 - 1) + pdg00013572pdg0004037*2(pdg0001790*2 - 1) + (pdg0001357pdg0001467pdg00017902 - pdg0004037(pdg00017902 - 1))2)/(pdg0001357*2pdg0001790**2)
Note about step 18: grouped by terms for $x^2$, $xt$, and $t^2$
18	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	1935543849 $\gamma^2 x^2 - \gamma^2 2 x v t + \gamma^2 v^2 t^2 + y^2 + z^2 = c^2 \gamma^2 \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x^2}{\gamma^2} + c^2 \gamma^2 2 t \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x}{\gamma} + c^2 \gamma^2 t^2$		1586866563 $\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)$	LHS diff is pdg0001357*2pdg0001467*2pdg0001790*2 - 2pdg0001467pdg00017902pdg0004037pdg00045672/pdg0001357 + 2pdg0001467pdg0004037pdg00045672/pdg0001357 + pdg00040372pdg00045672(pdg00017902 - 1)2/(pdg0001357*2pdg00017902) RHS diff is (pdg00013572pdg00014672pdg0001790*4 - 2pdg0001467pdg0001790pdg0004037pdg00045672(pdg00017902 - 1) - pdg00040372pdg00045672(pdg00017902 - 1))/pdg00017902
Note about step 19: based on the comparison of the $x^2$ terms
19	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 $\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)$ 4287102261 $x^2 + y^2 + z^2 = c^2 t^2$		3182633789 $\gamma^2 - c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1$	recognized infrule but not yet supported
Note about step 20: based on the comparison of the $t^2$ terms
20	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 $\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)$ 4287102261 $x^2 + y^2 + z^2 = c^2 t^2$		1916173354 $-\gamma^2 v^2 + c^2 \gamma^2 = c^2$	recognized infrule but not yet supported
Note about step 21: based on the comparison of the $(x t)$ terms
21	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 $\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)$ 4287102261 $x^2 + y^2 + z^2 = c^2 t^2$		2076171250 $-\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} = 0$	recognized infrule but not yet supported
Note about step 22: solve for $\gamma$
22	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	3182633789 $\gamma^2 - c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1$	5284610349 $\gamma^2$	2417941373 $- c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1 - \gamma^2$	valid
23	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	2417941373 $- c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1 - \gamma^2$	5787469164 $1 - \gamma^2$	1639827492 $- c^2 \frac{(1-\gamma^2)}{v^2 \gamma^2} = 1$	valid
24	0000111182: multiply both sides by number of inputs: 1; feeds: 1; outputs: 1 Multiply both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	1639827492 $- c^2 \frac{(1-\gamma^2)}{v^2 \gamma^2} = 1$	5669500954 $v^2 \gamma^2$	5763749235 $-c^2 + c^2 \gamma^2 = v^2 \gamma^2$	valid
25	0000111530: add X to both sides number of inputs: 1; feeds: 1; outputs: 1 Add $#1$ to both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	5763749235 $-c^2 + c^2 \gamma^2 = v^2 \gamma^2$	6408214498 $c^2$	2999795755 $c^2 \gamma^2 = v^2 \gamma^2 + c^2$	valid
26	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2999795755 $c^2 \gamma^2 = v^2 \gamma^2 + c^2$	3412946408 $v^2 \gamma^2$	2542420160 $c^2 \gamma^2 - v^2 \gamma^2 = c^2$	valid
27	0000111613: factor out X from LHS number of inputs: 1; feeds: 1; outputs: 1 Factor $#1$ from the LHS of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2542420160 $c^2 \gamma^2 - v^2 \gamma^2 = c^2$	7743841045 $\gamma^2$	7513513483 $\gamma^2 (c^2 - v^2) = c^2$	valid
28	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	7513513483 $\gamma^2 (c^2 - v^2) = c^2$	8571466509 $c^2 - \gamma^2$	7906112355 $\gamma^2 = \frac{c^2}{c^2 - \gamma^2}$	Algebraic error: LHS diff is pdg0001790*2(pdg00013572 - pdg00017902)/(pdg00017902 - pdg00045672), RHS diff is 0
29	0000111524: square root both sides number of inputs: 1; feeds: 0; outputs: 2 Take the square root of both sides of Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2} and Eq.~\ref{eq:#3}.	7906112355 $\gamma^2 = \frac{c^2}{c^2 - \gamma^2}$		8360117126 $\gamma = \frac{-1}{\sqrt{1-\frac{v^2}{c^2}}}$ 1528310784 $\gamma = \frac{1}{\sqrt{1-\frac{v^2}{c^2}}}$	recognized infrule but not yet supported
Note about step 30: Lorentz factor definition
30	0000111341: declare final expression number of inputs: 1; feeds: 0; outputs: 0 Eq.~\ref{eq:#1} is one of the final equations.	1528310784 $\gamma = \frac{1}{\sqrt{1-\frac{v^2}{c^2}}}$			no validation is available for declarations

Symbols used in Lorentz transformation

0000001790: $ \gamma $
0000004567: $ c $
0000001467: $ t $
0000004989: $ t' $
0000001357: $ v $
0000004037: $ x $
0000001464: $ x $
0000005456: $ x' $
0000005647: $ y $
0000001888: $ y' $
0000006728: $ z $
0000004306: $ z' $

d3js visualization of steps and expressions in Lorentz transformation

Hold the mouse over a node to highlight that node and its neighbors. You can zoom in/out. You can pan the image. You can move nodes by clicking and dragging.

Actions: Edit Derivation

Generate Tex file or PDF file

Delete Derivation and all associated steps

This does not remove expressions, symbols, and operations.

timing of Neo4j queries:

0.005 seconds for pdg_app/to_review_derivation 4c66e92d-aa8d-4d63-bb79-a5e4fddff279
0.013 seconds for compute/get_dict_of_steps_in_derivation: steps_in_this_derivationce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.005 seconds for compute/input_feed_output_infrule_for_step: get_inference_rule_connected_to_step_IDce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.005 seconds for compute/input_feed_output_infrule_for_step: get_expressions_from_step_id_and_expr_type HAS_INPUTce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.005 seconds for compute/input_feed_output_infrule_for_step: get_expressions_from_step_id_and_expr_type, HAS_FEEDce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.006 seconds for compute/input_feed_output_infrule_for_step: get_expressions_from_step_id_and_expr_type, HAS_OUTPUTce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.006 seconds for compute/get_dict_of_steps_in_derivation: get_sequence_index_for_stepce4d132e-06e1-4650-8dfa-3f24a59bbb55
0.006 seconds for pdg_app/ 4c66e92d-aa8d-4d63-bb79-a5e4fddff279

step	inference rule	input	feed	output	step validity (as per SymPy)
Note about step 1: equation 1-13 on page 21 in \cite{1999_Tipler_Llewellyn}
1	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			4662369843 \(x' = \gamma (x - v t)\)	no validation is available for declarations
Note about step 2: equation 1-14 on page 21 in \cite{1999_Tipler_Llewellyn}
2	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			2983053062 \(x = \gamma (x' + v t')\)	no validation is available for declarations
Note about step 3: solve output expr for $t$'
3	0000111556: substitute LHS of expr 1 into expr 2 number of inputs: 2; feeds: 0; outputs: 1 Substitute LHS of Eq.~\ref{eq:#1} into Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2983053062 \(x = \gamma (x' + v t')\) 4662369843 \(x' = \gamma (x - v t)\)		3426941928 \(x = \gamma ( \gamma (x - v t) + v t' )\)	LHS diff is -pdg0004037 + pdg0005456 RHS diff is pdg0001790(-pdg0001357pdg0001467 - pdg0001357pdg0004989 + pdg0001464 + pdg0001790(pdg0001357*pdg0001467 - pdg0004037))
4	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	3426941928 \(x = \gamma ( \gamma (x - v t) + v t' )\)		2096918413 \(x = \gamma ( \gamma x - \gamma v t + v t' )\)	LHS diff is 0 RHS diff is pdg0001790(pdg0001357pdg0004989 - pdg0001790(pdg0001357pdg0001467 - pdg0004037)) - pdg0001790(-pdg0001357pdg0001467pdg0001790 + pdg0001357pdg0004989 + pdg0001790pdg0004037)
5	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	2096918413 \(x = \gamma ( \gamma x - \gamma v t + v t' )\)		7741202861 \(x = \gamma^2 x - \gamma^2 v t + \gamma v t'\)	LHS diff is 0 RHS diff is pdg0001357pdg0001467pdg0001790*2 - pdg0001357pdg0001790pdg0004989 - pdg00017902pdg0004037 + pdg0001790(-pdg0001357pdg0001467pdg0001790 + pdg0001357pdg0004989 + pdg0001790pdg0004037)
6	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	7741202861 \(x = \gamma^2 x - \gamma^2 v t + \gamma v t'\)	7337056406 \(\gamma^2 x\)	4139999399 \(x - \gamma^2 x = - \gamma^2 v t + \gamma v t'\)	valid
7	0000111613: factor out X from LHS number of inputs: 1; feeds: 1; outputs: 1 Factor $#1$ from the LHS of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	4139999399 \(x - \gamma^2 x = - \gamma^2 v t + \gamma v t'\)	3495403335 \(x\)	9031609275 \(x (1 - \gamma^2 ) = - \gamma^2 v t + \gamma v t'\)	Not evaluated due to missing term in SymPy
8	0000111530: add X to both sides number of inputs: 1; feeds: 1; outputs: 1 Add $#1$ to both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	9031609275 \(x (1 - \gamma^2 ) = - \gamma^2 v t + \gamma v t'\)	8014566709 \(\gamma^2 v t\)	9409776983 \(x (1 - \gamma^2 ) + \gamma^2 v t = \gamma v t'\)	Not evaluated due to missing term in SymPy
9	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	9409776983 \(x (1 - \gamma^2 ) + \gamma^2 v t = \gamma v t'\)	2226340358 \(\gamma v\)	1974334644 \(\frac{x (1 - \gamma^2 )}{\gamma v} + \frac{\gamma^2 v t}{\gamma v} = t'\)	Not evaluated due to missing term in SymPy
10	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	1974334644 \(\frac{x (1 - \gamma^2 )}{\gamma v} + \frac{\gamma^2 v t}{\gamma v} = t'\)		8730201316 \(\frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t = t'\)	Not evaluated due to missing term in SymPy
11	0000111268: swap LHS with RHS number of inputs: 1; feeds: 0; outputs: 1 Swap LHS of Eq.~\ref{eq:#1} with RHS; yields Eq.~\ref{eq:#2}.	8730201316 \(\frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t = t'\)		5148266645 \(t' = \frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t\)	Not evaluated due to missing term in SymPy
12	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			4287102261 \(x^2 + y^2 + z^2 = c^2 t^2\)	no validation is available for declarations
13	0000111981: declare initial expression number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an initial equation.			1201689765 \(x'^2 + y'^2 + z'^2 = c^2 t'^2\)	no validation is available for declarations
14	0000111104: declare assumption number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an assumption.			7057864873 \(y' = y\)	no validation is available for declarations
15	0000111104: declare assumption number of inputs: 0; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is an assumption.			8515803375 \(z' = z\)	no validation is available for declarations
16	0000111797: substitute LHS of four expressions into expression number of inputs: 5; feeds: 0; outputs: 1 Substitute LHS of Eq.~\ref{eq:#1} and LHS of Eq.~\ref{eq:#2} and LHS of Eq.~\ref{eq:#3} and LHS of Eq.~\ref{eq:#4} into Eq.~\ref{eq:#5}; yields Eq.~\ref{eq:#6}.	1201689765 \(x'^2 + y'^2 + z'^2 = c^2 t'^2\) 4662369843 \(x' = \gamma (x - v t)\) 5148266645 \(t' = \frac{\gamma x (1 - \gamma^2 )}{\gamma^2 v} + \gamma t\) 7057864873 \(y' = y\) 8515803375 \(z' = z\)		9805063945 \(\gamma^2 (x - v t)^2 + y^2 + z^2 = c^2 \gamma^2 \left( t + \frac{ 1 - \gamma^2 }{ \gamma^2 } \frac{x}{v} \right)^2\)	recognized infrule but not yet supported
Note about step 17: expanded the squared terms
17	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	9805063945 \(\gamma^2 (x - v t)^2 + y^2 + z^2 = c^2 \gamma^2 \left( t + \frac{ 1 - \gamma^2 }{ \gamma^2 } \frac{x}{v} \right)^2\)		1935543849 \(\gamma^2 x^2 - \gamma^2 2 x v t + \gamma^2 v^2 t^2 + y^2 + z^2 = c^2 \gamma^2 \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x^2}{\gamma^2} + c^2 \gamma^2 2 t \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x}{\gamma} + c^2 \gamma^2 t^2\)	LHS diff is 0 RHS diff is pdg0004567*2(-pdg0001357*2pdg0001467*2pdg0001790*4 + 2pdg0001357*2pdg0001467pdg0001790pdg0004037(pdg00017902 - 1) + pdg00013572pdg0004037*2(pdg0001790*2 - 1) + (pdg0001357pdg0001467pdg00017902 - pdg0004037(pdg00017902 - 1))2)/(pdg0001357*2pdg0001790**2)
Note about step 18: grouped by terms for $x^2$, $xt$, and $t^2$
18	0000111457: simplify number of inputs: 1; feeds: 0; outputs: 1 Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.	1935543849 \(\gamma^2 x^2 - \gamma^2 2 x v t + \gamma^2 v^2 t^2 + y^2 + z^2 = c^2 \gamma^2 \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x^2}{\gamma^2} + c^2 \gamma^2 2 t \left(\frac{1-\gamma^2}{\gamma^2}\right)\frac{x}{\gamma} + c^2 \gamma^2 t^2\)		1586866563 \(\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)\)	LHS diff is pdg0001357*2pdg0001467*2pdg0001790*2 - 2pdg0001467pdg00017902pdg0004037pdg00045672/pdg0001357 + 2pdg0001467pdg0004037pdg00045672/pdg0001357 + pdg00040372pdg00045672(pdg00017902 - 1)2/(pdg0001357*2pdg00017902) RHS diff is (pdg00013572pdg00014672pdg0001790*4 - 2pdg0001467pdg0001790pdg0004037pdg00045672(pdg00017902 - 1) - pdg00040372pdg00045672(pdg00017902 - 1))/pdg00017902
Note about step 19: based on the comparison of the $x^2$ terms
19	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 \(\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)\) 4287102261 \(x^2 + y^2 + z^2 = c^2 t^2\)		3182633789 \(\gamma^2 - c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1\)	recognized infrule but not yet supported
Note about step 20: based on the comparison of the $t^2$ terms
20	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 \(\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)\) 4287102261 \(x^2 + y^2 + z^2 = c^2 t^2\)		1916173354 \(-\gamma^2 v^2 + c^2 \gamma^2 = c^2\)	recognized infrule but not yet supported
Note about step 21: based on the comparison of the $(x t)$ terms
21	0000111768: expr 1 is equivalent to expr 2 under the condition number of inputs: 2; feeds: 0; outputs: 1 Eq.~\ref{eq:#1} is equivalent to Eq.~\ref{eq:#2} under the condition in Eq.~\ref{eq:#3}.	1586866563 \(\left( \gamma^2 - c^2 \gamma^2 \left( \frac{1-\gamma^2}{\gamma^2} \right)^2 \frac{1}{v^2} \right) x^2 + y^2 + z^2 + \left( -\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} \right) = t^2 \left( c^2 \gamma^2 - \gamma^2 v^2 \right)\) 4287102261 \(x^2 + y^2 + z^2 = c^2 t^2\)		2076171250 \(-\gamma^2 2 x v t - c^2 \gamma^2 2 t \left( \frac{1-\gamma^2}{\gamma^2} \right) \frac{x}{v} = 0\)	recognized infrule but not yet supported
Note about step 22: solve for $\gamma$
22	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	3182633789 \(\gamma^2 - c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1\)	5284610349 \(\gamma^2\)	2417941373 \(- c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1 - \gamma^2\)	valid
23	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	2417941373 \(- c^2 \gamma^2 \frac{(1-\gamma^2)^2}{v^2 \gamma^4} = 1 - \gamma^2\)	5787469164 \(1 - \gamma^2\)	1639827492 \(- c^2 \frac{(1-\gamma^2)}{v^2 \gamma^2} = 1\)	valid
24	0000111182: multiply both sides by number of inputs: 1; feeds: 1; outputs: 1 Multiply both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	1639827492 \(- c^2 \frac{(1-\gamma^2)}{v^2 \gamma^2} = 1\)	5669500954 \(v^2 \gamma^2\)	5763749235 \(-c^2 + c^2 \gamma^2 = v^2 \gamma^2\)	valid
25	0000111530: add X to both sides number of inputs: 1; feeds: 1; outputs: 1 Add $#1$ to both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	5763749235 \(-c^2 + c^2 \gamma^2 = v^2 \gamma^2\)	6408214498 \(c^2\)	2999795755 \(c^2 \gamma^2 = v^2 \gamma^2 + c^2\)	valid
26	0000111282: subtract X from both sides number of inputs: 1; feeds: 1; outputs: 1 Subtract $#1$ from both sides of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2999795755 \(c^2 \gamma^2 = v^2 \gamma^2 + c^2\)	3412946408 \(v^2 \gamma^2\)	2542420160 \(c^2 \gamma^2 - v^2 \gamma^2 = c^2\)	valid
27	0000111613: factor out X from LHS number of inputs: 1; feeds: 1; outputs: 1 Factor $#1$ from the LHS of Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.	2542420160 \(c^2 \gamma^2 - v^2 \gamma^2 = c^2\)	7743841045 \(\gamma^2\)	7513513483 \(\gamma^2 (c^2 - v^2) = c^2\)	valid
28	0000111975: divide both sides by number of inputs: 1; feeds: 1; outputs: 1 Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.	7513513483 \(\gamma^2 (c^2 - v^2) = c^2\)	8571466509 \(c^2 - \gamma^2\)	7906112355 \(\gamma^2 = \frac{c^2}{c^2 - \gamma^2}\)	Algebraic error: LHS diff is pdg0001790*2(pdg00013572 - pdg00017902)/(pdg00017902 - pdg00045672), RHS diff is 0
29	0000111524: square root both sides number of inputs: 1; feeds: 0; outputs: 2 Take the square root of both sides of Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2} and Eq.~\ref{eq:#3}.	7906112355 \(\gamma^2 = \frac{c^2}{c^2 - \gamma^2}\)		8360117126 \(\gamma = \frac{-1}{\sqrt{1-\frac{v^2}{c^2}}}\) 1528310784 \(\gamma = \frac{1}{\sqrt{1-\frac{v^2}{c^2}}}\)	recognized infrule but not yet supported
Note about step 30: Lorentz factor definition
30	0000111341: declare final expression number of inputs: 1; feeds: 0; outputs: 0 Eq.~\ref{eq:#1} is one of the final equations.	1528310784 \(\gamma = \frac{1}{\sqrt{1-\frac{v^2}{c^2}}}\)			no validation is available for declarations