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 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
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
A general, system-agnostic `ConfigurationSpace` construction (a configuration manifold abstracting over the choice of mechanical system) usable across the Lagrangian API. api-map:Physlib/ClassicalMechanics/Lagrangian/API-map.yaml#requirement:1 Configuration Space · source reports planned source: planned	api requirement	reference only
A general treatment of generalized coordinates and the velocity phase space (tangent bundle `TQ`) built over a shared configuration-space abstraction, on which a Lagrangian is defined for the Euler-Lagrange API. api-map:Physlib/ClassicalMechanics/Lagrangian/API-map.yaml#requirement:2 Configuration Space · source reports planned source: planned	api requirement	reference only
The API shall contain the structure of a manifold on the configuration space. api-map:Physlib/ClassicalMechanics/Pendulum/API-map.yaml#requirement:2 Configuration space for pendulum · source reports planned source: planned	api requirement	reference only
The API shall contain a map from the configuration space to `Space`, giving the position of the pendulum in real space. api-map:Physlib/ClassicalMechanics/Pendulum/API-map.yaml#requirement:3 Configuration space for pendulum · source reports planned source: planned	api requirement	reference only
The API shall contain the definition of a trajectory based on the configuration space. api-map:Physlib/ClassicalMechanics/Pendulum/API-map.yaml#requirement:4 Configuration space for pendulum · source reports planned source: planned	api requirement	reference only
The API shall subsequently contain the definition of the lagrangian. api-map:Physlib/ClassicalMechanics/Pendulum/API-map.yaml#requirement:5 Configuration space for pendulum · source reports planned source: planned	api requirement	reference only
The API contains the definition of Euler angles for a rigid body. api-map:Physlib/ClassicalMechanics/RigidBody/API-map.yaml#requirement:12 Rigid body · source reports planned source: planned	api requirement	reference only
Redefine `RigidBody` using continuous linear maps instead of plain linear maps from the space of smooth functions to `ℝ` (existing TODO). api-map:Physlib/ClassicalMechanics/RigidBody/API-map.yaml#requirement:13 Rigid body · source reports planned source: planned	api requirement	reference only
The inertia tensor of the solid sphere equals `2/5 m R^2` times the identity. Stated as `solidSphere_inertiaTensor` but currently proved with `sorry`. api-map:Physlib/ClassicalMechanics/RigidBody/API-map.yaml#requirement:8 Rigid body · source reports planned source: planned	api requirement	reference only
The API shall contain the definition of the EM potential from a connection on a U(1)-gauge bundle. This relationship is only noted in the module documentation; no such construction is formalised. api-map:Physlib/Electromagnetism/Kinematics/API-map.yaml#requirement:4 Electromagnetic Potential · source reports planned source: planned	api requirement	reference only
The key data structure for a fluid, given by the spatial distribution of its velocity, density, and pressure, is defined. (FluidFlow currently provides the density and velocity fields; pressure is not a field of the structure and enters separately through the stress laws.) api-map:Physlib/FluidDynamics/API-map.yaml#requirement:1 Fluid · source reports planned source: planned with partial location	api requirement	reference only
Flow out of a volume: the flux of fluid through the boundary of a spatial region. api-map:Physlib/FluidDynamics/API-map.yaml#requirement:2 Fluid · source reports planned source: planned	api requirement	reference only
Definition of the entropy flux density. api-map:Physlib/FluidDynamics/API-map.yaml#requirement:7 Fluid · source reports planned source: planned	api requirement	reference only

A gauge field (connection) for a general/non-abelian structure group, valued in the Lie algebra of G