Skip to content

auto-task(positionOperatorSchwartz): fix doc-string mislabeling it the parity operator#1362

Open
jstoobysmith wants to merge 1 commit into
leanprover-community:masterfrom
jstoobysmith:auto-docfixer-20260703-131937
Open

auto-task(positionOperatorSchwartz): fix doc-string mislabeling it the parity operator#1362
jstoobysmith wants to merge 1 commit into
leanprover-community:masterfrom
jstoobysmith:auto-docfixer-20260703-131937

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Summary

Fixed one factually incorrect doc-string in
Physlib/QuantumMechanics/OneDimension/Operators/Position.lean.

Location: Physlib/QuantumMechanics/OneDimension/Operators/Position.lean:62

Before → After:

  • Before: /-- The parity operator on the Schwartz maps is defined as the linear map from 𝓢(ℝ, ℂ)to itself, such thatψis taken tofun x => x * ψ x. -/
  • After: /-- The position operator on the Schwartz maps is defined as the linear map from 𝓢(ℝ, ℂ)to itself, such thatψis taken tofun x => x * ψ x. -/

Evidence the original was wrong

The doc-string documents positionOperatorSchwartz
(Position.lean:64),
which is Distribution.powOneMul ℂ — the map ψ ↦ fun x => x * ψ x (confirmed by the
positionOperatorSchwartz_apply simp lemma). Multiplication by the coordinate x is the
position operator, and the enclosing section header (Position.lean:54) reads
"## The position operator on Schwartz maps".

The genuine parity operator is a different declaration, parityOperatorSchwartz
(Parity.lean:52-53),
which maps ψ ↦ fun x => ψ (-x) — not x * ψ x. The old wording was a copy-paste of that
doc-string, mislabeling the position operator as the "parity operator".

How to confirm in one step

Compare the doc-string at Position.lean:62 against the declaration name
positionOperatorSchwartz and its body Distribution.powOneMul ℂ (→ x * ψ x) two lines below:
the map is multiplication by x (position), not ψ(-x) (parity), so "position operator" is the
correct label.

Only the one word parity → position was changed; no code was touched. lake build of the
module succeeds, and ./scripts/lint-style.sh and lake exe runPhyslibLinters both pass.

…e parity operator

Co-authored-by: Claude <noreply@anthropic.com>
@github-actions

github-actions Bot commented Jul 3, 2026

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant