formal librarypublicsource:physlib

The Physlib community

Native namespace leanprover-community/physlib:API-map

232 source-native objects · 0 Repository bindings

Native API map

Browse 232 source-attributed requirements from the exact native revision. Implemented and planned are publisher labels, never Vela Standing.

All requirements Planned requirements Implemented requirements

Source-native objects

Stable native key order · 20 shown

Object	Kind	Availability
A gauge (structure) group: the concrete Standard Model group SU(3) x SU(2) x U(1) with its projections and central discrete subgroup api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:1 Gauge theory · source reports implemented source: implemented	api requirement	reference only
The gauge field (connection) in the abelian U(1) case: the electromagnetic potential A^μ as a spacetime-valued Lorentz vector api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:2 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Curvature (field strength) of the abelian gauge field, F^{μν} built from the potential api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:3 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Gauge transformation of the gauge potential in the abelian U(1) case: the pure-gauge potential and the shift A^μ ↦ A^μ + ∂^μ χ api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:4 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Gauge invariance of the field strength under abelian U(1) gauge transformations api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:5 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Pure-gauge (flat) configurations have vanishing curvature, and the bare gradient does not (necessity of the metric contraction) api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:6 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Group structure of gauge transformations: identity shift and composition of successive shifts api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:7 Gauge theory · source reports implemented source: implemented	api requirement	reference only
Compatibility of gauge transformations with the Lorentz group action (equivariance) api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:8 Gauge theory · source reports implemented source: implemented	api requirement	reference only
The key input data structure of the damped harmonic oscillator (mass, spring constant, and damping coefficient) is defined. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:1 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API shall contain the definition of the kinetic energy. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:10 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API shall contain the definition of the potential energy. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:11 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API shall contain the definition of the Lagrangian. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:12 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API shall contain a simplification of the variational gradient of the Lagrangian to the Euler-Lagrange equations. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:13 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API shall prove that the selected trajectory is the unique solution of the equation of motion with the given initial conditions. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:14 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API contains a definition of the equation of motion `m ẍ + γ ẋ + k x = 0`. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:2 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API defines the force `- k x - γ ẋ` and proves the equation of motion is equivalent to Newton's second law. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:3 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API proves that along a solution the mechanical energy dissipates at rate `-γ ‖ẋ‖²` and is strictly decreasing when the velocity is nonzero and `γ > 0`. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:4 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API classifies the underdamped, critically damped, and overdamped regimes via the discriminant `γ² - 4 m k`, and defines the decay rate and the regime-selected angular frequency. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:5 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API reduces the damped oscillator to the undamped harmonic oscillator when `γ = 0`, showing the equations of motion agree. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:6 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only
The API contains a definition of the initial conditions of the damped harmonic oscillator. api-map:Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml#requirement:7 Damped harmonic oscillator · source reports implemented source: implemented	api requirement	reference only

A gauge (structure) group: the concrete Standard Model group SU(3) x SU(2) x U(1) with its projections and central discrete subgroup