feat(Units): add analytic structures and transport for WithDim

[catlover-bot]

Summary

Refs #1628.

This PR adds an analytic foundation for WithDim and applies it to a harmonic-oscillator example.

WithDim d M gains a real-module structure, induced normed-space structures, explicit coordinate equivalences, and generic transport operations for functions and Fréchet derivatives.

Following review, the harmonic-oscillator example now uses a separate HarmonicOscillatorWithDim whose physical parameters themselves carry dimensions. The potential energy is assembled from dimension-tagged quantities, so its energy dimension is checked by the type of the expression. An explicit map back to the existing numerical HarmonicOscillator shows that the tagged expression agrees with the existing potential-energy definition in coordinates.

Scope

The norm and coordinate isometry remain tied to a fixed numerical unit representation; no claim is made that the norm is invariant under unit changes.

The derivative is still an ordinary continuous linear map between tagged coordinate spaces. A derivative value carrying the quotient of output and input dimensions remains follow-up work.

No fixed-dimension Ring or Field, implicit coercion that discards tags, or unit-system redesign is introduced.

Declarations

Physlib/Units/WithDim/Basic.lean

• WithDim.instModuleReal — real scalars act on tagged numerical values.
• WithDim.real_smul_val — projection of real scalar multiplication.

Physlib/Units/WithDim/Analysis.lean

• WithDim.toValueAddEquiv
• WithDim.toValueLinearEquiv
• WithDim.instNormedAddCommGroup
• WithDim.instNormedSpace
• WithDim.norm_eq
• WithDim.toValueLinearIsometryEquiv
• WithDim.toValueLinearIsometryEquiv_apply
• WithDim.toValueLinearIsometryEquiv_symm_apply
• WithDim.transport
• WithDim.transport_val
• WithDim.transportLinearMap
• WithDim.transportLinearMap_val
• WithDim.hasFDerivAt_transport

These form the fixed-coordinate analytic layer and reuse Mathlib's continuous-linear-equivalence calculus.

Physlib/ClassicalMechanics/HarmonicOscillator/WithDim.lean

• HarmonicOscillatorWithDim — harmonic-oscillator parameters with physical dimensions.
• HarmonicOscillatorWithDim.toHarmonicOscillator — forget the tags and recover the existing numerical model.
• HarmonicOscillatorWithDim.positionNormSq / positionNormSq_val — squared position norm with dimension L².
• HarmonicOscillatorWithDim.potentialEnergy — dimension-tagged 1/2 k x²; its output type enforces the energy dimension.
• HarmonicOscillatorWithDim.potentialEnergy_val — coordinate agreement with the existing numerical potential energy.
• HarmonicOscillatorWithDim.potentialEnergy_eq_transport — identifies the typed expression with explicit transport of the existing function.
• HarmonicOscillatorWithDim.hasFDerivAt_potentialEnergy — reuses the generic derivative transport API.
• HarmonicOscillatorWithDim.continuous_potentialEnergy — continuity of the tagged potential energy.

The earlier coordinate-only time-derivative lemma ending in .val has been removed rather than weakened.

Existing example and registration

• Physlib/Units/Examples.lean: the statement of UnitExamples.energyMass_isDimensionallyCorrect is unchanged; its proof reuses the existing dimensional-correctness API.
• Physlib.lean: imports the two new modules.
• Physlib/Units/API-map.yaml: records the analytic layer and the dimension-checked harmonic-oscillator example.

Validation

Passed locally with Lean 4.33.0:

• git diff --check
• style check for Physlib/ClassicalMechanics/HarmonicOscillator/WithDim.lean
• python3 scripts/api_map_linter.py --repo .
• targeted lake build -KCI Physlib.ClassicalMechanics.HarmonicOscillator.WithDim
• local review smoke test for the dimension-tagged oscillator API
• full lake build -KCI (9359 jobs)
• lake exe check_file_imports
• lake exe check_dup_tags
• lake exe sorry_lint
• lake exe runPhyslibLinters

The reviewed shared declarations inspected in the smoke test contain neither sorryAx nor Lean.ofReduceBool.

Remote CI must validate the pushed review revision.

Reviewer map

1. Physlib/Units/WithDim/Basic.lean and Physlib/Units/WithDim/Analysis.lean for the general analytic layer.
2. Physlib/ClassicalMechanics/HarmonicOscillator/WithDim.lean, especially HarmonicOscillatorWithDim.potentialEnergy, to see the dimension-checked physical example and its bridge to the existing model.
3. Physlib/Units/Examples.lean for the proof-only regression change.
4. Physlib/Units/API-map.yaml and Physlib.lean for registration.

AI-assisted implementation and PR description using ChatGPT.

[catlover-bot]

t-units

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[jstoobysmith]

Do you need the .val here?

[jstoobysmith]

Maybe we need a HarmonicOscillatorWithDim? then we could prove (I think) that the dimensions of this expression actually work! Which would be nice.

[catlover-bot]

I implemented this direction. The revised example now has a HarmonicOscillatorWithDim with dimension-tagged mass and spring constant, and the potential energy is constructed from those tagged quantities so that the energy dimension is checked by the type of the expression. I also added an explicit map back to the existing numerical HarmonicOscillator and proved that the potential energies agree in coordinates.

[jstoobysmith]

awaiting-author

[catlover-bot]

-awaiting-author

[catlover-bot]

Yes — I removed that coordinate-only derivative lemma rather than keeping the .val projection. The revised example now works directly with the dimension-tagged potential energy and uses HasFDerivAt on the tagged spaces.

[jstoobysmith]

Approved. Will merge shortly