Granularity Bridge: Just + Degree Morphology @cite{thomas-deo-2020}

@cite{deo-thomas-2025}

Connects the formal semantics of approximative just from Theories.Semantics.Degree.Granularity to the just flavor data in Phenomena.Focus.Exclusives.

The .precisifyingEquality flavor ("just as tall as" ≈ "exactly") follows from just_vacuous_iff: the negative component of just is vacuous for equatives. The .precisifyingProximity flavor ("just taller than" ≈ "barely") follows from just_rules_out: the negative component forces failure at coarser grains.

def Phenomena.Focus.Studies.ThomasDeo2020.justFlavorFromConstruction : Semantics.Degree.AdjectivalConstruction → Exclusives.JustFlavor

Derive just flavor from adjectival construction type. @cite{thomas-deo-2020} predict:

• comparative + just → precisifying proximity (barely)
• equative + just → precisifying equality (exactly)

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.comparative = Phenomena.Focus.Exclusives.JustFlavor.precisifyingProximity
• Phenomena.Focus.Studies.ThomasDeo2020.justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.equative = Phenomena.Focus.Exclusives.JustFlavor.precisifyingEquality
• Phenomena.Focus.Studies.ThomasDeo2020.justFlavorFromConstruction x✝ = Phenomena.Focus.Exclusives.JustFlavor.complementExclusion

theorem Phenomena.Focus.Studies.ThomasDeo2020.comparative_yields_proximity : justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.comparative = Exclusives.precisifying_prox_older.flavor

"Fafen is just older than Siri" — comparative + just = proximity.

theorem Phenomena.Focus.Studies.ThomasDeo2020.equative_yields_equality : justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.equative = Exclusives.precisifying_eq_full.flavor

Equative + just = equality ("just as tall as" ≈ "exactly as tall as"). Note: precisifying_eq_full ("just full") achieves equality via a closed-scale endpoint standard, not via equative morphology. The shared flavor (.precisifyingEquality) reflects parallel pragmatic effects through different compositional routes.

theorem Phenomena.Focus.Studies.ThomasDeo2020.equality_grounded {D : Type u_1} {G : Type u_2} [LinearOrder D] (p : G → D → Prop) (finest : G) (h : ∀ (g : G), Semantics.Degree.Granularity.atLeastAsStrong p finest g) (μ_x : D) : Semantics.Degree.Granularity.approxJust p finest μ_x ↔ p finest μ_x

The equality reading for equatives is grounded: when the finest grain is the strongest (largest lo → fine entails coarse), just's negative component is vacuous, so "just as tall as" reduces to the equative at finest grain. Instantiates just_vacuous_iff.

theorem Phenomena.Focus.Studies.ThomasDeo2020.proximity_grounded {D : Type u_1} {G : Type u_2} [LinearOrder D] (p : G → D → Prop) (finest g : G) (h : ¬Semantics.Degree.Granularity.atLeastAsStrong p finest g) (μ_x : D) (hjust : Semantics.Degree.Granularity.approxJust p finest μ_x) : ¬p g μ_x

The proximity reading for comparatives is grounded: when the finest grain is NOT the strongest at some coarser grain g, just rules out truth at g. Instantiates just_rules_out.

§3 data: just with equatives and comparatives

The paper's key empirical observations, encoded as JustDatum entries from Exclusives.lean. Each datum has a predicted flavor and a predicted cancellability status.

inductive Phenomena.Focus.Studies.ThomasDeo2020.Cancellability : Type

Whether just's inference can be cancelled with "but...".

• cancellable : Cancellability
• nonCancellable : Cancellability

instance Phenomena.Focus.Studies.ThomasDeo2020.instReprCancellability : Repr Cancellability

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.instReprCancellability = { reprPrec := Phenomena.Focus.Studies.ThomasDeo2020.instReprCancellability.repr }

def Phenomena.Focus.Studies.ThomasDeo2020.instReprCancellability.repr : Cancellability → ℕ → Std.Format

Equations

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

instance Phenomena.Focus.Studies.ThomasDeo2020.instDecidableEqCancellability : DecidableEq Cancellability

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.instDecidableEqCancellability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Focus.Studies.ThomasDeo2020.instBEqCancellability.beq : Cancellability → Cancellability → Bool

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.instBEqCancellability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Focus.Studies.ThomasDeo2020.instBEqCancellability : BEq Cancellability

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.instBEqCancellability = { beq := Phenomena.Focus.Studies.ThomasDeo2020.instBEqCancellability.beq }

structure Phenomena.Focus.Studies.ThomasDeo2020.GranularityDatum : Type

A granularity-specific datum: example + construction + predicted flavor + cancellability.

• sentence : String
• construction : Semantics.Degree.AdjectivalConstruction
• predictedFlavor : Exclusives.JustFlavor
• cancellability : Cancellability
• paraphrase : String
• exampleNum : ℕ

def Phenomena.Focus.Studies.ThomasDeo2020.instReprGranularityDatum.repr : GranularityDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Focus.Studies.ThomasDeo2020.instReprGranularityDatum : Repr GranularityDatum

Equations

• Phenomena.Focus.Studies.ThomasDeo2020.instReprGranularityDatum = { reprPrec := Phenomena.Focus.Studies.ThomasDeo2020.instReprGranularityDatum.repr }

def Phenomena.Focus.Studies.ThomasDeo2020.eq_amaryllis : GranularityDatum

(14) "The amaryllis are just as tall as the hollyhocks" → precisifying equality ("exactly as tall as").

Equations

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

def Phenomena.Focus.Studies.ThomasDeo2020.eq_anna_maria : GranularityDatum

(15) "Anna is just as old as Maria" → precisifying equality ("exactly as old as").

Equations

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

def Phenomena.Focus.Studies.ThomasDeo2020.comp_fafen_siri : GranularityDatum

(21) "Fafen is just older than Siri" → precisifying proximity ("barely older than").

Equations

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

def Phenomena.Focus.Studies.ThomasDeo2020.comp_fafen_cancel : GranularityDatum

(23) "#Fafen is just older than Siri, but by a lot" → proximity inference is non-cancellable. Contrast with (24): "Fafen is only older than Siri, but by a lot" (OK).

Equations

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

def Phenomena.Focus.Studies.ThomasDeo2020.comp_album : GranularityDatum

(25) "This album is just more expensive than that one" → precisifying proximity ("barely more expensive").

Equations

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

def Phenomena.Focus.Studies.ThomasDeo2020.allGranularityData : List GranularityDatum

Equations

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

theorem Phenomena.Focus.Studies.ThomasDeo2020.eq_data_flavor : eq_amaryllis.predictedFlavor = justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.equative ∧ eq_anna_maria.predictedFlavor = justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.equative

All equative data points get the predicted equality flavor.

theorem Phenomena.Focus.Studies.ThomasDeo2020.comp_data_flavor : comp_fafen_siri.predictedFlavor = justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.comparative ∧ comp_fafen_cancel.predictedFlavor = justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.comparative ∧ comp_album.predictedFlavor = justFlavorFromConstruction Semantics.Degree.AdjectivalConstruction.comparative

All comparative data points get the predicted proximity flavor.

theorem Phenomena.Focus.Studies.ThomasDeo2020.all_noncancellable : eq_amaryllis.cancellability = Cancellability.nonCancellable ∧ eq_anna_maria.cancellability = Cancellability.nonCancellable ∧ comp_fafen_siri.cancellability = Cancellability.nonCancellable ∧ comp_fafen_cancel.cancellability = Cancellability.nonCancellable ∧ comp_album.cancellability = Cancellability.nonCancellable

All data points have non-cancellable inferences — the granularity contribution of just is at-issue (§3.3), not a cancellable implicature.

theorem Phenomena.Focus.Studies.ThomasDeo2020.eq_data_matches_exclusives : eq_amaryllis.predictedFlavor = Exclusives.precisifying_eq_full.flavor ∧ eq_anna_maria.predictedFlavor = Exclusives.precisifying_eq_full.flavor

Equative data match the existing precisifying_eq_full flavor.

theorem Phenomena.Focus.Studies.ThomasDeo2020.comp_data_matches_exclusives : comp_fafen_siri.predictedFlavor = Exclusives.precisifying_prox_older.flavor ∧ comp_album.predictedFlavor = Exclusives.precisifying_prox_older.flavor

Comparative data match the existing precisifying_prox_older flavor.