Scored choice systems

A ConstraintSystem Cand Score packages the three components of a scored-choice problem into a single record:

1. a finite candidates : Finset Cand,
2. a score : Cand → Score function, and
3. a decoder : Decoder Cand Score mapping scored candidates to a probability distribution.

  Candidates  ──score──▶  Score   ──decoder──▶   P : Cand → ℝ

Every system exposes a single predict operation. Probability-preserving decoders (Decoder.IsProb) yield non-negative predictions that sum to 1.

A closed-form predict and standard monotonicity / equiprobability / sum-to-one lemmas for the softmaxDecoder specialisation also live here, since they depend only on the record + softmaxDecoder from Decoder.lean — no domain-specific score type is required.

Domain-specific instantiations (lex-min on integer cost vectors, weighted-sum scoring, softmax over weighted sums, ...) live in the consuming layer.

structure Core.Optimization.ConstraintSystem (Cand : Type u_1) (Score : Type u_2) : Type (max u_1 u_2)

A scored-choice system: candidate set + score function + decoder.

• candidates : Finset Cand

  The finite set of candidates this system evaluates.

• score : Cand → Score

  The aggregated score for each candidate.

• decoder : Decoder Cand Score

  The choice rule: scored candidates → probability distribution.

def Core.Optimization.ConstraintSystem.predict {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) : Cand → ℝ

The predicted probability of each candidate.

Equations

• s.predict = s.decoder.decode s.candidates s.score

theorem Core.Optimization.ConstraintSystem.predict_nonneg {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) [s.decoder.IsProb] (c : Cand) : 0 ≤ s.predict c

A system whose decoder is IsProb produces non-negative predictions.

theorem Core.Optimization.ConstraintSystem.predict_sum_eq_one {Cand : Type u_1} {Score : Type u_2} (s : ConstraintSystem Cand Score) [s.decoder.IsProb] (hne : s.candidates.Nonempty) : ∑ c ∈ s.candidates, s.predict c = 1

A system whose decoder is IsProb predicts a probability distribution over its candidate set.

Softmax-decoder specialisations

Closed-form / monotonicity / equiprobability lemmas for ConstraintSystems whose decoder = softmaxDecoder α. The hypothesis hd : s.decoder = softmaxDecoder α is rfl for the explicit-record construction pattern.

theorem Core.Optimization.ConstraintSystem.predict_softmax_of_mem {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) {c : Cand} (hc : c ∈ s.candidates) : s.predict c = Real.exp (α * s.score c) / ∑ c' ∈ s.candidates, Real.exp (α * s.score c')

For a system whose decoder is softmaxDecoder α, the predicted probability of an in-set candidate has the standard closed form exp(α · score(c)) / Σ exp(α · score(c')).

theorem Core.Optimization.ConstraintSystem.predict_softmax_lt_of_score_lt {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hα : 0 < α) (hd : s.decoder = softmaxDecoder α) {c1 c2 : Cand} (h1 : c1 ∈ s.candidates) (h2 : c2 ∈ s.candidates) (hlt : s.score c1 < s.score c2) : s.predict c1 < s.predict c2

Softmax monotonicity: for α > 0, the in-set candidate with strictly higher score gets strictly higher predicted probability.

theorem Core.Optimization.ConstraintSystem.predict_softmax_eq_of_score_eq {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) {c1 c2 : Cand} (h1 : c1 ∈ s.candidates) (h2 : c2 ∈ s.candidates) (heq : s.score c1 = s.score c2) : s.predict c1 = s.predict c2

Softmax equality: candidates with equal scores get equal predicted probability.

theorem Core.Optimization.ConstraintSystem.predict_softmax_isProb {Cand : Type u_1} (s : ConstraintSystem Cand ℝ) {α : ℝ} (hd : s.decoder = softmaxDecoder α) (hne : s.candidates.Nonempty) : ∑ c ∈ s.candidates, s.predict c = 1

For a system whose decoder is softmaxDecoder α, predicted probabilities sum to 1 over the (non-empty) candidate set. Specialises predict_sum_eq_one so consumers needn't supply the IsProb instance argument explicitly.