feat(Units): component lemmas for the Exponent power of a dimension

[NicolasRouquette]

Closes #1580.

What this does

Adds epow_length, epow_time, epow_mass, epow_charge, epow_temperature — the
Exponent-power twins of the existing npow_* component lemmas — derived through a
component_epow helper that mirrors component_npow line for line. One file, +41 lines,
no existing declaration touched.

This is Toy3 from https://github.com/NicolasRouquette/PL1580, without the notation, as
you asked in #1580.

Why

Pow (Dimension B) Exponent carries @[default_instance 10000], so an unascribed numeric
exponent elaborates to an Exponent power, not to the ℕ one. The npow_* lemmas match the
ℕ power only, so nothing in the simp set reached the component of such a power. Removing
the five new lemmas from the simp set recovers that state:

section
attribute [-simp] epow_length epow_time epow_mass epow_charge epow_temperature

-- `simp` makes no progress on the issue's own case
example (d : Dimension LTMCTDimensionBase) : (d ^ 2).length = d.length * 2 := by
  fail_if_success simp
  rfl

-- nor on a general `Exponent` exponent
example (d : Dimension LTMCTDimensionBase) (c : Exponent) : (d ^ c).length = d.length * c := by
  fail_if_success simp
  rfl

-- on the half-power it rewrites `1/2` to `2⁻¹` on both sides, but still does not close it
example (d : Dimension LTMCTDimensionBase) : (d ^ (1/2)).length = d.length * (1/2) := by
  fail_if_success (simp; done)
  rfl
end

Evidence

Every goal below is also true by rfl, so a bare by simp would demonstrate nothing about
the lemma. Each is paired instead: simp cannot reach the goal on its own, and can with the
lemma named.

example (d : Dimension LTMCTDimensionBase) (c : Exponent) : (d ^ c).length = d.length * c := by
  fail_if_success simp only []
  simp only [epow_length]

example (d : Dimension LTMCTDimensionBase) (c : Exponent) : (d ^ c).time = d.time * c := by
  fail_if_success simp only []
  simp only [epow_time]

example (d : Dimension LTMCTDimensionBase) (c : Exponent) : (d ^ c).mass = d.mass * c := by
  fail_if_success simp only []
  simp only [epow_mass]

example (d : Dimension LTMCTDimensionBase) (c : Exponent) : (d ^ c).charge = d.charge * c := by
  fail_if_success simp only []
  simp only [epow_charge]

example (d : Dimension LTMCTDimensionBase) (c : Exponent) :
    (d ^ c).temperature = d.temperature * c := by
  fail_if_success simp only []
  simp only [epow_temperature]

-- `npow_length` does not match an unascribed literal — this is what #1580 reported
example (d : Dimension LTMCTDimensionBase) : (d ^ 2).length = d.length * 2 := by
  fail_if_success simp only [npow_length]
  simp only [epow_length]

-- and the `ℕ` power is untouched: an ascribed exponent still routes to `npow_length`
example (d : Dimension LTMCTDimensionBase) (n : ℕ) : (d ^ n).length = n • d.length := by
  fail_if_success simp only [epow_length]
  simp only [npow_length]

lake build and lake exe lint_all exit 0; ./scripts/lint-style.sh clean.

Two things deliberately left out

• The d ^[1/2] notation (Toy3's Q3), per your call in Unascribed rational dimension exponents default to ℕ, silently making L𝓭 ^ (1/2) dimensionless #1580.
• qpow_* component lemmas. The ℚ power is never selected for an unascribed literal —
  only an explicit q : ℚ reaches it — so it needs no defaulting rescue, and five more
  @[simp] lemmas for it would be speculative. See the last section.

I also gave component_epow the same private visibility as component_npow.

The reason: LTMCTDimensionBase is the only basis in Physlib with named component
projections — ISQDimensionBase and the ParametricDimensionExamples bases go through
exponent directly, where the existing basis-generic epow_exponent already applies — so
there is no caller for a public or basis-generic version today.

On deleting Pow (Dimension B) ℚ

You floated this in #1580. Having checked it: the instance is removable at very low cost, and
this PR does not depend on the answer either way.

Pow (Dimension B) ℚ and Pow (Dimension B) Exponent have the same body, differing only in
where ofRat is applied (Physlib/Units/Dimension.lean):

instance : Pow (Dimension B) ℚ where
  pow d q := ofFunction fun b => d.exponent b * Exponent.ofRat q

@[default_instance 10000]
instance : Pow (Dimension B) Exponent where
  pow d c := ofFunction fun b => d.exponent b * c

So the ℚ power is definitionally the Exponent power at ofRat:

example (d : Dimension LTMCTDimensionBase) (q : ℚ) :
    d ^ q = d ^ (Dimension.Exponent.ofRat q) := rfl

Inside Physlib, deleting it costs nothing at all. Not a survey: I deleted the instance
and qpow_exponent together and ran lake build, which completed with exit 0 across
Physlib, PhyslibAlpha, and QuantumInfo. Nothing in the library raises a Dimension to
a ℚ-typed exponent, and qpow_exponent has no use outside its own declaration.

Downstream, the port is mechanical but I can only speak for one case. A statement of the
shape b.dim = a.dim ^ (p : ℚ) — a half-power certificate, say — restates as
b.dim = a.dim ^ Exponent.ofRat p and is the same proposition by rfl, so the exponent
stays rational in the signature and nothing weakens. I ported one such certificate in a
library of mine and it took two edits: Exponent.ofRat p in the statement, and
epow_exponent in place of qpow_exponent in the simp only. The rest of the proof was
untouched. That is one data point, not a claim about every downstream user.

So the trade is: whoever holds a genuine q : ℚ writes an extra Exponent.ofRat, against
one fewer competing Pow instance on Dimension — which is most of what made #1580 hard to
answer in the first place. This looks favorable to me, but it is your call and it is not this
PR.

Either way epow_* is what you asked for as Toy3. These lemmas are about the Exponent
power, which is the one unascribed literals actually select, and that is true whether the ℚ
instance stays or goes.

[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]

One small comment from me

[jstoobysmith]

Would make this not private