Pareto preorders on Cand → Profile β n score functions

Two natural preorders on a candidate type carrying a score function Cand → Profile β n, both instances of the Core.Order.PullbackPreorder pattern:

view	feature	feature-space order
paretoPullbackPreorder	score : Cand → Profile β n	pointwise ≤
supportPullbackPreorder	support : Cand → Finset (Fin n)	subset ⊆

Recognising both as PullbackPreorder instances means the implication "pointwise dominance ⇒ subset-of-supports dominance" is a one-line application of PullbackPreorder.coarsen_via_monotone with the support extractor as the connecting monotone map.

When 0 ≤ b for every b : β (so larger profile values are bigger), pointwise dominance implies subset dominance of the nonzero-coordinate set; the converse fails — see paretoPullbackPreorder_le_implies_supportPullbackPreorder_le.

def Core.Optimization.paretoPullbackPreorder {Cand : Type u_1} {β : Type u_2} {n : ℕ} [Preorder β] [(x y : β) → Decidable (x ≤ y)] (score : Cand → Profile β n) : Order.PullbackPreorder Cand (Profile β n)

Pointwise Pareto preorder as a PullbackPreorder: 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' pointwise" under the "lower is better" convention.

Equations

• Core.Optimization.paretoPullbackPreorder score = Core.Order.PullbackPreorder.ofProj score fun (a a' : Cand) => have this := inferInstance; this

def Core.Optimization.nonzeroSet {Cand : Type u_1} {β : Type u_2} {n : ℕ} [DecidableEq β] [Zero β] (score : Cand → Profile β n) (c : Cand) : Finset (Fin n)

The set of indices at which the score is nonzero.

Equations

• Core.Optimization.nonzeroSet score c = {i : Fin n | score c i ≠ 0}

def Core.Optimization.supportPullbackPreorder {Cand : Type u_1} {β : Type u_2} {n : ℕ} [DecidableEq β] [Zero β] (score : Cand → Profile β n) : Order.PullbackPreorder Cand (Finset (Fin n))

Qualitative coarsening as a PullbackPreorder: feature is the nonzero-coordinate set, feature-space order is Finset.⊆.

c ≤ c' iff the nonzero-index set of c is a subset of that of c' — every index at which c' = 0, also c = 0. This is the qualitative Pareto backbone underlying Core.Order.SatisfactionOrdering.

Equations

• Core.Optimization.supportPullbackPreorder score = Core.Order.PullbackPreorder.ofProj (Core.Optimization.nonzeroSet score) fun (x x_1 : Cand) => inferInstance

def Core.Optimization.nonzeroSetOf {β : Type u_2} {n : ℕ} [DecidableEq β] [Zero β] (p : Profile β n) : Finset (Fin n)

The violated-set extractor Profile β n → Finset (Fin n), as a function of the score profile alone (no ConstraintSystem needed).

Equations

• Core.Optimization.nonzeroSetOf p = {i : Fin n | p i ≠ 0}

theorem Core.Optimization.nonzeroSetOf_monotone {β : Type u_2} {n : ℕ} [PartialOrder β] [Zero β] [DecidableEq β] (h_zero_min : ∀ (b : β), 0 ≤ b) : Monotone nonzeroSetOf

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 index where p is nonzero (hence positive when 0 is the minimum), p' is also nonzero (p' i ≥ p i > 0). Without zero-as-min the implication can fail (e.g. p i = -5, p' i = 0 over ℝ).

theorem Core.Optimization.paretoPullbackPreorder_le_implies_supportPullbackPreorder_le {Cand : Type u_1} {β : Type u_2} {n : ℕ} [PartialOrder β] [Zero β] [DecidableEq β] [(x y : β) → Decidable (x ≤ y)] (score : Cand → Profile β n) (h_zero_min : ∀ (b : β), 0 ≤ b) {c c' : Cand} (h : c ≤ c') : c ≤ c'

Pointwise dominance implies qualitative dominance (when zero is the minimum value of β). A one-line corollary of PullbackPreorder.coarsen_via_monotone applied to nonzeroSetOf as the connecting monotone map between the two feature spaces.

The converse fails by design: equal nonzero values at a single index give qualitative equivalence but say nothing about further pointwise comparisons.