Hurford (2007): A performed practice explains a linguistic universal

This file formalizes Hurford's explanation of the Packing Strategy by the practice of counting. A counter goes as far as the recited sequence allows, sets what has been counted aside as a group, gathers the groups into one of the next base up once there are enough of them, and counts the groups and the remainder the same way. count computes the outcome over a language's list of bases, and the numerals the Packing Strategy admits are exactly the ones counting produces. Hurford's English, Mixtec and Hawaiian illustrations are packed and their starred rearrangements are not, while English twenty one hundred, one of his rare exceptions, is attested but rejected.

Main definitions

• count: counting with a list of bases

Main results

• packed_count: counting reaches a packed numeral
• packed_iff_eq_count: the packed numerals are the outcomes of counting
• Mixtec.count_eq_numeral7999, Hawaiian.count_eq_numeral609751: counting reaches the paper's Mixtec and Hawaiian numerals
• English.not_packed_twentyOneHundred: the Packing Strategy rejects twenty one hundred

Implementation notes

The trees use the 1975 grammar of Numeral, so a DIGIT is a tally and a PHRASE of a bare M is [one M]. English million is the base-power M of value 10 ^ 6, since the Packing Strategy compares only values. The Mixtec bases are the three of the example and the Hawaiian ones the seven Hurford lists.

References

• [Hur07]
• [Hur75]

Counting

@[irreducible]

def Hurford2007.count (L : List Numeral.M) (v : ℕ) : Numeral.Number

count L v counts v objects with the bases L. When every base exceeds v it recites the counting sequence up to v; otherwise it sets aside as many groups of the highest base that fits as possible, and counts the groups and the remainder the same way.

Equations

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

theorem Hurford2007.packed_count (L : List Numeral.M) {v : ℕ} (hv : 0 < v) : Numeral.Number.Packed {m : Numeral.M | m ∈ L} (count L v) ∧ (count L v).value = v

Counting reaches a packed numeral for every positive number.

theorem Hurford2007.packed_iff_eq_count {L : List Numeral.M} (hL : Set.InjOn Numeral.M.value {m : Numeral.M | m ∈ L}) {e : Numeral.Number} : Numeral.Number.Packed {m : Numeral.M | m ∈ L} e ↔ e = count L e.value

Over bases with distinct values, the numerals the Packing Strategy admits are exactly the ones counting produces.

theorem Hurford2007.count_eq_of_packed {L : List Numeral.M} (hL : Set.InjOn Numeral.M.value {m : Numeral.M | m ∈ L}) {e : Numeral.Number} {v : ℕ} (he : Numeral.Number.Packed {m : Numeral.M | m ∈ L} e) (hv : e.value = v) : count L v = e

Counting reaches every packed numeral, over bases with distinct values.

@[reducible, inline]

abbrev Hurford2007.digit (d : ℕ) : Numeral.Number

digit d is the tally of d marks.

Equations

• Hurford2007.digit d = Numeral.Number.tally (d - 1)

English

@[reducible, inline]

abbrev Hurford2007.English.hundred : Numeral.M

hundred is the M of value 10 ^ 2.

Equations

• Hurford2007.English.hundred = Numeral.M.tenPow 1

@[reducible, inline]

abbrev Hurford2007.English.thousand : Numeral.M

thousand is the M of value 10 ^ 3.

Equations

• Hurford2007.English.thousand = Numeral.M.tenPow 2

@[reducible, inline]

abbrev Hurford2007.English.million : Numeral.M

million is the M of value 10 ^ 6. [Hur75] builds it on thousand, with (31), p. 35, raising the exponent by one in American English.

Equations

• Hurford2007.English.million = Numeral.M.tenPow 5

def Hurford2007.English.bases : List Numeral.M

The English bases are ten, hundred, thousand and million.

Equations

• Hurford2007.English.bases = [Numeral.M.ten, Hurford2007.English.hundred, Hurford2007.English.thousand, Hurford2007.English.million]

theorem Hurford2007.English.injOn_bases : Set.InjOn Numeral.M.value {m : Numeral.M | m ∈ bases}

def Hurford2007.English.fiveMillionTwoThousandSixHundred : Numeral.Number

five million, two thousand, six hundred is [[five million] [[two thousand] [six hundred]]].

Equations

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

def Hurford2007.English.sixHundredTwoThousandFiveMillion : Numeral.Number

*six hundred, two thousand, five million packs the same PHRASEs the other way round.

Equations

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

def Hurford2007.English.sixHundredThousand : Numeral.Number

six hundred thousand is [[six hundred] thousand].

Equations

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

def Hurford2007.English.sixThousandHundred : Numeral.Number

*six thousand hundred is [[six thousand] hundred].

Equations

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

def Hurford2007.English.twoThousandOneHundred : Numeral.Number

two thousand, one hundred is [[two thousand] [one hundred]].

Equations

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

def Hurford2007.English.twentyOneHundred : Numeral.Number

twenty one hundred is [[twenty-one] hundred], twenty-one hundreds.

Equations

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

theorem Hurford2007.English.count_eq_fiveMillionTwoThousandSixHundred : count bases 5002600 = fiveMillionTwoThousandSixHundred

In additive constructions the higher-valued PHRASEs are packed nearer the top.

theorem Hurford2007.English.not_packed_sixHundredTwoThousandFiveMillion : ¬Numeral.Number.Packed {m : Numeral.M | m ∈ bases} sixHundredTwoThousandFiveMillion

theorem Hurford2007.English.count_eq_sixHundredThousand : count bases 600000 = sixHundredThousand

In multiplicative constructions the higher-valued bases are packed nearer the top.

theorem Hurford2007.English.not_packed_sixThousandHundred : ¬Numeral.Number.Packed {m : Numeral.M | m ∈ bases} sixThousandHundred

theorem Hurford2007.English.count_eq_twoThousandOneHundred : count bases 2100 = twoThousandOneHundred

theorem Hurford2007.English.not_packed_twentyOneHundred : ¬Numeral.Number.Packed {m : Numeral.M | m ∈ bases} twentyOneHundred

The Packing Strategy rejects twenty one hundred, which English allows, one of the rare counterexamples to its prediction that each number has a single numeral.

Mixtec

def Hurford2007.Mixtec.fifteen : Numeral.M

šiaʼu is the base 15.

Equations

• Hurford2007.Mixtec.fifteen = Numeral.M.base 15 Hurford2007.Mixtec.fifteen._proof_1

def Hurford2007.Mixtec.twenty : Numeral.M

šiko is the base 20.

Equations

• Hurford2007.Mixtec.twenty = Numeral.M.base 20 Hurford2007.Mixtec.twenty._proof_1

def Hurford2007.Mixtec.fourHundred : Numeral.M

tuu is the base 400.

Equations

• Hurford2007.Mixtec.fourHundred = Numeral.M.base 400 Hurford2007.Mixtec.fourHundred._proof_1

def Hurford2007.Mixtec.bases : List Numeral.M

The bases of the example are 15, 20 and 400.

Equations

• Hurford2007.Mixtec.bases = [Hurford2007.Mixtec.fifteen, Hurford2007.Mixtec.twenty, Hurford2007.Mixtec.fourHundred]

theorem Hurford2007.Mixtec.injOn_bases : Set.InjOn Numeral.M.value {m : Numeral.M | m ∈ bases}

def Hurford2007.Mixtec.nineteen : Numeral.Number

šiaʼu kuu, fifteen and four, is 19.

Equations

• Hurford2007.Mixtec.nineteen = Numeral.Number.phraseAnd (Numeral.Phrase.mk Numeral.Number.one Hurford2007.Mixtec.fifteen) (Hurford2007.digit 4)

def Hurford2007.Mixtec.numeral7999 : Numeral.Number

šiaʼu kuu tuu šiaʼu kuu šiko šiaʼu kuu, nineteen four-hundreds, nineteen twenties and nineteen, is 7999.

Equations

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

def Hurford2007.Mixtec.transposed : Numeral.Number

transposed has the two Ms of numeral7999 in each other's places.

Equations

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

theorem Hurford2007.Mixtec.count_eq_numeral7999 : count bases 7999 = numeral7999

The sisters of the recursive NUMBERs are the highest-valued the lexicon allows below the value of the dominating node.

theorem Hurford2007.Mixtec.not_packed_transposed : ¬Numeral.Number.Packed {m : Numeral.M | m ∈ bases} transposed

Transposing the two Ms loses well-formedness.

Hawaiian

def Hurford2007.Hawaiian.bases : List Numeral.M

The Hawaiian bases are 10, 20, 40, 400, 4000, 40,000 and 400,000.

Equations

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

theorem Hurford2007.Hawaiian.injOn_bases : Set.InjOn Numeral.M.value {m : Numeral.M | m ∈ bases}

def Hurford2007.Hawaiian.numeral609751 : Numeral.Number

The numeral for 609,751 is one 400,000, five 40,000s, two 4000s, four 400s, three 40s, twenty, ten and one.

Equations

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

theorem Hurford2007.Hawaiian.count_eq_numeral609751 : count bases 609751 = numeral609751