Jansen and Pollmann (2001): On round numbers: Pragmatic aspects of numerical expressions

Jansen and Pollmann take a number's roundness to be its suitability for approximation, measured by its frequency after about and its counterparts in four languages, and find it carried by 10-ness, 2-ness and 5-ness, with 2½-ness adding to frequency in general. They reach these properties through two-number approximations, about 5 or 6 books: the pairs are consecutive members of an arithmetic sequence whose first member and ratio are a power of ten, doubled, or halved, and in their earlier rule also halved again. A single round number is a member of the same sequences, among their first nine. They explain the inventory by a principle of favourite quantities, doubling and halving, sometimes followed by halving again, being the basic means of manipulating quantities.

Here the ratios are the powers of ten under those operations, in either rule (Rule.IsRatio), a pair is two consecutive members of a sequence (SeqPair), and a single number is among the first nine members of one (FirstNine). Among the first nine members of the revised rule's sequences are exactly the numbers with 10-ness, 2-ness or 5-ness, and the quarter sequences of the original rule add exactly 2½-ness.

Main statements

• firstNine_revised_iff, firstNine_original_iff: the single round numbers are the members of the pair sequences, the quarter sequences adding 2½-ness.
• seqPair_examples, pair_rows: the paper's example pairs and the starred and unstarred phrases, against the rules.
• not_isRatio_three_mul_pow: no favourite quantity is three times a power of ten.

Implementation notes

• Quantities are rational, since halving and quartering leave the integers (½ × 10⁰, ¼ × 10¹); pairs and single numbers are natural, so only the natural ratios 10ⁿ, 2 × 10ⁿ, 5 × 10ⁿ and 25 × 10ⁿ bear on them (isRatio_natCast_iff).
• The kinds of k-ness are Numerals.Roundness.Kness at the paper's zeroth power, 2½-ness of n being 5-ness of 2n.
• The rules are the paper's generalizations over corpus pairs, which they fit in 90.8 to 98.2 percent of cases (p. 197); the theorems test them on the paper's examples.

TODO

• The regressions of roundness and frequency on these properties (pp. 198–200) belong in Data/Experiments.

References

• [JP01]
• [Sig88]

Favourite quantities (p. 200)

inductive JansenPollmann2001.QuantityOp : Type

The basic means of manipulating quantities, doubling and halving, sometimes followed by halving again.

• id : QuantityOp

  Leave the quantity as it is.

• double : QuantityOp

  Double it.

• half : QuantityOp

  Halve it.

• halfAgain : QuantityOp

  Halve it twice.

@[instance_reducible]

instance JansenPollmann2001.instDecidableEqQuantityOp : DecidableEq QuantityOp

Equations

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

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

The quantity an operation makes of q.

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

The sequence rule (pp. 196–197)

inductive JansenPollmann2001.Rule : Type

The two sequence rules for two-number approximations (pp. 196–197).

• original : Rule

  The rule of the authors' earlier study, with ratios 1, 2, ½ and ¼ times 10ⁿ.

• revised : Rule

  The revised rule, without the quarters, which under half a percent of corpus pairs use.

@[instance_reducible]

instance JansenPollmann2001.instDecidableEqRule : DecidableEq Rule

Equations

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

def JansenPollmann2001.Rule.Allows : Rule → QuantityOp → Prop

The quantity operations whose results a rule takes as ratios.

Equations

• JansenPollmann2001.Rule.original.Allows x✝ = True
• JansenPollmann2001.Rule.revised.Allows x✝ = (x✝ ≠ JansenPollmann2001.QuantityOp.halfAgain)

@[instance_reducible]

instance JansenPollmann2001.instDecidablePredQuantityOpAllows (rule : Rule) : DecidablePred rule.Allows

Equations

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

def JansenPollmann2001.Rule.IsRatio (rule : Rule) (q : ℚ) : Prop

The ratios of a rule are the powers of ten under its operations, under the original rule all the favourite quantities.

Equations

• rule.IsRatio q = ∃ (op : JansenPollmann2001.QuantityOp), rule.Allows op ∧ ∃ (n : ℕ), q = op.apply (10 ^ n)

theorem JansenPollmann2001.exists_natCast_eq_id {r : ℕ} : (∃ (n : ℕ), ↑r = QuantityOp.id.apply (10 ^ n)) ↔ ∃ (n : ℕ), r = 10 ^ n

theorem JansenPollmann2001.exists_natCast_eq_double {r : ℕ} : (∃ (n : ℕ), ↑r = QuantityOp.double.apply (10 ^ n)) ↔ ∃ (n : ℕ), r = 2 * 10 ^ n

theorem JansenPollmann2001.exists_natCast_eq_half {r : ℕ} : (∃ (n : ℕ), ↑r = QuantityOp.half.apply (10 ^ n)) ↔ ∃ (n : ℕ), r = 5 * 10 ^ n

theorem JansenPollmann2001.exists_natCast_eq_halfAgain {r : ℕ} : (∃ (n : ℕ), ↑r = QuantityOp.halfAgain.apply (10 ^ n)) ↔ ∃ (n : ℕ), r = 25 * 10 ^ n

theorem JansenPollmann2001.isRatio_natCast_iff {r : ℕ} (rule : Rule) : rule.IsRatio ↑r ↔ (∃ (n : ℕ), r = 10 ^ n) ∨ (∃ (n : ℕ), r = 2 * 10 ^ n) ∨ (∃ (n : ℕ), r = 5 * 10 ^ n) ∨ rule = Rule.original ∧ ∃ (n : ℕ), r = 25 * 10 ^ n

The natural ratios of the rules are 10ⁿ, 2 × 10ⁿ, 5 × 10ⁿ, and under the original rule 25 × 10ⁿ.

theorem JansenPollmann2001.exists_pow_iff_le_log {r : ℕ} (c : ℕ) (hc : 0 < c) : (∃ (n : ℕ), r = c * 10 ^ n) ↔ ∃ n ≤ Nat.log 10 r, r = c * 10 ^ n

A power-of-ten family member is bounded by its exponent, so ratios are decidable.

@[instance_reducible]

instance JansenPollmann2001.instDecidableIsRatioCastRat (rule : Rule) (r : ℕ) : Decidable (rule.IsRatio ↑r)

Equations

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

Pairs

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

[a, b] are consecutive members of a sequence of the rule (p. 196).

Equations

• JansenPollmann2001.SeqPair rule a b = ∃ (q : ℚ), rule.IsRatio q ∧ ∃ (k : ℕ), 1 ≤ k ∧ ↑a = ↑k * q ∧ ↑b = (↑k + 1) * q

theorem JansenPollmann2001.isRatio_pos {rule : Rule} {q : ℚ} (h : rule.IsRatio q) : 0 < q

theorem JansenPollmann2001.seqPair_iff {rule : Rule} {a b : ℕ} : SeqPair rule a b ↔ 0 < a ∧ a < b ∧ b - a ∣ a ∧ rule.IsRatio ↑(b - a)

A pair of the rule is a pair whose difference is a ratio dividing the first member.

@[instance_reducible]

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

Equations

• JansenPollmann2001.instDecidableSeqPair rule a b = decidable_of_iff (0 < a ∧ a < b ∧ b - a ∣ a ∧ rule.IsRatio ↑(b - a)) ⋯

From pairs to single numbers (pp. 197–198)

def JansenPollmann2001.FirstNine (rule : Rule) (n : ℕ) : Prop

n is among the first nine members of a sequence of the rule (p. 197).

Equations

• JansenPollmann2001.FirstNine rule n = ∃ (q : ℚ), rule.IsRatio q ∧ ∃ (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * q

theorem JansenPollmann2001.firstNine_iff {rule : Rule} {n : ℕ} : FirstNine rule n ↔ ∃ (op : QuantityOp), rule.Allows op ∧ ∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * op.apply (10 ^ b)

theorem JansenPollmann2001.exists_id_iff {n : ℕ} : (∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.id.apply (10 ^ b)) ↔ Numerals.Roundness.HasKness 1 n

theorem JansenPollmann2001.exists_double_iff {n : ℕ} : (∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.double.apply (10 ^ b)) ↔ Numerals.Roundness.HasKness 2 n

theorem JansenPollmann2001.hasKness_of_half {n : ℕ} (h : ∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.half.apply (10 ^ b)) : Numerals.Roundness.HasKness 5 n ∨ Numerals.Roundness.HasKness 1 n

Halving a power of ten gives the 5-family, or below ten the halves of even digits.

theorem JansenPollmann2001.half_of_hasKness {n : ℕ} (h : Numerals.Roundness.HasKness 5 n) : ∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.half.apply (10 ^ b)

theorem JansenPollmann2001.hasKness_of_halfAgain {n : ℕ} (h : ∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.halfAgain.apply (10 ^ b)) : Numerals.Roundness.HasKness 5 (2 * n) ∨ Numerals.Roundness.HasKness 5 n ∨ Numerals.Roundness.HasKness 1 n

Quartering a power of ten gives 2½-ness, 2n having 5-ness, or a number already with 10-ness or 5-ness.

theorem JansenPollmann2001.halfAgain_of_hasKness {n : ℕ} (h : Numerals.Roundness.HasKness 5 (2 * n)) : ∃ (b : ℕ) (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ ↑n = ↑m * QuantityOp.halfAgain.apply (10 ^ b)

theorem JansenPollmann2001.firstNine_revised_iff {n : ℕ} : FirstNine Rule.revised n ↔ ∃ (κ : Numerals.Roundness.Kness), κ ≠ Numerals.Roundness.Kness.twoAndAHalf ∧ Numerals.Roundness.Kness.Holds 0 n κ

A number is among the first nine members of a sequence of the revised rule exactly when it has 10-ness, 2-ness or 5-ness (pp. 197–198).

theorem JansenPollmann2001.firstNine_original_iff {n : ℕ} : FirstNine Rule.original n ↔ ∃ (κ : Numerals.Roundness.Kness), Numerals.Roundness.Kness.Holds 0 n κ

With the original rule's quarter sequences, 2½-ness joins them, so the first nine members are the numbers with some kind of k-ness (pp. 197, 199–200).

theorem JansenPollmann2001.not_isRatio_three_mul_pow (rule : Rule) (m : ℕ) : ¬rule.IsRatio ↑(3 * 10 ^ m)

No favourite quantity is three times a power of ten, as no number with 3-ness alone owes it to doubling and halving (pp. 199–200).

The examples

theorem JansenPollmann2001.seqPair_examples : (SeqPair Rule.revised 3 4 ∧ SeqPair Rule.revised 40 50 ∧ SeqPair Rule.revised 18 20 ∧ SeqPair Rule.revised 100 150) ∧ (SeqPair Rule.original 100 125 ∧ ¬SeqPair Rule.revised 100 125) ∧ ¬SeqPair Rule.original 1 3 ∧ ¬SeqPair Rule.original 5 7 ∧ ¬SeqPair Rule.original 6 9 ∧ ¬SeqPair Rule.original 40 80

Of the paper's examples of the sequence rule, [3, 4], [40, 50], [18, 20] and [100, 150] follow both rules, [100, 125] only the original, and [1, 3], [5, 7], [6, 9] and [40, 80] neither (p. 196).

def JansenPollmann2001.pairRow (r : Datum) : Option (ℕ × ℕ × Bool)

The pair of a two-number approximation with its acceptability.

Equations

• JansenPollmann2001.pairRow r = do let a ← r.nat? "first" let b ← r.nat? "second" pure (a, b, decide (r.judgment = Judgment.acceptable))

def JansenPollmann2001.pairData : List (ℕ × ℕ × Bool)

The two-number approximations of p. 195.

Equations

• JansenPollmann2001.pairData = List.filterMap JansenPollmann2001.pairRow JansenPollmann2001.Examples.all

theorem JansenPollmann2001.pair_rows (d : ℕ × ℕ × Bool) : d ∈ pairData → (d.2.2 = true ↔ SeqPair Rule.revised d.1 d.2.1)

The unstarred approximations follow the revised sequence rule and the starred ones do not (p. 195).

theorem JansenPollmann2001.kness_examples : (Numerals.Roundness.HasKness 1 40 ∧ Numerals.Roundness.HasKness 2 40 ∧ Numerals.Roundness.HasKness 5 40) ∧ (Numerals.Roundness.HasKness 1 8 ∧ Numerals.Roundness.HasKness 2 8 ∧ ¬Numerals.Roundness.HasKness 5 8) ∧ (Numerals.Roundness.HasKness 1 300 ∧ ¬Numerals.Roundness.HasKness 2 300 ∧ Numerals.Roundness.HasKness 5 300) ∧ (Numerals.Roundness.HasKness 1 70 ∧ ¬Numerals.Roundness.HasKness 2 70 ∧ ¬Numerals.Roundness.HasKness 5 70) ∧ (¬Numerals.Roundness.HasKness 1 61 ∧ ¬Numerals.Roundness.HasKness 2 61 ∧ ¬Numerals.Roundness.HasKness 5 61) ∧ (Numerals.Roundness.HasKness 1 20 ∧ Numerals.Roundness.HasKness 2 20 ∧ Numerals.Roundness.HasKness 5 20) ∧ (Numerals.Roundness.HasKness 1 80 ∧ Numerals.Roundness.HasKness 2 80 ∧ ¬Numerals.Roundness.HasKness 5 80) ∧ (Numerals.Roundness.HasKness 1 50 ∧ ¬Numerals.Roundness.HasKness 2 50 ∧ Numerals.Roundness.HasKness 5 50) ∧ ¬Numerals.Roundness.HasKness 1 45 ∧ ¬Numerals.Roundness.HasKness 2 45 ∧ Numerals.Roundness.HasKness 5 45

Of the paper's numbers, 40 has 10-ness, 2-ness and 5-ness, 8 has 10-ness and 2-ness, 300 has 10-ness and 5-ness, 70 only 10-ness and 61 none; 20 has all three, 80 10-ness and 2-ness, 50 10-ness and 5-ness, and 45 only 5-ness (p. 198).