feat(Units): parameterize the typed unit side (UnitSystem, LTMCTUnitChoices, SIUnitChoices)

[NicolasRouquette]

Closes #1480.

Finishes the unit-side counterpart to #1447 (which parameterized Dimension over a basis and added the magnitude twin UnitScale B). The typed unit choice was still welded to LTMCTDimensionBase; this makes it basis-generic while keeping typed-unit safety, following Option D from the #1447 review. Full rationale, the blast-radius map, and the "why not A/B/C" analysis are in #1480.

What's here (three reviewable commits)

1. feat(Units): additive core — class UnitSystem B (Unit : B → Type, mag, mag_pos), TypedChoice B := (b : B) → UnitSystem.Unit b, TypedChoice.toScale : TypedChoice B → UnitScale B, the LTMCTDimensionBase instance, LTMCTUnitChoices ≃ TypedChoice LTMCTDimensionBase, and dimScale_eq_toScale_dimScale (the hand-rolled five-factor dimScale equals the generic Finset.prod fold — one source of truth). @[ext] added to UnitScale. No existing call site changes.
2. refactor(Units): rename UnitChoices → LTMCTUnitChoices — it is inherently the unit choice for LTMCTDimensionBase (its fields hardcode the five …Unit types), so the name now mirrors the dimension basis. Stays a record: { SI with length := … }, u.length, ⟨…⟩, @[ext] all unchanged. Whole-word rename, all ~112 references under Physlib/Units/.
3. feat(Units): SIUnitChoices — SIUnitChoices := TypedChoice ISQDimensionBase, the typed SI unit choice over the seven ISQ base quantities, from the same machinery. Adds CurrentUnit / AmountUnit / LuminousIntensityUnit (ampere / mole / candela), instance : UnitSystem ISQDimensionBase, the coherent SIUnitChoices.SI (m, kg, s, A, K, mol, cd), and a dimScale reused from the generic fold. Pairs ISQDimensionBase ↔ SIUnitChoices beside LTMCTDimensionBase ↔ LTMCTUnitChoices, with the existing ltmctToISQ / isqToLTMCT already bridging the bases.

(A fourth commit wraps two signatures the rename pushed past 100 columns.)

Acceptance criteria (from #1480)

• UnitSystem, TypedChoice, TypedChoice.toScale added and building, indexed in Physlib.lean.
• instance : UnitSystem LTMCTDimensionBase recovering the five typed unit names, with a u .length : LengthUnit type-safety check.
• LTMCTUnitChoices ≃ TypedChoice LTMCTDimensionBase.
• LTMCTUnitChoices.dimScale = UnitScale.dimScale ∘ toScale (law-unification), a single source of truth for the scaling law on the magnitude layer.
• UnitChoices renamed to LTMCTUnitChoices (record kept; ergonomics unchanged).
• SIUnitChoices := TypedChoice ISQDimensionBase with UnitSystem ISQDimensionBase, the three new ISQ typed unit types, SIUnitChoices.SI, and a u .current : CurrentUnit type-safety check; its dimScale reuses the generic fold.
• Full Physlib build green; axioms classical-only on the new results.

Verification

Ran the build.yml gate locally on this branch — all green:

• lake build -KCI — 9266 jobs
• check_file_imports, check_dup_tags, sorry_lint — pass
• runPhyslibLinters — Physlib + QuantumInfo pass
• scripts/lint-style.sh, api_map_linter.py, codespell — pass
• Axioms of the new results: propext, Classical.choice, Quot.sound only (no sorryAx).

Notes for reviewers: the three new unit types (CurrentUnit / AmountUnit / LuminousIntensityUnit) are minimal (positive-real magnitude + division); their full scale/relation API, and relocation to the appropriate physics directories following the LengthUnit convention, can be a follow-up. Happy to split this into separate PRs (core / rename / second basis) if that's easier to review.

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