Graded Numeral Roundness (k-ness Model)

[Kri07a] [Sig88] [WWL+23] [JP01] [Cum15]

Framework-agnostic infrastructure for graded numeral roundness, following [Sig88], [JP01], and [WWL+23].

A number n has k-ness if it lies in [JP01]'s set [k × (1–9 × 10ⁿ)] (their p. 198): n = m × k × 10^b with 1 ≤ m ≤ 9 — so 10-ness is the k = 1 family (divisors 10, 100, …), per their own example "70 has only 10-ness". Their original allows b ≥ 0; following [WWL+23] (fn. 3) the search starts at b ≥ 1, which drops the single digits from 10-ness and 15, 45, … from 5-ness (cf. Studies/JansenPollmann2001.lean for the original and the divergence).

The 6 properties, ordered by strength as frequency predictors in [WWL+23]'s negative binomial regression (strongest first): 10-ness (β = 4.46), 2.5-ness (β = 3.84), 5-ness (β = 3.39), 2-ness (β = 2.74), multiple of 10 (β = 2.45), multiple of 5 (β = 0.06); the 2-ness and multiple-of-10 credible intervals overlap.

Main definitions

• HasKness, Has2_5ness: the k-ness properties as decidable predicates
• roundnessScore: count of the six properties that hold (0–6)
• RoundnessGrade, roundnessGrade: the score binned into 4 levels
• contextualRoundnessScore, roundnessInContext: k-ness relative to a non-standard base (dozens, minutes)

k-ness primitives

def Semantics.Numerals.Roundness.HasKness (n k : ℕ) : Prop

n has integer k-ness: n = m × k × 10^b for some b ≥ 1 and 1 ≤ m ≤ 9 ([JP01]). The witness search is bounded at b ≤ 10, valid for n < 10¹¹.

Equations

• Semantics.Numerals.Roundness.HasKness n k = ∃ (b : ℕ), b < 11 ∧ 1 ≤ b ∧ ∃ (m : ℕ), m < 10 ∧ 1 ≤ m ∧ n = m * k * 10 ^ b

@[implicit_reducible]

instance Semantics.Numerals.Roundness.instDecidableHasKness (n k : ℕ) : Decidable (HasKness n k)

Equations

• Semantics.Numerals.Roundness.instDecidableHasKness n k = Semantics.Numerals.Roundness.instDecidableHasKness._aux_1 n k

def Semantics.Numerals.Roundness.Has2_5ness (n : ℕ) : Prop

n has 2.5-ness: n = m × 2.5 × 10^b for b ≥ 1, 1 ≤ m ≤ 9 — equivalently 2n = m × 5 × 10^b. Search bounded as in HasKness.

Equations

• Semantics.Numerals.Roundness.Has2_5ness n = ∃ (b : ℕ), b < 11 ∧ 1 ≤ b ∧ ∃ (m : ℕ), m < 10 ∧ 1 ≤ m ∧ 2 * n = m * 5 * 10 ^ b

@[implicit_reducible]

instance Semantics.Numerals.Roundness.instDecidableHas2_5ness (n : ℕ) : Decidable (Has2_5ness n)

Equations

• Semantics.Numerals.Roundness.instDecidableHas2_5ness n = Semantics.Numerals.Roundness.instDecidableHas2_5ness._aux_1 n

Roundness score

The six graded roundness properties of [Sig88] and [JP01] — multiple of 5, multiple of 10, 2-ness, 2.5-ness, 5-ness, 10-ness — counted equally. The count predicts numeral frequency and pragmatic behavior ([WWL+23]).

def Semantics.Numerals.Roundness.roundnessScore (n : ℕ) : ℕ

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

Equations

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

def Semantics.Numerals.Roundness.maxRoundnessScore : ℕ

Maximum possible roundness score.

Equations

• Semantics.Numerals.Roundness.maxRoundnessScore = 6

Roundness grade (binned score)

inductive Semantics.Numerals.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

  score ≥ 5 (e.g., 100, 50, 200)

• moderate : RoundnessGrade

  score 3–4 (e.g., 20, 40)

• low : RoundnessGrade

  score 1–2 (e.g., 110, 15)

• none : RoundnessGrade

  score 0 (e.g., 7, 99)

def Semantics.Numerals.Roundness.instReprRoundnessGrade.repr : RoundnessGrade → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Numerals.Roundness.instReprRoundnessGrade : Repr RoundnessGrade

Equations

• Semantics.Numerals.Roundness.instReprRoundnessGrade = { reprPrec := Semantics.Numerals.Roundness.instReprRoundnessGrade.repr }

@[implicit_reducible]

instance Semantics.Numerals.Roundness.instDecidableEqRoundnessGrade : DecidableEq RoundnessGrade

Equations

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

def Semantics.Numerals.Roundness.roundnessGrade (n : ℕ) : RoundnessGrade

Classify a number into a roundness grade.

Equations

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

Context-sensitive roundness

def Semantics.Numerals.Roundness.contextualRoundnessScore (n base : ℕ) : ℕ

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 Semantics.Numerals.Roundness.roundnessInContext (n base : ℕ) : ℕ

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.

Equations

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

Per-datum verification

theorem Semantics.Numerals.Roundness.score_ge_two_of_div10 (n : ℕ) (h10 : 10 ∣ n) : 2 ≤ roundnessScore n

Multiples of 10 have roundness score ≥ 2 (multiple-of-5 and multiple-of-10 both hold). The keystone for downstream sorry-free proofs.