Return to navigation page or list derivations

Review upper limit on velocity in condensed matter

step inference rule input feed output step validity (as per SymPy)
1
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 4560648264
    \(v=\sqrt{ \frac{K + (4/3) G}{\rho} }\)
 no validation is available for declarations
2
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 9376481176
    \(K=f \frac{E}{a^3}\)
 no validation is available for declarations
3
  • 111782: drop non-dominant term
  • number of inputs: 1; feeds: 1; outputs: 1
  • Based on the assumption $#1$, drop non-dominant term in Eq.~\\ref{#2}; yeilds Eq.~\\ref{#3}
  1. 4560648264
    \(v=\sqrt{ \frac{K + (4/3) G}{\rho} }\)
  1. 9674924517
    \(K >> G\)
  1. 6504442697
    \(v=\sqrt{ \frac{K}{\rho} }\)
 recognized infrule but not yet supported
4
  • 111556: 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}.
  1. 9376481176
    \(K=f \frac{E}{a^3}\)
  1. 6504442697
    \(v=\sqrt{ \frac{K}{\rho} }\)
  1. 8090924099
    \(v=\sqrt{ \left( f\frac{E}{a^3} \right) \frac{1}{\rho} }\)
 valid
5
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 8908736791
    \(\rho=\frac{m}{a^3}\)
 no validation is available for declarations
6
  • 111182: 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}.
  1. 8908736791
    \(\rho=\frac{m}{a^3}\)
  1. 2397692197
    \(a^3\)
  1. 8688588981
    \(a^3 \rho=m\)
 valid
7
  • 111634: substitute RHS of expr 1 into expr 2
  • number of inputs: 2; feeds: 0; outputs: 1
  • Substitute RHS of Eq.~\\ref{eq:#1} into Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 8688588981
    \(a^3 \rho=m\)
  1. 8090924099
    \(v=\sqrt{ \left( f\frac{E}{a^3} \right) \frac{1}{\rho} }\)
  1. 7837519722
    \(v=\sqrt{f} \sqrt{\frac{E}{m}}\)
 LHS diff is 0 RHS diff is -sqrt(pdg0006235)*sqrt(pdg0002241/pdg0009863) + sqrt(pdg0002241*pdg0006235/(pdg0003935*pdg0005854**3))
8
  • 111782: drop non-dominant term
  • number of inputs: 1; feeds: 1; outputs: 1
  • Based on the assumption $#1$, drop non-dominant term in Eq.~\\ref{#2}; yeilds Eq.~\\ref{#3}
  1. 7837519722
    \(v=\sqrt{f} \sqrt{\frac{E}{m}}\)
  1. 3685779219
    \(\sqrt{f} \approx 2\)
  1. 9854442418
    \(v=\sqrt{\frac{E}{m}}\)
 recognized infrule but not yet supported
9
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 1556389363
    \(E_{\rm Rydberg}=\frac{ m_e e^4 }{ 32 \pi^2 \epsilon_0^2 \hbar^2}\)
 no validation is available for declarations
10
  • 111104: declare assumption
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an assumption.
  1. 4107032818
    \(E_{\rm Rydberg}=E\)
 no validation is available for declarations
11
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 8106885760
    \(\alpha=\frac{1}{4 \pi \epsilon_0} \frac{e^2}{\hbar c}\)
 no validation is available for declarations
12
  • 111182: 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}.
  1. 8106885760
    \(\alpha=\frac{1}{4 \pi \epsilon_0} \frac{e^2}{\hbar c}\)
  1. 8857931498
    \(c\)
  1. 5838268428
    \(\alpha c=\frac{1}{4 \pi \epsilon_0} \frac{e^2}{\hbar}\)
 valid
13
  • 111556: 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}.
  1. 1556389363
    \(E_{\rm Rydberg}=\frac{ m_e e^4 }{ 32 \pi^2 \epsilon_0^2 \hbar^2}\)
  1. 4107032818
    \(E_{\rm Rydberg}=E\)
  1. 3291685884
    \(E=\frac{ m_e e^4 }{ 32 \pi^2 \epsilon_0^2 \hbar^2}\)
 LHS diff is -pdg0002241 + pdg0001999**4*pdg0002515/(32*pdg0001054**2*pdg0003141**2*pdg0007940**2) RHS diff is pdg0002241 - pdg0001999**4*pdg0002515/(32*pdg0001054**2*pdg0003141**2*pdg0007940**2)
14
  • 111556: 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}.
  1. 9854442418
    \(v=\sqrt{\frac{E}{m}}\)
  1. 3291685884
    \(E=\frac{ m_e e^4 }{ 32 \pi^2 \epsilon_0^2 \hbar^2}\)
  1. 3935058307
    \(v=\sqrt{ \frac{m_e}{m} \frac{e^4}{32 \pi^2 \epsilon_0^2 \hbar^2} }\)
 LHS diff is -pdg0002077 + pdg0002241 RHS diff is -sqrt(2)*sqrt(pdg0001999**4*pdg0002515/(pdg0001054**2*pdg0003141**2*pdg0007940**2*pdg0009863))/8 + pdg0001999**4*pdg0002515/(32*pdg0001054**2*pdg0003141**2*pdg0007940**2)
15
  • 111457: simplify
  • number of inputs: 1; feeds: 0; outputs: 1
  • Simplify Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}.
  1. 3935058307
    \(v=\sqrt{ \frac{m_e}{m} \frac{e^4}{32 \pi^2 \epsilon_0^2 \hbar^2} }\)
  1. 9640720571
    \(v=\frac{e^2}{4 \pi \epsilon_0 \hbar} \sqrt{\frac{m_e}{2 m}}\)
 LHS diff is 0 RHS diff is sqrt(2)*(pdg0001054*pdg0003141*pdg0007940*sqrt(pdg0001999**4*pdg0002515/(pdg0001054**2*pdg0003141**2*pdg0007940**2*pdg0009863)) - pdg0001999**2*sqrt(pdg0002515/pdg0009863))/(8*pdg0001054*pdg0003141*pdg0007940)
16
  • 111556: 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}.
  1. 9640720571
    \(v=\frac{e^2}{4 \pi \epsilon_0 \hbar} \sqrt{\frac{m_e}{2 m}}\)
  1. 5838268428
    \(\alpha c=\frac{1}{4 \pi \epsilon_0} \frac{e^2}{\hbar}\)
  1. 5789289057
    \(v=\alpha c \sqrt{ \frac{m_e}{2 m} }\)
 LHS diff is pdg0001370*pdg0004567 - pdg0002077 RHS diff is -sqrt(2)*pdg0001370*pdg0004567*sqrt(pdg0002515/pdg0009863)/2 + pdg0001999**2/(4*pdg0001054*pdg0003141*pdg0007940)
17
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 5646314683
    \(m=A m_p\)
 no validation is available for declarations
18
  • 111556: 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}.
  1. 5646314683
    \(m=A m_p\)
  1. 5789289057
    \(v=\alpha c \sqrt{ \frac{m_e}{2 m} }\)
  1. 2897612567
    \(v=\alpha c \sqrt{ \frac{m_e}{A m_p} }\)
 LHS diff is 0 RHS diff is pdg0001370*pdg0004567*sqrt(pdg0002515/(pdg0003285*pdg0005916))*(-2 + sqrt(2))/2
19
  • 111773: maximum of expression
  • number of inputs: 1; feeds: 1; outputs: 1
  • The maximum of Eq.~\\ref{eq:#2} with respect to $#1$ is Eq.~\\ref{eq:#3}
  1. 2897612567
    \(v=\alpha c \sqrt{ \frac{m_e}{A m_p} }\)
  1. 6259833695
    \(A\)
  1. 7701249282
    \(v_u=\alpha c \sqrt{ \frac{m_e}{m_p} }\)
 recognized infrule but not yet supported
20
  • 111341: declare final expression
  • number of inputs: 1; feeds: 0; outputs: 0
  • Eq.~\\ref{eq:#1} is one of the final equations.
  1. 7701249282
    \(v_u=\alpha c \sqrt{ \frac{m_e}{m_p} }\)
 no validation is available for declarations


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
   xor   

Delete Derivation and all associated steps

This does not remove expressions, symbols, and operations.

timing of Neo4j queries: