Bhadra 2024: Verb roots encode outcomes

[Bha24]

The reversative prefix un- and the restitutive prefix re- are result-state modifiers sensitive to the outcome set a verb root lexically encodes ([Bha24], §5). Every verb root carries a set of outcomes O — the states its object can be in after the action — and a contextual set of thresholds T of states it can start from.

The two affixes split along two independent axes:

• un- is driven by outcome-set cardinality (eq. 66): it needs O.Nontrivial (|O| > 1, the potential-for-change / PFC profile) plus inverse equivalence between the base result and the un-event's boundaries. Singleton or empty outcome sets block it.
• re- is not cardinality-sensitive (eq. 72); it needs result equivalence with a prior event (eq. 68 i) and that the object can re-enter a threshold state (eq. 68 ii). Consumption/destruction and impingement (IE) verbs block it ((25), (48)) because their outcome leaves the object outside every threshold.

One idealization: each VerbOutcomes fixes its outcome and threshold sets once per root, freezing the [verb + object] unit that Bhadra's Level-2 story varies with the object (✓rebreak a limb vs. #rebreak a sewer, her (73)).

Main definitions

• VerbOutcomes — a root's base predicate (EventRel), outcome set, threshold set
• resState / preState — state at the right / left event boundary (eqs. 64–65)
• unSem / reSem — the un- and re- denotations (eqs. 66, 68)
• LevinClass.outcomeCard — the single Levin-class → outcome-cardinality bridge (ℕ∞; eq. 62 hierarchy multi > singleton > empty)

Main results

• subsingleton_blocks_un — ¬ O.Nontrivial → ¬ unSem (eq. 67), with the singleton and empty corollaries
• *_un / *_re per-verb predictions, derived compositionally and bridged from Fragment entries via Verb.levinClass

References

• [Bha24] (the Verb-Root-Outcomes framework)
• [Bea11] (the affectedness hierarchy and the PFC class)
• [Bea10], [Dow91] (ground the profileToDegree projection only)
• [Lev93] (verb classes the outcome bridge keys on)

Outcome cardinality (eq. 62)

The cardinality tier of an outcome set — empty < singleton < multi — the light invariant of what a root encodes along the outcome axis. Only the tier, not an exact count, is grammatically load-bearing, so this is a three-element linear order rather than ℕ∞. Single-consumer substrate carried here with its anchoring study.

inductive Verb.OutcomeCardinality : Type

The cardinality tier of an outcome set (eq. 62).

• empty : OutcomeCardinality
• singleton : OutcomeCardinality
• multi : OutcomeCardinality

def Verb.instReprOutcomeCardinality.repr : OutcomeCardinality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprOutcomeCardinality : Repr OutcomeCardinality

Equations

• Verb.instReprOutcomeCardinality = { reprPrec := Verb.instReprOutcomeCardinality.repr }

def Verb.instBEqOutcomeCardinality.beq : OutcomeCardinality → OutcomeCardinality → Bool

Equations

• Verb.instBEqOutcomeCardinality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Verb.instBEqOutcomeCardinality : BEq OutcomeCardinality

Equations

• Verb.instBEqOutcomeCardinality = { beq := Verb.instBEqOutcomeCardinality.beq }

def Verb.OutcomeCardinality.toNat : OutcomeCardinality → ℕ

Rank embedding into ℕ, giving the empty < singleton < multi order.

Equations

• Verb.OutcomeCardinality.empty.toNat = 0
• Verb.OutcomeCardinality.singleton.toNat = 1
• Verb.OutcomeCardinality.multi.toNat = 2

theorem Verb.OutcomeCardinality.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance Verb.OutcomeCardinality.instLinearOrder : LinearOrder OutcomeCardinality

Equations

• Verb.OutcomeCardinality.instLinearOrder = LinearOrder.lift' Verb.OutcomeCardinality.toNat Verb.OutcomeCardinality.toNat_injective

theorem Verb.OutcomeCardinality.empty_lt_singleton : empty < singleton

theorem Verb.OutcomeCardinality.singleton_lt_multi : singleton < multi

noncomputable def Verb.OutcomeCardinality.ofSet {State : Type u_1} (O : Set State) : OutcomeCardinality

The tier of a concrete outcome set: multi-membered iff Nontrivial, empty iff there is no outcome, singleton otherwise.

Equations

• Verb.OutcomeCardinality.ofSet O = if O.Nontrivial then Verb.OutcomeCardinality.multi else if O.Nonempty then Verb.OutcomeCardinality.singleton else Verb.OutcomeCardinality.empty

theorem Verb.OutcomeCardinality.ofSet_eq_multi {State : Type u_1} {O : Set State} (h : O.Nontrivial) : ofSet O = multi

theorem Verb.OutcomeCardinality.ofSet_eq_singleton {State : Type u_1} {O : Set State} (hne : O.Nonempty) (hnt : ¬O.Nontrivial) : ofSet O = singleton

theorem Verb.OutcomeCardinality.ofSet_eq_empty {State : Type u_1} {O : Set State} (h : ¬O.Nonempty) : ofSet O = empty

@[simp]

theorem Verb.OutcomeCardinality.ofSet_singleton {State : Type u_1} (s : State) : ofSet {s} = singleton

@[simp]

theorem Verb.OutcomeCardinality.ofSet_empty {State : Type u_1} : ofSet ∅ = empty

Event boundaries (eqs. 64–65)

res and pre read an object's lexically-relevant state at the right and left boundaries of an event's temporal trace τ. They yield states, not times. Single-consumer substrate carried here with its anchoring study.

@[reducible, inline]

abbrev ArgumentStructure.StateFunction (Entity : Type u_1) (State : Type u_2) (Time : Type u_3) : Type (max (max u_1 u_2) u_3)

A state function tracks an object's state at each time point.

Equations

• ArgumentStructure.StateFunction Entity State Time = (Time → Entity → State)

def ArgumentStructure.resState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : StateFunction Entity State Time) (e : Event Time) (x : Entity) : State

res(e)(x) (eq. 64): the object's state at the right boundary of e.

Equations

• ArgumentStructure.resState k e x = k e.τ.toProd.2 x

def ArgumentStructure.preState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : StateFunction Entity State Time) (e : Event Time) (x : Entity) : State

pre(e)(x) (eq. 65): the object's state at the left boundary of e.

Equations

• ArgumentStructure.preState k e x = k e.τ.toProd.1 x

structure ArgumentStructure.VerbOutcomes (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) [LinearOrder Time] : Type (max (max u_4 u_5) u_6)

A verb root carrying an outcome set, the carrier result-state modifiers act on (eqs. 56, 60): the base predicate P(e)(x) with the lexical outcome set O and the contextual threshold set T.

• verb : EventRel Time Entity

  The base predicate P(e)(x) (⟨v,⟨e,t⟩⟩).

• outcomes : Set State

  The lexically-encoded outcome set O (states at the right boundary).

• thresholds : Set State

  The contextual threshold set T (states at the left boundary).

noncomputable def ArgumentStructure.VerbOutcomes.cardinality {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (vro : VerbOutcomes Entity State Time) : Verb.OutcomeCardinality

The cardinality tier of a root's outcome set.

Equations

• vro.cardinality = Verb.OutcomeCardinality.ofSet vro.outcomes

The compositional verb root (eqs. 53–60)

A verb root lexically encodes its base predicate P (the ⟨v,⟨e,t⟩⟩ meaning the affixes modify), its outcome set O (states at the right boundary, eq. 56a), and its threshold set T (left boundary, eq. 56b) — the local VerbOutcomes above, with resState/preState the eq. 64–65 boundary operators and StateFunction the paper's state k : t ↦ l(x) (eq. 53). APPLIES (eq. 59) is folded into verb.

un- and re- as result-state modifiers (eqs. 66, 68)

def Bhadra2024.unSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) : Prop

Reversative un- (eq. 66). unSem k vro e x holds iff there is a prior base event e' whose result is the un-event's start state (res(e') = pre(e)), the outcome set is multi-membered (O.Nontrivial, |O| > 1), and the un-event undoes it (res(e) = pre(e')). The vacuous ∃Q. Q(e)(x) — which sits in the assertion of eq. 66, not its presupposition — is dropped.

Equations

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

def Bhadra2024.reSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) : Prop

Restitutive re- (eq. 68). reSem k vro e x holds iff there is a prior base event e' with the same result (res(e) = res(e'), eq. 68 i), the re-event starts from a valid threshold state (pre(e) ∈ T), and the base predicate holds of the re-event (P(e)(x)). The threshold clause is a rational reconstruction — not a transcription — of eq. 68 ii's negative existential (no threshold state may render the re-action undefined; the cyclic-re- condition, eq. 72). Unlike unSem, this places no cardinality demand on O.

Equations

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

Cardinality blocks un- (eq. 67)

theorem Bhadra2024.subsingleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (h : ¬vro.outcomes.Nontrivial) (e : Event Time) (x : Entity) : ¬unSem k vro e x

The core asymmetry: a verb whose outcome set is not multi-membered cannot host un- ([Bha24], eq. 67). The multi-membered presupposition of unSem fails.

theorem Bhadra2024.singleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (s : State) (hs : vro.outcomes = {s}) (e : Event Time) (x : Entity) : ¬unSem k vro e x

Singleton outcome sets (IE and COS verbs) block un-.

theorem Bhadra2024.empty_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (hs : vro.outcomes = ∅) (e : Event Time) (x : Entity) : ¬unSem k vro e x

Empty outcome sets (no-change-specified verbs) block un-.

theorem Bhadra2024.un_requires_multi_cardinality {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : ArgumentStructure.StateFunction Entity State Time) (vro : ArgumentStructure.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) (h : unSem k vro e x) : vro.cardinality = Verb.OutcomeCardinality.multi

un-'s cardinality demand (eq. 67, |O| > 1) is exactly the substrate OutcomeCardinality.multi tier (eq. 62, empty < singleton < multi): hosting un- forces the verb root's outcome set into the top tier. Wires Bhadra's outcome cardinality to the OutcomeCardinality substrate.

The Levin-class → outcome-cardinality bridge (eq. 62)

The single per-class datum: the cardinality of a verb root's lexical outcome set, valued in ℕ∞. PFC roots have open-ended outcome sets (eq. 60: O = {k | k = APPLIES(e)(x)}, unbounded), idealized as ⊤; IE and COS roots have a single lexically-specified result (eqs. 61a–g); no-change roots have none (eq. 61h). Only 1 < · is load-bearing (it drives un-); the three tiers realize the eq. 62 hierarchy multi > singleton > empty.

def Bhadra2024.LevinClass.outcomeCard : ArgumentStructure.LevinClass → ℕ∞

Outcome-set cardinality of a Levin verb class ([Bha24], eq. 62).

Equations

• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.coil = ⊤
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.bend = ⊤
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.conceal = ⊤
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.dress = ⊤
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.hit = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.swat = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.wipe = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.touch = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.break_ = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.destroy = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.cooking = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.otherCoS = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.entitySpecificCoS = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.calibratableCoS = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.color = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.imageCreation = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.build = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.create = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.grow = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.knead = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.turn = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.cut = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.carve = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.eat = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.devour = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.murder = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.poison = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.mix = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.amalgamate = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.separate = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.split = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.clear = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.sprayLoad = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.pushPull = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.remove = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.throw = 1
• Bhadra2024.LevinClass.outcomeCard ArgumentStructure.LevinClass.put = 1
• Bhadra2024.LevinClass.outcomeCard x✝ = 0

theorem Bhadra2024.outcome_hierarchy : LevinClass.outcomeCard ArgumentStructure.LevinClass.bend = ⊤ ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.hit = 1 ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.break_ = 1 ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.mannerOfMotion = 0 ∧ 0 < 1 ∧ 1 < ⊤

The eq. 62 hierarchy, witnessed on a representative of each tier: multi-membered (PFC) > singleton (IE, COS) > empty (no change).

theorem Bhadra2024.bend_predicts_un : 1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.bend

un- prediction is derived from cardinality: PFC classes have 1 < outcomeCard, every other class does not.

theorem Bhadra2024.coil_predicts_un : 1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.coil

theorem Bhadra2024.break_blocks_un_class : ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.break_

theorem Bhadra2024.hit_blocks_un_class : ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.hit

theorem Bhadra2024.destroy_blocks_un_class : ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.destroy

theorem Bhadra2024.color_blocks_un_class : ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.color

theorem Bhadra2024.mannerOfMotion_blocks_un_class : ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.mannerOfMotion

Worked examples (eqs. 60–61, 66–71)

fold: a PFC root (multi-membered outcomes), un- and re- both attach

inductive Bhadra2024.ParchmentState : Type

States of a parchment under folding (eq. 54: a multi-membered outcome set).

• flat : ParchmentState
• slightlyCreased : ParchmentState
• folded : ParchmentState
• tightlyFolded : ParchmentState

@[instance_reducible]

instance Bhadra2024.instDecidableEqParchmentState : DecidableEq ParchmentState

Equations

• Bhadra2024.instDecidableEqParchmentState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bhadra2024.instReprParchmentState : Repr ParchmentState

Equations

• Bhadra2024.instReprParchmentState = { reprPrec := Bhadra2024.instReprParchmentState.repr }

def Bhadra2024.instReprParchmentState.repr : ParchmentState → ℕ → Std.Format

Equations

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

def Bhadra2024.foldVRO : ArgumentStructure.VerbOutcomes Unit ParchmentState ℤ

fold (Levin bend class): a multi-membered outcome set.

Equations

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

theorem Bhadra2024.fold_outcomes_multi : foldVRO.outcomes.Nontrivial

theorem Bhadra2024.fold_un_satisfiable : unSem Bhadra2024.foldUnfoldState✝ foldVRO Bhadra2024.ev₂✝ ()

Positive: un- IS satisfiable for fold (eq. 66 worked example, "Veena unfolded the parchment").

theorem Bhadra2024.fold_re_satisfiable : reSem Bhadra2024.foldRefoldState✝ foldVRO Bhadra2024.ev₃✝ ()

Positive: re- IS satisfiable for fold — the multi-membered (PFC) tier's re- cell, completing the Fig. 5 distribution: re- attaches across the multi and singleton tiers (eq. 72), where un- takes the multi tier only. Reuses the root of her worked unfold derivation (74)–(75).

break: a COS root (singleton outcome), un- blocked, re- allowed

inductive Bhadra2024.LimbState : Type

• intact : LimbState
• broken : LimbState

@[instance_reducible]

instance Bhadra2024.instDecidableEqLimbState : DecidableEq LimbState

Equations

• Bhadra2024.instDecidableEqLimbState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bhadra2024.instReprLimbState : Repr LimbState

Equations

• Bhadra2024.instReprLimbState = { reprPrec := Bhadra2024.instReprLimbState.repr }

def Bhadra2024.instReprLimbState.repr : LimbState → ℕ → Std.Format

Equations

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

def Bhadra2024.breakVRO : ArgumentStructure.VerbOutcomes Unit LimbState ℤ

break (Levin break_ class): a single lexically-specified result (eq. 61a).

Equations

• Bhadra2024.breakVRO = { verb := fun (x : Event ℤ) (x_1 : Unit) => True, outcomes := {Bhadra2024.LimbState.broken}, thresholds := {Bhadra2024.LimbState.intact} }

theorem Bhadra2024.break_blocks_un (k : ArgumentStructure.StateFunction Unit LimbState ℤ) (e : Event ℤ) : ¬unSem k breakVRO e ()

unbreak is blocked: the singleton outcome set fails eq. 67.

theorem Bhadra2024.break_re_satisfiable : reSem Bhadra2024.breakRebreakState✝ breakVRO Bhadra2024.ev₃✝ ()

Positive: re- IS satisfiable for break (rebreak a limb): result equivalence holds and the re-event starts from the intact threshold.

hit: an IE root (singleton outcome), un- and re- both blocked

inductive Bhadra2024.SurfaceState : Type

• unaltered : SurfaceState
• surfaceAltered : SurfaceState

@[instance_reducible]

instance Bhadra2024.instDecidableEqSurfaceState : DecidableEq SurfaceState

Equations

• Bhadra2024.instDecidableEqSurfaceState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprSurfaceState.repr : SurfaceState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprSurfaceState : Repr SurfaceState

Equations

• Bhadra2024.instReprSurfaceState = { reprPrec := Bhadra2024.instReprSurfaceState.repr }

def Bhadra2024.hitVRO : ArgumentStructure.VerbOutcomes Unit SurfaceState ℤ

hit (Levin hit class): impingement, a single surface-alteration result (eq. 61g).

Equations

• Bhadra2024.hitVRO = { verb := fun (x : Event ℤ) (x_1 : Unit) => True, outcomes := {Bhadra2024.SurfaceState.surfaceAltered}, thresholds := {Bhadra2024.SurfaceState.unaltered} }

theorem Bhadra2024.hit_blocks_un (k : ArgumentStructure.StateFunction Unit SurfaceState ℤ) (e : Event ℤ) : ¬unSem k hitVRO e ()

theorem Bhadra2024.hit_re_blocked : ¬reSem Bhadra2024.hitState✝ hitVRO Bhadra2024.ev₃✝ ()

Negative: re- is blocked for hit — IE verbs block re- as well as un- ((25), (48)): the impingement outcome never re-enters the pre-state (threshold) set, so the cyclic-re- condition (eq. 68 ii) fails.

load vs shatter: the re- minimal pair (eqs. 69–71)

Both are singleton-outcome (so both block un-); they differ on re- purely through the threshold condition (eq. 68 ii). After loading, the truck can be loaded again (it re-enters a threshold); after shattering, the mirror cannot.

inductive Bhadra2024.TruckState : Type

• empty : TruckState
• partlyLoaded : TruckState
• full : TruckState

@[instance_reducible]

instance Bhadra2024.instDecidableEqTruckState : DecidableEq TruckState

Equations

• Bhadra2024.instDecidableEqTruckState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprTruckState.repr : TruckState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprTruckState : Repr TruckState

Equations

• Bhadra2024.instReprTruckState = { reprPrec := Bhadra2024.instReprTruckState.repr }

def Bhadra2024.loadVRO : ArgumentStructure.VerbOutcomes Unit TruckState ℤ

load (degree achievement, eq. 70): a single contextually-salient result; the object stays loadable.

Equations

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

theorem Bhadra2024.load_re_satisfiable : reSem Bhadra2024.loadReloadState✝ loadVRO Bhadra2024.ev₃✝ ()

Positive: re- IS satisfiable for load (eq. 69a "reloaded the truck").

inductive Bhadra2024.MirrorState : Type

• intact : MirrorState
• shattered : MirrorState

@[instance_reducible]

instance Bhadra2024.instDecidableEqMirrorState : DecidableEq MirrorState

Equations

• Bhadra2024.instDecidableEqMirrorState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprMirrorState.repr : MirrorState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprMirrorState : Repr MirrorState

Equations

• Bhadra2024.instReprMirrorState = { reprPrec := Bhadra2024.instReprMirrorState.repr }

def Bhadra2024.shatterVRO : ArgumentStructure.VerbOutcomes Unit MirrorState ℤ

shatter (eq. 71): a single result that leaves the object outside every threshold — it cannot be shattered again.

Equations

• Bhadra2024.shatterVRO = { verb := fun (x : Event ℤ) (x_1 : Unit) => True, outcomes := {Bhadra2024.MirrorState.shattered}, thresholds := {Bhadra2024.MirrorState.intact} }

theorem Bhadra2024.shatter_re_blocked : ¬reSem Bhadra2024.shatterState✝ shatterVRO Bhadra2024.ev₃✝ ()

Negative: re- is blocked for shatter (eq. 69b "#reshattered the mirror"): the cyclic-re- threshold condition (eq. 68 ii) fails — the shattered mirror is never in the intact threshold the re-event needs.

End-to-end: Fragment entry → Levin class → prediction

The Fragment verb's levinClass drives the outcome cardinality, which drives the un- prediction.

theorem Bhadra2024.kick_un_blocked : English.Predicates.Verbal.kick.levinClass = some ArgumentStructure.LevinClass.hit ∧ ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.hit

kick (Levin 18.1 hit) → singleton outcomes → un- blocked.

theorem Bhadra2024.bend_un_predicted : English.Predicates.Verbal.bend.levinClass = some ArgumentStructure.LevinClass.bend ∧ 1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.bend

bend (Levin 45.2) → multi-membered outcomes → un- predicted.

theorem Bhadra2024.break_un_blocked : English.Predicates.Verbal.break_.levinClass = some ArgumentStructure.LevinClass.break_ ∧ ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.break_

break (Levin 45.1) → singleton outcomes → un- blocked.

Bridges to the substrate

The outcome-cardinality classification is finer than the change-of-state label ([Bha24]'s central move): bend is CoS per [Lev93] yet has a multi-membered (PFC) outcome set.

theorem Bhadra2024.bend_reclassification : ArgumentStructure.LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.bend = ⊤ ∧ 1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.bend

[Bha24] reclassifies bend from a flat change-of-state verb to a potential-for-change root: CoS per [Lev93]'s meaning components, but multi-membered (and hence un--compatible) by outcome cardinality.

theorem Bhadra2024.outcomeCard_orthogonal_to_hasResultState : ArgumentStructure.LevinClass.bend.eventTemplate.HasResultState ∧ ¬ArgumentStructure.LevinClass.coil.eventTemplate.HasResultState ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.bend = ⊤ ∧ LevinClass.outcomeCard ArgumentStructure.LevinClass.coil = ⊤

The outcome-cardinality classification is orthogonal to event-template result states: bend and coil share the PFC profile but differ on whether their template carries a result state.

theorem Bhadra2024.affectedness_bridge : ArgumentStructure.Affectedness.profileToDegree { causallyAffected := true, stationary := true } = ArgumentStructure.Affectedness.profileToDegree ArgumentStructure.contactObject ∧ 1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.bend ∧ ¬1 < LevinClass.outcomeCard ArgumentStructure.LevinClass.hit

Affectedness bridge ([Bha24] §2.4.2, §6.1): the affectedness projection cannot separate PFC roots from IE roots — the PFC object profile (causally affected, no entailed change) and kick's object profile both land on Beavers's potential-for-change degree, whose exemplars include surface-contact hit/kick. Bhadra carves the IE class (kick is named in her (25)) out of exactly that cell (§2.4.2), and her §6.1 point is that the split needs outcome-set structure a bare latent-scale existential cannot see: outcome cardinality separates the two (⊤ vs 1) where the affectedness degree does not.

theorem Bhadra2024.roottype_bridge : Verb.Root.ChangeType.result.entailsChange = true ∧ Verb.Root.ChangeType.result.allowsRestitutiveAgain = false ∧ Verb.Root.ChangeType.propertyConcept.entailsChange = false ∧ Verb.Root.ChangeType.propertyConcept.allowsRestitutiveAgain = true

Change-type bridge: result roots entail change and lack the restitutive again reading; property-concept roots are the reverse.