Selection and decreasing multiset complexity

Selection minimizes an ordinal priority, then maximizes an ordinal weight, with a fixed well-order resolving ties. Complexity records the weights of distinct members at least as heavy as the selection, followed by the selected multiplicity. Thus duplicating other members does not increase the first component.

Removing one selected copy, doubling the other multiplicities, and adjoining lighter members of no smaller priority strictly decreases this well-founded complexity. The argument abstracts the finite-expression reduction in Berarducci, Definitions 9.1--9.3 and Lemma 9.5; it assumes no series, ring, or valuation. The first component uses the Mathlib Dershowitz--Manna relation.

structure Multiset.SelectionWeights (α : Type v) : Type (max (u + 1) v)

Ordinal priorities and weights for selection in a finite multiset.

• priority : α → Ordinal.{u}

  The ordinal priority to minimize when selecting a multiset member.

• weight : α → Ordinal.{u}

  The ordinal weight to maximize among members of equal least priority.

structure Multiset.SelectionWeights.IsSelected {α : Type v} (s : SelectionWeights α) (w : Multiset α) (x : α) : Prop

A member of least priority, greatest weight among those, and least in a fixed well-order.

• mem : x ∈ w
• min_priority (y : α) : y ∈ w → s.priority x ≤ s.priority y
• max_weight (y : α) : y ∈ w → s.priority y = s.priority x → s.weight y ≤ s.weight x
• least (y : α) : y ∈ w → s.priority y = s.priority x → s.weight y = s.weight x → ¬WellOrderingRel y x

theorem Multiset.SelectionWeights.existsUnique_isSelected {α : Type v} (s : SelectionWeights α) {w : Multiset α} (hw : w ≠ 0) : ∃! x : α, s.IsSelected w x

Every nonempty finite multiset has a unique selected member.

noncomputable def Multiset.SelectionWeights.selected {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : α

The selected member of a nonempty multiset.

Equations

• s.selected w hw = Exists.choose ⋯

theorem Multiset.SelectionWeights.isSelected_selected {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : s.IsSelected w (s.selected w hw)

theorem Multiset.SelectionWeights.eq_selected_of_isSelected {α : Type v} (s : SelectionWeights α) {w : Multiset α} (hw : w ≠ 0) {x : α} (hx : s.IsSelected w x) : x = s.selected w hw

theorem Multiset.SelectionWeights.selected_singleton {α : Type v} (s : SelectionWeights α) (x : α) : s.selected {x} ⋯ = x

noncomputable def Multiset.SelectionWeights.selectedExponent {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : ℕ

The multiplicity of the selected member.

Equations

• s.selectedExponent w hw = Multiset.count (s.selected w hw) w

theorem Multiset.SelectionWeights.selected_cons_of_mem {α : Type v} (s : SelectionWeights α) {w : Multiset α} (hw : w ≠ 0) {y : α} (hy : y ∈ w) : s.selected (y ::ₘ w) ⋯ = s.selected w hw

theorem Multiset.SelectionWeights.selectedExponent_eq_count {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : s.selectedExponent w hw = count (s.selected w hw) w

noncomputable def Multiset.SelectionWeights.relevantValues {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : Multiset Ordinal.{u}

The weights of distinct members at least as heavy as the selected member.

Equations

• s.relevantValues w hw = Multiset.map (fun (y : α) => s.weight y) {y ∈ w.toFinset | s.weight (s.selected w hw) ≤ s.weight y}.val

theorem Multiset.SelectionWeights.relevantValues_eq_map {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : s.relevantValues w hw = map (fun (y : α) => s.weight y) {y ∈ w.toFinset | s.weight (s.selected w hw) ≤ s.weight y}.val

theorem Multiset.SelectionWeights.relevantValues_congr {α : Type v} (s : SelectionWeights α) {w w' : Multiset α} (hw : w ≠ 0) (hw' : w' ≠ 0) (hsel : s.selected w hw = s.selected w' hw') (hmem : ∀ (y : α), s.weight (s.selected w hw) ≤ s.weight y → (y ∈ w ↔ y ∈ w')) : s.relevantValues w hw = s.relevantValues w' hw'

Equal selections and equal relevant members give the same relevant-weight multiset.

noncomputable def Multiset.SelectionWeights.complexity {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : Multiset Ordinal.{u} × ℕ

The distinct relevant weights, followed by the selected multiplicity.

Equations

• s.complexity w hw = (s.relevantValues w hw, s.selectedExponent w hw)

def Multiset.SelectionWeights.ComplexityLT : Multiset Ordinal.{u_1} × ℕ → Multiset Ordinal.{u_1} × ℕ → Prop

Lexicographic decrease of relevant weights in the Dershowitz--Manna order, then multiplicity.

Equations

• Multiset.SelectionWeights.ComplexityLT = Prod.Lex Multiset.IsDershowitzMannaLT fun (x1 x2 : ℕ) => x1 < x2

theorem Multiset.SelectionWeights.wellFounded_complexityLT : WellFounded ComplexityLT

The complexity order is well-founded.

theorem Multiset.SelectionWeights.complexityLT_of_relevantValues {α : Type v} (s : SelectionWeights α) {w w' : Multiset α} {hw : w ≠ 0} {hw' : w' ≠ 0} {X Y Z : Multiset Ordinal.{u}} (hZ : Z ≠ 0) (hw'X : s.relevantValues w' hw' = X + Y) (hwX : s.relevantValues w hw = X + Z) (hYZ : ∀ y ∈ Y, ∃ z ∈ Z, y < z) : ComplexityLT (s.complexity w' hw') (s.complexity w hw)

theorem Multiset.SelectionWeights.complexityLT_of_selectedExponent {α : Type v} (s : SelectionWeights α) {w w' : Multiset α} {hw : w ≠ 0} {hw' : w' ≠ 0} (h₁ : s.relevantValues w' hw' = s.relevantValues w hw) (h₂ : s.selectedExponent w' hw' < s.selectedExponent w hw) : ComplexityLT (s.complexity w' hw') (s.complexity w hw)

noncomputable def Multiset.SelectionWeights.unselected {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : Multiset α

The multiset remaining after removing every copy of the selected member.

Equations

• s.unselected w hw = Multiset.filter (fun (x : α) => x ≠ s.selected w hw) w

theorem Multiset.SelectionWeights.unselected_eq {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : s.unselected w hw = filter (fun (x : α) => x ≠ s.selected w hw) w

theorem Multiset.SelectionWeights.mem_unselected {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {y : α} : y ∈ s.unselected w hw ↔ y ∈ w ∧ y ≠ s.selected w hw

noncomputable def Multiset.SelectionWeights.reduced {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) (t : Multiset α) : Multiset α

Remove one selected copy, double all other copies, and adjoin the replacement multiset.

Equations

• s.reduced w hw t = t + Multiset.replicate (s.selectedExponent w hw - 1) (s.selected w hw) + (s.unselected w hw + s.unselected w hw)

theorem Multiset.SelectionWeights.reduced_eq {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) (t : Multiset α) : s.reduced w hw t = t + replicate (s.selectedExponent w hw - 1) (s.selected w hw) + (s.unselected w hw + s.unselected w hw)

theorem Multiset.SelectionWeights.mem_reduced {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {t : Multiset α} {y : α} : y ∈ s.reduced w hw t ↔ y ∈ t ∨ s.selectedExponent w hw - 1 ≠ 0 ∧ y = s.selected w hw ∨ y ∈ w ∧ y ≠ s.selected w hw

theorem Multiset.SelectionWeights.one_le_selectedExponent {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : 1 ≤ s.selectedExponent w hw

theorem Multiset.SelectionWeights.count_selected_reduced {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {t : Multiset α} (ht : s.selected w hw ∉ t) : count (s.selected w hw) (s.reduced w hw t) = s.selectedExponent w hw - 1

A replacement excluding the selected member reduces its multiplicity by one.

theorem Multiset.SelectionWeights.count_reduced_of_ne {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {t : Multiset α} {y : α} (hy : y ≠ s.selected w hw) (hyt : y ∉ t) : count y (s.reduced w hw t) = 2 * count y w

A member distinct from the selection and absent from the replacement is doubled.

theorem Multiset.SelectionWeights.selected_mem_reduced {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {t : Multiset α} (hk : 1 < s.selectedExponent w hw) : s.selected w hw ∈ s.reduced w hw t

theorem Multiset.SelectionWeights.selectedExponent_lt_of_isSelected {α : Type v} (s : SelectionWeights α) {w : Multiset α} {hw : w ≠ 0} {t : Multiset α} (hw₂ : s.reduced w hw t ≠ 0) (ht : s.selected w hw ∉ t) (hsel : s.selected (s.reduced w hw t) hw₂ = s.selected w hw) : s.selectedExponent (s.reduced w hw t) hw₂ < s.selectedExponent w hw

theorem Multiset.SelectionWeights.isSelected_reduced {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) (t : Multiset α) (ht : ∀ u ∈ t, s.weight u < s.weight (s.selected w hw)) (htp : ∀ u ∈ t, s.priority (s.selected w hw) ≤ s.priority u) (hk : 1 < s.selectedExponent w hw) : s.IsSelected (s.reduced w hw t) (s.selected w hw)

If a selected copy remains, lighter replacements of no smaller priority preserve selection.

theorem Multiset.SelectionWeights.complexityLT_of_forall_lt_or_mem {α : Type v} (s : SelectionWeights α) {w w' : Multiset α} (hw : w ≠ 0) (hw' : w' ≠ 0) (h : ∀ u ∈ w', s.weight u < s.weight (s.selected w hw) ∨ u ∈ w ∧ u ≠ s.selected w hw) : ComplexityLT (s.complexity w' hw') (s.complexity w hw)

Deleting the selection and introducing only lighter new members strictly lowers complexity.

theorem Multiset.SelectionWeights.complexityLT_unselected {α : Type v} (s : SelectionWeights α) {w : Multiset α} (hw : w ≠ 0) (hr : s.unselected w hw ≠ 0) : ComplexityLT (s.complexity (s.unselected w hw) hr) (s.complexity w hw)

Removing every selected copy strictly lowers complexity when the remainder is nonempty.

theorem Multiset.SelectionWeights.complexityLT_reduced {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) (t : Multiset α) (ht : ∀ u ∈ t, s.weight u < s.weight (s.selected w hw)) (htp : ∀ u ∈ t, s.priority (s.selected w hw) ≤ s.priority u) (hw₂ : s.reduced w hw t ≠ 0) : ComplexityLT (s.complexity (s.reduced w hw t) hw₂) (s.complexity w hw)

Replacing one selected copy by lighter members of no smaller priority strictly lowers complexity, even while doubling every other member.

theorem Multiset.SelectionWeights.replicate_selectedExponent_add_unselected {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : replicate (s.selectedExponent w hw) (s.selected w hw) + s.unselected w hw = w

The selected copies and the remaining factors partition the original multiset.

theorem Multiset.SelectionWeights.complexity_eq {α : Type v} (s : SelectionWeights α) (w : Multiset α) (hw : w ≠ 0) : s.complexity w hw = (s.relevantValues w hw, s.selectedExponent w hw)

The complexity consists of the relevant distinct-factor weights and selected multiplicity.