@cite{bale-schwarz-2022} — Measurements from per without complex dimensions

@cite{bale-schwarz-2022} @cite{coppock-2021}

Proceedings of SALT 32: 543--560.

Key Claims

1. Against the division theory: @cite{coppock-2021}'s lexical entry ⟦per⟧ = λr. λq. q/r (eq. 1) forms quotient quantities (e.g., 0.9 g/mL). This theory both undergenerates (fails for measurement verbs, §3) and overgenerates (predicts unit insensitivity in pseudo-partitives, §6).

2. Free relatives against polysemy (exx. 10-14): The division theory's escape — making measurement verbs polysemous (eq. 8) — is ruled out because weigh only admits weight readings, never density.

3. Anaphoric theory (eq. 16): ⟦per⟧ = λq. λx. μ_{dim(q)}(x)/q — per derives measure functions mapping entities to pure numbers via a covert pronoun pro in the per-PP's specifier (eq. 17).

4. MUCH (eq. 25): A covert element ⟦MUCH⟧ = λq. λx. μ(x) = q mediates pseudo-partitives, with μ underspecified and resolved contextually.

5. Unit sensitivity (exx. 37-40, 44-45): The per-unit sets a lower bound on the entity's measure. Revised entry (eq. 43) adds a presupposition: μ_{dim(q)}(x) ≥ q.

6. Copular puzzle (§8): An acknowledged open problem where the anaphoric theory assigns density copular sentences a dimension mismatch.

Connection to @cite{bale-schwarz-2026}

This SALT paper is the precursor to the L&P paper. The anaphoric theory of per originates here. The 2026 paper extends it with:

• The No Division Hypothesis (grammar composes via × and +, not ÷)
• The math speak analysis (quotient-dimension per = mixed quotation)
• The substitution and sub-extraction diagnostics

The 2022 paper uses division explicitly in its lexical entry (eq. 16); the 2026 paper shows this is reformulable using multiplication only.

def Phenomena.Quantification.BaleSchwarz2022.perDivision (r q : ℚ) : ℚ

Division theory (@cite{coppock-2021}, eq. 1): ⟦per⟧ = λr. λq. q/r.

Takes a denominator quantity r and a numerator quantity q, outputs their ratio — a quotient quantity in a complex dimension (e.g., g/mL in WT/VOL).

Equations

• Phenomena.Quantification.BaleSchwarz2022.perDivision r q = q / r

def Phenomena.Quantification.BaleSchwarz2022.perAnaphoric {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : ℚ

Anaphoric theory (@cite{bale-schwarz-2022}, eq. 16): ⟦per⟧ = λq. λx. μ_{dim(q)}(x) / q.

Takes a unit quantity q and an entity x, returns a pure number: the entity's measure in q's dimension, divided by q. The entity argument is supplied by a covert pronoun pro (eq. 17).

Equations

• Phenomena.Quantification.BaleSchwarz2022.perAnaphoric μ q x = μ.apply x / q

def Phenomena.Quantification.BaleSchwarz2022.measureVerbSem {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : Bool

Measurement verb semantics (eq. 5): ⟦weigh⟧ = λq. λx. μ_WT(x) = q.

A measurement verb maps a quantity to a predicate over entities. The verb's measure function determines which simplex dimension is measured: μ_WT for weigh, μ_VOL for contain (in measure readings).

Equations

• Phenomena.Quantification.BaleSchwarz2022.measureVerbSem μ q x = decide (μ.apply x = q)

The dimension mismatch argument

Under the division theory, "The sample weighs 0.9 grams per milliliter" (ex. 6) assigns the complement the denotation 0.9 g/mL — a quantity in dimension WT/VOL. But weigh outputs quantities in dimension WT (eq. 5). The predicted truth conditions (eq. 7) are:

μ_WT(the sample) = 0.9 g/mL

This is a dimension contradiction: μ_WT outputs WT-quantities, but 0.9 g/mL is a WT/VOL-quantity.

The division theory could escape by making weigh polysemous: adding ⟦weigh⟧' = λq. λx. μ_{WT/VOL}(x) = q (eq. 8). This would give the non-contradictory truth conditions μ_{WT/VOL}(sample) = 0.9 g/mL (eq. 9). But free relatives rule out this polysemy (§4 below).

theorem Phenomena.Quantification.BaleSchwarz2022.undergen_dimensions : Fragments.English.MeasurePhrases.gram.dimension = Semantics.Probabilistic.Measurement.Dimension.mass ∧ Fragments.English.MeasurePhrases.milliliter.dimension = Semantics.Probabilistic.Measurement.Dimension.volume

Fragment entries confirm the dimensions involved in the undergeneration: grams measure mass, milliliters measure volume.

theorem Phenomena.Quantification.BaleSchwarz2022.density_is_mass_over_volume : Semantics.Probabilistic.Measurement.QuotientDimension.density.components = (Semantics.Probabilistic.Measurement.Dimension.mass, Semantics.Probabilistic.Measurement.Dimension.volume)

Density is the quotient of the gram and milliliter dimensions. Under the division theory, "grams per milliliter" denotes a quantity in this quotient dimension — incompatible with weigh's simplex mass dimension.

theorem Phenomena.Quantification.BaleSchwarz2022.quotient_dimension_differs_from_components (q : Semantics.Probabilistic.Measurement.QuotientDimension) : q.components.1 ≠ q.components.2

Quotient components are always distinct simplex dimensions.

The free relative argument

The division theory's only escape from undergeneration is to make weigh polysemous: the basic meaning (eq. 5) plus a density meaning (eq. 8). Free relatives rule this out.

(10) "This cube weighs what that cube weighs." Under the basic meaning: μ_WT(this cube) = μ_WT(that cube) — same WEIGHT ✓ If eq. 8 existed: μ_{WT/VOL}(this cube) = μ_{WT/VOL}(that cube) — same DENSITY

But (10) can ONLY be understood as same weight, not same density: a 1kg cube and a 2kg cube may have the same density but (10) is clearly false of them. This extends to comparatives (14a) and wh-interrogatives (14b).

The crucial feature of (10), setting it apart from (3) and (6), is that the complement of weigh does not constrain the dimension — so if the density meaning existed, nothing would block it.

inductive Phenomena.Quantification.BaleSchwarz2022.WeighReading : Type

Readings of weigh: only weight is attested. The division theory would need density (eq. 8), but free relatives rule it out.

• weight : WeighReading
• density : WeighReading

instance Phenomena.Quantification.BaleSchwarz2022.instReprWeighReading : Repr WeighReading

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprWeighReading = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprWeighReading.repr }

def Phenomena.Quantification.BaleSchwarz2022.instReprWeighReading.repr : WeighReading → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instDecidableEqWeighReading : DecidableEq WeighReading

Equations

• Phenomena.Quantification.BaleSchwarz2022.instDecidableEqWeighReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.BaleSchwarz2022.instBEqWeighReading.beq : WeighReading → WeighReading → Bool

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqWeighReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.BaleSchwarz2022.instBEqWeighReading : BEq WeighReading

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqWeighReading = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqWeighReading.beq }

structure Phenomena.Quantification.BaleSchwarz2022.FreeRelativeDatum : Type

Free relative data: weigh admits only weight readings.

• surface : String
• reading : WeighReading
• judgment : Core.Empirical.Acceptability

def Phenomena.Quantification.BaleSchwarz2022.instReprFreeRelativeDatum.repr : FreeRelativeDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instReprFreeRelativeDatum : Repr FreeRelativeDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprFreeRelativeDatum = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprFreeRelativeDatum.repr }

def Phenomena.Quantification.BaleSchwarz2022.instBEqFreeRelativeDatum.beq : FreeRelativeDatum → FreeRelativeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.BaleSchwarz2022.instBEqFreeRelativeDatum.beq x✝¹ x✝ = false

instance Phenomena.Quantification.BaleSchwarz2022.instBEqFreeRelativeDatum : BEq FreeRelativeDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqFreeRelativeDatum = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqFreeRelativeDatum.beq }

def Phenomena.Quantification.BaleSchwarz2022.ex10_weight : FreeRelativeDatum

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex10_density : FreeRelativeDatum

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex14a : FreeRelativeDatum

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex14b : FreeRelativeDatum

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.allFreeRelativeData : List FreeRelativeDatum

Equations

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

theorem Phenomena.Quantification.BaleSchwarz2022.free_relatives_rule_out_density (d : FreeRelativeDatum) : d ∈ allFreeRelativeData → (d.reading = WeighReading.weight → d.judgment = Core.Empirical.Acceptability.ok) ∧ (d.reading = WeighReading.density → d.judgment = Core.Empirical.Acceptability.unacceptable)

Weight readings are always acceptable; density readings never are. This rules out the polysemous entry for weigh that the division theory would need — confirming the undergeneration is genuine.

Compositional derivation

The anaphoric theory derives truth conditions for (6) "The sample weighs 0.9 grams per milliliter" via the following steps:

1. Parse (eq. 20): [sample] weighs [_MP [_MP 0.9 grams] [_PP pro [per mL]]]
2. ⟦per milliliter⟧ = λx. μ_VOL(x) / mL (eq. 15, instance of eq. 16)
3. ⟦per milliliter⟧(pro) = μ_VOL(sample) / mL — a pure number
4. ⟦[MP 0.9 grams] [PP pro per mL]⟧ = (0.9 * μ_VOL(sample)/mL) g (eq. 19)
5. ⟦weigh⟧(⟦fullMP⟧)(sample): μ_WT(sample) = (0.9 * μ_VOL(sample)/mL) g (eq. 22)

The final quantity is in dimension WT (mass), matching weigh's selection. No dimension mismatch arises.

def Phenomena.Quantification.BaleSchwarz2022.anaphoricTC {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) (numeral perUnit : ℚ) : Prop

Truth conditions under the anaphoric theory (eq. 22): μ_WT(sample) = numeral * (μ_VOL(sample) / perUnit).

Equations

• Phenomena.Quantification.BaleSchwarz2022.anaphoricTC μ_wt μ_vol sample numeral perUnit = (μ_wt.apply sample = numeral * Phenomena.Quantification.BaleSchwarz2022.perAnaphoric μ_vol perUnit sample)

theorem Phenomena.Quantification.BaleSchwarz2022.anaphoric_tc_equivalent {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) (numeral perUnit : ℚ) : anaphoricTC μ_wt μ_vol sample numeral perUnit ↔ μ_wt.apply sample = numeral * (μ_vol.apply sample / perUnit)

The anaphoric theory derives truth conditions for pseudo-partitives (ex. 27 "The mixture contains 0.1 grams per milliliter of salt") that are equivalent under the quantity calculus to the division theory's (eq. 32).

Both theories yield: ∃x[salt(x) ∧ μ_WT(x) = (0.1 * μ_VOL(mixture)/mL) g ∧ contain(mixture, x)]

The key difference is structural: the anaphoric theory reaches these truth conditions without ever forming a quotient quantity (0.1 g/mL), keeping all composed values in simplex dimensions. This matters because the anaphoric theory can then add the unit sensitivity presupposition (eq. 43), while the division theory cannot (the per-unit is structurally inaccessible).

theorem Phenomena.Quantification.BaleSchwarz2022.verb_dimension_matches_fragment : Fragments.English.MeasurePhrases.gram.dimension = Semantics.Probabilistic.Measurement.Dimension.mass ∧ Fragments.English.MeasurePhrases.kilo.dimension = Semantics.Probabilistic.Measurement.Dimension.mass

Both the gram and kilo Fragment entries measure mass — connecting the truth conditions' μ_wt to the Fragment's lexical data.

MUCH: a covert measure term

@cite{bale-schwarz-2022} adopt @cite{nakanishi-2007}'s analysis where a covert element MUCH mediates pseudo-partitives (eq. 24). MUCH's denotation (eq. 25):

⟦MUCH⟧ = λq. λx. μ(x) = q

This is identical to MeasureTermSem.applyNumeral — MUCH IS a measure term, but with an underspecified measure function μ resolved contextually:

• μ_WT in "0.9 grams of salt" (eq. 24a)
• μ_VOL in "0.8 milliliters of salt" (eq. 24b)
• An anaphorically determined function in per-phrases (eq. 30)

def Phenomena.Quantification.BaleSchwarz2022.MUCH {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) : Semantics.Probabilistic.Measurement.MeasureTermSem E

MUCH as a MeasureTermSem (eq. 25). The measure function μ is underspecified — resolved contextually to the appropriate dimension.

Equations

• Phenomena.Quantification.BaleSchwarz2022.MUCH μ = { measureFn := μ }

theorem Phenomena.Quantification.BaleSchwarz2022.MUCH_is_measureTerm {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (n : ℚ) (x : E) : (MUCH μ).applyNumeral n x = (μ.apply x == n)

MUCH's denotation matches measure term semantics by construction: ⟦MUCH⟧(q)(x) = (μ(x) == q) = MeasureTermSem.applyNumeral(q)(x).

theorem Phenomena.Quantification.BaleSchwarz2022.measureVerb_applied {E : Type u_1} (μ_wt : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : measureVerbSem μ_wt q x = decide (μ_wt.apply x = q)

The measure verb semantics (eq. 5) is used in the anaphoric derivation: the truth conditions are stated as measureVerbSem μ_wt q sample = true, where q is the composed quantity from the anaphoric per-phrase.

Unit insensitivity prediction

The division theory predicts that different unit pairs yielding the same quotient are interchangeable. Since kg = 1000g and L = 1000mL:

g/mL = kg/L

So "0.1 grams per milliliter of salt" (ex. 27) should have identical truth conditions to "0.1 kilograms per liter of salt" (ex. 36a). But speakers distinguish them: per liter implies volume ≥ 1L, while per milliliter implies volume ≥ 1mL only.

theorem Phenomena.Quantification.BaleSchwarz2022.division_scaling_invariant (r q k : ℚ) (hk : k ≠ 0) : perDivision r q = perDivision (k * r) (k * q)

Quantity division is invariant under uniform scaling: for any nonzero scaling factor k, q/r = (kq)/(kr). This is why the division theory cannot distinguish "per milliliter" from "per liter" — they are related by k = 1000.

theorem Phenomena.Quantification.BaleSchwarz2022.division_unit_insensitive : perDivision 1 1 = perDivision 1000 1000

Concrete instance: g/mL = kg/L (k = 1000). The division theory therefore cannot distinguish (27) from (36a).

theorem Phenomena.Quantification.BaleSchwarz2022.unit_pairs_share_dimensions : Fragments.English.MeasurePhrases.gram.dimension = Fragments.English.MeasurePhrases.kilo.dimension ∧ Fragments.English.MeasurePhrases.milliliter.dimension = Fragments.English.MeasurePhrases.liter.dimension

Gram and kilo share the mass dimension; milliliter and liter share volume. The unit sensitivity argument relies on same-dimension units that differ in magnitude, not dimension.

structure Phenomena.Quantification.BaleSchwarz2022.UnitSensitivityDatum : Type

Unit sensitivity datum: felicity depends on whether the entity's measure in the per-unit's dimension is at least as large as the unit quantity.

• surface : String
• entityVolume_mL : ℚ

  Volume of the entity (in mL).

• perUnit_mL : ℚ

  The per-unit quantity (in mL).

• presupSatisfied : Bool

  Is the entity's volume ≥ the per-unit?

• judgment : Core.Empirical.Acceptability

instance Phenomena.Quantification.BaleSchwarz2022.instReprUnitSensitivityDatum : Repr UnitSensitivityDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprUnitSensitivityDatum = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprUnitSensitivityDatum.repr }

def Phenomena.Quantification.BaleSchwarz2022.instReprUnitSensitivityDatum.repr : UnitSensitivityDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instBEqUnitSensitivityDatum : BEq UnitSensitivityDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqUnitSensitivityDatum = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqUnitSensitivityDatum.beq }

def Phenomena.Quantification.BaleSchwarz2022.instBEqUnitSensitivityDatum.beq : UnitSensitivityDatum → UnitSensitivityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.BaleSchwarz2022.instBEqUnitSensitivityDatum.beq x✝¹ x✝ = false

def Phenomena.Quantification.BaleSchwarz2022.ex37 : UnitSensitivityDatum

(37) ✓ The 5mL sample contained 0.1 grams of salt per milliliter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex38a : UnitSensitivityDatum

(38a) # The 5mL sample contained 0.1 grams of salt per liter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex38b : UnitSensitivityDatum

(38b) # The 0.1mL sample contained 0.1 grams of salt per milliliter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex44 : UnitSensitivityDatum

(44) ✓ The 5mL portion weighed 0.9 grams per milliliter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex45a : UnitSensitivityDatum

(45a) # The 5mL portion weighed 0.9 kilograms per liter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex45b : UnitSensitivityDatum

(45b) # The 0.1mL portion weighed 0.9 grams per milliliter.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.allUnitSensitivityData : List UnitSensitivityDatum

Equations

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

Typos per page: unit sensitivity generalizes

Unit sensitivity extends beyond chemistry to any per-phrase. Exx. (39-40) show that text-length units exhibit the same pattern:

• A monograph has at least one page → "per page" OK (39a)
• A paragraph has at least one line → "per line" OK (39b)
• A paragraph has less than a page → "#per page" anomalous (40)

structure Phenomena.Quantification.BaleSchwarz2022.TextUnitDatum : Type

Text-domain unit sensitivity data (exx. 39-40).

• surface : String
• presupSatisfied : Bool
• judgment : Core.Empirical.Acceptability

def Phenomena.Quantification.BaleSchwarz2022.instReprTextUnitDatum.repr : TextUnitDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instReprTextUnitDatum : Repr TextUnitDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprTextUnitDatum = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprTextUnitDatum.repr }

instance Phenomena.Quantification.BaleSchwarz2022.instBEqTextUnitDatum : BEq TextUnitDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqTextUnitDatum = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqTextUnitDatum.beq }

def Phenomena.Quantification.BaleSchwarz2022.instBEqTextUnitDatum.beq : TextUnitDatum → TextUnitDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.BaleSchwarz2022.instBEqTextUnitDatum.beq x✝¹ x✝ = false

def Phenomena.Quantification.BaleSchwarz2022.ex39a : TextUnitDatum

(39a) ✓ The monograph by Dole contained more than 3 typos per page.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex39b : TextUnitDatum

(39b) ✓ The paragraph by Dole contained more than 3 typos per line.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.ex40 : TextUnitDatum

(40) # The paragraph by Dole contained more than 3 typos per page.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.allTextUnitData : List TextUnitDatum

Equations

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

theorem Phenomena.Quantification.BaleSchwarz2022.text_unit_sensitivity (d : TextUnitDatum) : d ∈ allTextUnitData → (d.presupSatisfied = true → d.judgment = Core.Empirical.Acceptability.ok) ∧ (d.presupSatisfied = false → d.judgment = Core.Empirical.Acceptability.anomalous)

Unit sensitivity in the text domain matches the presupposition prediction: presup satisfied → ok, presup violated → anomalous.

def Phenomena.Quantification.BaleSchwarz2022.perAnaphoricWithPresup {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : Core.Presupposition.PrValue Unit ℚ

The revised lexical entry for per (eq. 43) as a PrValue: ⟦per⟧ = λq. λx: μ_{dim(q)}(x) ≥ q. μ_{dim(q)}(x) / q

• presup: μ_{dim(q)}(x) ≥ q (unit sensitivity)
• value: μ_{dim(q)}(x) / q (pure number)

This is the canonical use case for PrValue: the at-issue content is a pure number (ℚ), not a truth value (Bool). PrProp cannot represent this directly — it only handles presupposed propositions.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.perPresup {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : Bool

The unit sensitivity presupposition (eq. 43): μ_{dim(q)}(x) ≥ q.

Equations

• Phenomena.Quantification.BaleSchwarz2022.perPresup μ q x = decide (μ.apply x ≥ q)

theorem Phenomena.Quantification.BaleSchwarz2022.presup_satisfied_iff {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : (perAnaphoricWithPresup μ q x).presup () = true ↔ μ.apply x ≥ q

The presupposition is satisfied iff the entity's measure ≥ the unit.

theorem Phenomena.Quantification.BaleSchwarz2022.perValue_eq {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : ℚ) (x : E) : (perAnaphoricWithPresup μ q x).value () = perAnaphoric μ q x

The at-issue value is the pure number μ(x)/q.

def Phenomena.Quantification.BaleSchwarz2022.perSentenceWithPresup {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (perUnit numeral : ℚ) (x : E) : Core.Presupposition.PrProp Unit

At the sentence level, PrValue ℚ composes with a measurement verb to produce a PrProp — presupposition projects, assertion is boolean.

Equations

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

theorem Phenomena.Quantification.BaleSchwarz2022.assertion_matches_tc {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (perUnit numeral : ℚ) (x : E) : (perSentenceWithPresup μ_wt μ_vol perUnit numeral x).assertion () = true ↔ anaphoricTC μ_wt μ_vol x numeral perUnit

The sentence-level assertion matches anaphoricTC.

theorem Phenomena.Quantification.BaleSchwarz2022.presup_matches_data (d : UnitSensitivityDatum) : d ∈ allUnitSensitivityData → d.presupSatisfied = decide (d.entityVolume_mL ≥ d.perUnit_mL)

The presupSatisfied field in each datum correctly reflects the entity volume ≥ per-unit comparison.

theorem Phenomena.Quantification.BaleSchwarz2022.presup_predicts_felicity (d : UnitSensitivityDatum) : d ∈ allUnitSensitivityData → (d.presupSatisfied = true → d.judgment = Core.Empirical.Acceptability.ok) ∧ (d.presupSatisfied = false → d.judgment = Core.Empirical.Acceptability.anomalous)

Presupposition satisfaction predicts acceptability: satisfied → ok, not satisfied → anomalous.

theorem Phenomena.Quantification.BaleSchwarz2022.anaphoric_distinguishes_units {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (x : E) (h : μ.apply x = 5) : decide (μ.apply x ≥ 1) = true ∧ decide (μ.apply x ≥ 1000) = false

The anaphoric theory distinguishes "per milliliter" from "per liter" via different presuppositions, even when the ratios are numerically equal.

Open problem: copular density sentences

"The sample's density is 0.9 grams per milliliter" (ex. 46) is problematic for the anaphoric theory. The per-PP denotes a pure number, so the MP "0.9 grams per milliliter" denotes a weight quantity (dimension WT). But the copular sentence equates the sample's density (dimension WT/VOL) with a weight quantity — a dimension mismatch.

Under the division theory, (46) is straightforward: the MP denotes 0.9 g/mL, a quotient quantity matching the density dimension.

@cite{bale-schwarz-2022} note that for every paraphrases (ex. 48: "0.9 grams for every cubic centimeter") and naturally occurring density expressions (ex. 49: "968 people for every km²") suggest that density copular sentences may not require quantity division. This remains an open question.

theorem Phenomena.Quantification.BaleSchwarz2022.copular_anaphoric_mismatch : Fragments.English.MeasurePhrases.gram.dimension = Semantics.Probabilistic.Measurement.Dimension.mass ∧ Semantics.Probabilistic.Measurement.QuotientDimension.density.components = (Semantics.Probabilistic.Measurement.Dimension.mass, Semantics.Probabilistic.Measurement.Dimension.volume)

Under the anaphoric theory, the MP's dimension is determined by its head noun. "Grams" → mass (a simplex Dimension). But density predicates expect WT/VOL (a QuotientDimension). These are structurally incompatible: Dimension and QuotientDimension are different types in the formalization, and the MP is typed as mass, not as mass/volume.

theorem Phenomena.Quantification.BaleSchwarz2022.copular_division_matches : Semantics.Probabilistic.Measurement.QuotientDimension.density.components = (Fragments.English.MeasurePhrases.gram.dimension, Fragments.English.MeasurePhrases.milliliter.dimension)

Under the division theory, the copular sentence works: the MP denotes a quotient quantity whose numerator and denominator match the Fragment entries for "gram" (mass) and "milliliter" (volume) — precisely the components of the density dimension.

structure Phenomena.Quantification.BaleSchwarz2022.CopularDatum : Type

Copular density examples (exx. 46-49).

• surface : String
• usesPer : Bool

  Does the sentence use per (quantity-division vocabulary)?

• judgment : Core.Empirical.Acceptability

def Phenomena.Quantification.BaleSchwarz2022.instReprCopularDatum.repr : CopularDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instReprCopularDatum : Repr CopularDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprCopularDatum = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprCopularDatum.repr }

instance Phenomena.Quantification.BaleSchwarz2022.instBEqCopularDatum : BEq CopularDatum

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqCopularDatum = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqCopularDatum.beq }

def Phenomena.Quantification.BaleSchwarz2022.instBEqCopularDatum.beq : CopularDatum → CopularDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.BaleSchwarz2022.instBEqCopularDatum.beq x✝¹ x✝ = false

def Phenomena.Quantification.BaleSchwarz2022.ex46 : CopularDatum

(46) The sample's density is 0.9 grams per milliliter.

Equations

• Phenomena.Quantification.BaleSchwarz2022.ex46 = { surface := "The sample's density is 0.9 grams per milliliter", usesPer := true, judgment := Core.Empirical.Acceptability.ok }

def Phenomena.Quantification.BaleSchwarz2022.ex47 : CopularDatum

(47) #The sample's density is 0.9 grams. Without per, the MP denotes a WT quantity — dimension mismatch with density (WT/VOL) regardless of theory.

Equations

• Phenomena.Quantification.BaleSchwarz2022.ex47 = { surface := "The sample's density is 0.9 grams", usesPer := false, judgment := Core.Empirical.Acceptability.anomalous }

def Phenomena.Quantification.BaleSchwarz2022.ex48 : CopularDatum

(48) The sample's density is 0.9 grams for every cubic centimeter. For every paraphrase — expresses density WITHOUT quantity-division vocabulary. Challenges the assumption that copular density requires per.

Equations

• Phenomena.Quantification.BaleSchwarz2022.ex48 = { surface := "The sample's density is 0.9 grams for every cubic centimeter", usesPer := false, judgment := Core.Empirical.Acceptability.ok }

def Phenomena.Quantification.BaleSchwarz2022.ex49 : CopularDatum

(49) London's population density is 968 people for every km². Naturally occurring density expression without per.

Equations

• Phenomena.Quantification.BaleSchwarz2022.ex49 = { surface := "London's population density is 968 people for every km²", usesPer := false, judgment := Core.Empirical.Acceptability.ok }

def Phenomena.Quantification.BaleSchwarz2022.allCopularData : List CopularDatum

Equations

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

theorem Phenomena.Quantification.BaleSchwarz2022.copular_without_per : ex48.usesPer = false ∧ ex48.judgment = Core.Empirical.Acceptability.ok ∧ ex49.usesPer = false ∧ ex49.judgment = Core.Empirical.Acceptability.ok

Density copular sentences are felicitous with per (46) and with for every (48, 49), but not with bare measure phrases (47). The for every paraphrases show that density can be expressed without quantity-division vocabulary — undermining the division theory's advantage on copular data.

theorem Phenomena.Quantification.BaleSchwarz2022.copular_bare_mp_anomalous : ex47.usesPer = false ∧ ex47.judgment = Core.Empirical.Acceptability.anomalous

The only anomalous copular datum is the bare MP (47).

Dimension-tracking derivation for ex. (6) / eq. (20)

"The sample weighs 0.9 grams per milliliter"

Tree structure (eq. 20):

        S
       / \
   the    VP
  sample / \
      weighs  MP
             / \
          MP     PP
         / \   / \
       0.9 g pro  P'
                 / \
              per   mL

The paper's derivation uses dimensioned quantities throughout. The central insight of the anaphoric theory is that no quotient dimension is ever composed: per outputs a pure number (dimension ID), multiplication preserves the original dimension (WT), and weigh receives a WT quantity — dimensions match at every step.

We track dimensions explicitly via Quantity to verify this.

structure Phenomena.Quantification.BaleSchwarz2022.Quantity : Type

A dimensioned quantity: a rational value tagged with its dimension. This is the paper's notation "0.9g" = ⟨0.9, .mass⟩.

• value : ℚ
• dim : Semantics.Probabilistic.Measurement.Dimension

def Phenomena.Quantification.BaleSchwarz2022.instReprQuantity.repr : Quantity → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instReprQuantity : Repr Quantity

Equations

• Phenomena.Quantification.BaleSchwarz2022.instReprQuantity = { reprPrec := Phenomena.Quantification.BaleSchwarz2022.instReprQuantity.repr }

def Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity.beq : Quantity → Quantity → Bool

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity.beq { value := a, dim := a_1 } { value := b, dim := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity.beq x✝¹ x✝ = false

instance Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity : BEq Quantity

Equations

• Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity = { beq := Phenomena.Quantification.BaleSchwarz2022.instBEqQuantity.beq }

def Phenomena.Quantification.BaleSchwarz2022.instDecidableEqQuantity.decEq (x✝ x✝¹ : Quantity) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Quantification.BaleSchwarz2022.instDecidableEqQuantity : DecidableEq Quantity

Equations

• Phenomena.Quantification.BaleSchwarz2022.instDecidableEqQuantity = Phenomena.Quantification.BaleSchwarz2022.instDecidableEqQuantity.decEq

def Phenomena.Quantification.BaleSchwarz2022.unitQuantity (d : Semantics.Probabilistic.Measurement.Dimension) : Quantity

A unit quantity: 1 in a given dimension (e.g., g = ⟨1, .mass⟩).

Equations

• Phenomena.Quantification.BaleSchwarz2022.unitQuantity d = { value := 1, dim := d }

def Phenomena.Quantification.BaleSchwarz2022.numeralTimesUnit (n : ℚ) (unit : Quantity) : Quantity

Numeral × unit = quantity (e.g., 0.9 * g = 0.9g). The dimension comes from the unit.

Equations

• Phenomena.Quantification.BaleSchwarz2022.numeralTimesUnit n unit = { value := n * unit.value, dim := unit.dim }

def Phenomena.Quantification.BaleSchwarz2022.quantityTimesNumber (q : Quantity) (n : ℚ) : Quantity

Quantity × pure number = quantity, preserving dimension (eq. 18). This is the multiplication that combines "0.9 grams" with the pure number from the per-PP. The dimension is preserved — NO quotient dimension is formed.

Equations

• Phenomena.Quantification.BaleSchwarz2022.quantityTimesNumber q n = { value := q.value * n, dim := q.dim }

def Phenomena.Quantification.BaleSchwarz2022.step_perMilliliter {E : Type u_1} (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (mL : Quantity) : E → ℚ

⟦per milliliter⟧ = λx. μ_VOL(x) / mL (eq. 15). Instance of eq. (16): ⟦per⟧ = λq. λx. μ_{dim(q)}(x) / q. Output type: E → ℚ (entity to pure number).

Equations

• Phenomena.Quantification.BaleSchwarz2022.step_perMilliliter μ_vol mL x = μ_vol.apply x / mL.value

def Phenomena.Quantification.BaleSchwarz2022.step_PP {E : Type u_1} (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (mL : Quantity) (pro : E) : ℚ

⟦[PP pro [per milliliter]]⟧ = μ_VOL(pro) / mL (FA). pro is resolved to the subject. Result: a pure number.

Equations

• Phenomena.Quantification.BaleSchwarz2022.step_PP μ_vol mL pro = Phenomena.Quantification.BaleSchwarz2022.step_perMilliliter μ_vol mL pro

def Phenomena.Quantification.BaleSchwarz2022.step_innerMP (numeral : ℚ) (unit : Quantity) : Quantity

⟦[MP 0.9 grams]⟧ = 0.9 * g = 0.9g. A quantity in dimension WT (mass).

Equations

• Phenomena.Quantification.BaleSchwarz2022.step_innerMP numeral unit = Phenomena.Quantification.BaleSchwarz2022.numeralTimesUnit numeral unit

def Phenomena.Quantification.BaleSchwarz2022.step_fullMP {E : Type u_1} (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (pro : E) (numeral : ℚ) (unit mL : Quantity) : Quantity

⟦[MP [MP 0.9 grams] [PP pro per mL]]⟧ = 0.9g * (μ_VOL(pro)/mL) (eq. 18). Quantity × pure number → quantity in dimension WT (eq. 19). The dimension is STILL .mass — no quotient dimension arises.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.step_weighs {E : Type u_1} (μ_wt : Semantics.Probabilistic.Measurement.MeasureFn E) (q : Quantity) (x : E) : Bool

⟦weighs⟧ = λq. λx. μ_WT(x) = q (eq. 5). Takes a quantity and returns a predicate. The verb's measure function must match the quantity's dimension.

Equations

• Phenomena.Quantification.BaleSchwarz2022.step_weighs μ_wt q x = decide (μ_wt.apply x = q.value)

def Phenomena.Quantification.BaleSchwarz2022.step_sentence {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) (numeral : ℚ) (unit mL : Quantity) : Bool

⟦[S [the sample] [VP weighs [MP]]]⟧ — the full sentence (eq. 22). Applies the VP to the subject entity.

Equations

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

def Phenomena.Quantification.BaleSchwarz2022.gram_unit : Quantity

The gram unit quantity.

Equations

• Phenomena.Quantification.BaleSchwarz2022.gram_unit = Phenomena.Quantification.BaleSchwarz2022.unitQuantity Semantics.Probabilistic.Measurement.Dimension.mass

def Phenomena.Quantification.BaleSchwarz2022.mL_unit : Quantity

The milliliter unit quantity.

Equations

• Phenomena.Quantification.BaleSchwarz2022.mL_unit = Phenomena.Quantification.BaleSchwarz2022.unitQuantity Semantics.Probabilistic.Measurement.Dimension.volume

theorem Phenomena.Quantification.BaleSchwarz2022.innerMP_dimension : (step_innerMP (9 / 10) gram_unit).dim = Semantics.Probabilistic.Measurement.Dimension.mass

The inner MP "0.9 grams" is in dimension WT (mass).

theorem Phenomena.Quantification.BaleSchwarz2022.fullMP_dimension {E : Type u_1} (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (pro : E) : (step_fullMP μ_vol pro (9 / 10) gram_unit mL_unit).dim = Semantics.Probabilistic.Measurement.Dimension.mass

The full MP "0.9 grams per milliliter" is STILL in dimension WT. This is the paper's key claim: the anaphoric theory never forms a quotient dimension. The per-PP contributes a dimensionless scalar, and multiplication preserves the original dimension.

theorem Phenomena.Quantification.BaleSchwarz2022.dimensions_match {E : Type u_1} (μ_wt : Semantics.Probabilistic.Measurement.MeasureFn E) (hwt : μ_wt.dimension = Semantics.Probabilistic.Measurement.Dimension.mass) (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (pro : E) : μ_wt.dimension = (step_fullMP μ_vol pro (9 / 10) gram_unit mL_unit).dim

weigh's measure function is in dimension WT. When the composed quantity is also in WT, dimensions match — no type error.

theorem Phenomena.Quantification.BaleSchwarz2022.division_theory_mismatch : Semantics.Probabilistic.Measurement.QuotientDimension.density.components.1 = Semantics.Probabilistic.Measurement.Dimension.mass ∧ Semantics.Probabilistic.Measurement.QuotientDimension.density.components ≠ (Semantics.Probabilistic.Measurement.Dimension.mass, Semantics.Probabilistic.Measurement.Dimension.mass)

Under the division theory, the MP would be in WT/VOL — a quotient dimension. The verb's WT dimension would NOT match.

theorem Phenomena.Quantification.BaleSchwarz2022.derivation_eq22 {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) : step_sentence μ_wt μ_vol sample (9 / 10) gram_unit mL_unit = decide (μ_wt.apply sample = 9 / 10 * 1 * (μ_vol.apply sample / 1))

The derivation yields eq. (22): μ_WT(sample) = (0.9 * μ_VOL(sample)/mL) g. The numerical content is: μ_WT(sample) = 0.9 * 1 * (μ_VOL(sample) / 1), which simplifies to μ_WT(sample) = 0.9 * μ_VOL(sample).

theorem Phenomena.Quantification.BaleSchwarz2022.derivation_matches_tc {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) (numeral : ℚ) : step_sentence μ_wt μ_vol sample numeral gram_unit mL_unit = true ↔ anaphoricTC μ_wt μ_vol sample numeral 1

The derivation matches anaphoricTC (modulo unit normalization).

theorem Phenomena.Quantification.BaleSchwarz2022.concrete_derivation : step_sentence Phenomena.Quantification.BaleSchwarz2022.μ_wt_concrete✝ Phenomena.Quantification.BaleSchwarz2022.μ_vol_concrete✝ () (9 / 10) gram_unit mL_unit = true

A sample with μ_WT = 9g, μ_VOL = 10mL: "weighs 0.9 grams per milliliter" is TRUE. 9 = 0.9 * 1 * (10 / 1) = 9 ✓

def Phenomena.Quantification.BaleSchwarz2022.liter_unit : Quantity

The same sample does NOT weigh "0.9 grams per liter". A liter = 1000mL, so liter_unit has value 1000. 9 ≠ 0.9 * 1 * (10 / 1000) = 0.009

Equations

• Phenomena.Quantification.BaleSchwarz2022.liter_unit = { value := 1000, dim := Semantics.Probabilistic.Measurement.Dimension.volume }

theorem Phenomena.Quantification.BaleSchwarz2022.concrete_per_liter : step_sentence Phenomena.Quantification.BaleSchwarz2022.μ_wt_concrete✝ Phenomena.Quantification.BaleSchwarz2022.μ_vol_concrete✝ () (9 / 10) gram_unit liter_unit = false

The anaphoric theory derives pseudo-partitive truth conditions via the same mechanism. For (27) "The mixture contains 0.1 grams per milliliter of salt":

Parse (eq. 41): [the mixt.] contains [DP ∃ [AP [MP 0.1 grams] [PP pro [per milliliter]]] MUCH] of salt]

1. ⟦[MP 0.1 grams] [PP pro per mL]⟧ = (0.1 * μ_VOL(mixture)/mL) g (eq. 42)
2. ⟦MUCH⟧(⟦fullMP⟧)(x) = μ_WT(x) = (0.1 * μ_VOL(mixture)/mL) g (eq. 25)
3. ⟦sentence⟧ = ∃x[salt(x) ∧ μ_WT(x) = (0.1 * μ_VOL(mixture)/mL) g ∧ contain(mixture, x)] (eq. 32)

The MP denotation (step 1) is identical to the measurement verb case — step_fullMP produces the same dimensioned quantity. The only difference is that MUCH applies this quantity as a predicate, rather than weigh.

def Phenomena.Quantification.BaleSchwarz2022.step_MUCH {E : Type u_1} (μ : Semantics.Probabilistic.Measurement.MeasureFn E) (q : Quantity) (x : E) : Bool

MUCH applied to the composed quantity (eq. 25 + eq. 42). ⟦MUCH⟧(q)(x) = (μ(x) = q.value), where μ is contextually resolved to μ_WT for "grams of salt".

Equations

• Phenomena.Quantification.BaleSchwarz2022.step_MUCH μ q x = decide (μ.apply x = q.value)

def Phenomena.Quantification.BaleSchwarz2022.step_pseudoPartitive {E : Type u_1} (salt : E → Bool) (contain : E → E → Bool) (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (mixture : E) (numeral : ℚ) (unit mL : Quantity) (domain : List E) : Bool

Pseudo-partitive truth conditions (eq. 32): ∃x[salt(x) ∧ μ_WT(x) = (0.1 * μ_VOL(mixture)/mL) g ∧ contain(mixture, x)].

We represent the existential as a check over a domain list, matching the paper's eq. (26).

Equations

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

theorem Phenomena.Quantification.BaleSchwarz2022.pseudoPartitive_same_dimension {E : Type u_1} (μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (mixture : E) : (step_fullMP μ_vol mixture (1 / 10) gram_unit mL_unit).dim = (step_fullMP μ_vol mixture (9 / 10) gram_unit mL_unit).dim

The pseudo-partitive MP has the same dimension as the measurement verb MP — mass in both cases. This confirms that the anaphoric theory uses the same derivation mechanism for both environments.

theorem Phenomena.Quantification.BaleSchwarz2022.pseudoPartitive_eq32 {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (mixture x : E) : step_MUCH μ_wt (step_fullMP μ_vol mixture (1 / 10) gram_unit mL_unit) x = decide (μ_wt.apply x = 1 / 10 * 1 * (μ_vol.apply mixture / 1))

Pseudo-partitive truth conditions (eq. 32). MUCH equates μ_WT(x) with the composed quantity, where x is the salt entity and mixture is the container (pro's referent). These are DIFFERENT entities — unlike the measurement verb case where the same entity is both subject and pro's referent.

theorem Phenomena.Quantification.BaleSchwarz2022.pseudoPartitive_specializes_to_measureVerb {E : Type u_1} (μ_wt μ_vol : Semantics.Probabilistic.Measurement.MeasureFn E) (sample : E) (numeral : ℚ) : step_MUCH μ_wt (step_fullMP μ_vol sample numeral gram_unit mL_unit) sample = true ↔ anaphoricTC μ_wt μ_vol sample numeral 1

In the measurement verb case, pro = subject, so the pseudo-partitive machinery specializes to anaphoricTC when we set mixture = x.

Connection to the 2026 L&P paper

The measurement verb examples formalized here (ex. 6: "The sample weighs 0.9 grams per milliliter") are simplex-dimension uses of per with compositional interpretation — exactly the class that Phenomena.Quantification.BaleSchwarz2026.PerPhraseExample classifies as dimType := .simplex and source := .compositional.

The 2026 paper extends the anaphoric theory with:

• The No Division Hypothesis (compositional semantics uses × and +, not ÷)
• The math-speak analysis for quotient-dimension per-phrases
• Substitution and sub-extraction diagnostics

The unit sensitivity presupposition (eq. 43) originates in this 2022 paper and is carried forward into the 2026 analysis.