Lenient/strict mode: escalate tag-coherence widening to eager findings (incl. tag-blind min/max)

Background

docs/design/domain-type-algebra.md §"Lenient and strict modes" already specifies this. The produce rules widen a no-claim (Top) operand under an agreement-requiring operator rather than flagging it — the lenient default, right for a codebase being onboarded where an eager finding on every contact with an untyped magnitude would bury the real ones. A strict mode keeps the same lattice and produce rules and differs only in raising a finding where lenient widens, "on the reading that the author was obliged to tag every magnitude that reaches such an operator."

The doc is explicit that strict must be "a coherent switch rather than a scatter of flags," with a recorded list of divergence points.

Divergence points (recorded)

• Additive Top operand. money + untagged (and -). Lenient produces Top; strict flags adding an un-dimensioned magnitude to a dimensioned one.
• Comparison/ordering against a Top operand. money = untagged, join-key equality, ordering. Lenient produces a tag-free boolean and asks nothing of the untagged side; strict flags it.
• Tag-blind min/max selection (new, from #115). #115 classifies min/max as SELECT and widens the result tag to top on a varying companion (lenient, and near-silent today since the lazy catch sites — see #47 — are not built). Strict should raise an eager finding here: it is the "ordering against Top" divergence extended to the select-aggregate case (min(amount) over mixed currency compares raw numbers across currencies).

Requirements

• A single mode switch (CLI flag / project config), not per-check flags.
• Strict escalates exactly the recorded divergence points above; lenient stays the default.
• Strict findings must be suppressible via check-path suppression (separate issue) so an intentional case (a deliberate "cheapest line item") has a noqa escape hatch.
• Define the switch framework-wide so future conditional hazards (e.g. the unverified-FD discharge) attach to it coherently rather than as new ad-hoc flags.

Dependencies / related

• #115 lands the widen-to-top semantics strict escalates.
• Check-path suppression issue (the noqa escape hatch).
• #47 (typed/untyped seam-erasure diagnostic) is the lenient lazy-catch counterpart.

Start with docs/design/domain-type-algebra.md, especially the “Lenient and strict modes” section, then inspect the implementation areas affected by #115 and the lazy catch sites referenced in #47. Define one CLI or project-config switch and record the three divergence points; done means lenient remains default, strict eagerly reports exactly those cases, and the framework can support future conditional hazards.