Feature-Pullback Preorders

A FeaturePreorder Carrier Feature is a Preorder Carrier realized as the pullback of a Preorder Feature through feature : Carrier → Feature. The induced order is a ≤ a' ↔ feature a ≤ feature a'.

This is mathlib's Preorder.lift packaged with the witnessing feature data and decidability of ≤. It is the common pattern behind several constructions in linglib:

• Core.Order.SatisfactionOrdering α Criterion — feature is the satisfied criterion set, feature space is (Finset Criterion)ᵒᵈ (or equivalently, the violated set with standard ⊆).
• Core.Constraint.ConstraintSystem.paretoFeaturePreorder — feature is the score vector, feature space is Profile β n with pointwise ≤.
• Semantics.Modality.Kratzer.worldOrdering — feature is the satisfied proposition set, same shape as SatisfactionOrdering.

The reusable theorem

coarsen_via_monotone states that a monotone map φ : F1 → F2 between feature spaces lifts dominance under the finer feature to dominance under the coarser feature, provided f2 = φ ∘ f1. This is the schema underlying "Pareto-on-violations ⇒ Pareto-on-satisfaction" and any other forgetful coarsening between qualitatively-comparable representations.

structure Core.Order.FeaturePreorder (Carrier : Type u_1) (Feature : Type u_2) [Preorder Feature] extends Preorder Carrier : Type (max u_1 u_2)

A preorder on Carrier realized as the pullback of a Preorder Feature through feature : Carrier → Feature.

extends Preorder Carrier, so all of mathlib's order vocabulary (≤, <, Maximal, IsMax) is available; feature/decLE expose the construction data. le_iff_feature is the load-bearing coherence field — the bundled ≤ agrees with the feature pullback.

• le : Carrier → Carrier → Prop
• lt : Carrier → Carrier → Prop
• le_refl (a : Carrier) : a ≤ a
• le_trans (a b c : Carrier) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : Carrier) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• feature : Carrier → Feature
• decLE (a a' : Carrier) : Decidable (a ≤ a')
• le_iff_feature (a a' : Carrier) : a ≤ a' ↔ self.feature a ≤ self.feature a'

@[implicit_reducible]

instance Core.Order.FeaturePreorder.instDecidableLe {Carrier : Type u_1} {Feature : Type u_2} [Preorder Feature] (o : FeaturePreorder Carrier Feature) (a a' : Carrier) : Decidable (a ≤ a')

Equations

• o.instDecidableLe a a' = o.decLE a a'

def Core.Order.FeaturePreorder.ofFeature {Carrier : Type u_1} {Feature : Type u_2} [Preorder Feature] (feature : Carrier → Feature) (dec : (a a' : Carrier) → Decidable (feature a ≤ feature a')) : FeaturePreorder Carrier Feature

Smart constructor: build a FeaturePreorder from a feature map plus decidability of feature comparison. The induced ≤ is Preorder.lift, so le_iff_feature is Iff.rfl.

Equations

• Core.Order.FeaturePreorder.ofFeature feature dec = { toPreorder := Preorder.lift feature, feature := feature, decLE := dec, le_iff_feature := ⋯ }

theorem Core.Order.FeaturePreorder.coarsen_via_monotone {Carrier : Type u_3} {F1 : Type u_4} {F2 : Type u_5} [Preorder F1] [Preorder F2] (o1 : FeaturePreorder Carrier F1) (o2 : FeaturePreorder Carrier F2) (φ : F1 → F2) (hmono : Monotone φ) (hcoh : ∀ (c : Carrier), o2.feature c = φ (o1.feature c)) {a a' : Carrier} (h : a ≤ a') : a ≤ a'

Change of feature space (coarsening).

Given two FeaturePreorders on the same carrier with feature maps o1.feature : Carrier → F1 and o2.feature : Carrier → F2, plus a monotone map φ : F1 → F2 such that o2.feature = φ ∘ o1.feature, dominance under o1 implies dominance under o2.

The converse generally fails: collapsing the feature space discards information. This is the schema behind every "qualitative coarsening" bridge — e.g. pointwise-Pareto-on-violations ⇒ subset-of-satisfied in Core/Constraint/Pareto.lean.