[JP01]: On Round Numbers

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

[JP01] operationalize roundness as relative suitability for approximation contexts (frequency after Dutch ongeveer 'about') and find it carried by four numerical properties — 10-ness, 2-ness, 5-ness, and (following [Sig88]) 2½-ness: membership in [k × (1–9 × 10ⁿ)] (their p. 198). Their explanation (pp. 200–201) is the principle of favourite quantities: doubling and halving (sometimes followed by halving again) are the basic means of manipulating quantities, so the round-number unit inventory is the orbit of the decimal base powers under these operations — exactly the four k-families (favUnit_iff), and provably not the 3-family (not_favUnit_three_mul_pow; their p. 199: 3-, 4-, 6-, 7-ness contribute nothing).

Two-number approximative expressions (about 5 or 6 books) obey the revised sequence rule (their p. 197): the pair consists of consecutive members of an arithmetic sequence whose ratio and first member are 1×10ⁿ, 2×10ⁿ, or ½×10ⁿ. Quarters, which do round single numbers (2½-ness), are absent from pairs (quarter_unit_not_seqRatio).

Their p. 198 definition allows the zeroth power (hasKnessOrig); Roundness.HasKness follows [WWL+23]'s b ≥ 1 restriction (their fn. 3). The divergence matters downstream: under the original, 15 has 5-ness (fifteen_has_orig_fiveness) — roundness that the restricted variant, and hence Precision.inferPrecisionMode, misses at 15, 45, …. Reading this paper also corrected Roundness's 10-ness: it is the k = 1 family (divisors 10, 100, …) — their own example "70 has only 10-ness" — not the k = 10 family.

Their regression (frequency from magnitude n⁻¹, n⁻² plus the four properties, R² = 0.968, p. 200) stays prose per the no-regression-theorems rule, as does the FA operationalization itself.

Main definitions

• QuantityOp, IsFavUnit: doubling/halving over decimal base powers
• SeqRatio, SeqPair: the revised sequence rule
• hasKnessOrig: their original (b ≥ 0) k-ness

Main results

• favUnit_iff: the favourite units are exactly the four k-families
• not_favUnit_three_mul_pow: the 3-family is not derivable — why the inventory stops at four properties
• quarter_unit_not_seqRatio: quarters round single numbers, not pairs
• their p. 198 examples and p. 196 pair judgments, checked by decide
• fifteen_has_orig_fiveness: the b ≥ 0 vs b ≥ 1 divergence at 15

The principle of favourite quantities (their pp. 200–201)

inductive JansenPollmann2001.QuantityOp : Type

The basic quantity-manipulation operations: "doubling and halving (sometimes followed by halving again)".

• id : QuantityOp

  Leave the base quantity as is.

• double : QuantityOp

  Double it.

• half : QuantityOp

  Halve it.

• halfAgain : QuantityOp

  Halve it twice.

@[implicit_reducible]

instance JansenPollmann2001.instDecidableEqQuantityOp : DecidableEq QuantityOp

Equations

• JansenPollmann2001.instDecidableEqQuantityOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JansenPollmann2001.instReprQuantityOp.repr : QuantityOp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JansenPollmann2001.instReprQuantityOp : Repr QuantityOp

Equations

• JansenPollmann2001.instReprQuantityOp = { reprPrec := JansenPollmann2001.instReprQuantityOp.repr }

def JansenPollmann2001.QuantityOp.apply : QuantityOp → ℚ → ℚ

Apply a quantity operation.

Equations

• JansenPollmann2001.QuantityOp.id.apply x✝ = x✝
• JansenPollmann2001.QuantityOp.double.apply x✝ = 2 * x✝
• JansenPollmann2001.QuantityOp.half.apply x✝ = x✝ / 2
• JansenPollmann2001.QuantityOp.halfAgain.apply x✝ = x✝ / 4

def JansenPollmann2001.IsFavUnit (q : ℚ) : Prop

A favourite unit: a decimal base power manipulated by one quantity operation.

Equations

• JansenPollmann2001.IsFavUnit q = ∃ (op : JansenPollmann2001.QuantityOp) (n : ℕ), q = op.apply (10 ^ n)

theorem JansenPollmann2001.favUnit_iff (q : ℚ) : IsFavUnit q ↔ ∃ (n : ℕ), q = 10 ^ n ∨ q = 2 * 10 ^ n ∨ q = 10 ^ n / 2 ∨ q = 10 ^ n / 4

The favourite units are exactly the four k-ness families: powers of ten, their doubles, their halves, and their quarters.

theorem JansenPollmann2001.half_pow (n : ℕ) : 10 ^ (n + 1) / 2 = 5 * 10 ^ n

Halving a base power lands on the 5-family.

theorem JansenPollmann2001.halfAgain_pow (n : ℕ) : 10 ^ (n + 1) / 4 = 5 / 2 * 10 ^ n

Halving twice lands on the 2½-family.

theorem JansenPollmann2001.not_favUnit_three_mul_pow (m : ℕ) : ¬IsFavUnit (3 * 10 ^ m)

No quantity operation reaches the 3-family: the structural reason the roundness inventory has exactly four properties (their p. 199: 3-, 4-, 6-, 7-ness contribute nothing to frequency).

The revised sequence rule (their pp. 196–197)

Two-number approximative expressions ([about 5 or 6 books]) consist of consecutive members of an arithmetic sequence whose ratio equals its first member and is 1×10ⁿ, 2×10ⁿ, or ½×10ⁿ (in ℕ, the half-family is 5×10ⁿ). The original rule also allowed ¼×10ⁿ; the revision drops it (quarter-ratio pairs are under 0.5% in all four corpora).

def JansenPollmann2001.SeqRatio (r : ℕ) : Prop

A ratio licensed by the revised sequence rule.

Equations

• JansenPollmann2001.SeqRatio r = ∃ n < 11, r = 10 ^ n ∨ r = 2 * 10 ^ n ∨ r = 5 * 10 ^ n

@[implicit_reducible]

instance JansenPollmann2001.instDecidableSeqRatio (r : ℕ) : Decidable (SeqRatio r)

Equations

• JansenPollmann2001.instDecidableSeqRatio r = JansenPollmann2001.instDecidableSeqRatio._aux_1 r

def JansenPollmann2001.SeqPair (a b : ℕ) : Prop

The revised sequence rule: [a, b] are consecutive members of the sequence r, 2r, 3r, … for a licensed ratio r.

Equations

• JansenPollmann2001.SeqPair a b = ∃ r ≤ a, 0 < r ∧ JansenPollmann2001.SeqRatio r ∧ r ∣ a ∧ b = a + r

@[implicit_reducible]

instance JansenPollmann2001.instDecidableSeqPair (a b : ℕ) : Decidable (SeqPair a b)

Equations

• JansenPollmann2001.instDecidableSeqPair a b = JansenPollmann2001.instDecidableSeqPair._aux_1 a b

theorem JansenPollmann2001.quarter_unit_not_seqRatio : IsFavUnit 25 ∧ ¬SeqRatio 25

Quarters split single-number roundness from pair formation: 25 is a favourite unit (twice-halved 10², whence 2½-ness) but not a licensed sequence ratio — their pp. 197, 199–200 asymmetry.

The original k-ness and the b ≥ 1 restriction (their p. 198)

def JansenPollmann2001.hasKnessOrig (n k : ℕ) : Prop

Their original k-ness: n ∈ [k × (1–9 × 10ᵇ)] with b ≥ 0 — 10-ness is k = 1. Roundness.HasKness is this with [WWL+23]'s b ≥ 1 restriction. Search bounded as there.

Equations

• JansenPollmann2001.hasKnessOrig n k = ∃ b < 11, ∃ m < 10, 1 ≤ m ∧ n = m * k * 10 ^ b

@[implicit_reducible]

instance JansenPollmann2001.instDecidableHasKnessOrig (n k : ℕ) : Decidable (hasKnessOrig n k)

Equations

• JansenPollmann2001.instDecidableHasKnessOrig n k = JansenPollmann2001.instDecidableHasKnessOrig._aux_1 n k

theorem JansenPollmann2001.hasKnessOrig_of_hasKness {n k : ℕ} (h : Semantics.Numerals.Roundness.HasKness n k) : hasKnessOrig n k

The restricted variant entails the original.

theorem JansenPollmann2001.fifteen_has_orig_fiveness : hasKnessOrig 15 5 ∧ ¬Semantics.Numerals.Roundness.HasKness 15 5

The divergence that matters downstream: under the original definition 15 has 5-ness (15 = 3 × 5 × 10⁰), which the b ≥ 1 variant drops — the source of the 15/45-idealization noted at Precision.inferPrecisionMode.

10-ness as expression shape ([Hur75])

theorem JansenPollmann2001.hasKness_one_iff_phrase (n : ℕ) : Semantics.Numerals.Roundness.HasKness n 1 ↔ ∃ m ≤ 8, ∃ k ≤ 9, n = (Syntax.Numeral.Phrase.mk (Syntax.Numeral.Number.tally m) (Syntax.Numeral.M.tenPow k)).value

10-ness is two-word expressibility: n has 10-ness iff it is the value of a digit×base PHRASE — [Hur75]'s [NUMBER M] with a digit NUMBER and a pure ten-power M (forty, four hundred, …). The favourite-quantity properties are facts about numeral expression shape.