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.

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
A gauge field (connection) for a general/non-abelian structure group, valued in the Lie algebra of G api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:10 Gauge theory · source reports planned source: planned	api requirement	reference only
The gauge-covariant derivative D = d + A acting on matter fields, and its transformation law api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:11 Gauge theory · source reports planned source: planned	api requirement	reference only
Non-abelian field strength (Yang-Mills curvature) F = dA + A wedge A and its covariant transformation api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:12 Gauge theory · source reports planned source: planned	api requirement	reference only
The Yang-Mills action and its Euler-Lagrange (field) equations api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:13 Gauge theory · source reports planned source: planned	api requirement	reference only
Parallel transport, Wilson lines/loops, and holonomy of the connection api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:14 Gauge theory · source reports planned source: planned	api requirement	reference only
A principal-bundle / fibre-bundle formulation of gauge fields as connections api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:15 Gauge theory · source reports planned source: planned	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
A general abstract gauge group G (an arbitrary Lie group as structure group), not tied to the Standard Model api-map:Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml#requirement:9 Gauge theory · source reports planned source: planned	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

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