feat(Units): reducible rational arithmetic via Exponent

[RaunakChhatwal]

Reducible rational arithmetic for dimension exponents

Ideally, the product of speed and time should type-check as length. This does not happen at present because the product of their dimensions is not definitionally equal to the length dimension:

example (v : WithDim (L𝓭 / T𝓭) ℝ) (t : WithDim T𝓭 ℝ) : WithDim L𝓭 ℝ :=
  v * t -- Type mismatch `v * t` has type `WithDim (L𝓭 / T𝓭 * T𝓭) ℝ` but is expected to have type `WithDim L𝓭 ℝ` (Lean 4)

The root cause is that dimension arithmetic uses rational arithmetic, whose operations are irreducible in Lean:

example : (2 : ℕ) + 2 = 4 := rfl -- succeeds
example : (2 : ℚ) + 2 = 4 := rfl -- fails

Locally unsealing rational arithmetic does not export reducibility to downstream modules, while globally changing the reducibility of imported declarations requires allowUnsafeReducibility. This PR instead introduces a wrapper around ℚ with reducible arithmetic, enabling:

example :
  let Length : Exponent × Exponent := (1, 0)
  let Time : Exponent × Exponent := (0, 1)
  let Speed := Length - Time
  Length = Time + Speed := rfl

This enables definitional equality for tuple- or structure-based dimensions, but unfortunately not for Physlib's current parametric dimensions. Lean's definitional equality is less effective at comparing unapplied functions than concrete data structures, while the parametric approach relies on function representation to maintain basis independence. I would therefore like to follow this PR with a simpler, non-parametric formalization of dimensions using Exponent.

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

Maybe worth actually implementing this as the type for dimension exponent now, so it fits in with the rest of the project

[jstoobysmith]

Putting

awaiting-author

For above comment, but also the linters.

[RaunakChhatwal]

Sure, I updated Dimension to use Exponent. As noted in the initial description, simply replacing ℚ would not have improved the user-facing behavior. I also had to adapt the basis-parametric Dimension representation to support exponent tuples while retaining support for different choices of base dimensions.

Concrete cancellation now reduces as intended, so (L𝓭 / T𝓭) * T𝓭 = L𝓭 holds by rfl, and v * t can be used directly as a length without a cast.

cc @NicolasRouquette

-awaiting-author

[NicolasRouquette]

Thanks for digging into this, @RaunakChhatwal — and for the cc. I wrote the parametric
dimension/unit layer in #1447 and #1481, so let me respond in some detail.

Short version, in three parts:

• The ℚ → Exponent change is right, and I would support merging it — conditional on the
  three items marked [blocking] in §1. All three are small. (a) in particular is far cheaper
  now than as a retrofit, because retrofitting it means changing the coercion.
• The DimensionBasis representation change should not land in this PR (§3, §4). It appears
  in neither the title nor the description, and it introduces a canonicity problem of the kind
  Mathlib deliberately avoids — which I think has a fix that costs you nothing.
• The non-parametric follow-up proposed at the end of the description should not proceed (§2).
  It would close four requirements already accepted in API: Make Dimension's base-dimension set parametric #1441, and it is not a simplification of
  unused generality — that generality is load-bearing today.

---

1. Exponent is the right idea; a few practical bits are missing

Caution

Struck — this paragraph is wrong, on both counts. Rat.add and Rat.mul do carry
@[irreducible], inline on the definitions (Init/Data/Rat/Basic.lean:259 and :168), as
@RaunakChhatwal pointed out. And Nat.gcd is not the blocker — it reduces fine
(example : Nat.gcd 1234567 7654321 = 1 := rfl succeeds). The PR description's diagnosis was
correct as written and I replaced it with a fabricated one. Retained below only so the thread
stays readable; see my follow-up comment for the correction.

The diagnosis is correct and the fix is well aimed. Worth recording precisely why it works,
because it's not quite what the description says: Rat.add/Rat.mul aren't sealed — there is
no seal and no attribute [irreducible] on them in Init/Data/Rat/Basic.lean. The actual
blocker is one level down:

-- STRUCK: this is not the blocker.
-- Init/Data/Nat/Gcd.lean:35
def gcd (m n : @& Nat) : Nat := ... termination_by m

Nat.gcd is well-founded, hence kernel-opaque, and every Rat operation normalizes through it.
Nat.div/Nat.mod are kernel-accelerated on literals, which is exactly why your fuel-bounded
gcdAux works. Worth putting in the module docstring — it explains why the fuel trick is the
right shape of fix rather than a hack.

That said, Exponent is currently a Field and very little else, and this PR already pays for
the gaps. Four sites in the diff work around them:

• Units/Basic.lean — map_add inserted ahead of Rat.cast_add
• Units/ParametricUnits.lean — same, in dimScale.map_mul'
• Units/Examples.lean — map_ofNat added to a norm_num call
• Units/ISQBridge.lean — toISQHom_injective's time case now round-trips through
  congrArg Exponent.ringEquivRat + map_add before it can call linarith

Concretely, I'd ask for:

(a) A norm_cast API. [blocking] instance : Coe Exponent ℚ := ⟨ringEquivRat⟩ makes ↑x elaborate to
a RingEquiv coercion, which norm_cast/push_cast know nothing about and which prints as
⇑Exponent.ringEquivRat x in goals. Please add a @[coe]-tagged function and
@[simp, norm_cast] lemmas — coe_add, coe_sub, coe_neg, coe_mul, coe_inv, coe_div,
coe_zero, coe_one, coe_ofNat. Each of the four sites above is a downstream user's future
paper cut.

(b) Order instances. [follow-up — fine as a separate PR] Exponent is a Field but not an ordered one, so linarith,
positivity and the order tactics are simply unavailable — that's the real reason
toISQHom_injective needs the equiv round-trip. equivRat is already there;
LinearOrder/LinearOrderedField transfer is a few lines and buys the whole tactic surface back.

(c) Repr. [follow-up, but it is one line] deriving DecidableEq only, so exponents print as { toRat := 2/3 } in
diagnostics. Dimension mismatches are the main UX of this library; exponents should read well.

(d) A fractional-exponent test at the Dimension level. [blocking] Every definitional test in the PR
uses integer exponents. Section D of Exponent.lean exercises rationals, but only on raw
Exponent/Exponent × Exponent, never through Dimension — and Pow (Dimension B) ℚ now
routes through ofFunction, so qpow_exponent is no longer rfl. I think closed terms still
reduce, but that should be tested rather than assumed:

example : L𝓭 ^ (1/2 : ℚ) * L𝓭 ^ (1/2 : ℚ) = L𝓭 := rfl
example (a b : WithDim (L𝓭 ^ (1/2 : ℚ)) ℝ) : WithDim L𝓭 ℝ := a * b

(e) Keep the rfl tests, and please measure the defeq cost. [blocking] The section-C examples
(example : add = instField.add := rfl) are doing more work than they look like they are.
Function.Injective.field takes [Add K] [Mul K] [Inv K] [Div K] [Sub K] [Neg K] as ambient
instances and builds a Field whose operations are those instances — so those examples pin
the field structure to your reducible operations rather than to a transported copy. Please keep
them, and the section-D ones, as permanent regression tests, ideally as named lemmas; anonymous
examples are easy to delete in a later refactor without anyone noticing what broke. Adding the
instances in (a)–(c) is exactly the kind of change that could silently unpin them.

The related question is cost, and it is the one I'd most like to see a number for. A single
dimension comparison on LTMCTDimensionBase now runs five componentwise Exponent additions,
each going through normalize and the fuel-recursive gcdAux, in the kernel. gcdAux is
structural on its fuel argument, so it compiles through brecOn; kernel laziness should mean
only the O(log) accessed path is ever forced, but that is worth confirming rather than assuming —
particularly since a dimension mismatch must now run all of it before Lean can report a type
error, where previously the comparison failed immediately. A count_heartbeats measurement on
something like ((97/101 : Exponent) + 103/107) * 89/83 = … := rfl, and on a deliberately failing
WithDim unification, would settle whether there is a cliff here.

To summarise what I would want to see before this half merges:

• (a) @[coe] function + @[simp, norm_cast] lemmas for the Exponent → ℚ coercion
• (d) a rfl test for a fractional dimension exponent, at the Dimension/WithDim level
• (e) the section-C/D examples kept as named lemmas, and a count_heartbeats number for
  a passing rfl and for a failing WithDim unification

(b) and (c) I am happy to see as follow-ups; I will open issues for them if that helps.

Minor, while you're here: the ten simpa only [exponent_X] using X_exponent d n .X proofs in
LTMCTDimensionBase.lean and the five X𝓭_eq_single proofs (which now unfold all five
accessors) both got noticeably noisier — a helper lemma would collapse them. And
rw [@NNReal.rpow_add] with a bare @ and no arguments in Units/Basic.lean looks accidental.

---

2. Dimensions and units must stay parametric

I would therefore like to follow this PR with a simpler, non-parametric formalization of
dimensions using Exponent.

I definitely push back on this, and not on grounds of sunk cost. Parametricity over the base-dimension set
is not generalization for its own sake; it is what lets Physlib talk about more than one system
of physics at a time.

The set of base dimensions is an open question, not a settled taxonomy.

This is the most important point for reviewers to consider.
There is a decade-plus of live debate in the metrology community
over exactly which quantities deserve to be dimensions — concentrated on the so-called
dimensionless ones. Plane angle is the sharpest case: the SI treats the radian as a dimensionless
derived unit (m/m = 1, "a special name for the number one"), which is why torque and energy come
out with identical dimensions despite being different quantities, and why angular velocity in
rad/s is dimensionally indistinguishable from frequency in s⁻¹. A sustained line of argument in
Metrologia holds that this is a convention with costs, and that plane angle should carry a base
dimension of its own with solid angle its square. I collected that literature in the references
section of #1441 rather than repeat it here — seven papers, running from 2016 to a 2026
contribution from practising dimensional metrologists, with no convergence.

The parallel thread on quantities of dimension one runs alongside it — P J Mohr, W D Phillips,
Dimensionless units in the SI, Metrologia 52 (2015) 40; D Flater, Unit one is intrusive,
Metrologia 61 (2024) 3 — and the same style of argument applies to the candela (luminous
intensity is radiant intensity weighted by a biological response function; is that a physical
dimension?) and to the mole (since 2019 explicitly a count, so arguably a pure number).

Institutionally the question is live too. The Consultative Committee for Units (CCU) — the body
that prepares the SI Brochure and advises the International Committee for Weights and Measures
(CIPM) on units — maintains a standing Working Group on Angles and Dimensionless Quantities in the
SI (CCU-WGADQ). Its work fed the 2024 revision of the SI Brochure (v3.01), which clarified the
language around angles and quantities with the unit one and strengthened the guidance that
explicit units should be used wherever possible for quantities with the unit one — in effect a
request for precisely the discipline a type system is good at enforcing. Note the dates: 2015
through 2026, and still going. None of it is closed.

Physlib has already taken a position in that debate.

Its LTMCT basis is not the ISQ's: it drops amount of substance and luminous intensity,
and uses charge where the ISQ uses electric current.
That is three deviations from the international standard, and I think they are good
ones — but they are choices in an open argument, not settled facts. What makes them defensible
today is precisely that they are a basis rather than the basis, with ISQBridge proving the
relationship to the standard rather than asserting it. Monomorphizing would enshrine one
contested set of choices as the library's ontology.

Note also that neither LTMCT nor the ISQ currently carries angle. And the question is genuinely
unresolved rather than trending: that 2024 brochure revision deliberately left the dimensional
status of these quantities unchanged, clarifying language without settling the argument. That is
exactly why a library should not hard-code an answer. Should the status ever change, a parametric
Dimension absorbs it as an additive change — declare a basis, provide an Embedding — while a
monomorphic one requires a breaking change to the library's central type.
The Info basis (bit/symbol) already in ParametricDimensionExamples.lean is exactly this kind
of experiment, and it costs the core nothing.

It is already load-bearing.

Units/ISQBridge.lean exists to carry exactly that LTMCT-vs-ISQ gap,
and the translation is not a relabelling — the charge exponent migrates into two places:

| .time    => d.exponent .time + d.exponent .charge
| .current => d.exponent .charge

Today that bridge is a MonoidHom, so dimension-preservation holds by construction, and it
comes with toISQHom_injective and fromISQHom_comp_toISQHom = MonoidHom.id. A monomorphic
Dimension cannot state any of that. You would be left hand-rolling a conversion with no
algebraic guarantee that it respects products, inverses, or rational powers — precisely the class
of bug a formalization exists to rule out.

Physics uses several dimension bases, not several unit choices of one basis.

Rescaling metres to feet is a unit change, already handled
by LTMCTUnitChoices/dimScale. The following are basis changes and are not:

• Gaussian/CGS. Charge is not an independent base dimension at all; Coulomb's law forces
  q² = M L³ T⁻², i.e. q = M^(1/2) L^(3/2) T⁻¹. No unit choice on an LTMCT basis produces
  this — charge stops being a generator.
• Natural units (ℏ = c = 1). Mass, length and time collapse onto a single base dimension.
  This is the working convention across Physlib's QFT and Relativity material.
• Geometrized units (G = c = 1) in general relativity, and Heaviside–Lorentz in EM.

Each is a different basis B. With Dimension B parametric these are instances of one algebra
related by Embedding/Projection. Without it, Physlib can formalize exactly one and the rest
become informal commentary.

And this is not hypothetical — it is what #1441 asked for. The parameterization landed in
#1447 as the implementation of #1441, whose requirements are explicit that each of the following
must be expressible as an instantiation, none privileged:

• the full ISQ seven-base-quantity system of ISO/IEC 80000-1, taking electric current in place of
  charge and adding amount of substance and luminous intensity;
• Gaussian–CGS: three generators, with charge derived as M^(1/2) L^(3/2) T⁻¹ rather than an
  independent axis;
• a natural-unit system (c = ℏ = 1), which collapses generators;
• an angle-augmented basis: an added angle generator, with solid angle its square (sr = rad²).

That last one is the payoff of the literature above. With plane angle a generator, torque becomes
dimensionally distinct from energy and torque × angle = energy holds by genuine cancellation of
the angle exponent rather than by a hidden dimensionless 1 — so the algebra itself rules out the
spurious factors of 2π the reform papers are concerned with. None of it is expressible over a
monomorphic Dimension.

#1441 also asked for a change-of-basis map along an embedding of bases B ↪ B'. That is
Dimension.Embedding, and it is what makes cross-basis comparison a theorem rather than an appeal
to intuition. Reverting to a fixed basis closes every one of those requirements at once.

Your own design decisions point the same way.

Exponent is a field, not ℤ — you built inv, div and the whole gcd/normalize
apparatus to support fractional exponents. But on the LTMCT and ISQ bases fractional exponents
are close to a curiosity (spectral densities in V/√Hz and the like).
The clearest reason to need 1/2 in an exponent is Gaussian charge — a different basis.
The strongest argument for field-valued exponents is, at root, an argument for parametricity.

The cost is low and already paid.

Downstream users write L𝓭, T𝓭, WithDim exactly as they do today;
the generic core is a few hundred lines in Dimension.lean that nobody has to
read. Physlib is a library — a monomorphic Dimension is a policy imposed on every downstream
project, including ones needing a basis Physlib doesn't ship. Removal is also not cheaply
reversible: re-parameterizing later means touching every dimension-indexed declaration a second
time.

And the alternative is fragmentation.

If Physlib hard-codes one basis, anyone who needs a
different one — an angle-as-base-quantity experiment, natural units for a QFT development, an
application-specific basis — cannot use Physlib for it. They fork, or they start a competing
formalization. That is the outcome a foundational library should least want, and it is the same
interoperability failure discussed in §4 below, one level up: at the ecosystem scale rather than
the instance scale. Parametricity is what lets those experiments happen inside Physlib and stay
comparable to each other.

Finally, dimension parametricity is what the unit side is built on. UnitScale B,
dimScale : Dimension B →* ℝ≥0 and the dimScale_transitive cocycle in ParametricUnits.lean
are all generic over B (#1481). Dropping it on the dimension side strands that layer too.

If you want to make the case for monomorphic dimensions anyway, it needs to go to
Zulip before such a PR is
opened. It is an architectural decision for the library and a reversal of requirements already
accepted in #1441; it should not be settled as a side effect of a PR about exponent reducibility.

---

3. What is DimensionBasis actually buying?

Here I mainly want to understand your intent, because the PR doesn't say. DimensionBasis
appears in neither the title nor the description, which makes a substantial redesign of
Dimension look like unmotivated complexity to anyone reading the diff cold.

Is its entire purpose to eliminate the .cast in ParametricDimensionExamples.lean? If so, I
don't yet see how it gets there, and I'd ask for the reasoning to be written into the
description.

My own reconstruction, which you should correct if it's wrong: Exponent alone is not enough
to deliver the headline example. With Dimension B := B → Exponent, checking
(L𝓭 / T𝓭) * T𝓭 =?= L𝓭 descends under the binder with b free, so the fun | .length => …
matches are stuck and no amount of exponent reducibility helps. Only an eta-expanded, positional
representation — your five-tuple — makes the components concrete enough to reduce.

If that is the argument, it is a good one and deserves stating, because it is the non-obvious
half of the PR. It also means the two halves are independent: Exponent is a workaround for a
toolchain limitation that could be retired if Nat.gcd were ever fixed upstream, whereas the
tuple representation solves a binder problem that no arithmetic fix touches. They have
different lifetimes.

One thing that would help me weigh it: could you show a case where .cast genuinely blocks
something — a rewrite that fails on a motive, a simp that can't fire under a dimension-indexed
type — rather than a case where it is merely noise? Its auto-param
(by ext <;> {simp; try ring}) already discharged the equality with no user-written proof, so
what it cost was one token. If the defeq buys real proving power the calculus changes; if it is
purely ergonomic, one token of .cast may be the cheaper trade.

---

4. DimensionBasis has no canonicity — and the fix is free

This is my main technical concern, and I think it is fixable without giving up anything.

DimensionBasis is a class whose Type-valued content becomes a type index: Dimension B
means different things under different instances. Type-class resolution is not confluent across a
corpus, so this is the pattern Mathlib deliberately avoids — it is why Fintype-style classes
keep their content out of type indices, and why DecidableEq in an index is handled through
Subsingleton. DimensionBasis is emphatically not a Subsingleton: two instances have
different Exponents types.

I checked what this does in practice, on a standalone repro (Lean 4.33.0, no Mathlib). With two
modules each declaring an instance for the same basis:

-- ModA.lean:  instance piB  : Basis Lbl := ⟨Lbl → Nat⟩
-- ModB.lean:  instance tupB : Basis Lbl := ⟨Nat × Nat⟩

import ModA; import ModB   →   #synth Basis Lbl   ⟹   tupB
import ModB; import ModA   →   #synth Basis Lbl   ⟹   piB

Swapping two import lines silently changes what Dimension B means. Everything indexed on
it then fails to interoperate — which for Physlib means every WithDim, i.e. every physical
quantity:

Type mismatch
  lenB
has type   @Dim Lbl tupB
but is expected to have type   @Dim Lbl piB

Two mitigations worth stating fairly: the failure is loud (Lean's pretty-printer disambiguates
the instances, so this is a legible compile error, never a wrong proof), and for LTMCTDimensionBase
and ISQDimensionBase a downstream project would have to declare a competing instance
deliberately. But the basis-generic API does not paper over the split — applying a lemma
stated over variable [DimensionBasis B] to an object built on the other instance fails with
synthesized type class instance is not definitionally equal ..., and only goes through with an
explicit @. And the realistic scenario needs no bad actor: two Physlib-based projects that both
define dimensions over some new shared basis — natural units, Gaussian, an application-specific
one — will each declare their own DimensionBasis for it, and their quantities won't compose.

The fix: bundle the basis as a value instead of inferring it as an instance

structure DimBasis where
  Label : Type
  Exponents : Type
  [addCommGroup : AddCommGroup Exponents]
  exponentEquiv : Exponents ≃+ (Label → Exponent)

structure Dimension (b : DimBasis) where
  exponents : b.Exponents

There is no inference, so no import-order dependence and nothing to resolve non-confluently. Two
projects can still disagree, but the disagreement is then a named value visible in the source
(Dimension Gaussian vs Dimension LTMCT) rather than something emergent from import order.

And — this is the part I checked before proposing it — you keep the whole win. I built the
bundled design in the same standalone repro and both of the things this PR is after still hold
definitionally:

def LTMCT : DimBasis := ⟨Int × Int⟩
def L : Dim LTMCT := ⟨(1, 0)⟩
def T : Dim LTMCT := ⟨(0, 1)⟩

example : (L * T⁻¹) * T = L := rfl                              -- ✓
example (v : Qty (L * T⁻¹) Nat) (t : Qty T Nat) : Qty L Nat := v * t   -- ✓ no cast

Projections of a concrete structure value reduce exactly as class projections do, so the
tuple representation reduces the same way. Two further properties fall out that the class design
doesn't have:

• Accidental duplication is harmless. Two projects that independently bundle the same
  representation get defeq types, so their quantities compose (verified — Dim LTMCT_projA and
  Dim LTMCT_projB unify).
• Genuine disagreement is named. A mismatch reports the basis values involved, not
  autogenerated instance names.

If you'd rather keep the class, then at minimum I'd ask for the invariant to be documented
("at most one DimensionBasis instance per B, declared in the module that declares B") and
enforced — Physlib already ships lake exe runPhyslibLinters, check_dup_tags and
check_file_imports, so a duplicate-instance check would be in idiom. I'd also want a transport
DimensionBasis.congr (i j : DimensionBasis B) : @Dimension B i ≃* @Dimension B j as an escape
hatch, though note the irony: that reintroduces exactly the cast tax this PR is trying to
abolish, one level up.

One thing to please not do, which I briefly thought was a good idea and then measured: adding a
low-priority default instance : DimensionBasis B := DimensionBasis.pi B to remove the
per-basis boilerplate. It manufactures the one genuinely silent failure — a module that forgets
to import the specialized instance compiles clean, with no warning, on the wrong representation
and without the rfl win. Without the default, the same module fails immediately with
failed to synthesize instance of type class DimensionBasis B. The boilerplate is the price of
the error being loud.

---

Suggested sequencing

1. This PR: Exponent + the mechanical ℚ → Exponent swap, plus the three blocking items in
   §1. Uncontroversial, reviewable on its own merits, and I would be glad to see it merged.
2. Zulip: parametric vs. monomorphic dimensions, on its own thread.
3. A separate PR: the representation change, with the binder argument from §3 written into the
   description and the canonicity question from §4 settled. The different lifetimes of the two
   halves — Exponent a workaround upstream could obsolete, the representation a permanent
   design decision — seem like a good reason on their own not to land them together.

Happy to help with any of these, and thanks again for taking this on. The Exponent idea is a
real improvement and I'd like to see it land.

+awaiting-author

[RaunakChhatwal]

The size and scope of that comment is uncalled for, and it reads like an AI-generated review dump. The first section opens with an outright hallucination:

Rat.add/Rat.mul aren't sealed — there is no seal and no attribute [irreducible] on them in Init/Data/Rat/Basic.lean

The irreducible attributes are explicitly present at Rat/Basic.lean#L259 and Rat/Basic.lean#L168.

What then follows is a combination of concrete blockers, follow-up suggestions, minor cleanup, benchmarking requests, documentation requests, a lengthy argument about a future design mentioned in the description, a broader architectural critique, an alternative design proposal, and proposed sequencing for future work. This is an extremely large amount of material to put on one PR and then mark awaiting-author.

On the "main technical concern"

-- ModA.lean:  instance piB  : Basis Lbl := ⟨Lbl → Nat⟩
-- ModB.lean:  instance tupB : Basis Lbl := ⟨Nat × Nat⟩

import ModA; import ModB   →   #synth Basis Lbl   ⟹   tupB
import ModB; import ModA   →   #synth Basis Lbl   ⟹   piB

This applies to many Mathlib type classes, and is not a concern specific to having a Type-valued field. If one defines two incompatible Module R M instances, or two different Field K instances, incoherence or import-order-sensitive elaboration are possible. This is an appropriate trade-off when incompatible instances are not a realistic scenario, as is the case for DimensionBasis.

DimensionBasis is a class whose Type-valued content becomes a type index: Dimension B means different things under different instances.

Any dependent type indexed on an instance parameter (e.g. Submodule) will produce different elaborated types under different instances. That is not particular to DimensionBasis, nor particular to having a Type-valued field. Again, the trade-off is appropriate when incompatible instances are not a realistic scenario.

-awaiting-author

[RaunakChhatwal]

@jstoobysmith Ideally, quantities/units should be the foundation for higher-level core APIs throughout the library. A Particle data type should have quantity-valued mass, not real-valued. At present, this section is unused by rest of Physlib. Practicality, ergonomics, and usability should therefore be high priority, and frictionless type checking for concrete dimensionful expressions enabled by this PR would be a step toward that.

[NicolasRouquette]

You are right, and the correction is worse than you stated: I was wrong twice, not once.

Rat.add and Rat.mul do carry @[irreducible] — inline on the definitions, at
Rat/Basic.lean:259 and :168 as you linked. And my replacement explanation was also wrong.
Nat.gcd is not the blocker; I re-checked against v4.33.0:

example : Nat.gcd 1234567 7654321 = 1 := rfl   -- succeeds

unseal Rat.add Rat.mul Rat.inv Rat.sub
example : ((1/3:Rat) + 1/6 + 1/7 + 2/9 + 5/11) * (3/5) - 1/13 = 21467/30030 := rfl   -- succeeds

Irreducibility is the whole of it, and unsealing is sufficient to lift it — which is exactly what
your description and the Exponent module docstring already say, including the point about
unsealing not exporting downstream. Your diagnosis was accurate as written and I substituted a
fabricated one for it. I have struck that paragraph from my comment above.

On the length

Fair, and I have taken the point. That comment mixed diff-scoped review with an argument about a
design that is not in this PR, which is not a reasonable thing to hand an author at once. I am
withdrawing most of it from this thread. The length came from wanting to show my reasoning rather
than assert conclusions, and I do think that reasoning matters — which is why I would rather
relocate it than drop it.

Where it should go is a question for @jstoobysmith: #1441 is where those requirements were
accepted, but it is closed, and re-opening it to host a design argument may not be what you want.
If the case for keeping the basis parametric is worth recording, it may belong in the Physlib
documentation rather than in an issue at all — an issue implies someone should close it with a
PR, and this is a rationale, not a work item. Happy to put it wherever is most useful, or to drop
it if you would rather it not be written up.

On canonicity

You are right that I over-generalised. Import-order-sensitive elaboration under competing
instances is not specific to a Type-valued field — Submodule is a fair counter-example — and
the failure is not silent, since Lean prints the disambiguated form.

What I would still raise, narrowly: DimensionBasis.pi is exported and applies to any basis, so a
second instance for a basis that already has one is a natural thing for a downstream author to
write — while testing an angle-augmented basis, say. On this PR's head, one such file is enough to
make Physlib's own generators unusable inside it:

@[instance_reducible] instance altBasis : DimensionBasis LTMCTDimensionBase := DimensionBasis.pi _

def speed : Dimension LTMCTDimensionBase := L𝓭 / T𝓭
-- Type mismatch: @Dimension LTMCTDimensionBase LTMCTDimensionBase.instDimensionBasis
--            vs  @Dimension LTMCTDimensionBase altBasis

Both instances are correct and neither author has erred. The cost is composition: two downstream
libraries that each build alone fail to compose when a third imports both, and which one breaks
depends on import order.

Carrying the basis as a bundled value rather than an instance removes the search that makes this
possible. I ported Physlib/Units/Dimension.lean to that form to check it is not just a
suggestion — every proof goes through with its tactics unchanged, (L𝓭 / T𝓭) * T𝓭 = L𝓭 still
holds by rfl, and an accidental duplicate basis becomes defeq rather than a rival instance. It
costs 81 use sites across 7 files, which is why it is plainly not this PR's business. I will write
it up separately — as an issue or a PR against master, whichever @jstoobysmith prefers — rather
than argue the design here.

One thing that does not work yet — and a patch for it

Rational exponents do not get the rfl win. Checked at this PR's head:

-- integer exponents: the motivating example from your description now works
example (v : WithDim (L𝓭 / T𝓭) ℝ) (t : WithDim T𝓭 ℝ) : WithDim L𝓭 ℝ := v * t    -- succeeds

-- rational exponents: unchanged from before the PR
example (a b : WithDim (L𝓭 ^ (1/2 : ℚ)) ℝ) : WithDim L𝓭 ℝ := a * b               -- fails

The second fails with the same error your description opens with — WithDim (L𝓭 ^ (1/2) * L𝓭 ^ (1/2)) ℝ against WithDim L𝓭 ℝ.

The cause is not the Dimension layer. Exponent.ofRat q = ⟨q⟩ wraps a rational without
normalising, so the irreducible ℚ arithmetic comes straight back in:

example : (1 : Exponent)/2 + (1 : Exponent)/2 = 1 := rfl              -- succeeds
example : Exponent.ofRat (1/2) + Exponent.ofRat (1/2) = 1 := rfl      -- fails

All three of your section-D examples are of the first shape — the arithmetic happens in
Exponent. But Pow (Dimension B) ℚ has to call ofRat, so every rational dimension power takes
the second path.

Which makes the fix small. Adding a Pow at the reducible representation, alongside the existing
ℚ one, is a few added lines in Dimension.lean, and changes nothing that exists:

/-- Raising a dimension to an `Exponent` power.

`^ (q : ℚ)` must call `Exponent.ofRat q`, which wraps a rational whose own arithmetic is
irreducible, so concrete rational powers do not reduce. Taking the exponent in the reducible
representation keeps the definitional win for fractional dimensions. -/
instance : Pow (Dimension B) Exponent where
  pow d c := ofFunction fun b => d.exponent b * c

@[simp]
lemma epow_exponent (d : Dimension B) (c : Exponent) (b : B) :
    (d ^ c).exponent b = d.exponent b * c :=
  ofFunction_exponent _ _

With that, on your branch:

example : (L𝓭 ^ (1/2 : Exponent)) * (L𝓭 ^ (1/2 : Exponent)) = L𝓭 := rfl           -- succeeds
example : (L𝓭 ^ (2/3 : Exponent)) * (L𝓭 ^ (1/3 : Exponent)) = L𝓭 := rfl           -- succeeds
example (a b : WithDim (L𝓭 ^ (1/2 : Exponent)) ℝ) : WithDim L𝓭 ℝ := a * b         -- succeeds

The call site stays the same shape as before — (1/2 : ℚ) becomes (1/2 : Exponent). The whole
of Physlib still builds. This is yours to take or leave: happy to push it to your branch, open
it as a follow-up PR, or just leave the snippet here. It seemed more useful than reporting the gap
and stopping.

A related one, now filed as #1580. While testing the above I found that an unascribed
rational exponent silently defaults to ℕ, where 1/2 = 0:

example : L𝓭 ^ (1/2) = 1 := rfl   -- succeeds: a "square root of a length" is dimensionless

This one is not yours — it reproduces on the pre-PR base 4a4de62f, so I opened it separately
rather than hanging it on your branch. I raise it here only because the fix lands in the same
Pow family as the patch above, and it is one line:

@[default_instance 10000] instance : Pow (Dimension B) Exponent where ...

Priority matters — at the default and at 2000, instOfNatNat still wins.

If the Exponent-valued power goes in, that attribute is the natural companion to it, and you get
both the right meaning and rfl on L𝓭 ^ (1/2) * L𝓭 ^ (1/2) = L𝓭. Full Physlib builds either
way (4558 jobs on your head with the Exponent route; 4557 on 4a4de62f with the attribute on
the existing ℚ power instead). It is small enough that folding it in here would not be much of a
scope increase, but that is your call and #1580 is there to catch it if you would rather keep this PR to one idea.

On adoption

Your point to @jstoobysmith is a fair one and the numbers support it: exactly one of the 538
non-Units modules in Physlib imports Units today, and it does not use what it imports.
Ergonomics and frictionless type-checking should be the priority, which is why both things I have
offered above are usability fixes rather than design arguments.

The one implication I would draw is about timing. Precisely because nothing depends on this layer
yet, the foundational choices — how the basis is carried, what a bare 1/2 means — are cheap to
settle now and expensive later. The canonicity change costs 81 use sites today; after the
Particle-with-quantity-valued-mass work you describe, it would cost considerably more.

What I would still ask for on this PR

A norm_cast API. A @[coe] function and @[simp, norm_cast] lemmas for Exponent → ℚ,
so push_cast/norm_cast work on exponent arithmetic. Much cheaper now than as a retrofit,
because retrofitting means changing the coercion.

That is the only thing I would hold out for. Everything else above is withdrawn, offered as a
patch you are free to ignore, or filed elsewhere — none of it should hold up this PR.