feat(Units): parameterise Dimension and its unit twin over a basis (Stacked on #1445)

[NicolasRouquette]

Closes #1441 — makes Dimension's base-dimension set parametric, and moves the unit-side twin (UnitChoices / dimScale) with it, as the issue requires.

Thanks to Daniel Morrison for a very useful and constructive design discussion on the Physlib Zulip that shaped this.

This builds on #1445 (the v4.32.0 bump); the substantive change is the final commit, feat(Units): parameterise Dimension and its unit twin over a basis.

Requirements coverage (from the issue)

Already satisfied — preserved by the generic API

• ℚ exponents / fractional powers — exponent : B → ℚ, Pow (Dimension B) ℚ
• commutative group — instance : CommGroup (Dimension B) for every B
• extensional equality — @[ext] Dimension.ext

Core — parametrise the generating set

• Dimension parametric in a basis B — structure Dimension (B)
• CommGroup / ℚ-power derived generically for every B
• DecidableEq (Dimension B) for finite B — instance [Fintype B] : DecidableEq (Dimension B)
• generic base vector per b : B — Dimension.single b, with L𝓭 = single .length, … (*_eq_single)
• unit side parametrised in the same basis; dimScale folds over B — UnitScale B and UnitScale.dimScale : UnitScale B → UnitScale B → Dimension B →* ℝ≥0 (d ↦ ∏ b, (u₁ b / u₂ b) ^ d.exponent b); UnitChoices.toScale exhibits the current five-field UnitChoices as the PhyslibBase instance

Backward compatibility

• current basis recoverable — Dimension PhyslibBase over PhyslibBase = {length, time, mass, charge, temperature} (neutrally named; charge-based, i.e. not the SI/ISQ set)
• named projections (.length, …) and @[simp] lemmas preserved — every existing Units/ result builds unchanged (full build: 9238 jobs)

Coverage — the motivating quantity systems (Physlib/Units/BasisExamples.lean)

• ISQ seven base quantities — current-based, with amount of substance and luminous intensity
• Gaussian–CGS — three generators, charge derived M^(1/2)·L^(3/2)·T^(-1)
• natural units — c = ħ = 1, a single generator (length = time = mass⁻¹)
• angle-augmented — solid angle the derived square of plane angle (sr = rad²)

Optional / stretch

• change-of-basis map for B ↪ B' — Dimension.extend (exponent-preserving on an embedding), with a PhyslibBase ↪ angle-augmented demo
• documented SI recovery + worked non-SI instantiations — the two example modules

Design decisions on the issue's open questions

• B → ℚ vs B →₀ ℚ — total function (structure Dimension (B) where exponent : B → ℚ); Fintype B is required only where a fold is taken (dimScale, DecidableEq). This keeps the dimension-comparison cast (below) ergonomic.
• Replace or extend — the parametric type replaces Dimension; the current type is recovered as Dimension PhyslibBase with the projections re-exposed (the issue's "thin wrapper" path), so nothing downstream changes.
• One basis or many — a single default basis (PhyslibBase) for the HasDim / CarriesDimension carrier layer, with parametricity available to separate developments and to the other bases above. (So the unit-scaling carrier still shares one basis; per-type mixed bases are not introduced.)
• Conventions (c = ħ = 1) — modelled by choosing a smaller basis and deriving the rest (see Natural), the first option the issue lists.

Dimension comparison

WithDim is parametric over the basis. A quantity of dimension length and a product of quantities of dimension length/time and time have propositionally but not definitionally equal dimensions (rfl and decide both fail — the equality is group cancellation over ℚ exponents). WithDim.cast bridges the two types, discharging the equality automatically; see Physlib/Units/ParametricDimensionExamples.lean.

Checks

lake build (Physlib + QuantumInfo): 9238 jobs, 0 errors / 0 warnings / 0 sorry. lint-style.py and lake exe lint_all clean on all changed files. No new axioms beyond propext / Classical.choice / Quot.sound; no sorryAx.

---

AI-assisted per the repository's AI policy; commits carry the Co-authored-by trailer.

[github-actions]

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.

[NicolasRouquette]

Note on dependencies and review order.

This PR is stacked on #1445 (the v4.32.0 toolchain bump). Since it targets master, the first two commits — 48fad30 and 978ce09 — belong to #1445 and will drop out of this diff automatically once #1445 merges. The substantive change here is the final commit, 97c70b5 (feat(Units): parameterise Dimension and its unit twin over a basis); that's the one to review.

Because of that dependency:

• It's probably easiest to review/merge chore: Bump v4.32.0 #1445 first — this PR then reduces to the single parametric commit with nothing further needed from me.
• If chore: Bump v4.32.0 #1445 takes further review changes (new or amended commits), I'll rebase this branch onto the updated chore: Bump v4.32.0 #1445 head so the two stay consistent. So please expect the occasional force-push here for that reason, rather than as a change to this PR's own content.

Since the original issue arose in the context of my metrology work which depends on Caltech's TorchLean that already migrated to 4.32.0, I chose to stack this PR on top of #1445.

[NicolasRouquette]

-awaiting-author

Separate from the toolchain fix — a naming question raised in review. It came to me by email and I couldn't find it in the PR comments, so I'm recording it here for visibility:

Is there a better name for this which doesn't refer to Physlib?

For context: this is PhyslibBase, the top-level inductive in Physlib/Units/Dimension.lean (its fully-qualified name is the bare PhyslibBase). In this PR Dimension becomes parameterised over a basis B of base dimensions — Dimension B — and PhyslibBase is PhysLib's default basis: the five generators length, time, mass, charge, temperature. Dimension PhyslibBase reproduces the previous five-exponent Dimension exactly, so existing code is unaffected.

I named it after its provenance rather than generically because this basis is a specific, deliberate choice, not a neutral or canonical one. It is charge-based with five generators, so it is not the SI/ISQ base-quantity set (which takes electric current as base and adds amount of substance and luminous intensity); ISQ, Gaussian–CGS, natural units, and the angle-augmented system are other instantiations of Dimension B for different B.

The previous unparameterised Dimension had this choice baked in implicitly, so the generic name was arguably misleading — it looked basis-neutral but wasn't. Tagging the basis with its origin documents that it is PhysLib's historical convention, one option among several.

That said, I'm very open to renaming it. My one constraint is that the name should still signal "a specific, non-ISQ choice of base quantities" rather than implying a canonical basis. If there's a preferred convention — or a good descriptive name for this charge-based, five-generator set — I'll gladly adopt it. Suggestions welcome.

[NicolasRouquette]

Thanks @nateabr for the retitle (and the Stacked on #1445 note — that's the right base).

Want to confirm scope before I build anything further, since "and its unit twin" could mean two things.

What's in the PR today is additive: Dimension B is parameterised over a basis, and the unit side gets a basis-generic twin UnitScale B (scale : B → ℝ≥0 + positivity, with dimScale : UnitScale B → UnitScale B → Dimension B →* ℝ≥0 proved once via Finset.prod).

The existing five-field UnitChoices is untouched; UnitChoices.toScale exhibits it as the PhyslibBase instance of the generic fold. UnitScale lives entirely in the new file; nothing downstream moves.

The open question is whether you also want to parameterise UnitChoices itself. I see four levels:

A — Keep the bridge (status quo).

UnitChoices stays bespoke; toScale is the equivalence. Generic machinery is available for other bases (ISQ, Gaussian–CGS, natural, angle-augmented) without disturbing anything.

• Pro: smallest diff, cleanly stacked, zero risk to the 107 existing UnitChoices call sites.
• Con: the ~12 hand-rolled UnitChoices.dimScale lemmas remain a parallel copy of the generic ones — the two sides are twinned but not unified.

B — Consolidate the proofs, keep the API.

Leave the UnitChoices structure and its public surface as-is, but re-derive UnitChoices.dimScale and its lemmas through toScale/UnitScale.dimScale, deleting the duplicated manual proofs.

• Pro: single source of truth for the scaling laws; blast radius is Units/Basic.lean only; downstream and SI/API unchanged.
• Con: a little proof-plumbing; UnitChoices stays PhyslibBase-only (which is arguably correct — it's the default basis).

C — Make UnitChoices fully basis-generic.

Fold UnitChoices into UnitScale PhyslibBase and migrate the 107 references, so quantity code can be written over any basis.

• Pro: genuinely generic unit choices end-to-end.
• Con: invasive across 12 files incl. UnitDependent; UnitScale B's scale : B → ℝ≥0 erases the LengthUnit/MassUnit/… typed-unit names (they carry no algebraic content, but they're real ergonomics/type-safety). Hard to review while stacked on the bump.

D — Basis-generic and typed.

Attach to a basis B a family of unit types, one per base dimension, each carrying a positive-real magnitude — then let the typed layer project onto the magnitude layer already in the PR:

class UnitSystem (B : Type) where
  Unit    : B → Type                    -- the typed unit at each base
  mag     : {b : B} → Unit b → ℝ≥0      -- its magnitude
  mag_pos : ∀ {b} (u : Unit b), 0 < mag u

/-- A typed unit choice: pick a typed unit at every base dimension. -/
def TypedChoice (B : Type) [UnitSystem B] := (b : B) → UnitSystem.Unit b

/-- Forget the types down to the magnitude layer already in the PR. -/
noncomputable def TypedChoice.toScale {B : Type} [UnitSystem B]
    (u : TypedChoice B) : UnitScale B where
  scale     b := UnitSystem.mag (u b)
  scale_pos b := UnitSystem.mag_pos (u b)

/-- `PhyslibBase`'s instance recovers exactly today's typed names. -/
noncomputable instance : UnitSystem PhyslibBase where
  Unit
    | .length => LengthUnit | .time => TimeUnit | .mass => MassUnit
    | .charge => ChargeUnit | .temperature => TemperatureUnit
  mag {b} := match b with
    | .length | .time | .mass | .charge | .temperature =>
        fun u => ⟨u.val, u.val_pos.le⟩
  mag_pos {b} := match b with
    | .length | .time | .mass | .charge | .temperature =>
        fun u => NNReal.coe_pos.mp u.val_pos

Now u .length : LengthUnit, LengthUnit.meters still works, and you cannot put a MassUnit in the length slot — the dependent type forbids it, same guarantee as the original record.

• Pro: the only option that keeps both properties that matter — full basis-genericity and the typed-unit names/safety. No proof duplication either: the scaling laws stay proved once on the magnitude layer UnitScale B, and the typed layer is a thin faithful wrapper that projects onto it via toScale.
• Pro (already validated): the sketch above isn't hypothetical -- it compiles as-is against this PR (lake env lean over Physlib.Units.ParametricUnits), the PhyslibBase instance and the u .length : LengthUnit type-safety check included.
• Con: the most machinery of the four — a new UnitSystem class plus a dependent (b : B) → Unit b encoding that's marginally less simp/elaboration-friendly than a flat record; and its payoff over B only materialises once a second typed basis actually exists.

Why D makes the most sense. The other three each give up something:

• A leaves the two sides duplicated;
• B unifies the proofs but stays PhyslibBase-only;
• C reaches genericity but discards the typed-unit names that are the whole reason UnitChoices is nicer than a bare B → ℝ≥0.

D is the only one that is generic and type-safe, and it does so by reusing what the PR already has — the laws live once on UnitScale B, with the typed layer sitting cleanly on top.

But the blast radius is real, so I want your concurrence before expanding the diff. D can land two ways:

• D-additive (my preference for this PR) — add UnitSystem/TypedChoice/toScale alongside, keep UnitChoices, and prove UnitChoices ≃ TypedChoice PhyslibBase. Zero churn to the 107 call sites; reviewable stacked on chore: Bump v4.32.0 #1445.

• D-migrate — redefine UnitChoices := TypedChoice PhyslibBase and migrate all 107 references. Type-safe, but as invasive as C; better as its own follow-up PR.

Does D (and specifically D-additive for this PR) match the direction you had in mind, or would you rather keep #1447 to A/B and take the typed-generic layer D separately?

[nateabr]

Hey @NicolasRouquette, please give me a bit to go through the details of your PR and your comment and I will get back to you. Many apologies for the delay

[nateabr]

The core abstraction you have done with parametric Dimension B, PhyslibBase, and backward compat layer looks clean and I'm happy with the math and the proofs. However, the three new files (BasisExamples, ParametricDimensionExamples, ParametricUnits) and the extend/single API have no current use at the moment and seem to be illustrative. My first thought would be to focus the PR to the core parts.

However, even with regards to the core abstraction you have provided; I see the utility in having a parametric type that we could possibly instantiate with a different basis in the future. But purely from a maintenance perspective, this does add complexity to the core dimension type. Furthermore, if the motivation for this PR does lie in a downstream repo, would it make sense for this machinery to live in that repo and not Physlib?

That being said, I do believe I am unable to provide you with a constructive review at the moment, the above is more of my thoughts out loud. So I would say hold off on any changes and wait for a better look from a maintainer.

[NicolasRouquette]

Thanks @nateabr for the feedback.

There were already several examples in the Physlib library per se, so it seemed to me sensible to add other examples for the parametric dimension and basis. However, we're getting to the point where it would make sense to move them out of the library:

public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Examples
public import Physlib.QuantumMechanics.Operators.Examples
public import Physlib.Units.BasisExamples
public import Physlib.Units.Examples
public import Physlib.Units.ParametricDimensionExamples

If someone can provide guidance where to move the unit-related examples, e.g., a ./examples/physlib folder with a separate PhyslibExamples library in the lakefile, I'm OK in doing that refactoring in this PR.

[jstoobysmith]

I think for the units examples we could put them in .Units/Examples for now. Will hopefully get chance to look at this tomorrow. But generally I think the concept of this is good, and should be included.

[jstoobysmith]

Would it be possible to rebase this so only the relevant changes are shown? Also I think a PhyslibBase could have a better more physical name if still called that

[NicolasRouquette]

Thanks @jstoobysmith. Done on the first point, and a pointer on the second.

Rebased to reduce the scope. #1445 landed on master (squashed as c217bdd), so I rebased this branch onto current master. The four v4.32.0 bump-chain commits dropped out — they're already in master — leaving a single feature commit. The PR now shows only the parametric change: 9 files under Physlib/Units/ (Dimension, Basic, UnitDependent, WithDim/Basic, Integral, the new ParametricUnits/BasisExamples/ParametricDimensionExamples, and the Physlib.lean imports), with no toolchain collateral. The feature patch itself is unchanged — only the base moved.

On the name. Agreed that PhyslibBase is worth reconsidering, and I'd raised the same question earlier here: #1447 (comment). Short version: it's the default basis B for the now-parameterised Dimension B — the charge-based five-generator set (length, time, mass, charge, temperature), which is deliberately not the SI/ISQ base-quantity set. I named it after its provenance to flag that it's a specific choice rather than a canonical one, but I'm very open to a more physical/descriptive name. My only constraint is that it should still signal "a specific, non-ISQ choice of base quantities" rather than implying a neutral basis. If you have a preferred convention or a name in mind for this charge-based five-generator set, I'll gladly adopt it.

[jstoobysmith]

awaiting-author

[NicolasRouquette]

Thank you @jstoobysmith for the careful, constructive review — it genuinely sharpened both the scope and the design. Two of your observations reshaped the PR:

1. Two concrete bases instead of illustrative examples. You were right that the example modules carried no weight. I removed them and kept exactly two instantiations:

• LTMCTDimensionBase — the existing basis, renamed after its five base dimensions (length, time, mass, charge, temperature) so the name announces a specific, deliberately non-ISQ choice rather than "the" basis; and
• ISQDimensionBase — the seven ISO/IEC 80000-1 (VIM 3) base quantities, as a reference.

Dimension is now trimmed to the generic algebra, with LTMCT's projections and generators in their own file.

2. Truth-preserving maps between bases, enforced by construction. This is where I'd argue from metrology. Relating two systems of quantities is not a relabelling of base symbols: base-vs-derived is a choice the system makes, not a property of the quantity. Electric charge is a base dimension in the LTMCT system but the derived I·T in the ISQ. The label injection I'd first sketched silently permitted exactly that category error — it could map the charge generator onto the current generator, equating two dimensionally distinct quantities.

So I made the admissible maps first-class, as bundled requirements on Dimension:

• Dimension.Embedding — an injective monoid homomorphism of dimensions (a faithful, dimension-preserving inclusion into a richer basis); and
• Dimension.Projection — a surjective monoid homomorphism (a truth-preserving reduction onto a coarser basis).

Requiring a MonoidHom is what enforces dimensional truth — the map must respect products, inverses and rational powers — so a relabelling that conflates inequivalent base quantities is simply not constructible as either. The LTMCT↔ISQ bridge is then the metrologically honest one: the embedding sends charge to the derived I·T; the projection reads current as charge/time and forgets amount-of-substance and luminous-intensity; and projection ∘ embedding = id states precisely that ISQ reduces onto LTMCT, but not the reverse without adding those base quantities back.

Green across the full build and the style/meta linters. Happy to iterate.

[NicolasRouquette]

-awaiting-author

[jstoobysmith]

Approved - many thanks. Will merge shortly.