Public atlas
PhysAtlas
A map of the mathematics inside physics.
Explore the ideas, equations, and checked formalizations that connect physical intuition to precise mathematics.
- Fields
- 8
- Guided theorems
- 6
Start with a visual walkthrough, then inspect the exact Lean statement and sources.
Browse by area
Find your way into the atlas
Choose an area to filter all 211 public topics.
Choose a route
Explore in the way that suits you
The atlas, map, stories, and library collection are different views of the same public results.
Start here
EM Poynting Local Conservation
See how changing field energy, energy flow, and work on charges balance at a single point in electromagnetism.
7-step walkthrough · 201 walkthrough declaration lines · 6 source files
- Meaning reviewed
- Proof checked in Lean
Public atlas
Explore all topics
How topics are ordered
Recognizable physics, source substance, checked breadth, reviewed walkthroughs, and recorded connections shape the opening selection. Subject diversity keeps closely related results from crowding the first screen. This is a browsing aid, not a proof-difficulty or trust score.
211 topics
Download atlas JSONTry a broader phrase, or clear the current search and filters.
Physics formalizations · Formalized result
Finite Gibbs Free-Energy Attainment
Among finite normalized trial weights, the supplied Gibbs profile reaches the checked free-energy lower bound.
6-step walkthrough · 150 walkthrough declaration lines
Physics formalizations · Formalized result
Electromagnetic Plane-Wave Relations in Free Space
Orthogonal electric and magnetic field structures accompany one pointwise free-space propagation and energy-flow direction.
6-step walkthrough · 96 walkthrough declaration lines
Quantum theory · Formalized result
Finite-Target Unitary Time Evolution
A finite state follows a coherent unitary orbit around a fixed Hermitian Hamiltonian.
Quantum theory · Formalized result
Binary CPTP Product Composition
Two finite channels act as one binary product stage, then pass through a second paired stage by sequential composition.
3-step walkthrough · 42 walkthrough declaration lines
Quantum theory · Formalized result
Finite-Dimensional Ehrenfest Theorem
Finite-state evolution and a fixed observable meet in an instantaneous commutator-controlled expectation change.
Physics formalizations · Formalized result
Pointwise Maxwell Stress Momentum Balance
A magnified local field patch pictures Maxwell stress, Lorentz-force density, and field-momentum change at one point.
Physics formalizations · Formalized result
Finite Reversible Markov Entropy-Rate Seed
Balanced reversible rates on a finite network accompany one instantaneous nonpositive relative-entropy slope.
Physics formalizations · Formalized result
Acoustic Impedance Normal Incidence
One scalar pressure wave divides at a normal fluid interface into distinct reflected and transmitted branches.
5-step walkthrough · 98 walkthrough declaration lines
Quantum theory · Formalized result
Finite-Target Matrix Liouville-von Neumann Bridge
A finite matrix orbit is pictured through two Hamiltonian orderings and one instantaneous commutator tangent.
Quantum theory · Formalized result
Finite Robertson-Schrodinger Uncertainty Package
Centered finite-dimensional observable vectors combine variance, covariance, and an oriented commutator contribution.
Units and dimensions · Formalized result
Free-Space Energy-Density Unit Bridge
Separate FreeSpace scalar energy terms reach the same energy-density dimension and remain distinct in the final value-sum cradle.
Quantum theory · Formalized result
Hadamard Measurement Probability Components
A fixed basis-zero input passes through one finite Hadamard transform into two equal probability components.
Quantum theory · Formalized result
Finite Density-State Invariants Under Conjugation
A supplied finite isometry or unitary conjugation changes the density matrix while preserving positivity and trace-one structure.
Quantum theory · Definition
Born Rule Projection Probability
A fixed finite basis resolves one pure state into squared coordinate contributions inside a normalized whole.
Quantum theory · Formalized result
Finite POVM Naimark Compression
A finite POVM is pictured through an isometric bridge to separated projective outcomes in a larger finite frame.
Mechanics · Formalized result
Cyclotron Motion in a Uniform Magnetic Field
One explicit signed helical trajectory advances through a uniform z-directed magnetic field at constant radius.
5-step walkthrough · 80 walkthrough declaration lines
Quantum theory · Formalized result
Finite Welch Bound Maximum-Correlation Core
A finite coordinate-vector family forces one squared cross-correlation to meet the retained Welch maximum-correlation bound.
Physics formalizations · Formalized result
EM Plane-Wave Poynting Algebra Identity
Supplied transverse field strands meet at one local algebraic junction and produce a raw plane-wave energy-flow pairing.
Quantum theory · Formalized result
Finite-Target Density Evolution Bridge
A selected two-sided finite-basis transformation carries one density mosaic to a specified finite target.
Units and dimensions · Formalized result
Damped Oscillator Regime Product Dimensions
Two damped-oscillator product constructions share a dimension before forming a difference and a dimensionless bookkeeping quotient.
Quantum theory · Formalized result
Two-Qubit Pauli-String Tensor Bridge
Two ordered one-qubit Pauli factors combine through a finite tensor-order bridge into one two-qubit matrix value.
Units and dimensions · Formalized result
Lennard-Jones Monomial Unit Dimensions
Two Lennard-Jones-style monomial branches cancel different powers of one length scale into the same energy dimension.
Units and dimensions · Formalized result
Harmonic Oscillator Unit Dimensions
Two scalar harmonic-oscillator products share an energy dimension while remaining separate physical values.
Mechanics · Formalized result
Autonomous Hamiltonian Energy Conservation
Supplied coordinate derivative contributions cancel pointwise under the finite canonical Hamilton equations.
Physics formalizations · Formalized result
Two-Anchor Polynomial Certificate
Two fixed anchors constrain one candidate locus and a compact finite residual-certificate construction.
Quantum theory · Formalized result
Finite Lindblad Trace-Preservation Seed
The retained finite Lindblad right-hand side balances algebraically to zero trace.
Units and dimensions · Formalized result
Harmonic Oscillator Frequency Scale
Two separate finite bookkeeping routes terminate in the same frequency-squared dimension class.
Quantum theory · Formalized result
Conditional Hellmann-Feynman Differentiated-Eigenbranch Wrapper
A supplied differentiable eigenbranch carries a local tangent through a finite spectral family.
Units and dimensions · Formalized result
Electromagnetic Energy And Poynting Unit Dimensions
Scalar electromagnetic constructions sort into reviewed energy-density, energy-flux, and impedance dimension classes.
Mechanics · Formalized result
Reduced Vertical Noether Charge Seed
A vertical infinitesimal displacement and momentum pairing form one reduced pointwise Noether-charge cancellation seed.
Physics formalizations · Formalized result
Finite XY Global Rotation Invariance
One global planar rotation turns every spin in the same finite XY configuration while preserving its pairwise geometry.
Quantum theory · Formalized result
One-Qubit Pauli-String Matrix Bridge
One-site Pauli-string values pass through an explicit two-element reindexing into the one-qubit gate-matrix representation.
Units and dimensions · Theorem Target
Dimensional Homogeneity
Distinct additive terms must share the same dimensional profile before a homogeneous combination is even well-formed.
Physics formalizations · Formalized result
Elastic Collision Polynomial Certificate
Paired before-and-after states share momentum and energy constraint geometry around one finite algebraic certificate.
Mathematical analysis · Formalized result
Classical Wave Energy Conservation
Time-change and spatial-gradient strands meet at one local wave-energy junction and continue as directed pointwise flux.
Units and dimensions · Definition
SI Base Units
Seven SI calibration channels form one convention layer aligned with, but distinct from, an underlying dimension lattice.
Quantum theory · Formalized result
Bell-State Preparation by Hadamard and CNOT
A balanced first-qubit operation followed by fixed upper-control lower-target coupling prepares one two-component Bell-state vector.
Mechanics · Formalized result
Reduced Autonomous Lagrangian Energy Cancellation
Two grouped inputs from a supplied joint derivative interface cancel at one reduced pointwise Lagrangian junction.
Quantum theory · Formalized result
Finite CPTP Stinespring Dilation
A selected finite environment and enlarged unitary realize one channel after two specified subsystem traces.
Physics formalizations · Formalized result
Finite Canonical Log-Partition Derivative
A finite Gibbs-weight family at a selected inverse temperature is paired with the local log-partition derivative.
Physics formalizations · Formalized result
Polynomial Constraint Circle-Line Certificate
Circle-line constraints feed a finite algebraic elimination picture and a narrow certificate candidate set.
Quantum theory · Formalized result
Finite CPTP Relative Entropy Data Processing
The same finite CPTP channel acts on an ordered state pair without increasing their relative-entropy distinguishability.
Mathematical analysis · Formalized result
Poisson-Coulomb Source Divergence Bridge
A translated point source anchors open inverse-square bundles and a distributional divergence-source bridge.
Units and dimensions · Formalized result
Free-Space Vacuum-Impedance Unit Bridge
Two wrapped FreeSpace scalar constants combine through a unit bridge into one impedance-dimension scalar form.
Mechanics · Formalized result
Hamiltonian Liouville Density-Form Bridge
Local conservative and transport descriptions meet on one finite-coordinate Hamiltonian density tile.
Physics formalizations · Formalized result
Finite Lieb-Yngvason Accessibility Scaffold
A finite accessibility preorder shows only the reviewed orientation, reflexivity, and transitivity scaffold.
Quantum theory · Formalized result
Mixed-State Computational-Basis Diagonal Measurement
One fixed computational-basis measurement reads the finite mixed-state diagonal into a discrete probability distribution.
Mechanics · Formalized result
Hamiltonian First Integral by Poisson Commutation
A vanishing canonical Poisson pairing leaves one finite-dimensional observable contour locally unchanged.
Mechanics · Formalized result
Finite-Dimensional Virial Identity Seed
Position-momentum pairing, an instantaneous tangent, kinetic contribution, and conservative-force term meet in one finite virial identity seed.
Units and dimensions · Definition
Dimension Algebraic Structure
Physical dimensions compose as finite signed exponent data over a selected anonymous basis.
Units and dimensions · Convention Bridge
Natural Units c = hbar = 1
Two distinct calibration channels set light propagation and quantum action to normalized standards while retaining dimensional memory.
Quantum theory · Formalized result
Finite-Dimensional Kato Projection Calculus Seed
A local finite-dimensional idempotent-curve tangent occupies the cross-block sector and returns through nested commutator geometry.
Units and dimensions · Formalized result
Pendulum Dimensionless Parameter
A still dimensional ledger cancels acceleration, length, and repeated time factors into a dimensionless pendulum parameter.
Physics formalizations · Formalized result
Charge Continuity from Maxwell Identities
Paired local Maxwell curl channels cancel into one pointwise charge-current continuity junction.
Units and dimensions · Problem
Reynolds Number Dimensionless Check
Density, speed, length, and dynamic-viscosity dimensions cancel pairwise into one empty dimensionless aperture.
Units and dimensions · Problem
Buckingham Pi Basic Example
A bounded chosen variable set passes through finite dimension-vector organization to one schematic dimensionless combination.
Units and dimensions · Problem
Maxwell Equations Dimension Check
Three local Maxwell-term comparison lanes expose dimensional bookkeeping and one unresolved record.
Conventions · Convention Bridge
SI vs Natural Units
One physical subject passes between distinct SI-like and natural-unit-like coordinate frames without discarding scale information.
Mathematical analysis · Formalized result
Distributional Irrotational Coulomb Field
Quiet equipotential shells and untwisted radial spokes picture the distributionally irrotational Coulomb field.
Quantum theory · Formalized result
Finite Periodic Circulant Fourier-Mode Theorem
A finite periodic circulant rule preserves one discrete Fourier-mode pattern up to a common complex multiplier.
Quantum theory · Definition
Pauli Matrices: Basic Definition
Three finite two-by-two matrix plaques encode the basic one-qubit Pauli family, with identity context kept separate.
Units and dimensions · Convention Bridge
Planck Units Base Dimension Bridge
Four selected physical ingredients braid into explicit length, time, mass, and temperature scale records.
Physics formalizations · Formalized result
Bernoulli Endpoint Equality Along One Streamline
One streamline connects two endpoints while pressure, speed, and elevation contributions trade across the path.
Physics formalizations · Formalized result
Scalar Rankine–Hugoniot Orientation from Moving-Frame Balance
Two scalar states meet at one translating interface whose moving-frame fluxes are supplied as equal.
Quantum theory · Formalized result
Finite-Dimensional Matrix-Exponential Frechet Derivative
A bounded seven-sample ordered family assembles the finite matrix-exponential Frechet derivative into one matrix output.
Quantum theory · Theorem Target
Pauli Matrix Commutation Relations
Three one-qubit Pauli operators follow an order-sensitive cyclic commutator orientation.
Conventions · Convention Bridge
Fourier: Physics vs Mathlib Conventions
Two Fourier convention systems organize the same oscillatory subject with different phase, frequency, measure, and normalization choices.
Physics formalizations · Formalized result
EM Poynting Local Conservation
A close-up field patch relates local electromagnetic energy change, Poynting flow, and current work.
7-step walkthrough · 201 walkthrough declaration lines
Quantum theory · Theorem Target
Wick's Theorem for Time-Ordered Fields
A finite field list branches into partial Wick contractions, including normal-ordered uncontracted fields.
Physics formalizations · Theorem Target
Gauss and Ampère–Maxwell from the Field Action
This theorem presents two recognizable Maxwell equations while retaining the exact variational and matrix-valued formal statement supported by PhysLib.
Physics formalizations · Theorem Target
Lorentz Covariance of the Electromagnetic Field Equation
Lorentz covariance is the defining synthesis of electromagnetism and special relativity, and this proof follows the transformed tensor equation explicitly.
Mathematical analysis · Theorem Target
Joint Convexity of Ando’s Trace Functional
Ando's joint-convexity theorem is a central operator inequality whose sharply defined exponent region organizes important finite-dimensional trace functionals.
Quantum theory · Theorem Target
Finite-Dimensional Unitary Dilation of a Quantum Channel
Unitary dilation is a foundational structural theorem explaining finite quantum channels as reversible dynamics on a larger system.
Quantum theory · Theorem Target
Kadison–Schwarz for Completely Positive Subunital Maps
Kadison–Schwarz is a foundational structural inequality for positive maps, and PhysLib's concrete finite-matrix proof exposes Kraus positivity, block matrices, and a Schur-complement argument.
Geometry · Definition
Boost–Rotation Coordinates for the Restricted Lorentz Group
The decomposition gives a global coordinate picture of the proper orthochronous Lorentz subgroup in terms of the two familiar ingredients: relativistic velocity and spatial rotation.
Physics formalizations · Theorem Target
Electric-Field Wave Equation with Charge and Current Sources
The result makes explicit how charge gradients and changing currents drive electric waves under the smooth Maxwell field equations encoded by PhysLib.
Quantum theory · Theorem Target
Lieb's Trace Functional Is Jointly Concave
Lieb's concavity theorem is a famous trace inequality underpinning major monotonicity and entropy results in quantum information.
Quantum theory · Theorem Target
The Position–Momentum Commutator on Schwartz Space
The canonical position–momentum commutator is among quantum mechanics's most famous formulas, and the Schwartz-space statement makes its otherwise delicate operator domain explicit.
Mathematical analysis · Theorem Target
Shannon Entropy Bound in Finite Dimension
The finite maximum-entropy bound is a foundational theorem shared by information theory and statistical mechanics, with a direct geometric explanation on the probability simplex.
Mechanics · Theorem Target
Uniqueness of Harmonic-Oscillator Motion
This is a proof-rich uniqueness result that turns the explicit formula from one candidate solution into the only smooth solution with the prescribed initial data.
Physics formalizations · Theorem Target
The Electromagnetic Lagrangian in E, B, Charge, and Current
The theorem exposes the recognizable electric, magnetic, charge, and current content hidden inside PhysLib's covariant field Lagrangian.
Quantum theory · Theorem Target
Every Finite-Dimensional Mixed State Has a Purification
Purification is a basic structural fact behind entanglement and many channel and entropy arguments.
Physics formalizations · Theorem Target
Every Future-Cone Vector Is a Two-Higgs Gram Vector
The theorem turns the four gauge-invariant Gram coordinates into an exact future-cone geometry rather than only an orbit label.
Physics formalizations · Theorem Target
Positive Quartic Form Implies Stability of the Two-Higgs-Doublet Potential
Boundedness of the 2HDM scalar potential is a physically consequential theorem, and this proof exposes a substantive compactness argument.
Geometry · Theorem Target
Lorentz Invariance of the Minkowski Product
Preservation of the Minkowski product is the defining geometric invariant behind Lorentz transformations and gives the collection a direct spacetime theorem.
Quantum theory · Theorem Target
The Löwner–Heinz Operator Monotonicity Theorem
The Löwner–Heinz theorem is a landmark noncommutative order result: fractional powers preserve positive-operator order.
Physics formalizations · Theorem Target
Electric Field Parallel to an Axis Boost
The parallel electric sector isolates the invariant part of the electromagnetic Lorentz-transformation law and provides a clean counterpart to transverse electric–magnetic mixing.
Physics formalizations · Theorem Target
Mixed Magnetic Components Under an Axis Boost
This is the magnetic counterpart of transverse electric mixing and exposes the reciprocal beta-over-c coefficient in PhysLib's matrix convention.
Physics formalizations · Theorem Target
Transverse Electric Field Under an Axis Boost
The theorem displays the familiar electric-magnetic mixing that makes electromagnetic Lorentz covariance physically concrete.
Mathematical analysis · Theorem Target
Araki–Lieb–Thirring Trace Inequality
The Araki–Lieb–Thirring inequality is a major bridge between spectral matrix powers and trace comparison, with applications across operator theory and quantum information.
Quantum theory · Theorem Target
Quantum Channels Cannot Improve Binary Hypothesis Testing
Data processing for binary quantum hypothesis testing gives an operational expression of information loss: a channel cannot make two finite quantum states easier to distinguish at a fixed type-I error tolerance.
Physics formalizations · Theorem Target
The Covariant Maxwell Equation from the Field Lagrangian
The covariant inhomogeneous Maxwell equation is a central landmark, and this theorem ties it exactly to PhysLib's field-action extremum predicate.
Quantum theory · Theorem Target
Complementary Subsystems of a Pure State Have Equal Entropy
Equality of complementary pure-state entropies is the central finite-dimensional signature of bipartite entanglement.
Geometry · Theorem Target
Coordinate Formula for an Axis-Aligned Lorentz Boost
This theorem is a substantive and immediately recognizable coordinate-level Lorentz transformation, with all time, parallel, and transverse cases visible in one checked declaration.
Quantum theory · Theorem Target
Choi's Theorem for Completely Positive Maps
Choi's theorem is the central finite-dimensional bridge between complete positivity and matrix positivity.
Quantum theory · Theorem Target
Harmonic-Oscillator Eigenfunctions Solve the Schrödinger Equation
The quantized harmonic-oscillator spectrum and Hermite–Gaussian eigenfunctions are among quantum mechanics' most recognizable exact solutions.
Quantum theory · Theorem Target
Orthonormal Harmonic-Oscillator Eigenfunctions
Orthonormality is a central spectral fact for the quantum harmonic oscillator and supplies a clear bridge between explicit Hermite-Gaussian wavefunctions and Hilbert-space geometry.
Quantum theory · Theorem Target
Pure-State Separability from the Reduced State
The theorem gives a standard and operationally meaningful entanglement test for pure bipartite states, connecting tensor-product structure to a directly computed reduced density matrix.
Quantum theory · Theorem Target
Sandwiched Rényi Data Processing
A finite-dimensional CPTP channel cannot increase PhysLib's sandwiched Rényi relative entropy for alpha at least one.
Mechanics · Theorem Target
The Explicit Harmonic-Oscillator Trajectory
The explicit oscillator solution is universally recognizable and adds a trajectory-level theorem distinct from the existing conservation-law landmark.
Physics formalizations · Theorem Target
Magnetic-Field Wave Equation with Current Sources
The theorem derives an explicit sourced magnetic wave equation from the field equations rather than checking one preselected plane-wave solution.
Mathematical analysis · Theorem Target
Inverse Temperature as an Entropy–Energy Derivative Ratio
This is a recognizable thermodynamic derivative identity presented with the exact analytic and nondegeneracy conditions that make the quotient meaningful.
Quantum theory · Theorem Target
Angular Momentum Generates the so(d) Commutation Algebra
The angular-momentum commutation algebra is the operator form of rotational symmetry in arbitrary dimension.
Geometry · Theorem Target
Path-Connected Relativistic Velocity Space
Path-connectedness turns the local unit-hyperboloid constraint into a global topological statement and adds a visually compelling relativity theorem not already represented by a coordinate identity.
Quantum theory · Theorem Target
Strong Subadditivity of Quantum Entropy
Strong subadditivity is one of quantum information theory's central inequalities and governs how correlations and conditional entropy can be distributed across three systems.
Physics formalizations · Theorem Target
Purely Transverse Magnetic Matrix Components Under an Axis Boost
The transverse–transverse magnetic sector identifies the part of the antisymmetric field matrix that an axis boost leaves unchanged apart from evaluation at the transformed event.
Mechanics · Theorem Target
Velocity-Only Total Derivatives Are Linear
Total-derivative equivalence is central to Lagrangian mechanics, and this theorem gives a concrete finite-dimensional characterization instead of only motivational prose.
Physics formalizations · Theorem Target
Every CKM Matrix Has the Standard Four-Parameter Form, up to Rephasing
The standard three-angle, one-phase CKM parameterization is the canonical description of quark flavor mixing.
Quantum theory · Theorem Target
The Araki–Lieb Entropy Inequality
The Araki–Lieb inequality is the triangle inequality complement to entropy subadditivity.
Mathematical foundations · Theorem Target
Generic Even Pure-U(1) Anomaly Solutions Are Parameterized
The theorem gives a constructive rational parameterization for the generic branch across an infinite sequence of even pure-U(1) charge counts.
Mathematical foundations · Theorem Target
Generic Odd Pure-U(1) Anomaly Solutions Are Parameterized
This is the odd-charge-count counterpart of the constructive rational anomaly-solution parameterization and completes a natural parity pair.
Quantum theory · Theorem Target
Kraus Representation of Completely Positive Maps
The Kraus representation is the standard finite-dimensional operator-sum description of completely positive dynamics.
Mechanics · Theorem Target
The Variational Gradient Is the Euler–Lagrange Operator
Position and velocity variation channels recombine into PhysLib's pointwise Euler–Lagrange operator.
Quantum theory · Theorem Target
Subadditivity of Von Neumann Entropy
Entropy subadditivity is a foundational statement that total uncertainty cannot exceed the sum of marginal uncertainties.
Physics formalizations · Theorem Target
Plane-Wave Magnetic Field from the Electric Field
The transverse electric-magnetic geometry of a plane wave is visually and physically important, while the retained theorem makes its additive-constant boundary explicit.
Quantum theory · Theorem Target
Canonical Position–Momentum Commutation in d Dimensions
This is the multidimensional canonical commutation relation, with off-diagonal commutators and the Schwartz-space domain made explicit.
Mathematical foundations · Theorem Target
Gamma Matrices Generate the Dirac Algebra
Gamma matrices and Clifford algebras are central to relativistic quantum theory, and the theorem exposes their exact generated-algebra relationship.
Mechanics · Theorem Target
Harmonic Oscillator Energy Conservation
An undamped one-dimensional spring oscillator exchanges kinetic and potential energy around one closed cycle.
Physics formalizations · Theorem Target
An Ideal-Gas Adiabatic Product Law
The theorem is a substantial positive-domain derivation of a dimensionless adiabatic invariant directly from an explicit ideal-gas entropy formula.
Quantum theory · Theorem Target
No-Cloning: Two Nonidentical Perfectly Cloneable Pure States Must Be Orthogonal
One shared unitary can perfectly clone a nonidentical pair only when their transition probability is zero.
Mechanics · Theorem Target
Damped-Oscillator Solutions in All Three Regimes
The damping trichotomy is a standard physics classification and offers three visibly distinct trajectories tied together by one checked theorem.
Geometry · Theorem Target
Twin-Paradox Example: 15 Versus 9
A concrete, memorable numerical twin-paradox calculation makes invariant proper time immediately legible without claiming a general acceleration model.
Mathematical analysis · Theorem Target
Mean Energy of a Canonical Two-State System
The two-level system is a central exactly solvable statistical-mechanics model, and the tanh form exposes both the energy midpoint and temperature-dependent bias.
Physics formalizations · Theorem Target
A Harmonic Electromagnetic Wave Solves the Free-Space Field Equations
An explicit source-free wave solution connects the electromagnetic potential, its derived fields, and the Euler–Lagrange equations in one visually legible theorem.
Mechanics · Theorem Target
Circular-Orbit Speed: v² = GM/r
The circular-orbit speed formula is widely recognizable, while this exact declaration is a useful API lemma exposing the square of PhysLib's already-defined positive speed.
Mathematical analysis · Theorem Target
Smooth Plane Waves Solve the Wave Equation
Plane-wave reduction is a foundational method across acoustics, electromagnetism, elasticity, and quantum theory, and the theorem supports a clear derivative-based walkthrough.
Physics formalizations · Theorem Target
The Ideal-Gas Law from PhysLib's Phase-Space Model
A cubic-box phase-space model leads from a partition function to the dimensionless relation P V = n T.
Mathematical foundations · Theorem Target
One-Family Gauge Anomalies Force the Gravitational Condition
The theorem records a striking dependency among anomaly equations: in the one-family rational model, the gravitational condition follows from the others.
Mathematical analysis · Theorem Target
Schatten–Hölder Inequality for Matrix Products
Schatten–Hölder is a major noncommutative norm inequality and exposes the singular-value machinery supporting many quantum-information estimates.
Mathematical foundations · Theorem Target
A Seven-Dimensional Family of Anomaly-Free Charges
The theorem turns anomaly cancellation into explicit high-dimensional algebra: seven independent rational charge patterns generate an entire family of solutions.
Quantum theory · Theorem Target
Channel Duality Preserves Expectation Values
The equality is the defining bridge between the Schrödinger state picture and Heisenberg observable picture for finite quantum channels.
Quantum theory · Theorem Target
Quantum Relative Entropy Adds across Product States
Product additivity is a defining structural property of quantum relative entropy and underlies independent-system calculations throughout quantum information.
Mathematical analysis · Theorem Target
Helmholtz Free Energy of a Product Ensemble
The result formalizes the familiar composition law for independent canonical systems and exposes the precise partition-function and phase-space assumptions behind the free-energy sum.
Geometry · Theorem Target
A Generalized Lorentz Boost Between Velocities
The theorem makes a geometric existence statement concrete: an explicit Lorentz transformation transports any normalized future velocity to another.
Quantum theory · Theorem Target
Harmonic-Oscillator Eigenfunctions Span the Hilbert Space—Assuming Plancherel
Completeness of Hermite eigenfunctions is a central spectral fact for the quantum harmonic oscillator, and the formal proof architecture reveals exactly where Plancherel enters.
Quantum theory · Theorem Target
The Pinching Inequality
The pinching inequality is a named operator bound central to matrix estimates and quantum-information asymptotics.
Mathematical analysis · Theorem Target
Rotfel’d Trace Subadditivity
Rotfel'd's inequality is a recognizable noncommutative trace-power result whose exact distinction between trace subadditivity and operator subadditivity is worth making explicit.
Physics formalizations · Theorem Target
Gauge Invariance of the Two-Higgs-Doublet Potential
Gauge invariance is the defining structural consistency check for a scalar potential in a gauge theory.
Quantum theory · Theorem Target
Nonnegative Logarithmic Core of Quantum Relative Entropy
Nonnegativity is a foundational property of quantum relative entropy, while this declaration's exact support-aware logarithmic expression also illustrates how the α → 1 Rényi limit is used formally.
Physics formalizations · Theorem Target
CKM Row Normalization from Unitarity
Row normalization is the most direct experimentally recognizable CKM unitarity sum rule.
Quantum theory · Theorem Target
The Dual of a Trace-Preserving Matrix Map Is Unital
The theorem is the structural bridge behind the Schrödinger and Heisenberg descriptions of finite-dimensional quantum dynamics, linking normalization of states to preservation of the identity observable.
Physics formalizations · Theorem Target
Uniform Electric and Magnetic Fields Solve the Vacuum Field Equation
Uniform electric and magnetic fields are among the simplest exact Maxwell configurations, and PhysLib connects their explicit potential directly to its variational free-space field equation.
Mathematical analysis · Theorem Target
Nonnegativity of Finite Canonical Entropy
Nonnegative discrete entropy is a basic consistency property of finite statistical mechanics, reflecting that every canonical probability lies between zero and one.
Mathematical analysis · Theorem Target
Horn's Weak Log-Majorization for Singular Values
Horn's inequality is the structural singular-value theorem that drives a broad family of matrix product norm bounds.
Mathematical analysis · Theorem Target
Joint Concavity of the Operator Power Mean
Joint concavity of operator means is a high-value theorem in noncommutative analysis with applications to quantum trace inequalities.
Quantum theory · Theorem Target
Lower Semicontinuity of Quantum Relative Entropy
Lower semicontinuity is the analytic compactness property that lets relative entropy behave correctly in optimization and limiting arguments.
Quantum theory · Theorem Target
Relative-Entropy Pythagoras for Spectral Pinching
This exact entropy decomposition gives spectral pinching a geometric projection interpretation and connects operator structure to information loss.
Mathematical analysis · Theorem Target
Trace Young Inequality for Positive Matrices
The trace Young inequality is a useful noncommutative bridge from scalar convexity to matrix trace estimates.
Quantum theory · Theorem Target
Wick Expansion for a Time-Ordered Normal Product
The normal-ordered form of Wick's theorem is a standard perturbative-QFT identity and exposes how equal-time restrictions alter the allowed contraction family.
Physics formalizations · Theorem Target
Minima of the Quartic Higgs Potential
The theorem formalizes the recognizable symmetry-breaking geometry of a quartic Higgs potential while keeping the exact sign convention and pointwise boundary visible.
Quantum theory · Theorem Target
Quantum Mutual Information as Relative Entropy
This identity gives quantum mutual information its fundamental geometric interpretation as distinguishability from the uncorrelated product of the marginals.
Mathematical analysis · Theorem Target
Canonical Ensemble: F = U − TS
The identity F = U − TS is a central thermodynamic relation, and this theorem exposes how PhysLib's probability normalization and phase-space entropy correction enter it.
Physics formalizations · Theorem Target
Polarization Ellipse of a Harmonic Electromagnetic Wave
Polarization geometry supplies a new observable-facing result beyond the existing plane-wave solution and E-B relation pages.
Quantum theory · Theorem Target
Purity One Characterizes Pure Quantum States
The scalar test Tr(rho squared)=1 is the standard finite-dimensional criterion separating pure states from genuinely mixed states.
Quantum theory · Theorem Target
Entanglement of Formation of a Maximally Entangled State
The result gives a clean quantitative value to maximal bipartite entanglement and connects a convex-roof resource measure to the local Hilbert-space dimension.
Quantum theory · Theorem Target
Harmonic-Oscillator Eigenfunctions Have Alternating Parity
Alternating parity is a memorable symmetry property of the oscillator eigenbasis and explains its even/odd wavefunction pattern.
Geometry · Theorem Target
SL(2,C) Matrices Induce Lorentz Transformations
The map from SL(2,C) to Lorentz transformations is the algebraic bridge between two-component spinors and four-dimensional spacetime symmetry.
Physics formalizations · Theorem Target
The Complex CKM Quartet Is Rephasing-Invariant
Rephasing invariance isolates physical content from arbitrary fermion phase choices and gives a compact formal view of the complex quartet behind the Jarlskog invariant.
Quantum theory · Theorem Target
A Pure Bipartite State Is Separable Exactly When It Is a Product
For pure bipartite states, product factorization is the clean algebraic boundary between separability and entanglement.
Quantum theory · Theorem Target
Characterization of Finite Unitary Quantum Channels
The result makes the abstract unitary-channel predicate concrete as the familiar transformation rho maps to U rho U-star on every state.
Mathematical analysis · Theorem Target
Operator Monotonicity of the Matrix Logarithm
Operator monotonicity of logarithm is a central matrix-analysis theorem used throughout quantum entropy and relative-entropy arguments.
Quantum theory · Theorem Target
Spectral Decomposition of a Finite Quantum State
The spectral decomposition is the central finite-dimensional structure theorem for density matrices and gives a direct bridge from operator spectra to ensembles of pure states.
Quantum theory · Theorem Target
Spectral Pinching Is Idempotent
Idempotence captures the physical and algebraic meaning of pinching as removal of coherence between fixed spectral sectors.
Mathematical analysis · Theorem Target
Thermodynamic Entropy Equals Shannon Entropy for Finite Ensembles
The theorem pinpoints when thermodynamic entropy and the information-theoretic Shannon formula are literally the same quantity: PhysLib's discrete finite canonical convention.
Mathematical foundations · Theorem Target
An Exceptional Even U(1) Orbit Has a Basis-Plane Representative
The result gives a concrete geometric restriction on an exceptional even-charge branch: under its strong all-permutations hypothesis, the orbit reaches a designated rational basis plane.
Geometry · Theorem Target
Four-Velocity Lies on the Unit Timelike Hyperboloid
Although mechanically short because the invariant is built into the subtype, this equation is the geometric signature of relativistic four-velocity and complements Lorentz invariance.
Quantum theory · Theorem Target
Von Neumann Entropy Is at Most log d
The dimension bound is the basic entropy ceiling for finite quantum systems.
Quantum theory · Theorem Target
A POVM Channel Produces Its Outcome Distribution
The theorem gives a precise finite-dimensional bridge from a POVM channel to its classical Born-rule outcome distribution.
Quantum theory · Theorem Target
Peierls' Inequality for Hermitian Matrices
Peierls' inequality is a classic spectral-to-diagonal convexity result used throughout statistical mechanics and quantum information.
Mathematical analysis · Theorem Target
Temperature and Inverse-Temperature Entropy Formulas Agree
The theorem makes a delicate change of thermodynamic parameter explicit and retains the analytic assumptions needed for differentiating the partition function.
Physics formalizations · Theorem Target
Pauli-Minkowski Anticommutator Identity
The symmetrized Pauli contraction is the Weyl-spinor form of the spacetime Clifford relation, tying spinor indices directly to the Minkowski metric.
Physics formalizations · Theorem Target
An Infinite Straight Wire Solves the Maxwell Extremum Equation
An infinite straight wire is one of electromagnetism's canonical singular sources, and this theorem checks its field equation at the distributional level where the wire itself is included.
Mathematical foundations · Theorem Target
If Every Permutation Is Exceptional, the Odd U(1) Charge Vector Vanishes
The exceptional odd branch has a sharp algebraic conclusion: the strong all-permutations exceptional-case hypothesis forces the underlying rational charge vector to vanish.
Mathematical analysis · Theorem Target
Sion's Minimax Theorem
Sion's theorem is a widely used minimax principle underlying optimization arguments in information theory, game theory, and variational analysis.
Mathematical analysis · Theorem Target
Energy Variance Identity
The decomposition Var(E)=⟨E²⟩-⟨E⟩² is the moment identity underlying canonical energy fluctuations and later heat-capacity relations.
Quantum theory · Theorem Target
Full Wick Pairings Are Counted by a Double Factorial
The double-factorial count is the familiar combinatorial growth law behind complete Wick pairings.
Mathematical analysis · Theorem Target
Heat Capacity from Energy Fluctuations
The finite canonical fluctuation relation is a foundational bridge between microscopic energy variation and a macroscopic thermal response, and its finite-state hypotheses are unusually explicit.
Geometry · Theorem Target
Timelike Separation Has Positive Proper Time
Positive elapsed proper time for timelike separation is a fundamental causal-geometric fact and a clean precursor to the twin-paradox example.
Physics formalizations · Theorem Target
Canonical Electromagnetic Momentum from the Electric Field
Canonical momentum is the bridge from the electromagnetic Lagrangian to Hamiltonian dynamics.
Mathematical analysis · Theorem Target
Logarithm of a Kronecker Product
The tensor-logarithm identity is a compact but powerful structural fact behind entropy and relative-entropy additivity calculations.
Mathematical analysis · Theorem Target
Operator Concavity of the Matrix Logarithm
Operator concavity of logarithm is a foundational noncommutative Jensen inequality with direct importance for quantum entropy.
Quantum theory · Theorem Target
Quantum Effects Have Probabilistic Expectation Values
The interval bound is the minimal mathematical reason that an effect expectation can serve as a probability in finite quantum measurement.
Quantum theory · Theorem Target
Quantum Mutual Information Is Symmetric under Subsystem Swap
Mutual information measures shared correlations without privileging either subsystem, and swap symmetry expresses that principle exactly.
Quantum theory · Theorem Target
The Maximally Entangled-State Transpose Trick
The transpose trick is an iconic finite-dimensional identity behind channel-state duality, teleportation algebra, and tensor-network manipulations.
Quantum theory · Theorem Target
Trace Distance as an Eigenvalue Sum
Trace distance is one of quantum information's standard state distances, and its spectral formula makes the matrix norm directly interpretable.
Quantum theory · Theorem Target
Plane-Wave Eigenstates of a Tight-Binding Chain
The cosine band of a nearest-neighbor lattice is one of condensed matter physics's most recognizable formal structures, and the theorem connects it directly to a finite Hamiltonian eigenvalue equation.
Physics formalizations · Theorem Target
A Bounded Higgs Potential Requires Nonnegative Quartic Coupling
The sign of the quartic coupling controls the large-field tail of the classical Higgs potential, so nonnegativity is a necessary obstruction to runaway instability.
Physics formalizations · Theorem Target
Gauss's Law for a Point Charge, Distributionally
The point-charge singularity is exactly where a pointwise account of Gauss's law fails, making the distributional theorem both physically familiar and mathematically revealing.
Mathematical analysis · Theorem Target
Mean Energy as the Negative Beta Derivative of log Z
The logarithmic partition function is the generating object for equilibrium thermodynamics; recovering mean energy from its beta slope connects the ensemble definition to practical calculations.
Quantum theory · Theorem Target
Plane Waves as Generalized Momentum Eigenvectors
The theorem connects translation frequency to momentum and records the exact 2π normalization imposed by PhysLib's ordinary-frequency Fourier convention.
Physics formalizations · Theorem Target
Electromagnetic Hamiltonian in Electric and Magnetic Variables
The Hamiltonian expression complements the Lagrangian page while retaining the exact potential-current terms.
Geometry · Theorem Target
Spatial Rotations Lie in the Restricted Lorentz Group
Embedding ordinary spatial rotations into the proper orthochronous Lorentz group confirms that familiar rotational symmetry lies in the physically connected spacetime sector.
Physics formalizations · Theorem Target
Two-Higgs-Doublet Gauge Orbits Classified by the Gram Vector
Completeness of the Gram vector turns four real gauge invariants into a full classifier of PhysLib's two-Higgs-doublet gauge orbits.
Quantum theory · Theorem Target
Fidelity One Characterizes Identical Quantum States
Fidelity is a standard measure of state similarity, and the sharp equality case explains why its top value means indistinguishable density states.
Physics formalizations · Theorem Target
CKM Column Normalization
Column normalization is a direct observable consequence of CKM unitarity and complements the already displayed row normalization constraints.
Quantum theory · Theorem Target
Continuity of Finite-Dimensional von Neumann Entropy
Continuity is the basic stability property that makes finite-dimensional entropy robust under small state perturbations.
Quantum theory · Theorem Target
The Angular-Momentum Casimir Commutes with Every Generator
Commutation of the quadratic Casimir with every generator encodes rotational invariance and organizes angular-momentum representations.
Mechanics · Theorem Target
Hamilton's Equations from a Variational Gradient
This theorem exposes the mechanism behind Hamilton's equations: the phase-space action gradient is exactly the pair of equation residuals, rather than merely quoting the final dynamics.
Mathematical analysis · Theorem Target
Finite Boltzmann Probabilities Sum to One
A finite canonical ensemble becomes a probability model only after its Boltzmann weights are proved to normalize, making this the entry point for every later expectation and entropy calculation.
Physics formalizations · Theorem Target
CKM Row Orthogonality and a Unitarity Triangle
The three-term row-orthogonality relation is the exact complex-vector closure behind a CKM unitarity triangle and CP-violation geometry.
Mechanics · Theorem Target
Damped Oscillator Energy Loss Rate
The formula pinpoints where oscillator energy goes: linear damping converts the conservative energy balance into an exact negative squared-speed term.
Geometry · Theorem Target
Every Three-Dimensional Rotation Has a Fixed Axis
A fixed axis is the geometric content of every proper three-dimensional rotation and underlies axis-angle coordinates and rigid-body kinematics.
Mechanics · Theorem Target
Periodicity of the Classical Harmonic Oscillator
Exact return after 2π/ω is the defining temporal signature of the undamped harmonic oscillator and makes the frequency parameter physically interpretable.
Quantum theory · Theorem Target
Zero Quantum Variance Exactly Characterizes Eigenstates
It formalizes the textbook statement that an observable has a perfectly sharp value in a normalized state exactly when that state is an eigenstate.
Geometry · Theorem Target
Exponentiating the Lorentz Algebra
The exponential map is the concrete bridge from infinitesimal Lorentz generators to finite transformations connected to the identity.
Mathematical analysis · Theorem Target
Orthogonality of the Physicists' Hermite Polynomials
Gaussian-weighted Hermite orthogonality is the analytic mechanism separating harmonic-oscillator modes into distinct quantum states.
Quantum theory · Theorem Target
Position States as Generalized Position Eigenvectors
Ideal position states are not square-integrable wavefunctions; this theorem gives their correct role as generalized eigenvectors acting on Schwartz test functions.
Quantum theory · Theorem Target
Quantum Conditional Mutual Information Is Nonnegative
QCMI is a central measure of correlations remaining between A and C when B is known.
Mathematical analysis · Theorem Target
Schur Decomposition
Schur decomposition is the universal unitary triangularization behind spectral analysis of finite complex operators, including non-normal Hamiltonian and channel matrices.
Quantum theory · Theorem Target
A Generalized Quantum Stein Limit for Free States
The theorem links asymptotic quantum hypothesis testing to a regularized resource measure, unifying an operational task and an entropy quantity in a substantial formal result.
Mechanics · Theorem Target
Symmetry of the Inertia Tensor
Inertia-tensor symmetry is the exact checked structural result that underlies the familiar principal-axis picture of rigid-body mechanics.
Search and filters always include every public topic.
