English Measure Phrase Fragment

[BS22] [BS26a] [Cop21] [Sco14] [Dav79]

Lexical entries for English measure terms and the preposition per.

This fragment provides the English-specific data layer for measurement:

• Measure term entries (gram, kilo, mile,...) typed by Dimension
• The preposition per with its dual interpretation
• Context-dependent interpretation selection

Architecture

The Dimension / QuotientDimension / DimensionType taxonomies live in Features/Dimension.lean. The MeasureFn structure and MeasureFn.applyNumeral semantics live in Semantics/Measurement/Basic.lean. This file provides English lexical entries — pure data typed by those substrate types, following the Theories → Fragments dependency discipline.

structure English.MeasurePhrases.MeasureTermEntry : Type

A measure term entry: an English noun that names a specific measure function.

This is the Fragment-level data for measure terms. The Theory-level semantics (MeasureFn, MeasureFn.applyNumeral) is in Semantics.Measurement.Basic.

• form : String

  Surface form (e.g., "gram", "milliliter", "mile").

• formPlural : String

  Plural form.

• dimension : Features.Dimension.Dimension

  Which dimension this term measures.

@[implicit_reducible]

instance English.MeasurePhrases.instReprMeasureTermEntry : Repr MeasureTermEntry

Equations

• English.MeasurePhrases.instReprMeasureTermEntry = { reprPrec := English.MeasurePhrases.instReprMeasureTermEntry.repr }

def English.MeasurePhrases.instReprMeasureTermEntry.repr : MeasureTermEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.MeasurePhrases.instBEqMeasureTermEntry : BEq MeasureTermEntry

Equations

• English.MeasurePhrases.instBEqMeasureTermEntry = { beq := English.MeasurePhrases.instBEqMeasureTermEntry.beq }

def English.MeasurePhrases.instBEqMeasureTermEntry.beq : MeasureTermEntry → MeasureTermEntry → Bool

Equations

• English.MeasurePhrases.instBEqMeasureTermEntry.beq { form := a, formPlural := a_1, dimension := a_2 } { form := b, formPlural := b_1, dimension := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• English.MeasurePhrases.instBEqMeasureTermEntry.beq x✝¹ x✝ = false

def English.MeasurePhrases.gram : MeasureTermEntry

Equations

• English.MeasurePhrases.gram = { form := "gram", formPlural := "grams", dimension := Features.Dimension.Dimension.mass }

def English.MeasurePhrases.kilo : MeasureTermEntry

Equations

• English.MeasurePhrases.kilo = { form := "kilo", formPlural := "kilos", dimension := Features.Dimension.Dimension.mass }

def English.MeasurePhrases.pound : MeasureTermEntry

Equations

• English.MeasurePhrases.pound = { form := "pound", formPlural := "pounds", dimension := Features.Dimension.Dimension.mass }

def English.MeasurePhrases.milliliter : MeasureTermEntry

Equations

• English.MeasurePhrases.milliliter = { form := "milliliter", formPlural := "milliliters", dimension := Features.Dimension.Dimension.volume }

def English.MeasurePhrases.liter : MeasureTermEntry

Equations

• English.MeasurePhrases.liter = { form := "liter", formPlural := "liters", dimension := Features.Dimension.Dimension.volume }

def English.MeasurePhrases.mile : MeasureTermEntry

Equations

• English.MeasurePhrases.mile = { form := "mile", formPlural := "miles", dimension := Features.Dimension.Dimension.distance }

def English.MeasurePhrases.kilometer : MeasureTermEntry

Equations

• English.MeasurePhrases.kilometer = { form := "kilometer", formPlural := "kilometers", dimension := Features.Dimension.Dimension.distance }

def English.MeasurePhrases.meter : MeasureTermEntry

Equations

• English.MeasurePhrases.meter = { form := "meter", formPlural := "meters", dimension := Features.Dimension.Dimension.distance }

def English.MeasurePhrases.hour : MeasureTermEntry

Equations

• English.MeasurePhrases.hour = { form := "hour", formPlural := "hours", dimension := Features.Dimension.Dimension.time }

def English.MeasurePhrases.second_ : MeasureTermEntry

Equations

• English.MeasurePhrases.second_ = { form := "second", formPlural := "seconds", dimension := Features.Dimension.Dimension.time }

def English.MeasurePhrases.allMeasureTerms : List MeasureTermEntry

Equations

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

structure English.MeasurePhrases.QuantizingNounEntry : Type

A quantizing noun entry: an English noun that turns a mass term into a countable expression.

[Sco14] identifies three classes, each with different semantics:

• Measure terms (kilo, liter): type ⟨n, ⟨e,t⟩⟩, always quantity-uniform. Already covered by MeasureTermEntry above.
• Container nouns (glass, box, cup): ambiguous between a CONTAINER reading (individuated physical objects, NOT quantity-uniform) and a MEASURE reading (functions as a volume/mass unit, IS quantity-uniform).
• Atomizers (grain, piece, drop): impose a minimal-part structure on a mass noun, creating countable atoms without naming a measure function.

The Fragment entry captures the lexical form and class. The semantic distinction (quantity-uniformity, CONTAINER vs MEASURE reading) comes from the Theory types QuantizingNounClass and ContainerReading.

• form : String

  Surface form (e.g., "glass", "grain").

• formPlural : String

  Plural form.

• nounClass : Semantics.Measurement.QuantizingNounClass

  Which class of quantizing noun.

• measureDimension : Option Features.Dimension.Dimension

  For container nouns in their MEASURE reading: which dimension they measure. A glass measures volume; a bag might measure volume or mass. Atomizers and pure containers have none.

• availableReadings : List Semantics.Measurement.ContainerReading

  Available readings. Measure terms and atomizers have only one reading; container nouns are ambiguous between CONTAINER and MEASURE.

@[implicit_reducible]

instance English.MeasurePhrases.instReprQuantizingNounEntry : Repr QuantizingNounEntry

Equations

• English.MeasurePhrases.instReprQuantizingNounEntry = { reprPrec := English.MeasurePhrases.instReprQuantizingNounEntry.repr }

def English.MeasurePhrases.instReprQuantizingNounEntry.repr : QuantizingNounEntry → ℕ → Std.Format

Equations

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

def English.MeasurePhrases.instBEqQuantizingNounEntry.beq : QuantizingNounEntry → QuantizingNounEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• English.MeasurePhrases.instBEqQuantizingNounEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance English.MeasurePhrases.instBEqQuantizingNounEntry : BEq QuantizingNounEntry

Equations

• English.MeasurePhrases.instBEqQuantizingNounEntry = { beq := English.MeasurePhrases.instBEqQuantizingNounEntry.beq }

def English.MeasurePhrases.glass : QuantizingNounEntry

"glass" — prototypical container noun (Scontras §3.2).

• CONTAINER: "three glasses of water" = three individual glasses containing water
• MEASURE: "three glasses of water" = a quantity of water equal to three glass-volumes

The CONTAINER reading is NOT quantity-uniform: three glasses ⊕ three glasses ≠ three glasses. The MEASURE reading IS quantity-uniform (like any measure term).

Equations

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

def English.MeasurePhrases.box : QuantizingNounEntry

Equations

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

def English.MeasurePhrases.cup : QuantizingNounEntry

Equations

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

def English.MeasurePhrases.bag : QuantizingNounEntry

Equations

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

def English.MeasurePhrases.bottle : QuantizingNounEntry

Equations

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

def English.MeasurePhrases.grain : QuantizingNounEntry

"grain" — atomizer (Scontras §3.3).

"three grains of rice" imposes a minimal-part structure on the mass noun "rice". Unlike measure terms, "grain" does not name a standard measure function — it creates contextually-determined atoms.

Equations

• English.MeasurePhrases.grain = { form := "grain", formPlural := "grains", nounClass := Semantics.Measurement.QuantizingNounClass.atomizer }

def English.MeasurePhrases.piece : QuantizingNounEntry

Equations

• English.MeasurePhrases.piece = { form := "piece", formPlural := "pieces", nounClass := Semantics.Measurement.QuantizingNounClass.atomizer }

def English.MeasurePhrases.drop : QuantizingNounEntry

Equations

• English.MeasurePhrases.drop = { form := "drop", formPlural := "drops", nounClass := Semantics.Measurement.QuantizingNounClass.atomizer }

def English.MeasurePhrases.slice : QuantizingNounEntry

Equations

• English.MeasurePhrases.slice = { form := "slice", formPlural := "slices", nounClass := Semantics.Measurement.QuantizingNounClass.atomizer }

def English.MeasurePhrases.chunk : QuantizingNounEntry

Equations

• English.MeasurePhrases.chunk = { form := "chunk", formPlural := "chunks", nounClass := Semantics.Measurement.QuantizingNounClass.atomizer }

def English.MeasurePhrases.allQuantizingNouns : List QuantizingNounEntry

Equations

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

def English.MeasurePhrases.allContainerNouns : List QuantizingNounEntry

Equations

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

def English.MeasurePhrases.allAtomizers : List QuantizingNounEntry

Equations

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

inductive English.MeasurePhrases.PerInterpretation : Type

Interpretation mode for per-phrases.

Per exhibits a dual interpretive pattern:

• Compositional: when saturating measure predicates that select for simplex dimensions (weight, distance). The grammar computes meaning via multiplication.
• Math speak: when describing quotient dimensions (density, speed). The phrase verbalizes quantity calculus notation and gets its meaning from extra-grammatical conventions, parallel to mixed quotation.

• compositional : PerInterpretation

  Grammatically composed: per interacts with a covert pronoun pro whose value is determined anaphorically ([BS22], eq. 16). ⟦per⟧ = λq. λx. μ_{dim(q)}(x) / q The result is a pure number that composes with the measure phrase via multiplication ([BS26a]: multiplication only).

• mathSpeak : PerInterpretation

  Math speak: the per-phrase verbalizes a quantity calculus expression. Not derived from the syntactic structure of English.

• idiomatic : PerInterpretation

  Non-compositional, idiomatic unit (e.g., "pounds per square inch" = psi). Speakers know the abbreviation without knowing the underlying ratio.

@[implicit_reducible]

instance English.MeasurePhrases.instReprPerInterpretation : Repr PerInterpretation

Equations

• English.MeasurePhrases.instReprPerInterpretation = { reprPrec := English.MeasurePhrases.instReprPerInterpretation.repr }

def English.MeasurePhrases.instReprPerInterpretation.repr : PerInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.MeasurePhrases.instDecidableEqPerInterpretation : DecidableEq PerInterpretation

Equations

• English.MeasurePhrases.instDecidableEqPerInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure English.MeasurePhrases.PerEntry : Type

Entry for the preposition per in measure phrases.

• form : String
• interpretations : List PerInterpretation

  Per is ambiguous between compositional and math-speak interpretations.

• usesMultiplicationOnly : Bool

  Compositional per composes via multiplication only (No Division Hypothesis).

def English.MeasurePhrases.instReprPerEntry.repr : PerEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.MeasurePhrases.instReprPerEntry : Repr PerEntry

Equations

• English.MeasurePhrases.instReprPerEntry = { reprPrec := English.MeasurePhrases.instReprPerEntry.repr }

@[implicit_reducible]

instance English.MeasurePhrases.instBEqPerEntry : BEq PerEntry

Equations

• English.MeasurePhrases.instBEqPerEntry = { beq := English.MeasurePhrases.instBEqPerEntry.beq }

def English.MeasurePhrases.instBEqPerEntry.beq : PerEntry → PerEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• English.MeasurePhrases.instBEqPerEntry.beq x✝¹ x✝ = false

def English.MeasurePhrases.per : PerEntry

Equations

• English.MeasurePhrases.per = { }

def English.MeasurePhrases.perInterpInContext (selectsDimension : Features.Dimension.Dimension) (predicateDimension : Option Features.Dimension.Dimension) : PerInterpretation

Which interpretation is available depends on the dimension type of the measure predicate. Simplex dimensions license compositional interpretation; quotient dimensions force math speak.

Equations

• One or more equations did not get rendered due to their size.
• English.MeasurePhrases.perInterpInContext selectsDimension none = English.MeasurePhrases.PerInterpretation.mathSpeak

theorem English.MeasurePhrases.gram_is_mass : gram.dimension = Features.Dimension.Dimension.mass

All measure terms have distinct dimensions appropriately assigned.

theorem English.MeasurePhrases.liter_is_volume : liter.dimension = Features.Dimension.Dimension.volume

theorem English.MeasurePhrases.mile_is_distance : mile.dimension = Features.Dimension.Dimension.distance

theorem English.MeasurePhrases.hour_is_time : hour.dimension = Features.Dimension.Dimension.time

theorem English.MeasurePhrases.glass_is_container : glass.nounClass = Semantics.Measurement.QuantizingNounClass.containerNoun

Container nouns are classified correctly.

theorem English.MeasurePhrases.box_is_container : box.nounClass = Semantics.Measurement.QuantizingNounClass.containerNoun

theorem English.MeasurePhrases.grain_is_atomizer : grain.nounClass = Semantics.Measurement.QuantizingNounClass.atomizer

Atomizers are classified correctly.

theorem English.MeasurePhrases.piece_is_atomizer : piece.nounClass = Semantics.Measurement.QuantizingNounClass.atomizer

theorem English.MeasurePhrases.glass_has_both_readings : glass.availableReadings = [Semantics.Measurement.ContainerReading.container, Semantics.Measurement.ContainerReading.measure]

Container nouns have both readings available.

theorem English.MeasurePhrases.glass_measures_volume : glass.measureDimension = some Features.Dimension.Dimension.volume

Container nouns in MEASURE reading measure volume.

theorem English.MeasurePhrases.grain_no_dimension : grain.measureDimension = none

Atomizers have no measure dimension (they don't name a measure function).

theorem English.MeasurePhrases.piece_no_dimension : piece.measureDimension = none

theorem English.MeasurePhrases.all_containers_are_containers (n : QuantizingNounEntry) : n ∈ allContainerNouns → n.nounClass = Semantics.Measurement.QuantizingNounClass.containerNoun

All container nouns are container nouns; all atomizers are atomizers.

theorem English.MeasurePhrases.all_atomizers_are_atomizers (n : QuantizingNounEntry) : n ∈ allAtomizers → n.nounClass = Semantics.Measurement.QuantizingNounClass.atomizer

theorem English.MeasurePhrases.containers_have_dimension (n : QuantizingNounEntry) : n ∈ allContainerNouns → n.measureDimension.isSome = true

Container nouns all have a measure dimension; atomizers never do.

theorem English.MeasurePhrases.atomizers_lack_dimension (n : QuantizingNounEntry) : n ∈ allAtomizers → n.measureDimension.isNone = true

theorem English.MeasurePhrases.per_default_interps : per.interpretations = [PerInterpretation.compositional, PerInterpretation.mathSpeak]

Per defaults to compositional and math-speak interpretations.

theorem English.MeasurePhrases.per_multiplication_only : per.usesMultiplicationOnly = true

Compositional per uses multiplication only.

theorem English.MeasurePhrases.same_dimension_compositional (d : Features.Dimension.Dimension) : perInterpInContext d (some d) = PerInterpretation.compositional

When a verb selects for the same dimension as the per-phrase's unit, the interpretation is compositional.

theorem English.MeasurePhrases.different_dimension_mathSpeak (d₁ d₂ : Features.Dimension.Dimension) (h : d₁ ≠ d₂) : perInterpInContext d₁ (some d₂) = PerInterpretation.mathSpeak

When the verb selects for a different dimension (or none), the interpretation is math speak.

theorem English.MeasurePhrases.no_dimension_mathSpeak (d : Features.Dimension.Dimension) : perInterpInContext d none = PerInterpretation.mathSpeak

When no predicate dimension is available, the interpretation is math speak.