@cite{tham-2025}

Shiao Wei Tham (2025). Multidimensionality and the scalar components of physical disturbance predicates. Glossa: a journal of general linguistics 10(1): 1–30.

Key claims

Physical disturbance predicates (crack/cracked, dent/dented, scratch/scratched) — Tham's "host irregularities" in the sense of @cite{karmo-1977} — are associated with a totally closed, multi-point scale. Four substantive claims:

1. Contra @cite{rappaport-hovav-2014}: crack/cracked is NOT two-point (like die/dead). The verb allows durative for adverbials and the adjective accepts comparatives (more cracked).
2. Contra @cite{rotstein-winter-2004}: cracked is NOT a "partial" adjective with a lower-bounded, upper-open scale. It accepts completely (upper bound) and partially (lower bound).
3. Multidimensional in the sense of @cite{sassoon-2013}: dimensions are quantity of disturbances, quality (depth, length), and spatial positioning (centrality, array, functional impact).
4. Lower bound = physical instantiation (objective: no faultless disagreement under simple predication, §3.2.1). Upper bound = spatial extent of host (structural integrity limit).

The verb-adjective asymmetry: the adjective allows quantificational access to individual dimensions via respect PPs and operators; the verb allows only conceptual access (§4.2).

File organization

• §1 Schema for disturbance predicates + 3 attested data points
• §2 Contrast predicates (die/dead, shatter/shattered, damage/damaged)
• §3 Total closure (completely + partially)
• §4 Variable telicity + result-state entailment
• §5 Objective simple predication, subjective degree modification (§3.2)
• §6 Deverbal adjectives don't entail a preceding change of state (§5.1)
• §7 Multidimensionality + verb-adjective asymmetry (§3.1, §4.2)
• §8 Substrate readouts: Fragment scale-types match Tham's classification
• §9 Cross-paper engagement: Kennedy-Levin pipeline (variable telicity gap)
• §10 Cross-paper engagement: Hay-Kennedy-Levin matrix refutation
• §11 Cross-paper engagement: Kennedy 2007 licensing convergence
• §12 Cross-paper engagement: Sassoon 2013 binding insufficiency (real refutation against MultidimAdj apparatus)
• §13 Tham eq. 47b: spatially-normalized weighted measure (vase example
  • bounded-by-one via substrate's spatialNormalizedScore_le_one)
• §14 Cross-paper engagement: Beavers & Koontz-Garboden 2020 root eventivity (Tham §5.1 refutes strict root → deverbal-adjective result-state inheritance, against B&KG's crack : Root := ⟨"crack", [.becomesState "fissured", .hasCause]⟩)
• §15 Cross-paper engagement: Waldon et al. 2023 normalization contrast (substrate-level: shared numerator, divergent denominator)
• §16 Cross-paper engagement: Solt 2018 SuB reciprocal bridge (substrate's _le_one consumed by both files at different specializations)
• §17 Cross-paper engagement: Kennedy 2007 Interpretive Economy vs Tham §3.2.1 lower bound — wedge made Lean-checkable
• §18 Cross-paper engagement: Solt 2018 multidim typology — cracked belongs to the AbsPart class (partially-closed, physical-property, intermediate ordering subjectivity)

Attestation policy

Tham's primary case study is cracked. dented and scratched are included in most data points (e.g., ex. 11a/11b for more dented/scratched, 18a/18b/18c for badly scratched/dented/cracked, 36a/36b/36c for completely dented/cracked/scratched). A few fields are stipulated by class-level extension where Tham only attests cracked directly; these are flagged in comments as "extends crack" rather than dropped, since the paper's argument is that disturbance predicates are a uniform class.

inductive Tham2025.DisturbanceDimension : Type

The three dimensions Tham identifies for disturbance predicates (§3.1, §3.4): quantity of disturbances (number), quality (severity — depth, length), and positioning (centrality, array, functional impact). Used to encode dimension-selection facts about individual modifiers (e.g. much selects only quantity per §3.3).

• quantity : DisturbanceDimension

  Number of disturbances (Tham §3.1, ex. 23a/24a/25a).

• quality : DisturbanceDimension

  Severity: depth, length, width (Tham §3.1, ex. 23b/24b/25b).

• positioning : DisturbanceDimension

  Centrality, array, functional impact (Tham §3.4, ex. 29).

@[implicit_reducible]

instance Tham2025.instReprDisturbanceDimension : Repr DisturbanceDimension

Equations

• Tham2025.instReprDisturbanceDimension = { reprPrec := Tham2025.instReprDisturbanceDimension.repr }

def Tham2025.instReprDisturbanceDimension.repr : DisturbanceDimension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tham2025.instBEqDisturbanceDimension : BEq DisturbanceDimension

Equations

• Tham2025.instBEqDisturbanceDimension = { beq := Tham2025.instBEqDisturbanceDimension.beq }

def Tham2025.instBEqDisturbanceDimension.beq : DisturbanceDimension → DisturbanceDimension → Bool

Equations

• Tham2025.instBEqDisturbanceDimension.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Tham2025.instDecidableEqDisturbanceDimension : DecidableEq DisturbanceDimension

Equations

• Tham2025.instDecidableEqDisturbanceDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Tham2025.DisturbancePredicate : Type

A physical disturbance predicate entry, encoding the scalar and distributional properties argued for in Tham (2025).

The schema separates adverb compatibility (closure tests) from subjectivity profile (objective lower bound vs subjective degree modification, §3.2) and change-of-state status (whether the deverbal adjective entails a preceding event of change, §5.1).

• root : String

  Root form (shared by verb, adjective, and count noun).

• hasCountNoun : Bool

  Whether the root has a count noun form (a crack, a dent). Distinguishes disturbance predicates from other CoS predicates like shatter (no *a shatter) and damage (mass only).

• adjGradable : Bool

  Whether the deverbal adjective is gradable (more cracked).

• adjCompletely : Bool

  Compatible with completely (tests upper closure).

• adjPartially : Bool

  Compatible with partially (tests lower closure).

• adjSlightly : Bool

  Compatible with slightly (indicates lower bound).

• adjBadly : Bool

  Compatible with badly/well (degree modifier for closed scales).

• adjMuchSelects : List DisturbanceDimension

  Which dimensions much selects when modifying the deverbal adjective. Tham §3.3 (p. 16) argues much "evoke[s] only the 'quantity' dimension" — selectivity, not mere compatibility. The empty list encodes much-incompatibility; [.quantity] encodes Tham's single-dimension claim.

• verbForX : Bool

  Whether the verb allows durative for X adverbials (atelic reading).

• verbInX : Bool

  Whether the verb allows in X adverbials (telic reading).

• verbCompletely : Bool

  Whether the verb is compatible with completely.

• verbBadly : Bool

  Whether the verb is compatible with badly.

• adjRespectPP : Bool

  Whether the adjective allows respect PPs (dented with respect to dent size).

• verbRespectPP : Bool

  Whether the verb allows respect PPs (degraded for intransitive disturbance CoS verbs, but accepted for causative uses).

• verbInXEntailsResult : Bool

  Whether verb + in X entails the result state (cracked in a minute ⊨ is cracked, Tham (17a)).

• simplePredicationObjective : Bool

  Tham §3.2.1: simple predication is OBJECTIVE — no faultless disagreement (ex. 26: "My watch face is scratched / No, it's smooth" — one speaker must be mistaken).

• degreeModifiedSubjective : Bool

  Tham §3.2.2: degree-modified predication is SUBJECTIVE — faultless disagreement is possible (ex. 27: "badly scratched / not badly scratched at all, the scratch is long but not deep").

• adjEntailsPrecedingChange : Bool

  Tham §5.1: the deverbal adjective does NOT entail a preceding event of change. (ex. 45a–c: pumpkin skin texture, computer- modelled dented helmet, scratched-look decal — all describe surfaces that have not undergone a CoS event.)

@[implicit_reducible]

instance Tham2025.instReprDisturbancePredicate : Repr DisturbancePredicate

Equations

• Tham2025.instReprDisturbancePredicate = { reprPrec := Tham2025.instReprDisturbancePredicate.repr }

def Tham2025.instReprDisturbancePredicate.repr : DisturbancePredicate → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tham2025.instBEqDisturbancePredicate : BEq DisturbancePredicate

Equations

• Tham2025.instBEqDisturbancePredicate = { beq := Tham2025.instBEqDisturbancePredicate.beq }

def Tham2025.instBEqDisturbancePredicate.beq : DisturbancePredicate → DisturbancePredicate → Bool

Equations

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

def Tham2025.crack : DisturbancePredicate

Equations

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

def Tham2025.dent : DisturbancePredicate

Equations

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

def Tham2025.scratch : DisturbancePredicate

Equations

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

def Tham2025.allDisturbancePredicates : List DisturbancePredicate

Equations

• Tham2025.allDisturbancePredicates = [Tham2025.crack, Tham2025.dent, Tham2025.scratch]

structure Tham2025.ContrastPredicate : Type

Data for predicates that contrast with disturbance predicates, demonstrating that the disturbance pattern is class-specific.

• root : String
• hasCountNoun : Bool
• adjGradable : Bool
• verbDurative : Bool

def Tham2025.instReprContrastPredicate.repr : ContrastPredicate → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tham2025.instReprContrastPredicate : Repr ContrastPredicate

Equations

• Tham2025.instReprContrastPredicate = { reprPrec := Tham2025.instReprContrastPredicate.repr }

@[implicit_reducible]

instance Tham2025.instBEqContrastPredicate : BEq ContrastPredicate

Equations

• Tham2025.instBEqContrastPredicate = { beq := Tham2025.instBEqContrastPredicate.beq }

def Tham2025.instBEqContrastPredicate.beq : ContrastPredicate → ContrastPredicate → Bool

Equations

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

def Tham2025.dieDead : ContrastPredicate

die/dead: two-point scale, non-gradable (#more dead), punctual. Tham §2.3: crack ≠ die despite both being Levin 45.1. Tham's Table 1 (= @cite{rappaport-hovav-2014} Table 1) groups both as "Two-valued" — Tham contests this for crack.

Equations

• Tham2025.dieDead = { root := "die", hasCountNoun := false, adjGradable := false, verbDurative := false }

def Tham2025.shatterShattered : ContrastPredicate

shatter/shattered: punctual, non-gradable. Like die/dead: describes physical objects but NOT a disturbance predicate. Crucial for showing that gradability of disturbance predicates is NOT simply a consequence of applying to physical objects.

Equations

• Tham2025.shatterShattered = { root := "shatter", hasCountNoun := false, adjGradable := false, verbDurative := false }

def Tham2025.damageDamaged : ContrastPredicate

damage/damaged: has mass noun (damage to X) but NOT count noun (*a damage in X). Not a disturbance predicate per Tham (4).

Equations

• Tham2025.damageDamaged = { root := "damage", hasCountNoun := false, adjGradable := true, verbDurative := true }

theorem Tham2025.all_disturbance_totally_closed : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.adjCompletely && p.adjPartially) = true

All disturbance predicates accept both completely (upper bound) and partially (lower bound), demonstrating total closure.

theorem Tham2025.all_disturbance_gradable : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.adjGradable) = true

All disturbance predicates are gradable (contra two-point classification in @cite{rappaport-hovav-2014} Table 1).

theorem Tham2025.all_disturbance_have_count_noun : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.hasCountNoun) = true

All disturbance predicates have a count noun form, distinguishing them from other CoS predicates (§2.1, ex. 3–5).

theorem Tham2025.die_not_gradable : dieDead.adjGradable = false

Contrast: non-disturbance predicates are NOT gradable.

theorem Tham2025.shatter_not_gradable : shatterShattered.adjGradable = false

theorem Tham2025.die_not_durative : dieDead.verbDurative = false

Contrast: non-disturbance verbs lack durative readings.

theorem Tham2025.shatter_not_durative : shatterShattered.verbDurative = false

Tham §2.4 (10), (14): physical disturbance verbs allow BOTH telic (cracked in a minute, ex. 14a) and atelic (cracked for a while, ex. 14b) readings. They differ from canonical degree achievements like cool in that BOTH readings entail the result state (Tham (17a): cracked completely/slightly ⊨ is cracked; contrast Tham (13b) "soup cooled for ten minutes" ⊭ "is cool"). The class-level claim "disturbance verbs always entail their result state" is asserted at Tham §2.4.

theorem Tham2025.crack_allows_both_aspects : crack.verbInX = true ∧ crack.verbForX = true

Physical disturbance verbs allow BOTH telic and atelic readings, unlike standard degree achievements which have only one.

theorem Tham2025.disturbance_always_entails_result : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.verbInXEntailsResult) = true

All disturbance verbs entail their result state under both in X and for X readings.

Tham §3.2 — the central evidence for the lower bound = physical instantiation claim. Two minimally-different exchanges:

(26)  My watch face is scratched. / No, it's smooth.       ← objective
(27)  My watch face is badly scratched. / No, it's not badly scratched
      at all, the scratch is long but not deep.            ← subjective

In (26) one speaker must be mistaken — disagreement is NOT faultless.
In (27) the disagreement IS faultless (about *degree* of damage). The
asymmetry follows from the lower bound being "physically bounded"
(Tham p. 14): "Whether a physical disturbance does exist on a host
entity, however, seems to be a matter of objective observation. This
is presumably because the state they describe has a minimum
instantiation that is physically bounded." 

theorem Tham2025.all_disturbance_simple_predication_objective : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.simplePredicationObjective) = true

All disturbance predicates: simple predication is objective.

theorem Tham2025.all_disturbance_degree_modified_subjective : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.degreeModifiedSubjective) = true

All disturbance predicates: degree-modified predication is subjective.

theorem Tham2025.tham_objective_subjective_wedge : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.simplePredicationObjective && p.degreeModifiedSubjective) = true

The Tham §3.2 wedge: simple predication is objective but degree-modified predication is subjective. This is the central asymmetry from which the lower bound = physical instantiation / upper bound = host extent split is derived.

Tham §5.1 — the second-most-load-bearing claim after multi- dimensionality. Tham (p. 23) writes that deverbal disturbance adjectives "do not necessarily express the resultant state of an event of change" (emphasis added). The (45) examples are EXISTENCE PROOFS of uses without a preceding CoS event:

(45)  a. The white pumpkin had a completely **cracked surface**.
          (= textured pumpkin skin; no cracking event)
      b. My computer model has a **dented surface**.
          (= visual modeling effect; no denting event)
      c. **Scratched Surface** vinyl decal for Google Pixel.
          (= graphical pattern; no scratching event)

The Bool field `adjEntailsPrecedingChange = false` encodes the
existential possibility — at least some uses of the deverbal
adjective lack the entailment. The class-level claim is NOT a
universal "always lacks" but the existential "does not necessarily
express." Compare related discussion of *bend/bent* and
*darken/darkened* in @cite{gawron-2009} and @cite{koontz-garboden-2011}. 

theorem Tham2025.all_disturbance_adj_can_lack_preceding_change : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => !p.adjEntailsPrecedingChange) = true

All disturbance adjectives have at least one well-attested use where the deverbal adjective does NOT entail a preceding CoS event (Tham §5.1 ex. 45a/b/c). The theorem name reflects the existential nature of Tham's claim — it does not assert "no use ever entails preceding change," only that the entailment is cancellable.

Disturbance adjectives have three dimensions (§3.1): - Quantity: number of disturbances (23a, 24a, 25a) - Quality: severity — depth, length, width (23b, 24b, 25b) - Positioning: centrality, array pattern, functional impact (29)

The adjective allows **quantificational** access to individual
dimensions via *respect* PPs and quantificational operators (*every
respect*, *at least with respect to*); the verb allows only
**conceptual** access (§4.2). This aligns with @cite{ruiz-faroldi-2022}'s
quantificational/conceptual typology of multidimensionality. 

theorem Tham2025.adj_access_quantificational : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.adjRespectPP) = true

Adjective: quantificational access (respect PPs accepted).

theorem Tham2025.verb_access_conceptual : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => !p.verbRespectPP) = true

Verb: conceptual access only (respect PPs degraded).

theorem Tham2025.much_selects_quantity_only : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => p.adjMuchSelects == [DisturbanceDimension.quantity]) = true

much selects ONLY the quantity dimension (Tham §3.3, p. 16: much "evoke[s] only the 'quantity' dimension"). This is a selectivity claim, not just compatibility — a much cracked dish means many cracks, not one deep crack.

theorem Tham2025.all_disturbance_compatible_with_much : (allDisturbancePredicates.all fun (p : DisturbancePredicate) => !p.adjMuchSelects.isEmpty) = true

Compatibility of much (Tham §3.3 ex. 30): all three predicates accept much-modification. The substantive claim is the selectivity in much_selects_quantity_only above; this is the weaker compatibility check.

Verify that the Fragment adjective entries classify disturbance adjectives with the correct Boundedness value. These are consumption sites for the substrate, not bridges — closedAdj_licensed and LicensingPipeline.isLicensed are foundational and are called inline.

theorem Tham2025.cracked_is_closed : Fragments.English.Predicates.Adjectival.cracked.scaleType = Core.Scale.Boundedness.closed

theorem Tham2025.dented_is_closed : Fragments.English.Predicates.Adjectival.dented.scaleType = Core.Scale.Boundedness.closed

theorem Tham2025.scratched_is_closed : Fragments.English.Predicates.Adjectival.scratched.scaleType = Core.Scale.Boundedness.closed

theorem Tham2025.dead_also_closed : Fragments.English.Predicates.Adjectival.dead.scaleType = Core.Scale.Boundedness.closed

dead also has .closed — but is non-gradable (two-point). Same Boundedness, different gradability. Boundedness alone does not distinguish two-point from multi-point closed scales.

theorem Tham2025.crack_verb_closed_scale : Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get!.scaleBoundedness = Core.Scale.Boundedness.closed

Verb fragment entries have closed degreeAchievementScale.

theorem Tham2025.dent_verb_closed_scale : Fragments.English.Predicates.Verbal.dent.degreeAchievementScale.get!.scaleBoundedness = Core.Scale.Boundedness.closed

theorem Tham2025.scratch_verb_closed_scale : Fragments.English.Predicates.Verbal.scratch.degreeAchievementScale.get!.scaleBoundedness = Core.Scale.Boundedness.closed

theorem Tham2025.crack_adj_verb_scale_agree : Fragments.English.Predicates.Adjectival.cracked.scaleType = Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get!.scaleBoundedness

Adjective-verb scale agreement: each verb inherits the same Boundedness as its deverbal adjective.

theorem Tham2025.dent_adj_verb_scale_agree : Fragments.English.Predicates.Adjectival.dented.scaleType = Fragments.English.Predicates.Verbal.dent.degreeAchievementScale.get!.scaleBoundedness

theorem Tham2025.scratch_adj_verb_scale_agree : Fragments.English.Predicates.Adjectival.scratched.scaleType = Fragments.English.Predicates.Verbal.scratch.degreeAchievementScale.get!.scaleBoundedness

theorem Tham2025.cracked_licensed {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Gradability.adjMeasure μ Fragments.English.Predicates.Adjectival.cracked).licensed = true

Disturbance adjectives are licensed for degree modification by the Kennedy pipeline, just like full and clean.

theorem Tham2025.cracked_pipeline_licensed : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.cracked.scaleType = true

Interpretive Economy predicts a max-endpoint standard for disturbance adjectives (closed → maxEndpoint). This interacts non-trivially with Tham's analysis: simple predication (is cracked) requires only the minimum physical instantiation (lower bound, §3.2.1), but Interpretive Economy selects the maximum as the positive standard. The resolution is that the positive standard determines the degree needed for the positive form to apply, while the lower bound determines the threshold for being on the scale at all.

theorem Tham2025.cracked_standard_maxEndpoint : Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.cracked.scaleType = Semantics.Degree.PositiveStandard.maxEndpoint

@cite{kennedy-levin-2008}'s pipeline maps closed scales to telic (accomplishment) interpretations. Tham §2.4 shows that disturbance verbs allow BOTH telic and atelic readings — variable telicity in a single closed-scale verb. Tham does not commit to "achievement" vs "accomplishment" as the lexical Vendler class; she observes that crack is "consistent with" being punctual (Tham p. 8 on ex. 9 "the mirror will crack in five minutes") while ALSO admitting durative readings.

Inside linglib, the Fragment makes a stipulation: `Verbal.crack`
receives `vendlerClass = some .achievement`. The `defaultVendlerClass`
derived from the closed scale via the Kennedy-Levin pipeline is
`.accomplishment`. This divergence is a Lean-internal artifact of
the Fragment's choice, not Tham's claim — but it makes the variable-
telicity gap Lean-checkable. 

theorem Tham2025.crack_pipeline_predicts_accomplishment : Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get!.defaultVendlerClass = Features.VendlerClass.accomplishment

The pipeline predicts accomplishment for crack (closed → telic → durative).

theorem Tham2025.crack_stipulated_achievement : Fragments.English.Predicates.Verbal.crack.vendlerClass = some Features.VendlerClass.achievement

The Fragment stipulates achievement (punctual telic), capturing the in X = "after" reading (Tham (9) "The mirror will crack in five minutes").

theorem Tham2025.crack_pipeline_vendler_diverges : Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get!.defaultVendlerClass ≠ Fragments.English.Predicates.Verbal.crack.vendlerClass.get!

Pipeline and Fragment stipulation diverge for crack. The divergence is internal to linglib (Fragment vs pipeline default), not a claim Tham herself makes — see the docstring above.

theorem Tham2025.break_fits_pipeline : Fragments.English.Predicates.Verbal.break_.vendlerClass = some Features.VendlerClass.accomplishment

break (also Levin 45.1) IS an accomplishment — the standard pipeline works for it. So the Fragment-level divergence is specific to disturbance predicates within the same Levin class.

theorem Tham2025.crack_break_same_levin_different_vendler : Fragments.English.Predicates.Verbal.crack.levinClass = Fragments.English.Predicates.Verbal.break_.levinClass ∧ Fragments.English.Predicates.Verbal.crack.vendlerClass ≠ Fragments.English.Predicates.Verbal.break_.vendlerClass

crack and break share LevinClass but differ in VendlerClass. Both are Levin 45.1 Break verbs, but crack is achievement (punctual + optional durative extension) while break is accomplishment (durative). This within-class split is exactly what Tham's analysis predicts: disturbance predicates have distinctive aspectual behavior.

theorem Tham2025.shatter_also_achievement : Fragments.English.Predicates.Verbal.shatter.vendlerClass = some Features.VendlerClass.achievement

shatter is also achievement — but unlike crack, shatter ONLY has the punctual reading. Same Vendler class, different aspectual flexibility. VendlerClass is too coarse for disturbance predicates.

theorem Tham2025.crack_boundedness_converges_despite_vendler_divergence : Core.Scale.LicensingPipeline.toBoundedness Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get! = Core.Scale.LicensingPipeline.toBoundedness Fragments.English.Predicates.Verbal.crack.vendlerClass.get!

Boundedness convergence: both pipelines agree crack is .closed. Achievement and accomplishment are both telic → .closed, so the disturbance-specific VendlerClass divergence is invisible at the Boundedness granularity. The Kennedy-Levin pipeline is correct about scale closure but wrong about what that closure implies for aspectual class.

Contrast with Phenomena/TenseAspect/Studies/KennedyLevin2008.lean, which proves convergence for 12 standard DAs — there, convergence at Boundedness ALSO means convergence at VendlerClass. For crack, only Boundedness converges.

@cite{hay-kennedy-levin-1999}'s central thesis (HKL §3.2): closed- range adjectives → telic DA verbs; open-range adjectives → atelic. The substrate sibling Phenomena/TenseAspect/Studies/HayKennedyLevin1999.lean proves this holds for straighten (closed → accomplishment) and lengthen, widen, cool, warm (open → activity).

Tham §2.4 shows the *strict* version of this matrix fails for
disturbance verbs. *crack* has a closed scale (HKL would predict
"telic only") but ALSO admits atelic readings (Tham (10a) "ice will
crack for two days", (14b) "cracked for a while"). HKL's matrix is
correct as a default but does not capture the variable-telicity
behavior of disturbance verbs. 

theorem Tham2025.crack_refutes_strict_hkl_matrix : Fragments.English.Predicates.Verbal.crack.degreeAchievementScale.get!.scaleBoundedness = Core.Scale.Boundedness.closed ∧ crack.verbInX = true ∧ crack.verbForX = true

crack refutes the strict HKL matrix: closed scale, but BOTH telic and atelic readings attested.

@cite{kennedy-2007}'s closedAdj_licensed substrate (consumed in Phenomena/Gradability/Studies/Kennedy2007Licensing.lean for full, wet, dry, straight) extends to disturbance adjectives without modification. The convergence at Boundedness is the partner of the §9 divergence at VendlerClass: same substrate, different granularity, different verdict.

theorem Tham2025.cracked_licensing_converges_with_kennedy2007 {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Semantics.Gradability.adjMeasure μ Fragments.English.Predicates.Adjectival.cracked).licensed = (Semantics.Gradability.adjMeasure μ Fragments.English.Predicates.Adjectival.full).licensed

cracked shares licensing status with full (Kennedy 2007's canonical totally-closed adjective). The convergence is at the Boundedness level — both are .closed, hence both license degree modification.

theorem Tham2025.all_disturbance_pipeline_licensed : Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.cracked.scaleType = true ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.dented.scaleType = true ∧ Core.Scale.LicensingPipeline.isLicensed Fragments.English.Predicates.Adjectival.scratched.scaleType = true

All three disturbance adjectives converge with Kennedy 2007 at Boundedness.

Honesty caveat. Tham herself does not engage @cite{sassoon-2013}'s binding-type typology directly. She cites Sassoon for the fact of multidimensionality and respect-PP diagnostics (Tham pp. 13, 24), and adopts Solt's representation (@cite{solt-2018}) rather than Sassoon's. The argument below is the formaliser's reconstruction of what Tham's data WOULD force on Sassoon's apparatus — a cross-paper engagement constructed in linglib, not drawn out by Tham.

@cite{sassoon-2013}'s typology of multidimensional adjectives
assigns each adjective a single `DimensionBindingType` —
`.conjunctive` (*healthy* — all dimensions), `.disjunctive` (*sick*
— some dimension), or `.mixed` (*intelligent* — context-dependent).
That apparatus is in
`Phenomena/Gradability/Studies/Sassoon2013.lean` (`MultidimAdj`).

Tham §3.2.1 + §3 (ex. 20a), TAKEN TOGETHER, yield a tension under
Sassoon's framework: in the SAME context (one host entity with one
high dimension), the lexical entry *cracked* must support both
- "is cracked" → TRUE (lower-bound = any physical instantiation);
- "completely cracked" → FALSE (upper-bound = spatial coverage).

Sassoon's framework derives the truth-condition of the modified
predicate from the bare adjective's binding. So if *cracked*'s
binding is fixed to b, the prediction profile under b is
(b(oneHigh), b(oneHigh)) — both judgments come from the same b.
No single b satisfies the (true, false) target.

`.mixed` (Sassoon's context-modulated escape hatch) shifts ∀/∃
with discourse context, not with the modifier. The *same* mirror,
in the *same* discourse, gives different verdicts under bare vs
*completely* — that's modifier-driven, not context-driven, so
`.mixed` doesn't help either. 

@[reducible, inline]

abbrev Tham2025.CrackedDims : Type

A 3-dimension Bool model: (quantity, quality, positioning).

Equations

• Tham2025.CrackedDims = (Bool × Bool × Bool)

def Tham2025.crackedDims : List (CrackedDims → Bool)

Equations

• Tham2025.crackedDims = [fun (s : Tham2025.CrackedDims) => s.1, fun (s : Tham2025.CrackedDims) => s.2.1, fun (s : Tham2025.CrackedDims) => s.2.2]

def Tham2025.oneHigh : CrackedDims

"One dimension high" — Tham's lower-bound case (§3.2.1: any physical instantiation suffices for simple predication).

Equations

• Tham2025.oneHigh = (true, false, false)

def Tham2025.sassoonBareTruth (b : Semantics.Gradability.DimensionBindingType) (s : CrackedDims) : Bool

The truth-value Sassoon's framework assigns to bare cracked on a state, given a binding type. (.mixed has to commit to one of the two modes per discourse context — modeled here as .disjunctive, Sassoon's default when polarity is positive.)

Equations

• Tham2025.sassoonBareTruth Semantics.Gradability.DimensionBindingType.conjunctive s = Semantics.Gradability.conjunctiveBinding Tham2025.crackedDims s
• Tham2025.sassoonBareTruth Semantics.Gradability.DimensionBindingType.disjunctive s = Semantics.Gradability.disjunctiveBinding Tham2025.crackedDims s
• Tham2025.sassoonBareTruth Semantics.Gradability.DimensionBindingType.mixed s = Semantics.Gradability.disjunctiveBinding Tham2025.crackedDims s

Tham's two empirical targets on the one-dimension-high state: simple "is cracked" must come out true (Tham §3.2.1, lower bound = physical instantiation); "completely cracked" must come out false (Tham §3 ex. 20a, upper bound = spatial coverage).

theorem Tham2025.conjunctive_matches_completely_only : sassoonBareTruth Semantics.Gradability.DimensionBindingType.conjunctive oneHigh = false ∧ sassoonBareTruth Semantics.Gradability.DimensionBindingType.conjunctive oneHigh ≠ true

.conjunctive matches Tham's completely target (both predict NOT-cracked on oneHigh) but NOT the bare-predication target.

theorem Tham2025.disjunctive_matches_bare_only : sassoonBareTruth Semantics.Gradability.DimensionBindingType.disjunctive oneHigh = true ∧ sassoonBareTruth Semantics.Gradability.DimensionBindingType.disjunctive oneHigh ≠ false

.disjunctive matches Tham's bare target (both predict cracked on oneHigh) but NOT the completely target.

theorem Tham2025.mixed_inherits_disjunctive_gap : sassoonBareTruth Semantics.Gradability.DimensionBindingType.mixed oneHigh = true ∧ sassoonBareTruth Semantics.Gradability.DimensionBindingType.mixed oneHigh ≠ false

.mixed (Sassoon's positive-polarity default = disjunctive) inherits the disjunctive verdict — same gap.

theorem Tham2025.no_sassoon_binding_captures_cracked (b : Semantics.Gradability.DimensionBindingType) : ¬(sassoonBareTruth b oneHigh = true ∧ sassoonBareTruth b oneHigh = false)

The Sassoon insufficiency theorem: in the SAME context, Sassoon's binding cannot account for both simple-predication objectivity (Tham §3.2.1) and completely-modification (Tham §3 ex. 20a) simultaneously, because a single binding gives a single truth-value on the test state. Sassoon's mixed-type escape hatch is context-modulated, not modifier-modulated, so it doesn't discharge the gap either.

Engagement with Sassoon2013.MultidimAdj

To make the cross-paper engagement explicit at the schema level, we construct cracked as a member of Sassoon's MultidimAdj data type for each candidate binding type, and observe how Sassoon's own H3 prediction (closed → conjunctive) interacts with Tham's data.

def Tham2025.crackedAsConjunctive : Sassoon2013.MultidimAdj

cracked coerced into Sassoon's MultidimAdj schema with the binding type Sassoon's H3 predicts for closed-scale adjectives.

Equations

• Tham2025.crackedAsConjunctive = { form := "cracked", isPositive := true, scaleType := Core.Scale.Boundedness.closed, binding := Semantics.Gradability.DimensionBindingType.conjunctive }

def Tham2025.crackedAsDisjunctive : Sassoon2013.MultidimAdj

cracked coerced into Sassoon's schema with the binding type Tham's §3.2.1 lower-bound data WOULD select if mapped naively.

Equations

• Tham2025.crackedAsDisjunctive = { form := "cracked", isPositive := true, scaleType := Core.Scale.Boundedness.closed, binding := Semantics.Gradability.DimensionBindingType.disjunctive }

def Tham2025.crackedAsMixed : Sassoon2013.MultidimAdj

cracked coerced with Sassoon's escape-hatch binding.

Equations

• Tham2025.crackedAsMixed = { form := "cracked", isPositive := true, scaleType := Core.Scale.Boundedness.closed, binding := Semantics.Gradability.DimensionBindingType.mixed }

theorem Tham2025.crackedAsConjunctive_satisfies_sassoon_h3 : Sassoon2013.hypothesis3Holds crackedAsConjunctive = true

The conjunctive entry SATISFIES Sassoon's H3 (closed scaleType predicts conjunctive binding) — but, per conjunctive_matches_completely_only above, this binding gives the WRONG simple-predication verdict.

theorem Tham2025.crackedAsDisjunctive_violates_sassoon_h3 : Sassoon2013.hypothesis3Holds crackedAsDisjunctive = false

The disjunctive entry VIOLATES Sassoon's H3 (closed should yield conjunctive, not disjunctive) — yet this is the binding Tham's §3.2.1 simple-predication data would select.

theorem Tham2025.no_cracked_multidimAdj_satisfies_both : (Sassoon2013.hypothesis3Holds crackedAsConjunctive = true ∧ sassoonBareTruth crackedAsConjunctive.binding oneHigh ≠ true) ∧ (Sassoon2013.hypothesis3Holds crackedAsDisjunctive = false ∧ sassoonBareTruth crackedAsDisjunctive.binding oneHigh = true) ∧ Sassoon2013.hypothesis3Holds crackedAsMixed = false ∧ sassoonBareTruth crackedAsMixed.binding oneHigh = true

The crack between the frameworks made explicit on Sassoon's own schema: NO entry of crackedAs{Conjunctive,Disjunctive,Mixed} simultaneously satisfies Sassoon's H3 prediction AND Tham's simple-predication data. The conjunctive H3-conformer fails Tham; the disjunctive Tham-conformer fails H3; the mixed entry inherits the disjunctive verdict and fails H3 too.

Tham §5.2 eq. (47b) gives the multidimensional measure for deverbal disturbance adjectives:

    μ_CRACKED(x) = Σᵢ kᵢ · μ_EXTENT(distᵢ(x)) / μ_SPATIAL_EXTENT(x)

The numerator is a weighted sum of per-dimension EXTENT measures
(captured by `weightedScore`); the denominator is the host's spatial
extent. The substrate primitive is
`spatialNormalizedScore` (Theories/Semantics/Degree/Aggregation.lean
§2). The boundedness of the upper end of the scale (Tham §3.4
"structural integrity limit") comes from the denominator: the same
physical disturbance counts as more severe on a smaller host.

Below: a worked example WE construct to exercise the substrate.
Tham's actual intuition (p. 18, windshield: "one more crack and it
will break") is that disturbance APPROACHES the structural-integrity
limit from below; the vase example illustrates the inverse — same
physical crack on a smaller host yields a higher normalized score.
Both directions are consistent with eq. 47b mathematically; the
framing is ours, not Tham's. The minimal claim the example makes
Lean-checkable is that the spatial denominator is what introduces
host-relativity (without it, the score is invariant). 

structure Tham2025.Vase : Type

Vase scenario: a host of variable size with a single crack of extent 1 along dimension 1 (quantity), and 0 along quality and positioning.

• spatial : ℚ

def Tham2025.instReprVase.repr : Vase → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tham2025.instReprVase : Repr Vase

Equations

• Tham2025.instReprVase = { reprPrec := Tham2025.instReprVase.repr }

def Tham2025.smallVase : Vase

Equations

• Tham2025.smallVase = { spatial := 1 }

def Tham2025.largeVase : Vase

Equations

• Tham2025.largeVase = { spatial := 4 }

def Tham2025.vaseMeasures : List (Vase → ℚ)

One unit of disturbance along the quantity dimension; zero along the quality and positioning dimensions.

Equations

• Tham2025.vaseMeasures = [fun (x : Tham2025.Vase) => 1, fun (x : Tham2025.Vase) => 0, fun (x : Tham2025.Vase) => 0]

def Tham2025.equalWeights : List ℚ

Equations

• Tham2025.equalWeights = [1, 1, 1]

theorem Tham2025.weighted_score_blind_to_spatial_extent : Semantics.Gradability.Aggregation.weightedScore equalWeights vaseMeasures smallVase = Semantics.Gradability.Aggregation.weightedScore equalWeights vaseMeasures largeVase

Plain weighted score is the same for small and large vases — the Tham eq. 47b numerator cannot detect host-extent differences.

theorem Tham2025.spatial_normalization_separates_small_from_large : Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial smallVase > Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial largeVase

Tham's eq. 47b DOES distinguish: the same physical crack scores higher on a small vase than on a large vase.

theorem Tham2025.small_vase_cracked_large_vase_not : Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial smallVase ≥ 1 / 2 ∧ Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial largeVase < 1 / 2

A threshold that the small vase clears but the large vase doesn't — Tham's "boundedness from spatial extent" claim made Lean-checkable.

theorem Tham2025.largeVase_score_le_one : Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial largeVase ≤ 1

Boundedness from spatial extent (Tham §3.4) made Lean-checkable via the substrate's mathlib-style structural property spatialNormalizedScore_le_one. When the weighted disturbance does not exceed the host's spatial extent, the normalized score is bounded by 1. The largeVase score (1/4) is well below this bound.

@cite{beavers-koontz-garboden-2020} formalize verbal roots as bundles of lexical entailments (Theories/Semantics/Lexical/Roots/Basic.lean). Their classification of √crack is [.becomesState "fissured", .hasCause] — the "result + cause, no manner, no state" four-feature signature ⟨hasState=false, hasManner=false, hasResult=true, hasCause=true⟩ (Phenomena/ArgumentStructure/Studies/BeaversKoontzGarboden2020.lean line 52).

Tham §5.1 (the (45) examples — cracked pumpkin, dented helmet
model, scratched decal) is in tension with strict result-state
INHERITANCE from this root signature to the deverbal adjective:
the adjective applies to surfaces that have not undergone the
CoS event. The substrate-level contrast: B&KG's *crack* root
asserts `becomesState` (the verbal entry derived from this root
inherits it via `Verbal.crack.toVerbCore.degreeAchievementScale`),
yet the adjectival side `Tham2025.crack.adjEntailsPrecedingChange`
is false. 

theorem Tham2025.cracked_adj_refutes_bkg_crack_root_inheritance : Phenomena.ArgumentStructure.Studies.BeaversKoontzGarboden2020.crack.hasResult = true ∧ crack.adjEntailsPrecedingChange = false

B&KG's crack root has hasResult = true (the becomesState "fissured" entailment provides it), but Tham's deverbal adjective cracked does NOT entail a preceding CoS event. Strict result- state inheritance from root to deverbal adjective is refuted at substrate level.

@cite{waldon-etal-2023} formalize artifact-noun multidimensionality using the same weightedScore substrate that powers Tham's eq. 47b numerator. Both consume the substrate; they differ at the DENOMINATOR. Waldon's artifact-noun domain doesn't have a host-extent denominator naturally — there's nothing meaningful to spatially normalize over for "is this object an electronic device." Tham's disturbance-predicate domain does have one (the host's spatial extent), and her eq. 47b commits to using it.

The substrate-level contrast: `weightedScore` (Waldon's surface
arithmetic) is invariant under host-extent changes;
`spatialNormalizedScore` (Tham's eq. 47b) is not. The substrate
accommodates both — the choice between them is a lexical
commitment of the predicate class, not a deeper theoretical
disagreement. 

theorem Tham2025.tham_spatial_normalization_distinguishes_what_waldon_does_not : Semantics.Gradability.Aggregation.weightedScore equalWeights vaseMeasures smallVase = Semantics.Gradability.Aggregation.weightedScore equalWeights vaseMeasures largeVase ∧ Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial smallVase ≠ Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial largeVase

Tham vs Waldon at the substrate level: the same weighted-sum numerator gives the SAME verdict on small vs large vases, but spatial normalization makes them DIFFER. The contrast lives entirely in the denominator.

Solt 2018 SuB (Phenomena/Gradability/Studies/Solt2018Proportional.lean) and Tham 2025 are the substrate's two consumers. Solt's proportionalMeasure μ tot y (her eq. 21) is spatialNormalizedScore [1] [μ] (fun _ => μ tot) y — the single-dimension specialization of Tham's eq. 47b. Both files consume the same spatialNormalizedScore_le_one and _nonneg substrate theorems; this section makes the reciprocal bridge explicit.

The substrate-level identity: any consumer can derive the unit-
interval bound from the substrate primitives, regardless of
whether they specialize to single-dim (Solt) or multi-dim (Tham)
aggregation. 

theorem Tham2025.solt_tham_share_substrate_bounded_by_one : Semantics.Gradability.Aggregation.spatialNormalizedScore equalWeights vaseMeasures Vase.spatial largeVase ≤ 1

Tham's largeVase_score_le_one (above, §13) and Solt's proportionalMeasure_le_one are the SAME mathlib-style theorem instantiated on different aggregation specializations. The shared substrate primitive is spatialNormalizedScore_le_one.

@cite{kennedy-2007}'s Interpretive Economy principle predicts a max-endpoint standard for closed-scale adjectives (cracked → .maxEndpoint, witnessed by cracked_standard_maxEndpoint in §8 above). Tham's §3.2.1 lower-bound argument (simple predication is OBJECTIVE: any physical instantiation suffices, witnessed by simplePredicationObjective = true in §5 above) requires only the MINIMUM physical instantiation to be on the scale at all.

These are not strictly contradictory — IE selects the standard for
the positive form ("the threshold for *applies as a positive
predicate*"); the lower bound is the threshold for *being on the
scale at all*. But they do place different demands on the same
`Boundedness` substrate. The wedge made Lean-checkable: 

theorem Tham2025.cracked_ie_max_vs_tham_lower_bound : Semantics.Degree.interpretiveEconomy Fragments.English.Predicates.Adjectival.cracked.scaleType = Semantics.Degree.PositiveStandard.maxEndpoint ∧ crack.simplePredicationObjective = true ∧ Semantics.Degree.PositiveStandard.maxEndpoint ≠ Semantics.Degree.PositiveStandard.minEndpoint

The IE-vs-Tham §3.2.1 wedge: K2007's Interpretive Economy selects .maxEndpoint for cracked's standard (cracked_standard_maxEndpoint), while Tham's §3.2.1 simple-predication objectivity claim requires only the lower bound. The wedge is at the level of WHICH endpoint of the closed scale is load-bearing for which prediction.

@cite{solt-2018} (the Springer multidim chapter, distinct from the SuB proportional-comparatives paper engaged in §16) presents an experimental five-class subjectivity typology (RelNum/AbsTot/AbsPart/RelNo/Eval, Fig. 1, pp. 5–6). The class is encoded as a substrate-adjacent enum at Phenomena/Gradability/Studies/Solt2018Multidim.lean.

*cracked* belongs to the AbsPart class — partially-closed scale,
physical-property domain, intermediate ordering subjectivity
(~67% "fact" judgments per Solt's experiment). The closest
siblings are *clean*/*dirty*/*salty*/*wet*/*dry*. 

theorem Tham2025.cracked_is_solt_AbsPart : Solt2018Multidim.crackedClass = Solt2018Multidim.SubjectivityClass.absPart

cracked belongs to Solt's AbsPart class, alongside clean/dirty/wet/dry. The class membership is consumed from Solt2018Multidim.crackedClass.