⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.
Summary
The documentation in Physlib/ClassicalMechanics/EulerLagrange.lean (around line 63) is incorrect.
Current text
- The variational derivative of `L t (q' t) (deriv q' t))` for a lagrangian `L` is equal to the `eulerLagrangeOp`.
Why this is wrong
The docstring for euler_lagrange_varGradient claims the variational derivative of L t (q' t) (deriv q' t) equals eulerLagrangeOp, but this is incorrect. The theorem actually proves that the variational derivative of the action functional — the integral of the Lagrangian over time — equals the Euler-Lagrange operator.
The confusion arises because the docstring refers to the Lagrangian itself rather than its time integral, which is the correct object whose variational derivative yields the operator. The theorem's proof and statement in the code correctly handle the action functional, not the pointwise Lagrangian value.
The correction aligns the documentation with the mathematical content of euler_lagrange_varGradient, which applies to the integral of L over time, ensuring consistency between the declaration and its formal proof.
Suggested correction
- The variational derivative of the action `∫ t, L t (q' t) (deriv q' t)` for a Lagrangian `L` is equal to the `eulerLagrangeOp`.
Summary
The documentation in
Physlib/ClassicalMechanics/EulerLagrange.lean(around line 63) is incorrect.Current text
Why this is wrong
The docstring for
euler_lagrange_varGradientclaims the variational derivative ofL t (q' t) (deriv q' t)equalseulerLagrangeOp, but this is incorrect. The theorem actually proves that the variational derivative of the action functional — the integral of the Lagrangian over time — equals the Euler-Lagrange operator.The confusion arises because the docstring refers to the Lagrangian itself rather than its time integral, which is the correct object whose variational derivative yields the operator. The theorem's proof and statement in the code correctly handle the action functional, not the pointwise Lagrangian value.
The correction aligns the documentation with the mathematical content of
euler_lagrange_varGradient, which applies to the integral ofLover time, ensuring consistency between the declaration and its formal proof.Suggested correction