Pareto Bridge: Constraint Systems as Feature-Pullback Preorders #
A ConstraintSystem Cand (Profile β n) carries a quantitative violation
profile per candidate plus a decoder. Forgetting the decoder, two natural
preorders on candidates emerge — both are instances of the
Core.Order.FeaturePreorder pattern:
| view | feature | feature-space order |
|---|---|---|
paretoFeaturePreorder | score : Cand → Profile β n | pointwise ≤ |
qualitativeFeaturePreorder | violatedSet : Cand → Finset (Fin n) | subset ⊆ |
Recognising both as FeaturePreorder instances means the implication
"pointwise dominance ⇒ qualitative dominance" is no longer a bespoke
proof — it is a one-line application of
FeaturePreorder.coarsen_via_monotone with the violated-set extractor as
the connecting monotone map.
The gap (qualitative is strictly weaker) #
The forward direction holds whenever zero is the minimum value of β
(e.g. β = Nat, raw violation counts). The converse fails — and worse,
a quantitative winner under OT or HG can be qualitatively dominated.
In OT with constraints C₁ ≫ C₂, a candidate w with profile (0, 5)
beats c' with profile (1, 0) lexicographically, yet w and c' are
qualitatively incomparable: each satisfies one constraint the other
violates. The qualitative coarsening forgets the magnitude trade-off
that lex-min and weighted-sum decoders use to choose a winner. This is
a feature, not a bug — it exposes when a numerical framework's winner
deviates from the Pareto frontier of satisfactions.
Pointwise Pareto preorder as a FeaturePreorder: feature is the
score vector s.score : Cand → Profile β n, feature-space order is
Pi.preorder (pointwise ≤). Read as "c is at-most-as-bad-as c'
on every constraint" under the OT/HG "lower is better" convention.
Equations
- s.paretoFeaturePreorder = Core.Order.FeaturePreorder.ofFeature s.score fun (a a' : Cand) => have this := inferInstance; this
Instances For
The set of constraint indices that c violates (score ≠ 0).
Equations
- s.violatedSet c = {i : Fin n | s.score c i ≠ 0}
Instances For
Qualitative coarsening as a FeaturePreorder: feature is the
violated-constraint set, feature-space order is Finset.⊆.
c ≤ c' iff violatedSet c ⊆ violatedSet c' — every constraint c
violates, c' also violates — equivalently, every constraint c'
satisfies (zero), c also satisfies. This is the qualitative Pareto
backbone underlying Core.Order.SatisfactionOrdering.
Equations
- s.qualitativeFeaturePreorder = Core.Order.FeaturePreorder.ofFeature s.violatedSet fun (x x_1 : Cand) => inferInstance
Instances For
The violated-set extractor Profile β n → Finset (Fin n), as a function
of the score profile alone (no ConstraintSystem needed).
Equations
- Core.Constraint.ConstraintSystem.violatedSetOf p = {i : Fin n | p i ≠ 0}
Instances For
The violated-set extractor is monotone in the pointwise order on
profiles, provided 0 is the minimum element of β. With that
hypothesis, p ≤ p' ⇒ violated p ⊆ violated p': any constraint that
p violates (p i ≠ 0, hence 0 < p i), p' also violates
(p' i ≥ p i > 0). Without zero-as-min the implication can fail
(e.g. p i = -5, p' i = 0 over ℝ).
Pointwise dominance implies qualitative dominance (when zero is
the minimum value of β). A one-line corollary of
FeaturePreorder.coarsen_via_monotone applied to violatedSetOf as
the connecting monotone map between the two feature spaces.
The converse fails by design: equal nonzero counts on a violated constraint give qualitative equivalence but say nothing about further pointwise comparisons.