Numeral roundness

A number is round by having roundness properties: for Sigurd, divisibility by a power of ten from ten up or by its half or quarter; for Jansen and Pollmann, 10-ness, 2-ness, 5-ness and 2½-ness, k-ness being a digit times k times a power of ten; for Woodin et al., these over positive powers of ten together with being a multiple of five or of ten; and for Haslinger, lying on the conventionalized scales salient in a context, Krifka's scales of multiples of a width.

Numbers and properties form a formal context. A number is at least as round as another when it has every property the other has, Haslinger's ordering, so the numbers at least as round as d are the extent closure of d; counting properties gives the roundness scores. On scales of multiples the closure is again a scale, the multiples of the lcm of the widths through d.

Main definitions

• Numerals.Roundness.AtLeastAsRound: having every roundness property of a number, the criteria-derived preorder with the roundness properties as criteria (atLeastAsRound_iff_ofCriteria).
• Numerals.Roundness.score: the number of roundness properties a number has.
• Numerals.Roundness.OnScale: lying on a scale of multiples.
• Numerals.Roundness.HasKness, Numerals.Roundness.Kness: Jansen and Pollmann's k-ness and its four kinds, over powers of ten from a given one.

Main statements

• Numerals.Roundness.atLeastAsRound_iff_mem_extentClosure: the numbers at least as round as d are its extent closure.
• Numerals.Roundness.extentClosure_onScale: on scales of multiples, that closure is the scale of multiples of scaleLcm W d.
• Numerals.Roundness.atLeastAsRound_onScale_iff_dvd: roundness on scales of multiples is divisibility of these lcms.
• Numerals.Roundness.isLeast_atLeastAsRound_onScale: the least number above d at least as round as d is d + scaleLcm W d, the next point of that scale.

Implementation notes

A roundness property is an attribute of the formal context r : D → ι → Prop, so a family of properties and a set of salient scales are the same kind of object. Woodin et al.'s regression weights the properties unequally; score counts them equally.

References

• [Sig88]
• [JP01]
• [Kri07a]
• [WWL+24]
• [Has25a]

Roundness profiles

def Numerals.Roundness.AtLeastAsRound {D : Type u_1} {ι : Type u_2} (r : D → ι → Prop) (d e : D) : Prop

e is at least as round as d when it has every roundness property that d has.

Equations

• Numerals.Roundness.AtLeastAsRound r d e = ∀ ⦃i : ι⦄, r d i → r e i

theorem Numerals.Roundness.atLeastAsRound_iff_ofCriteria {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e : D} : AtLeastAsRound r d e ↔ e ≤ d

Being at least as round is the criteria-derived preorder with every scale as a criterion.

theorem Numerals.Roundness.AtLeastAsRound.refl {D : Type u_1} {ι : Type u_2} (r : D → ι → Prop) (d : D) : AtLeastAsRound r d d

theorem Numerals.Roundness.AtLeastAsRound.trans {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e f : D} (h₁ : AtLeastAsRound r d e) (h₂ : AtLeastAsRound r e f) : AtLeastAsRound r d f

theorem Numerals.Roundness.atLeastAsRound_iff_upperPolar_subset {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e : D} : AtLeastAsRound r d e ↔ upperPolar r {d} ⊆ upperPolar r {e}

theorem Numerals.Roundness.atLeastAsRound_iff_mem_extentClosure {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e : D} : AtLeastAsRound r d e ↔ e ∈ (extentClosure r) {d}

The numbers at least as round as d are the extent closure of d.

def Numerals.Roundness.profile {D : Type u_1} {ι : Type u_2} [Fintype ι] (r : D → ι → Prop) [(d : D) → DecidablePred (r d)] (d : D) : Finset ι

The roundness properties a number has.

Equations

• Numerals.Roundness.profile r d = Finset.filter (r d) Finset.univ

@[simp]

theorem Numerals.Roundness.mem_profile {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d : D} [Fintype ι] [(d : D) → DecidablePred (r d)] {i : ι} : i ∈ profile r d ↔ r d i

theorem Numerals.Roundness.coe_profile {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d : D} [Fintype ι] [(d : D) → DecidablePred (r d)] : ↑(profile r d) = Preorder.satisfied r Set.univ d

The roundness properties of a number are the criteria it satisfies, as a finite set.

theorem Numerals.Roundness.profile_subset_profile {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e : D} [Fintype ι] [(d : D) → DecidablePred (r d)] : profile r d ⊆ profile r e ↔ AtLeastAsRound r d e

def Numerals.Roundness.score {D : Type u_1} {ι : Type u_2} [Fintype ι] (r : D → ι → Prop) [(d : D) → DecidablePred (r d)] (d : D) : ℕ

The roundness score of a number is the number of roundness properties it has.

Equations

• Numerals.Roundness.score r d = (Numerals.Roundness.profile r d).card

theorem Numerals.Roundness.score_le_card {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} [Fintype ι] [(d : D) → DecidablePred (r d)] (d : D) : score r d ≤ Fintype.card ι

theorem Numerals.Roundness.AtLeastAsRound.score_le {D : Type u_1} {ι : Type u_2} {r : D → ι → Prop} {d e : D} [Fintype ι] [(d : D) → DecidablePred (r d)] (h : AtLeastAsRound r d e) : score r d ≤ score r e

Scales of multiples

def Numerals.Roundness.OnScale (W : Finset ℤ) (d : ℤ) (w : ↥W) : Prop

d lies on the scale of width w, the multiples of w, among the widths W.

Equations

• Numerals.Roundness.OnScale W d w = (d ∈ AddSubgroup.zmultiples ↑w)

theorem Numerals.Roundness.atLeastAsRound_onScale_iff {W : Finset ℤ} {d e : ℤ} : AtLeastAsRound (OnScale W) d e ↔ ∀ w ∈ W, w ∣ d → w ∣ e

@[instance_reducible]

instance Numerals.Roundness.instDecidableAtLeastAsRoundIntSubtypeMemFinsetOnScale {W : Finset ℤ} {d e : ℤ} : Decidable (AtLeastAsRound (OnScale W) d e)

Equations

• Numerals.Roundness.instDecidableAtLeastAsRoundIntSubtypeMemFinsetOnScale = decidable_of_iff (∀ w ∈ W, w ∣ d → w ∣ e) ⋯

def Numerals.Roundness.scaleLcm (W : Finset ℤ) (d : ℤ) : ℤ

The lcm of the widths of the scales through d.

Equations

• Numerals.Roundness.scaleLcm W d = {x ∈ W | x ∣ d}.lcm id

theorem Numerals.Roundness.atLeastAsRound_onScale_iff_scaleLcm_dvd {W : Finset ℤ} {d e : ℤ} : AtLeastAsRound (OnScale W) d e ↔ scaleLcm W d ∣ e

theorem Numerals.Roundness.scaleLcm_dvd (W : Finset ℤ) (d : ℤ) : scaleLcm W d ∣ d

theorem Numerals.Roundness.extentClosure_onScale {W : Finset ℤ} {d : ℤ} : (extentClosure (OnScale W)) {d} = ↑(AddSubgroup.zmultiples (scaleLcm W d))

On scales of multiples, the numbers at least as round as d are the meet of the scales through d, the scale of multiples of their lcm.

theorem Numerals.Roundness.atLeastAsRound_onScale_iff_dvd {W : Finset ℤ} {d e : ℤ} : AtLeastAsRound (OnScale W) d e ↔ scaleLcm W d ∣ scaleLcm W e

On scales of multiples, roundness is divisibility of the lcms of the widths.

theorem Numerals.Roundness.scaleLcm_pos {W : Finset ℤ} (hW : 0 ∉ W) (d : ℤ) : 0 < scaleLcm W d

theorem Numerals.Roundness.AtLeastAsRound.scaleLcm_dvd_sub {W : Finset ℤ} {d e : ℤ} (h : AtLeastAsRound (OnScale W) d e) : scaleLcm W d ∣ e - d

theorem Numerals.Roundness.AtLeastAsRound.scaleLcm_le_abs_sub {W : Finset ℤ} {d e : ℤ} (h : AtLeastAsRound (OnScale W) d e) (hne : e ≠ d) : scaleLcm W d ≤ |e - d|

A number other than d at least as round as d lies at least the lcm of the widths through d away from it.

theorem Numerals.Roundness.atLeastAsRound_add_scaleLcm (W : Finset ℤ) (d : ℤ) : AtLeastAsRound (OnScale W) d (d + scaleLcm W d)

theorem Numerals.Roundness.isLeast_atLeastAsRound_onScale {W : Finset ℤ} (hW : 0 ∉ W) (d : ℤ) : IsLeast {e : ℤ | d < e ∧ AtLeastAsRound (OnScale W) d e} (d + scaleLcm W d)

On scales of multiples, the least number above d at least as round as d is the next point of the scale of multiples of scaleLcm W d.

theorem Numerals.Roundness.scaleLcm_eq_of_aligned {W : Finset ℤ} {d : ℤ} (hpos : ∀ w ∈ W, 0 < w) (hW : ∀ a ∈ W, ∀ b ∈ W, a ∣ b ∨ b ∣ a) {m : ℤ} (hm : m ∈ W) (hmd : m ∣ d) (hmax : ∀ w ∈ W, w ∣ d → w ≤ m) : scaleLcm W d = m

On positive aligned widths, each pair comparable by divisibility, the lcm of the widths through d is the widest width dividing d ([Kri07a]'s aligned granularity levels).

theorem Numerals.Roundness.scaleLcm_mem_of_aligned {W : Finset ℤ} {d : ℤ} (hpos : ∀ w ∈ W, 0 < w) (hW : ∀ a ∈ W, ∀ b ∈ W, a ∣ b ∨ b ∣ a) (hne : {x ∈ W | x ∣ d}.Nonempty) : scaleLcm W d ∈ W ∧ scaleLcm W d ∣ d ∧ ∀ w ∈ W, w ∣ d → w ≤ scaleLcm W d

On positive aligned widths, a number on some scale has a widest scale, the lcm of the widths through it.

k-ness

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

n has k-ness when n = m × k × 10^b for some digit 1 ≤ m ≤ 9 and exponent b, that is n ∈ k × {1, …, 9} × 10^ℕ ([JP01]).

Equations

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

theorem Numerals.Roundness.hasKness_iff_exists_le_log {k n : ℕ} : HasKness k n ↔ ∃ b ≤ Nat.log 10 n, ∃ m < 10, 1 ≤ m ∧ n = m * k * 10 ^ b

The exponent of a k-ness witness is at most log₁₀ n, so k-ness is decidable.

@[instance_reducible]

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

Equations

• Numerals.Roundness.instDecidableHasKness k n = decidable_of_iff (∃ b ≤ Nat.log 10 n, ∃ m < 10, 1 ≤ m ∧ n = m * k * 10 ^ b) ⋯

theorem Numerals.Roundness.HasKness.dvd {k n : ℕ} (h : HasKness k n) : k ∣ n

k-ness forces divisibility by k.

theorem Numerals.Roundness.hasKness_mul_pow_iff {k b₀ n : ℕ} : HasKness (k * 10 ^ b₀) n ↔ ∃ b ≥ b₀, ∃ (m : ℕ), 1 ≤ m ∧ m ≤ 9 ∧ n = m * k * 10 ^ b

k × 10^b₀-ness is k-ness with an exponent of at least b₀.

inductive Numerals.Roundness.Kness : Type

Jansen and Pollmann's four kinds of k-ness.

• ten : Kness
• two : Kness
• five : Kness
• twoAndAHalf : Kness

@[instance_reducible]

instance Numerals.Roundness.instDecidableEqKness : DecidableEq Kness

Equations

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

def Numerals.Roundness.instReprKness.repr : Kness → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Numerals.Roundness.instReprKness : Repr Kness

Equations

• Numerals.Roundness.instReprKness = { reprPrec := Numerals.Roundness.instReprKness.repr }

@[instance_reducible]

instance Numerals.Roundness.instFintypeKness : Fintype Kness

Equations

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

def Numerals.Roundness.Kness.Holds (b₀ n : ℕ) : Kness → Prop

n has κ-ness over powers of ten from 10^b₀, where Jansen and Pollmann take b₀ = 0 and Woodin et al. b₀ = 1; 2½-ness of n is 5-ness of 2n.

Equations

• Numerals.Roundness.Kness.Holds b₀ n Numerals.Roundness.Kness.ten = Numerals.Roundness.HasKness (10 ^ b₀) n
• Numerals.Roundness.Kness.Holds b₀ n Numerals.Roundness.Kness.two = Numerals.Roundness.HasKness (2 * 10 ^ b₀) n
• Numerals.Roundness.Kness.Holds b₀ n Numerals.Roundness.Kness.five = Numerals.Roundness.HasKness (5 * 10 ^ b₀) n
• Numerals.Roundness.Kness.Holds b₀ n Numerals.Roundness.Kness.twoAndAHalf = Numerals.Roundness.HasKness (5 * 10 ^ b₀) (2 * n)

@[instance_reducible]

instance Numerals.Roundness.instDecidablePredKnessHolds (b₀ n : ℕ) : DecidablePred (Kness.Holds b₀ n)

Equations

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