Derivations, CAS, Lean, and Assumptions in Physics

Initially the Physics Derivation Graph documented expressions as Latex. Then SymPy was added to support validation of steps (is the step self-consistent) and dimensionality (is the expression self-consistent?). 

Recently I learned that Lean could be used to prove each step in a derivation. The difference between a Computer Algebra System (e.g., SymPy) and Lean is whether "a = b  --> a/b = 1" is a valid step -- it isn't when b is zero. Lean catches that; SymPy does not. 

While Lean proofs sound like the last possible refinement, there are two additional complications to account for not addressed by Lean. 

Challenge: Bounded ranges of applicability

In classical mechanics the relation between momentum, mass, and velocity is "p = m v". That hold when "v << c". Near the speed of light we need to switch to relativistic mass, 

m = m_{rest} / sqrt{1-((v^2)/(c^2))}.

The boundary between "v << c" and "v ~ c" is usually set by the context being considered. 

One response for users of Lean would be to always use the "correct" relativistic equation, even when "v << c."  A more conventional approach used by Physicists is to use

p = m v, where v << c

then drop the "v << c" clause and rely on context.

Challenge: Real versus Float versus experimental characterization

Lean forces you to characterize numbers as Real or Integer or Complex. This presents a problem for numerical simulations that have something like a 64 bit float representation.

In thermodynamics we assume the number of particles involved is sufficiently large that we focus on the behavior of the ensemble rather than individual particles. The imprecision of floats is not correct, but neither is the infinite precision assumed by Real numbers. 

Example applications of Lean proofs needing bounds on values

Math doesn't have convenient ways of indicating "finite precision, as set by the Plank scale."  The differential element used in calculus cannot actually go to zero, but we use that concept because it works at the scales we are used to. 

Physicists make simplifying assumptions that sometimes ignore reality (e.g., assuming continuous media when particles are discrete). Then again the assumption that particles are discrete is also a convenient fiction that ignores the wavefunction of quantum mechanics. 

Lean can be used to prove derivations in classical mechanics, but to be explicit about the bounds of those proofs we'd also need to indicate "v << c" and "assume space is Euclidean." 

For molecular dynamics, another constraint to account for is "temperature << 1E10 Kelvin" or whatever temperature the atoms breaks down into plasma. 

Distinguishing the context of (classical mechanics from quantum) and (classical from relativistic) and (conventional gas versus plasma) seems important so that we know when a claim proven in Lean is applicable. 

dichotomy of assumptions

In Physics there are some assumptions that form a dichotomy:

• is the speed of light constant or variable?
• is the measure of energy discrete or continuous?

In the dichotomy of assumptions, one of the two assumptions is reflective of reality, and the other is an oversimplification. The oversimplification is related to reality by assumptions, constraints, and limits. 

(I define "oversimplification" as the extension of useful assumptions to incorrect regions.)

Another case where oversimplification is the link between domains is quantum physics and (classical) statistical physics. Quantum particles are either Fermions (odd half integer spin) or Bosons (integer spin), but that is practically irrelevant for large ensembles of particles at room temperature. The aspects that get measured at one scale (e.g., particle velocity) are related to but separate from metrics at another scale (e.g, temperature, entropy). Mathematically this transition manifests as the switch from summation to integration.

So what? 
This is a new-to-me category of derivations which span domains. What constitutes a domain is set by the assumptions that form the boundaries, and oversimplification is how to cross the boundaries. 

What boundaries should the Physics Derivation Graph transgress? What oversimplifications are adjacent?

• quantum mechanics to classical - https://en.wikipedia.org/wiki/Canonical_quantization
• https://en.wikipedia.org/wiki/Optics
• https://en.wikipedia.org/wiki/Condensed_matter_physics
• https://en.wikipedia.org/wiki/Statistical_mechanics
• https://scholar.harvard.edu/files/schwartz/files/10-quantumstatmech_0.pdf
• https://physics.stackexchange.com/questions/374647/for-ideal-classical-gasses-in-terms-of-the-energy-levels-why-do-we-ignore-wheth
• relativity to classical
• https://en.wikipedia.org/wiki/Astrometry
• https://en.wikipedia.org/wiki/Orbital_mechanics
• https://en.wikipedia.org/wiki/Celestial_mechanics
• https://en.wikipedia.org/wiki/Galactic_astronomy
• https://en.wikipedia.org/wiki/Astronomy#Stellar_astronomy
• https://physics.stackexchange.com/questions/580494/difference-between-relativistic-and-non-relativistic-classical-equations-of-elec
• "The EFE reduce to Newton's law of gravity by using both the weak-field approximation and the slow-motion approximation." source
• quantum field theory to quantum mechanics
• https://en.wikipedia.org/wiki/Quantum_field_theory#Mathematical_rigor -- see particle in a box

The evidences of dissonance (e.g, Mercury’s perihelion based on Newtonian gravitation versus relativity, the Deflection of Starlight; source) are not relevant for bridging domains. They are illustrations of the oversimplification.

Update 2024-03-10: on the page https://en.wikipedia.org/wiki/Phase_space#Quantum_mechanics

"by expressing quantum mechanics in phase space (the same ambit as for classical mechanics), the Weyl map facilitates recognition of quantum mechanics as a deformation (generalization) of classical mechanics, with deformation parameter ħ/S, where S is the action of the relevant process. (Other familiar deformations in physics involve the deformation of classical Newtonian into relativistic mechanics, with deformation parameter v/c; or the deformation of Newtonian gravity into general relativity, with deformation parameter Schwarzschild radius/characteristic dimension.)
 
Classical expressions, observables, and operations (such as Poisson brackets) are modified by ħ-dependent quantum corrections, as the conventional commutative multiplication applying in classical mechanics is generalized to the noncommutative star-multiplication characterizing quantum mechanics and underlying its uncertainty principle."

See also https://en.wikipedia.org/wiki/Wigner%E2%80%93Weyl_transform#Deformation_quantization

derivations, identities, and other categories of mathematical physics

Transforming from one expression to another is carried out with respect to a goal. There are different categories of goals (listed below). I don't yet know what distinguishes one category from another.

My motivation for the Physics Derivation Graph is exclusively the first category -- derivations, specifically across domains. This motivation is more specific than a broader question, "what is the relation between every expression in mathematical physics and every other expression?" because the answer might be "symbols and inference rules are common."

The other categories are neat but not as rewarding for me. These other categories are included in the PDG because the infrastructure for software and UI and data format are the same.

Examples of Derivations

Relation between two disparate descriptions of nature:

• Maxwell equations to electric field wave equation
• optics: Law of refraction to Brewster's angle

Derivation of expression from simpler observations plus assumptions:

• Newton's Law of Gravitation
• first law of thermodynamics

An expression in one domain simplifies to another expression in a different domain under modified assumptions

• https://en.wikipedia.org/wiki/Correspondence_principle
• https://www.physicsforums.com/threads/schroedinger-equation-in-the-classical-limit.775531/
• https://mathoverflow.net/questions/102313/classical-limit-of-quantum-mechanics
• "A wave equation interpolating between classical and quantum mechanics"
• https://mathoverflow.net/questions/225814/does-quantum-mechanics-ever-really-quantize-classical-mechanics
• https://farside.ph.utexas.edu/teaching/sm1/lectures/node82.html

The same concept appears in multiple domains

• Anderson localization (for electron transport, photonics; anywhere with waves)
• simple harmonic oscillator, particle in a box
• https://en.wikipedia.org/wiki/Continuity_equation, aka transport equation

Examples of Identities

An equation can be expressed differently but be equivalent:

• Euler equation: trig square root

Examples of Proofs

Show that two sides of an equation are, in fact, the same:

• Euler equation proof

Examples of Use Case

Start from one or more expressions to derive a conclusion with practical utility

• escape velocity
• Schwarzschild radius for non-rotating black hole
• angle of maximum distance for projectile motion
• speed of Earth around Sun
• mass of the Earth

This is the focus of the ATOMS lab at UMBC, specifically enacted using Lean.

Python dependencies visualization using pydeps

To see what Python modules are available on my system I can run

pydoc3 modules

One of the modules is pandas. Here's a script that just loads pandas module:

cat load_pandas.py 
import warnings
warnings.filterwarnings("ignore", category=DeprecationWarning)
import pandas as pd 

When the script is run nothing happens

python3 load_pandas.py

I have pydeps installed:

pydeps --version
pydeps v1.12.17

Output of analysis by pydeps:

pydeps -o myfile.png --show-dot -T png --noshow load_pandas.py 

digraph G {
    concentrate = true;

    rankdir = TB;
    node [style=filled,fillcolor="#ffffff",fontcolor="#000000",fontname=Helvetica,fontsize=10];

    load_pandas_py [fillcolor="#a65959",fontcolor="#ffffff",label="load_pandas.py"];
    pandas [fillcolor="#039595",fontcolor="#ffffff"];
    pandas__config [fillcolor="#24d0d0",label="pandas._config"];
    pandas__version [fillcolor="#47c2c2",label="pandas\.\n_version"];
    pandas__version_meson [fillcolor="#47c2c2",label="pandas\.\n_version_meson"];
    pandas_api [fillcolor="#3db8b8",label="pandas.api"];
    pandas_arrays [fillcolor="#46a4a4",label="pandas.arrays"];
    pandas_compat [fillcolor="#17d3d3",label="pandas.compat"];
    pandas_compat__optional [fillcolor="#31c4c4",label="pandas\.\ncompat\.\n_optional"];
    pandas_compat_pyarrow [fillcolor="#3db8b8",label="pandas\.\ncompat\.\npyarrow"];
    pandas_core [fillcolor="#10f9f9",label="pandas.core"];
    pandas_core_api [fillcolor="#3a8888",fontcolor="#ffffff",label="pandas\.\ncore\.\napi"];
    pandas_core_computation [fillcolor="#3bcece",label="pandas\.\ncore\.\ncomputation"];
    pandas_core_computation_api [fillcolor="#46a4a4",label="pandas\.\ncore\.\ncomputation\.\napi"];
    pandas_core_config_init [fillcolor="#3a8888",fontcolor="#ffffff",label="pandas\.\ncore\.\nconfig_init"];
    pandas_core_dtypes [fillcolor="#2fdbdb",label="pandas\.\ncore\.\ndtypes"];
    pandas_core_dtypes_dtypes [fillcolor="#339999",fontcolor="#ffffff",label="pandas\.\ncore\.\ndtypes\.\ndtypes"];
    pandas_core_reshape [fillcolor="#47c2c2",label="pandas\.\ncore\.\nreshape"];
    pandas_core_reshape_api [fillcolor="#46a4a4",label="pandas\.\ncore\.\nreshape\.\napi"];
    pandas_errors [fillcolor="#3ab0b0",label="pandas.errors"];
    pandas_io [fillcolor="#0bdfdf",label="pandas.io"];
    pandas_io_api [fillcolor="#46a4a4",label="pandas.io.api"];
    pandas_io_json [fillcolor="#23c8c8",label="pandas.io.json"];
    pandas_io_json__normalize [fillcolor="#4cb3b3",label="pandas\.\nio\.\njson\.\n_normalize"];
    pandas_plotting [fillcolor="#31c4c4",label="pandas\.\nplotting"];
    pandas_testing [fillcolor="#4cb3b3",label="pandas.testing"];
    pandas_tseries [fillcolor="#23c8c8",label="pandas.tseries"];
    pandas_tseries_api [fillcolor="#46a4a4",label="pandas\.\ntseries\.\napi"];
    pandas_tseries_offsets [fillcolor="#26d9d9",label="pandas\.\ntseries\.\noffsets"];
    pandas_util [fillcolor="#05e5e5",label="pandas.util"];
    pandas_util__print_versions [fillcolor="#409696",fontcolor="#ffffff",label="pandas\.\nutil\.\n_print_versions"];
    pandas_util__tester [fillcolor="#46a4a4",label="pandas\.\nutil\.\n_tester"];
    pandas -> load_pandas_py [fillcolor="#039595",minlen="2"];
    pandas__config -> pandas [fillcolor="#24d0d0"];
    pandas__config -> pandas_core_config_init [fillcolor="#24d0d0",minlen="2"];
    pandas__config -> pandas_errors [fillcolor="#24d0d0"];
    pandas__version -> pandas [fillcolor="#47c2c2"];
    pandas__version -> pandas_util__print_versions [fillcolor="#47c2c2",minlen="2"];
    pandas__version_meson -> pandas [fillcolor="#47c2c2"];
    pandas__version_meson -> pandas_util__print_versions [fillcolor="#47c2c2",minlen="2"];
    pandas_api -> pandas [fillcolor="#3db8b8"];
    pandas_arrays -> pandas [fillcolor="#46a4a4"];
    pandas_compat -> pandas [fillcolor="#17d3d3"];
    pandas_compat -> pandas_core_dtypes_dtypes [fillcolor="#17d3d3",minlen="3"];
    pandas_compat -> pandas_util__print_versions [fillcolor="#17d3d3",minlen="2"];
    pandas_compat -> pandas_util__tester [fillcolor="#17d3d3",minlen="2"];
    pandas_compat__optional -> pandas [fillcolor="#31c4c4",minlen="2"];
    pandas_compat__optional -> pandas_util__print_versions [fillcolor="#31c4c4",minlen="2"];
    pandas_compat__optional -> pandas_util__tester [fillcolor="#31c4c4",minlen="2"];
    pandas_compat_pyarrow -> pandas [fillcolor="#3db8b8",minlen="2"];
    pandas_compat_pyarrow -> pandas_compat [fillcolor="#3db8b8",weight="2"];
    pandas_core -> pandas [fillcolor="#10f9f9"];
    pandas_core -> pandas_arrays [fillcolor="#10f9f9"];
    pandas_core -> pandas_util [fillcolor="#10f9f9"];
    pandas_core_api -> pandas [fillcolor="#3a8888",minlen="2"];
    pandas_core_computation -> pandas [fillcolor="#3bcece",minlen="2"];
    pandas_core_computation -> pandas_core_config_init [fillcolor="#3bcece",weight="2"];
    pandas_core_computation_api -> pandas [fillcolor="#46a4a4",minlen="3"];
    pandas_core_config_init -> pandas [fillcolor="#3a8888",minlen="2"];
    pandas_core_dtypes -> pandas [fillcolor="#2fdbdb",minlen="2"];
    pandas_core_dtypes -> pandas_core_api [fillcolor="#2fdbdb",weight="2"];
    pandas_core_dtypes -> pandas_core_config_init [fillcolor="#2fdbdb",weight="2"];
    pandas_core_dtypes_dtypes -> pandas [fillcolor="#339999",minlen="3"];
    pandas_core_dtypes_dtypes -> pandas_core_api [fillcolor="#339999",minlen="2",weight="2"];
    pandas_core_reshape -> pandas [fillcolor="#47c2c2",minlen="2"];
    pandas_core_reshape_api -> pandas [fillcolor="#46a4a4",minlen="3"];
    pandas_errors -> pandas [fillcolor="#3ab0b0"];
    pandas_errors -> pandas_core_dtypes_dtypes [fillcolor="#3ab0b0",minlen="3"];
    pandas_io -> pandas [fillcolor="#0bdfdf"];
    pandas_io -> pandas_core_api [fillcolor="#0bdfdf",minlen="2"];
    pandas_io -> pandas_core_config_init [fillcolor="#0bdfdf",minlen="2"];
    pandas_io_api -> pandas [fillcolor="#46a4a4",minlen="2"];
    pandas_io_json -> pandas [fillcolor="#23c8c8",minlen="2"];
    pandas_io_json -> pandas_io [fillcolor="#23c8c8",weight="2"];
    pandas_io_json -> pandas_io_api [fillcolor="#23c8c8",weight="2"];
    pandas_io_json__normalize -> pandas [fillcolor="#4cb3b3",minlen="3"];
    pandas_plotting -> pandas [fillcolor="#31c4c4"];
    pandas_plotting -> pandas_core_config_init [fillcolor="#31c4c4",minlen="2"];
    pandas_testing -> pandas [fillcolor="#4cb3b3"];
    pandas_tseries -> pandas [fillcolor="#23c8c8"];
    pandas_tseries -> pandas_core_api [fillcolor="#23c8c8",minlen="2"];
    pandas_tseries_api -> pandas [fillcolor="#46a4a4",minlen="2"];
    pandas_tseries_offsets -> pandas [fillcolor="#26d9d9",minlen="2"];
    pandas_tseries_offsets -> pandas_core_api [fillcolor="#26d9d9",minlen="2"];
    pandas_tseries_offsets -> pandas_tseries [fillcolor="#26d9d9",weight="2"];
    pandas_tseries_offsets -> pandas_tseries_api [fillcolor="#26d9d9",weight="2"];
    pandas_util -> pandas [fillcolor="#05e5e5"];
    pandas_util -> pandas_arrays [fillcolor="#05e5e5"];
    pandas_util -> pandas_compat__optional [fillcolor="#05e5e5",minlen="2"];
    pandas_util -> pandas_compat_pyarrow [fillcolor="#05e5e5",minlen="2"];
    pandas_util -> pandas_core_dtypes_dtypes [fillcolor="#05e5e5",minlen="3"];
    pandas_util -> pandas_errors [fillcolor="#05e5e5"];
    pandas_util__print_versions -> pandas [fillcolor="#409696",minlen="2"];
    pandas_util__tester -> pandas [fillcolor="#46a4a4",minlen="2"];
}