Graded Numeral Roundness (k-ness Model)

@cite{krifka-2007} @cite{sigurd-1988} @cite{woodin-etal-2023} @cite{jansen-pollmann-2001} @cite{cummins-2015}

Framework-agnostic infrastructure for graded numeral roundness, following @cite{sigurd-1988}, @cite{jansen-pollmann-2001}, and @cite{woodin-etal-2023}.

A number n has k-ness (for k ∈ {2, 2.5, 5, 10}) if n = m × k × 10^b for some b ≥ 1 and 1 ≤ m ≤ 9.

The 6 properties (ordered by frequency effect, @cite{woodin-etal-2023}):

1. 10-ness (β = 4.46) — strongest predictor of frequency
2. 2.5-ness (β = 3.84)
3. 5-ness (β = 2.61)
4. 2-ness (β = 1.56)
5. Multiple of 10 (β = 0.52)
6. Multiple of 5 (β = 0.06) — weakest predictor

This module lives in Core because both Phenomena (empirical data) and Theories (Semantics.Montague, NeoGricean, RSA) depend on the roundness score, avoiding a cross-layer Theories→Phenomena import.

def Core.Roundness.hasIntKness (n k : Nat) : Bool

Check if n has integer k-ness: n = m × k × 10^b for b ≥ 1, 1 ≤ m ≤ 9.

Equations

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

def Core.Roundness.has2_5ness (n : Nat) : Bool

Check if n has 2.5-ness: n = m × 2.5 × 10^b for b ≥ 1, 1 ≤ m ≤ 9. Equivalent to: 2n = m × 5 × 10^b.

Equations

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

structure Core.Roundness.RoundnessProperties : Type

The 6 graded roundness properties from Sigurd/Jansen & Pollmann.

Each field is an independent Boolean property. The number of true properties predicts numeral frequency and pragmatic behavior.

• multipleOf5 : Bool
• multipleOf10 : Bool
• twoness : Bool
• twoPointFiveness : Bool
• fiveness : Bool
• tenness : Bool

instance Core.Roundness.instReprRoundnessProperties : Repr RoundnessProperties

Equations

• Core.Roundness.instReprRoundnessProperties = { reprPrec := Core.Roundness.instReprRoundnessProperties.repr }

def Core.Roundness.instReprRoundnessProperties.repr : RoundnessProperties → Nat → Std.Format

Equations

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

def Core.Roundness.instDecidableEqRoundnessProperties.decEq (x✝ x✝¹ : RoundnessProperties) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.Roundness.instDecidableEqRoundnessProperties : DecidableEq RoundnessProperties

Equations

• Core.Roundness.instDecidableEqRoundnessProperties = Core.Roundness.instDecidableEqRoundnessProperties.decEq

instance Core.Roundness.instBEqRoundnessProperties : BEq RoundnessProperties

Equations

• Core.Roundness.instBEqRoundnessProperties = { beq := Core.Roundness.instBEqRoundnessProperties.beq }

def Core.Roundness.instBEqRoundnessProperties.beq : RoundnessProperties → RoundnessProperties → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.Roundness.instBEqRoundnessProperties.beq x✝¹ x✝ = false

def Core.Roundness.roundnessProperties (n : Nat) : RoundnessProperties

Compute all 6 roundness properties for a natural number.

Equations

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

def Core.Roundness.roundnessScore (n : Nat) : Nat

Count of true roundness properties (0–6). Higher = rounder.

Equations

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

def Core.Roundness.maxRoundnessScore : Nat

Maximum possible roundness score.

Equations

• Core.Roundness.maxRoundnessScore = 6

inductive Core.Roundness.RoundnessGrade : Type

Binned roundness grade for use in width/tolerance functions.

Collapses the 0–6 score into 4 levels to avoid duplicating step-function logic across Theory files.

• high : RoundnessGrade
• moderate : RoundnessGrade
• low : RoundnessGrade
• none : RoundnessGrade

def Core.Roundness.instReprRoundnessGrade.repr : RoundnessGrade → Nat → Std.Format

Equations

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

instance Core.Roundness.instReprRoundnessGrade : Repr RoundnessGrade

Equations

• Core.Roundness.instReprRoundnessGrade = { reprPrec := Core.Roundness.instReprRoundnessGrade.repr }

instance Core.Roundness.instDecidableEqRoundnessGrade : DecidableEq RoundnessGrade

Equations

• Core.Roundness.instDecidableEqRoundnessGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Roundness.instBEqRoundnessGrade.beq : RoundnessGrade → RoundnessGrade → Bool

Equations

• Core.Roundness.instBEqRoundnessGrade.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Roundness.instBEqRoundnessGrade : BEq RoundnessGrade

Equations

• Core.Roundness.instBEqRoundnessGrade = { beq := Core.Roundness.instBEqRoundnessGrade.beq }

def Core.Roundness.roundnessGrade (n : Nat) : RoundnessGrade

Classify a number into a roundness grade.

Equations

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

def Core.Roundness.contextualRoundnessScore (n base : Nat) : Nat

Count k-ness-like properties relative to a non-standard base.

For base b, checks divisibility by b, 2b, 5b, and 10b — mirroring the standard k-ness properties but on a different scale.

Examples:

• contextualRoundnessScore 48 12 = 2 (48 ÷ 12 = 4, 48 ÷ 24 = 2)
• contextualRoundnessScore 120 12 = 4 (divides by 12, 24, 60, 120)

Equations

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

def Core.Roundness.roundnessInContext (n base : Nat) : Nat

Context-sensitive roundness: compose default k-ness with a non-standard base.

On a base-12 (dozens) scale, 48 = 4 × 12 is "round" even though its default k-ness score is 0. On base-60 (minutes), 120 = 2 × 60 is round.

The contextual score derives from actual divisibility properties relative to the base (not a flat bonus), paralleling how standard k-ness derives from divisibility by 2/2.5/5/10 × powers of 10.

Composes with GranularityDatum in Phenomena.Gradability.Imprecision.Numerals.

Equations

• Core.Roundness.roundnessInContext n base = max (Core.Roundness.roundnessScore n) (Core.Roundness.contextualRoundnessScore n base)

theorem Core.Roundness.roundness_100 : roundnessScore 100 = 6

theorem Core.Roundness.roundness_7 : roundnessScore 7 = 0

theorem Core.Roundness.roundness_50 : roundnessScore 50 = 4

theorem Core.Roundness.roundness_1000 : roundnessScore 1000 = 6

theorem Core.Roundness.score_ge_two_of_div10 (n : Nat) (h10 : n % 10 = 0) : roundnessScore n ≥ 2

Multiples of 10 have roundness score ≥ 2 (multipleOf5 + multipleOf10 both true). This is the key lemma for all downstream sorry-free proofs.

theorem Core.Roundness.grade_ne_none_of_score_ge_one (n : Nat) (h : roundnessScore n ≥ 1) : roundnessGrade n ≠ RoundnessGrade.none

Grade is never .none when score ≥ 1.