Documentation

Studies.WoodinEtAl2024

Woodin, Winter, Littlemore, Perlman & Grieve (2024): Large-Scale Patterns of Number Use #

Woodin et al. model the frequency of numbers in the British National Corpus: the log frequency of a number is a linear function of its log magnitude and of which roundness properties it has. The six properties are being a multiple of five or of ten and Jansen and Pollmann's four kinds of k-ness over positive powers of ten. They nest, since 10-ness, 2-ness and 5-ness make a number a multiple of ten and every property makes it a multiple of five, and with non-negative weights the predicted frequency is monotone in the roundness ordering of Numerals.Roundness.

Main results #

Implementation notes #

The fitted coefficients, the ordering of the properties by effect size, the residual analysis of culturally salient numbers, and the register comparisons are results of the corpus study and are not restated here; the theorems are over an arbitrary model, with the sign conditions the study reports as hypotheses.

References #

The roundness properties #

source
inductive WoodinEtAl2024.Property :
Type

A roundness property is being a multiple of five or of ten, or one of the four kinds of k-ness.

Instances For
    source
    @[instance_reducible]
    instance WoodinEtAl2024.instDecidableEqProperty :
    DecidableEq Property
    Equations
    source
    def WoodinEtAl2024.instDecidableEqProperty.decEq (x✝ x✝¹ : Property) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance WoodinEtAl2024.instReprProperty :
      Repr Property
      Equations
      source
      def WoodinEtAl2024.instReprProperty.repr :
      Property → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance WoodinEtAl2024.instFintypeProperty :
        Fintype Property
        Equations
        source
        def WoodinEtAl2024.Property.Holds (n : ℕ) :
        Property → Prop

        A number has a roundness property; the k-ness properties take a positive power of ten (footnote 3).

        Equations
        Instances For
          source
          @[instance_reducible]
          instance WoodinEtAl2024.instDecidablePredPropertyHolds (n : ℕ) :
          DecidablePred (Property.Holds n)
          Equations
          • One or more equations did not get rendered due to their size.
          source
          theorem WoodinEtAl2024.dvd_ten_of_holds {κ : Numerals.Roundness.Kness} {n : ℕ} (hκ : κ ≠ Numerals.Roundness.Kness.twoAndAHalf) (h : Numerals.Roundness.Kness.Holds 1 n κ) :
          10 ∣ n

          10-ness, 2-ness and 5-ness make a number a multiple of ten.

          source
          theorem WoodinEtAl2024.dvd_five_of_holds {p : Property} {n : ℕ} (h : Property.Holds n p) :
          5 ∣ n

          Every roundness property makes a number a multiple of five.

          The frequency model #

          source
          structure WoodinEtAl2024.Model :
          Type

          A model of log frequency has a coefficient on log magnitude and a weight per roundness property.

          • magnitude : ℝ
          • weight : Property → ℝ
          Instances For
            source
            noncomputable def WoodinEtAl2024.Model.predicted (M : Model) (n : ℕ) :
            ℝ

            The predicted log frequency of a number.

            Equations
            Instances For
              source
              theorem WoodinEtAl2024.Model.sum_weight_le_of_atLeastAsRound (M : Model) (hw : ∀ (p : Property), 0 ≤ M.weight p) {n m : ℕ} (h : Numerals.Roundness.AtLeastAsRound Property.Holds n m) :
              ∑ p ∈ Numerals.Roundness.profile Property.Holds n, M.weight p ≤ ∑ p ∈ Numerals.Roundness.profile Property.Holds m, M.weight p

              With non-negative weights, the roundness term is monotone in the roundness ordering.

              source
              theorem WoodinEtAl2024.Model.predicted_anti (M : Model) (hM : M.magnitude ≤ 0) {n m : ℕ} (hn : 0 < n) (hnm : n ≤ m) (h : Numerals.Roundness.profile Property.Holds n = Numerals.Roundness.profile Property.Holds m) :
              M.predicted m ≤ M.predicted n

              At equal roundness, a negative magnitude coefficient predicts the smaller number more frequent.

              source
              theorem WoodinEtAl2024.Model.predicted_le_iff (M : Model) {n m : ℕ} (h : Numerals.Roundness.AtLeastAsRound Property.Holds n m) :
              M.predicted n ≤ M.predicted m ↔ -M.magnitude * (Real.logb 10 ↑m - Real.logb 10 ↑n) ≤ ∑ p ∈ Numerals.Roundness.profile Property.Holds m \ Numerals.Roundness.profile Property.Holds n, M.weight p

              A rounder number is predicted at least as frequent as a less round one exactly when the weights of its extra properties make up the magnitude difference.

              source
              theorem WoodinEtAl2024.Model.predicted_99_le_100_iff (M : Model) :
              M.predicted 99 ≤ M.predicted 100 ↔ -M.magnitude * Real.logb 10 (100 / 99) ≤ ∑ p : Property, M.weight p

              In the study's illustration 100 has every property and 99 none, so 100 is predicted more frequent exactly when the summed weights make up the magnitude penalty of one part in a hundred.