Harmony: evaluation and dominance lemmas #
The reusable lemma layer over harmonyScore/weightedViolations
(Constraints.Defs), shaped so Harmonic-Grammar study files reason about
concrete grammars without hand-unfolding Finset.sum.
Main results #
harmonyScore_cons/harmonyScore_nil,weightedViolations_cons/weightedViolations_nil—@[simp]cons-recursion that evaluates harmony on a literal grammar![C₀, …]/.harmonyScore_le_of_forall_le,harmonyDominates_of_lt— harmonic bounding: a candidate with pointwise-fewer violations under non-negative weights has at least (resp. strictly greater) harmony. The Pareto argument most HG studies make, stated directly over the violation profile rather than via the weighted sum.
Evaluation by cons-recursion #
@[simp]
theorem
Constraints.weightedViolations_nil
(w : Fin 0 → ℝ)
(v : Fin 0 → ℕ)
:
weightedViolations w v = 0
@[simp]
theorem
Constraints.weightedViolations_cons
{n : ℕ}
(w₀ : ℝ)
(w : Fin n → ℝ)
(v₀ : ℕ)
(v : Fin n → ℕ)
:
weightedViolations (Matrix.vecCons w₀ w) (Matrix.vecCons v₀ v) = w₀ * ↑v₀ + weightedViolations w v
@[simp]
theorem
Constraints.harmonyScore_nil
{C : Type u_1}
(con : CON C 0)
(w : Fin 0 → ℝ)
(x : C)
:
harmonyScore con w x = 0
@[simp]
theorem
Constraints.harmonyScore_cons
{C : Type u_1}
{n : ℕ}
(c₀ : Constraint C)
(con : CON C n)
(w₀ : ℝ)
(w : Fin n → ℝ)
(x : C)
:
harmonyScore (Matrix.vecCons c₀ con) (Matrix.vecCons w₀ w) x = -(w₀ * ↑(c₀ x)) + harmonyScore con w x
Harmonic bounding (Pareto dominance) #
theorem
Constraints.harmonyScore_le_of_forall_le
{C : Type u_1}
{n : ℕ}
{con : CON C n}
{w : Fin n → ℝ}
{a b : C}
(hw : ∀ (i : Fin n), 0 ≤ w i)
(h : ∀ (i : Fin n), con i a ≤ con i b)
:
Harmonic bounding (weak): with non-negative weights, a candidate a
that incurs no more violations than b on every constraint has at least b's
harmony. The monotone core of OT's harmonic-bounding argument.
theorem
Constraints.harmonyDominates_of_lt
{C : Type u_1}
{n : ℕ}
{con : CON C n}
{w : Fin n → ℝ}
{a b : C}
(hw : ∀ (i : Fin n), 0 ≤ w i)
(hle : ∀ (i : Fin n), con i a ≤ con i b)
(hlt : ∃ (i : Fin n), 0 < w i ∧ con i a < con i b)
:
harmonyDominates con w a b
Harmonic bounding (strict): with non-negative weights, if a incurs no
more violations than b everywhere and strictly fewer on some positively-weighted
constraint, then a strictly dominates b in harmony. Lets a study conclude
harmonyDominates con w a b from a violation-profile comparison alone.