OT Constraints for Numerical Expressions

@cite{cummins-2015} @cite{cummins-franke-2021}

Optimality-Theoretic constraint system for numeral production. Speakers choose among candidate numeral expressions by optimizing across four ranked constraints:

1. INFO (informativeness): prefer smaller admitted set
2. Granularity: match contextual precision level
3. QSIMP (quantifier simplicity): prefer bare numerals
4. NSAL (numeral salience): prefer round/salient numerals

The key insight connecting to the k-ness model (Phenomena.Gradability.Imprecision.Numerals): NSAL violations = maxRoundnessScore - roundnessScore(n). Rounder numbers incur fewer NSAL violations, making them preferred candidates.

Connection to RSA

The OT constraints map onto RSA parameters:

• INFO ↔ literal semantics φ (truth-conditional informativeness)
• Granularity ↔ QUD (contextual precision level)
• QSIMP ↔ utterance cost (modifier complexity)
• NSAL ↔ utterance cost (roundness-based salience)

Connection to @cite{cummins-franke-2021}

enrichmentWidth predicts pragmatic enrichment range width from roundnessScore. 100 (score 6) gets a wider enriched range than 110 (score 2), explaining why "more than 100" has weaker argumentative strength per C&F's pragmatic reversal.

inductive Implicature.Constraints.NumericalExpressions.QuantifierForm : Type

Form of the numeral expression.

Bare numerals are simplest; modified forms add complexity.

• bare : QuantifierForm
• modified : QuantifierForm
• interval : QuantifierForm

instance Implicature.Constraints.NumericalExpressions.instReprQuantifierForm : Repr QuantifierForm

Equations

• Implicature.Constraints.NumericalExpressions.instReprQuantifierForm = { reprPrec := Implicature.Constraints.NumericalExpressions.instReprQuantifierForm.repr }

def Implicature.Constraints.NumericalExpressions.instReprQuantifierForm.repr : QuantifierForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Implicature.Constraints.NumericalExpressions.instDecidableEqQuantifierForm : DecidableEq QuantifierForm

Equations

• Implicature.Constraints.NumericalExpressions.instDecidableEqQuantifierForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.Constraints.NumericalExpressions.instBEqQuantifierForm.beq : QuantifierForm → QuantifierForm → Bool

Equations

• Implicature.Constraints.NumericalExpressions.instBEqQuantifierForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.Constraints.NumericalExpressions.instBEqQuantifierForm : BEq QuantifierForm

Equations

• Implicature.Constraints.NumericalExpressions.instBEqQuantifierForm = { beq := Implicature.Constraints.NumericalExpressions.instBEqQuantifierForm.beq }

structure Implicature.Constraints.NumericalExpressions.NumeralCandidate : Type

A candidate numeral expression for OT evaluation.

• numeral : ℕ

  The numeral used

• actualValue : ℕ

  Actual value being communicated

• form : QuantifierForm

  Quantifier form

• contextGranularity : ℕ

  Contextual granularity level (trailing zeros in context numeral)

def Implicature.Constraints.NumericalExpressions.instReprNumeralCandidate.repr : NumeralCandidate → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Implicature.Constraints.NumericalExpressions.instReprNumeralCandidate : Repr NumeralCandidate

Equations

• Implicature.Constraints.NumericalExpressions.instReprNumeralCandidate = { reprPrec := Implicature.Constraints.NumericalExpressions.instReprNumeralCandidate.repr }

def Implicature.Constraints.NumericalExpressions.inferGranularity (n : ℕ) : ℕ

Infer granularity from a numeral's trailing zeros.

100 → 2 (precision to hundreds) 110 → 1 (precision to tens) 111 → 0 (precision to units)

Equations

• One or more equations did not get rendered due to their size.

def Implicature.Constraints.NumericalExpressions.infoViolations (admittedCount : ℕ) : ℕ

INFO (informativeness): prefer more informative expressions.

Violations = |admitted set| - 1. An expression that admits more values is less informative and incurs more violations.

Equations

• Implicature.Constraints.NumericalExpressions.infoViolations admittedCount = admittedCount - 1

def Implicature.Constraints.NumericalExpressions.granularityViolations (contextGranularity uttGranularity : ℕ) : ℕ

Granularity: match the contextual precision level.

Violations = absolute difference between context granularity and utterance granularity. A granularity mismatch (e.g., saying "100" when context demands unit precision) is penalized.

Equations

• One or more equations did not get rendered due to their size.

def Implicature.Constraints.NumericalExpressions.qsimpViolations : QuantifierForm → ℕ

QSIMP (quantifier simplicity): prefer bare numerals.

bare = 0, modified = 1, interval = 2

Equations

• Implicature.Constraints.NumericalExpressions.qsimpViolations Implicature.Constraints.NumericalExpressions.QuantifierForm.bare = 0
• Implicature.Constraints.NumericalExpressions.qsimpViolations Implicature.Constraints.NumericalExpressions.QuantifierForm.modified = 1
• Implicature.Constraints.NumericalExpressions.qsimpViolations Implicature.Constraints.NumericalExpressions.QuantifierForm.interval = 2

def Implicature.Constraints.NumericalExpressions.nsalViolations (n : ℕ) : ℕ

NSAL (numeral salience): prefer round/salient numerals.

Violations = maxRoundnessScore - roundnessScore(n). Maximally round numbers (score 6) incur 0 violations. Non-round numbers (score 0) incur 6 violations.

This is the key connection to the k-ness model: NSAL is the complement of the graded roundness score.

Equations

• Implicature.Constraints.NumericalExpressions.nsalViolations n = Core.Roundness.maxRoundnessScore - Core.Roundness.roundnessScore n

theorem Implicature.Constraints.NumericalExpressions.nsal_100 : nsalViolations 100 = 0

theorem Implicature.Constraints.NumericalExpressions.nsal_7 : nsalViolations 7 = 6

theorem Implicature.Constraints.NumericalExpressions.nsal_50 : nsalViolations 50 = 2

theorem Implicature.Constraints.NumericalExpressions.nsal_is_complement (n : ℕ) (h : Core.Roundness.roundnessScore n ≤ Core.Roundness.maxRoundnessScore) : nsalViolations n + Core.Roundness.roundnessScore n = Core.Roundness.maxRoundnessScore

NSAL violations are the complement of roundness score.

structure Implicature.Constraints.NumericalExpressions.OTConstraint : Type

An OT constraint with name, violation function, and rank.

Higher rank = more dominant in the hierarchy.

• name : String
• rank : ℕ

instance Implicature.Constraints.NumericalExpressions.instReprOTConstraint : Repr OTConstraint

Equations

• Implicature.Constraints.NumericalExpressions.instReprOTConstraint = { reprPrec := Implicature.Constraints.NumericalExpressions.instReprOTConstraint.repr }

def Implicature.Constraints.NumericalExpressions.instReprOTConstraint.repr : OTConstraint → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Implicature.Constraints.NumericalExpressions.INFO : OTConstraint

The four constraints with default ranking.

Equations

• Implicature.Constraints.NumericalExpressions.INFO = { name := "INFO", rank := 4 }

def Implicature.Constraints.NumericalExpressions.GRANULARITY : OTConstraint

Equations

• Implicature.Constraints.NumericalExpressions.GRANULARITY = { name := "Granularity", rank := 3 }

def Implicature.Constraints.NumericalExpressions.QSIMP : OTConstraint

Equations

• Implicature.Constraints.NumericalExpressions.QSIMP = { name := "QSIMP", rank := 2 }

def Implicature.Constraints.NumericalExpressions.NSAL : OTConstraint

Equations

• Implicature.Constraints.NumericalExpressions.NSAL = { name := "NSAL", rank := 1 }

def Implicature.Constraints.NumericalExpressions.defaultRanking : List OTConstraint

Default ranking: INFO >> Granularity >> QSIMP >> NSAL.

Equations

• One or more equations did not get rendered due to their size.

structure Implicature.Constraints.NumericalExpressions.ViolationProfile : Type

Violation profile for a candidate: one Nat per constraint, in ranking order.

• info : ℕ
• granularity : ℕ
• qsimp : ℕ
• nsal : ℕ

def Implicature.Constraints.NumericalExpressions.instReprViolationProfile.repr : ViolationProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Implicature.Constraints.NumericalExpressions.instReprViolationProfile : Repr ViolationProfile

Equations

• Implicature.Constraints.NumericalExpressions.instReprViolationProfile = { reprPrec := Implicature.Constraints.NumericalExpressions.instReprViolationProfile.repr }

instance Implicature.Constraints.NumericalExpressions.instDecidableEqViolationProfile : DecidableEq ViolationProfile

Equations

• Implicature.Constraints.NumericalExpressions.instDecidableEqViolationProfile = Implicature.Constraints.NumericalExpressions.instDecidableEqViolationProfile.decEq

def Implicature.Constraints.NumericalExpressions.instDecidableEqViolationProfile.decEq (x✝ x✝¹ : ViolationProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance Implicature.Constraints.NumericalExpressions.instBEqViolationProfile : BEq ViolationProfile

Equations

• Implicature.Constraints.NumericalExpressions.instBEqViolationProfile = { beq := Implicature.Constraints.NumericalExpressions.instBEqViolationProfile.beq }

def Implicature.Constraints.NumericalExpressions.instBEqViolationProfile.beq : ViolationProfile → ViolationProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Implicature.Constraints.NumericalExpressions.instBEqViolationProfile.beq x✝¹ x✝ = false

def Implicature.Constraints.NumericalExpressions.violationProfile (c : NumeralCandidate) (admittedCount : ℕ) : ViolationProfile

Compute the violation profile for a candidate.

Equations

• One or more equations did not get rendered due to their size.

def Implicature.Constraints.NumericalExpressions.lexLessThan : List (ℕ × ℕ) → Bool

Lexicographic comparison of paired violation counts. Returns true if the first profile wins at the first point of difference. Factored out for provability (e.g., transitivity of harmonic bounding).

Equations

• Implicature.Constraints.NumericalExpressions.lexLessThan [] = false
• Implicature.Constraints.NumericalExpressions.lexLessThan ((a, b) :: rest) = if a < b then true else if a > b then false else Implicature.Constraints.NumericalExpressions.lexLessThan rest

def Implicature.Constraints.NumericalExpressions.harmonicallyBounds (v1 v2 : ViolationProfile) : Bool

OT strict domination: v1 harmonically bounds v2 if at the first constraint where they differ (in ranking order), v1 has fewer violations.

Equations

• One or more equations did not get rendered due to their size.

def Implicature.Constraints.NumericalExpressions.optimalCandidate (candidates : List (NumeralCandidate × ℕ)) : Option NumeralCandidate

Select the optimal candidate from a list (first candidate that is not harmonically bounded by any other).

Equations

• One or more equations did not get rendered due to their size.

theorem Implicature.Constraints.NumericalExpressions.round_beats_nonround_nsal (n₁ n₂ : ℕ) (h : Core.Roundness.roundnessScore n₁ > Core.Roundness.roundnessScore n₂) (h1 : Core.Roundness.roundnessScore n₁ ≤ Core.Roundness.maxRoundnessScore) (h2 : Core.Roundness.roundnessScore n₂ ≤ Core.Roundness.maxRoundnessScore) : nsalViolations n₁ < nsalViolations n₂

A rounder numeral always has fewer NSAL violations.

def Implicature.Constraints.NumericalExpressions.enrichmentWidth (n : ℕ) : ℕ

Enrichment width: predicted pragmatic enrichment range from roundnessScore.

Connects to CumminsFranke2021.lean's pragmatic enrichment model:

• 100 (score 6) → wider enrichment (±10, 20 total)
• 110 (score 2) → narrower enrichment (±5, 10 total)
• 7 (score 0) → minimal enrichment (±2, 4 total)

Semantically, "more than 110" is stronger than "more than 100" (higher Bayes factor). But pragmatic enrichment reverses this: "more than 100" enriched to (100,150] retains assertability in goal-worlds, while "more than 110" enriched to (110,120] loses nearly all goal-world assertability. So pragmatically, "more than 100" becomes stronger.

Equations

• One or more equations did not get rendered due to their size.

theorem Implicature.Constraints.NumericalExpressions.rounder_wider_enrichment : enrichmentWidth 100 > enrichmentWidth 110

Rounder M → wider enrichment.

def Implicature.Constraints.NumericalExpressions.nsalAsRSACost (n : ℕ) : ℚ

NSAL violations as a normalized RSA cost ∈ [0, 1].

This bridges the OT constraint to the RSA cost parameter: round numerals are "cheap" (cost ≈ 0), non-round are "expensive" (cost ≈ 1).

Equations

• Implicature.Constraints.NumericalExpressions.nsalAsRSACost n = ↑(Implicature.Constraints.NumericalExpressions.nsalViolations n) / ↑Core.Roundness.maxRoundnessScore

theorem Implicature.Constraints.NumericalExpressions.round_cheaper_in_rsa : nsalAsRSACost 100 < nsalAsRSACost 7

Round numerals are cheaper in RSA terms.

inductive Implicature.Constraints.NumericalExpressions.NumeralConstraint : Type

The four OT constraints as a criterion type.

• info : NumeralConstraint
• granularity : NumeralConstraint
• qsimp : NumeralConstraint
• nsal : NumeralConstraint

instance Implicature.Constraints.NumericalExpressions.instReprNumeralConstraint : Repr NumeralConstraint

Equations

• Implicature.Constraints.NumericalExpressions.instReprNumeralConstraint = { reprPrec := Implicature.Constraints.NumericalExpressions.instReprNumeralConstraint.repr }

def Implicature.Constraints.NumericalExpressions.instReprNumeralConstraint.repr : NumeralConstraint → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Implicature.Constraints.NumericalExpressions.instDecidableEqNumeralConstraint : DecidableEq NumeralConstraint

Equations

• Implicature.Constraints.NumericalExpressions.instDecidableEqNumeralConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.Constraints.NumericalExpressions.instBEqNumeralConstraint.beq : NumeralConstraint → NumeralConstraint → Bool

Equations

• Implicature.Constraints.NumericalExpressions.instBEqNumeralConstraint.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.Constraints.NumericalExpressions.instBEqNumeralConstraint : BEq NumeralConstraint

Equations

• Implicature.Constraints.NumericalExpressions.instBEqNumeralConstraint = { beq := Implicature.Constraints.NumericalExpressions.instBEqNumeralConstraint.beq }

def Implicature.Constraints.NumericalExpressions.constraintSatisfied (v : ViolationProfile) : NumeralConstraint → Bool

Coarse-grain a violation profile: a constraint is "satisfied" iff it has 0 violations. This discards degree-of-violation information but connects to SatisfactionOrdering's Bool-valued framework.

Equations

• Implicature.Constraints.NumericalExpressions.constraintSatisfied v Implicature.Constraints.NumericalExpressions.NumeralConstraint.info = (v.info == 0)
• Implicature.Constraints.NumericalExpressions.constraintSatisfied v Implicature.Constraints.NumericalExpressions.NumeralConstraint.granularity = (v.granularity == 0)
• Implicature.Constraints.NumericalExpressions.constraintSatisfied v Implicature.Constraints.NumericalExpressions.NumeralConstraint.qsimp = (v.qsimp == 0)
• Implicature.Constraints.NumericalExpressions.constraintSatisfied v Implicature.Constraints.NumericalExpressions.NumeralConstraint.nsal = (v.nsal == 0)

def Implicature.Constraints.NumericalExpressions.cumminsOrdering : Core.SatisfactionOrdering.SatisfactionOrdering ViolationProfile NumeralConstraint

A SatisfactionOrdering over violation profiles using the four @cite{cummins-2015} constraints.

This coarse-grains the OT system: a candidate "satisfies" a constraint iff it incurs 0 violations on that constraint. The resulting ordering is weaker than OT's lexicographic ranking — OT additionally discriminates by violation degree — but captures the structural backbone: a candidate that satisfies a strict superset of constraints is always OT-preferred.

Equations

• One or more equations did not get rendered due to their size.

theorem Implicature.Constraints.NumericalExpressions.zero_violations_best (v : ViolationProfile) : cumminsOrdering.atLeastAsGood { info := 0, granularity := 0, qsimp := 0, nsal := 0 } v = true

A candidate with zero violations everywhere is at-least-as-good as any other under the satisfaction ordering.

theorem Implicature.Constraints.NumericalExpressions.zero_bounds_any_violated (v : ViolationProfile) (h : v.info > 0 ∨ v.granularity > 0 ∨ v.qsimp > 0 ∨ v.nsal > 0) : harmonicallyBounds { info := 0, granularity := 0, qsimp := 0, nsal := 0 } v = true

Bridge: zero violations harmonically bounds any profile with at least one violation. This is the strongest case of the general principle that satisfaction-ordering dominance implies OT dominance when the superset constraint is the highest-ranked difference.

The converse fails: harmonicallyBounds can distinguish candidates that satisfy the same set of constraints but differ in violation degree (e.g., INFO violations 1 vs 3).