@cite{cummins-2015}: OT Constraints, k-ness, NSAL, and RSA Cost

@cite{cummins-2015} @cite{kao-etal-2014-hyperbole} @cite{lasersohn-1999} @cite{woodin-etal-2023}

Self-contained study of @cite{cummins-2015}: an Optimality-Theoretic constraint system for numeral production plus the bridges to graded roundness, RSA cost, and the @cite{kao-etal-2014-hyperbole} PrecisionMode switch.

OT Constraints

Speakers choose among candidate numeral expressions by trading off four 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 empirical bridge to the k-ness model is nsalViolations: NSAL violations equal maxRoundnessScore - roundnessScore(n), so rounder numbers incur fewer NSAL violations.

A ViolationProfile is Core.Constraint.Profile Nat 4 (i.e. Fin 4 → Nat), matching the codebase's standard violation-profile abstraction. Profile indices fix the constraint order: 0 = INFO, 1 = Granularity, 2 = QSIMP, 3 = NSAL.

Two preorders on profiles are exposed, both as Core.Order.FeaturePreorder instances so they fit the schema established in Core/Constraint/Pareto.lean:

view	feature	feature-space order
paretoPreorder	id : ViolationProfile → ViolationProfile	pointwise ≤
qualPreorder	violatedSetOf : … → Finset (Fin 4)	subset ⊆

paretoPreorder_le_implies_qualPreorder_le is a one-line application of FeaturePreorder.coarsen_via_monotone with violatedSetOf as the connecting monotone map. The legacy criterion-based view via SatisfactionOrdering is preserved as cumminsOrdering.

Downstream Bridges

1. NSAL as RSA cost — the OT violation count, normalised to [0, 1], serves as the RSA cost : U → ℚ parameter. Round numerals are cheap; non-round are expensive.
2. k-ness as PrecisionMode threshold — roundnessScore ≥ 2 triggers .approximate mode, grounding the binary switch used by @cite{kao-etal-2014-hyperbole}. The pragmatic halo width (@cite{lasersohn-1999}, @cite{krifka-2007}) is also wider for round numerals.

The lexical bridge to Fragments.English.NumeralModifiers documents the expected interaction between requiresRound modifiers and high k-ness anchors.

inductive Phenomena.Numerals.Studies.Cummins2015.QuantifierForm : Type

Form of the numeral expression. Bare numerals are simplest; modified forms add complexity (and pay a QSIMP cost).

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

@[implicit_reducible]

instance Phenomena.Numerals.Studies.Cummins2015.instReprQuantifierForm : Repr QuantifierForm

Equations

• Phenomena.Numerals.Studies.Cummins2015.instReprQuantifierForm = { reprPrec := Phenomena.Numerals.Studies.Cummins2015.instReprQuantifierForm.repr }

def Phenomena.Numerals.Studies.Cummins2015.instReprQuantifierForm.repr : QuantifierForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Numerals.Studies.Cummins2015.instDecidableEqQuantifierForm : DecidableEq QuantifierForm

Equations

• Phenomena.Numerals.Studies.Cummins2015.instDecidableEqQuantifierForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Numerals.Studies.Cummins2015.NumeralCandidate : Type

A candidate numeral expression for OT evaluation.

• numeral : ℕ
• form : QuantifierForm
• contextGranularity : ℕ

@[implicit_reducible]

instance Phenomena.Numerals.Studies.Cummins2015.instReprNumeralCandidate : Repr NumeralCandidate

Equations

• Phenomena.Numerals.Studies.Cummins2015.instReprNumeralCandidate = { reprPrec := Phenomena.Numerals.Studies.Cummins2015.instReprNumeralCandidate.repr }

def Phenomena.Numerals.Studies.Cummins2015.instReprNumeralCandidate.repr : NumeralCandidate → ℕ → Std.Format

Equations

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

def Phenomena.Numerals.Studies.Cummins2015.inferGranularity (n : ℕ) : ℕ

Infer granularity from a numeral's trailing zeros: 100 → 2, 110 → 1, 111 → 0.

Equations

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

def Phenomena.Numerals.Studies.Cummins2015.infoViolations (admittedCount : ℕ) : ℕ

INFO: violations = |admittedSet| - 1. Less informative expressions (which admit more values) incur more violations.

Equations

• Phenomena.Numerals.Studies.Cummins2015.infoViolations admittedCount = admittedCount - 1

def Phenomena.Numerals.Studies.Cummins2015.granularityViolations (contextGranularity uttGranularity : ℕ) : ℕ

Granularity: violations = |contextGranularity − utteranceGranularity|.

Equations

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

def Phenomena.Numerals.Studies.Cummins2015.qsimpViolations : QuantifierForm → ℕ

QSIMP: bare = 0, modified = 1, interval = 2.

Equations

• Phenomena.Numerals.Studies.Cummins2015.qsimpViolations Phenomena.Numerals.Studies.Cummins2015.QuantifierForm.bare = 0
• Phenomena.Numerals.Studies.Cummins2015.qsimpViolations Phenomena.Numerals.Studies.Cummins2015.QuantifierForm.modified = 1
• Phenomena.Numerals.Studies.Cummins2015.qsimpViolations Phenomena.Numerals.Studies.Cummins2015.QuantifierForm.interval = 2

def Phenomena.Numerals.Studies.Cummins2015.nsalViolations (n : ℕ) : ℕ

NSAL: violations = maxRoundnessScore - roundnessScore(n). Maximally round numbers (score 6) → 0; non-round (score 0) → 6. The complement of the graded roundness score, which is the load-bearing connection between the OT account and the k-ness model.

Equations

• Phenomena.Numerals.Studies.Cummins2015.nsalViolations n = Core.Roundness.maxRoundnessScore - Core.Roundness.roundnessScore n

theorem Phenomena.Numerals.Studies.Cummins2015.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.

theorem Phenomena.Numerals.Studies.Cummins2015.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.

@[reducible, inline]

abbrev Phenomena.Numerals.Studies.Cummins2015.ViolationProfile : Type

A ViolationProfile is a Profile Nat 4 — a 4-vector of violation counts indexed by Fin 4. Index order: 0 = INFO, 1 = Granularity, 2 = QSIMP, 3 = NSAL. Reusing Core.Constraint.Profile means the abstractions in Core/Constraint/Pareto.lean (Pareto preorder, qualitative coarsening, coarsen_via_monotone) apply directly without an extra projection layer.

Equations

• Phenomena.Numerals.Studies.Cummins2015.ViolationProfile = Core.Constraint.Profile ℕ 4

def Phenomena.Numerals.Studies.Cummins2015.violationProfile (c : NumeralCandidate) (admittedCount : ℕ) : ViolationProfile

Compute the violation profile for a candidate. Indices: 0 = INFO, 1 = Granularity, 2 = QSIMP, 3 = NSAL.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Numerals.Studies.Cummins2015.violationProfile c admittedCount 0 = Phenomena.Numerals.Studies.Cummins2015.infoViolations admittedCount
• Phenomena.Numerals.Studies.Cummins2015.violationProfile c admittedCount 2 = Phenomena.Numerals.Studies.Cummins2015.qsimpViolations c.form
• Phenomena.Numerals.Studies.Cummins2015.violationProfile c admittedCount 3 = Phenomena.Numerals.Studies.Cummins2015.nsalViolations c.numeral

def Phenomena.Numerals.Studies.Cummins2015.paretoPreorder : Core.Order.FeaturePreorder ViolationProfile ViolationProfile

Pointwise Pareto preorder on violation profiles as a FeaturePreorder with the identity feature: v ≤ v' iff every component of v is ≤ the corresponding component of v'. The partial-order backbone that lex-OT extends; lex breaks ties using the constraint ranking.

Equations

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

def Phenomena.Numerals.Studies.Cummins2015.qualPreorder : Core.Order.FeaturePreorder ViolationProfile (Finset (Fin 4))

Qualitative coarsening as a FeaturePreorder: feature is the set of violated constraint indices, feature-space order is Finset.⊆. The underlying preorder is identical in extension to cumminsOrdering's, but presented as a feature pullback so the same coarsen_via_monotone schema applies.

Equations

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

theorem Phenomena.Numerals.Studies.Cummins2015.paretoPreorder_le_implies_qualPreorder_le {v v' : ViolationProfile} (h : v ≤ v') : v ≤ v'

Pointwise dominance ⇒ qualitative dominance. A one-line corollary of FeaturePreorder.coarsen_via_monotone with the violated-index extractor as the connecting monotone map — identical in shape to paretoFeaturePreorder_le_implies_qualitativeFeaturePreorder_le in Core/Constraint/Pareto.lean.

inductive Phenomena.Numerals.Studies.Cummins2015.NumeralConstraint : Type

The four OT constraints as a criterion type. Field order matches ViolationProfile indices (info ↔ 0, …, nsal ↔ 3).

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

def Phenomena.Numerals.Studies.Cummins2015.instReprNumeralConstraint.repr : NumeralConstraint → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Numerals.Studies.Cummins2015.instReprNumeralConstraint : Repr NumeralConstraint

Equations

• Phenomena.Numerals.Studies.Cummins2015.instReprNumeralConstraint = { reprPrec := Phenomena.Numerals.Studies.Cummins2015.instReprNumeralConstraint.repr }

@[implicit_reducible]

instance Phenomena.Numerals.Studies.Cummins2015.instDecidableEqNumeralConstraint : DecidableEq NumeralConstraint

Equations

• Phenomena.Numerals.Studies.Cummins2015.instDecidableEqNumeralConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Numerals.Studies.Cummins2015.constraintSatisfied (v : ViolationProfile) : NumeralConstraint → Bool

Coarse-grain a violation profile: a constraint is "satisfied" iff it has 0 violations. Bool-valued for SatisfactionOrdering.

Equations

• Phenomena.Numerals.Studies.Cummins2015.constraintSatisfied v Phenomena.Numerals.Studies.Cummins2015.NumeralConstraint.info = (v 0 == 0)
• Phenomena.Numerals.Studies.Cummins2015.constraintSatisfied v Phenomena.Numerals.Studies.Cummins2015.NumeralConstraint.granularity = (v 1 == 0)
• Phenomena.Numerals.Studies.Cummins2015.constraintSatisfied v Phenomena.Numerals.Studies.Cummins2015.NumeralConstraint.qsimp = (v 2 == 0)
• Phenomena.Numerals.Studies.Cummins2015.constraintSatisfied v Phenomena.Numerals.Studies.Cummins2015.NumeralConstraint.nsal = (v 3 == 0)

def Phenomena.Numerals.Studies.Cummins2015.cumminsOrdering : Core.Order.SatisfactionOrdering ViolationProfile NumeralConstraint

A SatisfactionOrdering over violation profiles using the four @cite{cummins-2015} constraints. Coarsens the OT system: a candidate "satisfies" a constraint iff it incurs 0 violations. The resulting ordering is weaker than lex-OT (which 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 Phenomena.Numerals.Studies.Cummins2015.zero_violations_best (v : ViolationProfile) : (fun (x : Fin 4) => 0) ≤ v

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

def Phenomena.Numerals.Studies.Cummins2015.nsalAsRSACost (n : ℕ) : ℚ

NSAL violations as a normalised RSA cost ∈ [0, 1]. Bridges the OT NSAL constraint to the RSA cost parameter: round numerals are "cheap" (≈ 0), non-round are "expensive" (≈ 1). The denominator is maxRoundnessScore, so the codomain is exactly [0, 1].

Equations

• Phenomena.Numerals.Studies.Cummins2015.nsalAsRSACost n = ↑(Phenomena.Numerals.Studies.Cummins2015.nsalViolations n) / ↑Core.Roundness.maxRoundnessScore

theorem Phenomena.Numerals.Studies.Cummins2015.maximally_round_free : nsalAsRSACost 100 = 0 ∧ nsalAsRSACost 1000 = 0

Maximally round numerals are free (zero cost). Reduces to the Nat-level fact nsalViolations 100 = 0 (closed by decide) plus 0 / x = 0 over ℚ.

theorem Phenomena.Numerals.Studies.Cummins2015.round_cheaper_in_rsa : nsalAsRSACost 100 < nsalAsRSACost 99

Round numerals incur strictly lower RSA cost than non-round ones. Nat-level reduction of nsalViolations followed by norm_num over ℚ.

inferPrecisionMode (in Numerals.Precision) is defined by roundnessScore n ≥ 2 → .approximate. This subsection records the grounding theorems for representative numerals plus the general bridge that every multiple of 10 falls in .approximate mode.

theorem Phenomena.Numerals.Studies.Cummins2015.precision_100_approximate : Semantics.Numerals.Precision.inferPrecisionMode 100 = Semantics.Numerals.Precision.PrecisionMode.approximate

100 is round (score 6) → .approximate mode.

theorem Phenomena.Numerals.Studies.Cummins2015.precision_7_exact : Semantics.Numerals.Precision.inferPrecisionMode 7 = Semantics.Numerals.Precision.PrecisionMode.exact

7 is non-round (score 0) → .exact mode.

theorem Phenomena.Numerals.Studies.Cummins2015.multipleOf10_implies_approximate (n : ℕ) (hr : n % 10 = 0) : Semantics.Numerals.Precision.inferPrecisionMode n = Semantics.Numerals.Precision.PrecisionMode.approximate

General bridge. Every multiple of 10 is interpreted in .approximate mode. Follows from score_ge_two_of_div10: the score is at least 2, so the roundnessScore n ≥ 2 branch of inferPrecisionMode fires.

theorem Phenomena.Numerals.Studies.Cummins2015.round_wider_halo : Semantics.Numerals.Precision.haloWidth 100 > Semantics.Numerals.Precision.haloWidth 7

Pragmatic halo width is strictly wider for round numerals (100) than for non-round (7) — the quantitative content of @cite{lasersohn-1999}'s halo intuition under the k-ness operationalisation.

theorem Phenomena.Numerals.Studies.Cummins2015.approximately_tolerates_nonround : Fragments.English.NumeralModifiers.approximately.requiresRound = false

The lexical entry for "approximately" carries requiresRound = false. @cite{cummins-2015} predicts that combinations with low-k anchors are grammatical but marked — naturalness correlates with k-ness rather than being a hard constraint.