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?