Outcome cardinality

The cardinality tier of a verb root's outcome set ([Bha24], eq. 62): the light invariant of what a root encodes along the outcome axis — empty (no change specified), singleton (a single lexically-specified result — change-of- state and impingement roots), or multi (potential-for-change roots). Only the tier, not an exact count, is grammatically load-bearing, so this is a three-element linear order rather than ℕ∞.

Factored out from Semantics/Verb/Root/Outcomes.lean (which carries the heavy event-relative machinery — res/pre, VerbOutcomes) so that Root itself can carry the outcome axis without depending on Event/EventRel.

Main definitions

• OutcomeCardinality — the empty < singleton < multi tier
• OutcomeCardinality.ofSet — the tier of a concrete outcome set

References

• [Bha24] (roots encode outcome sets; the eq. 62 hierarchy)

inductive Verb.OutcomeCardinality : Type

The cardinality tier of an outcome set ([Bha24], 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.

@[implicit_reducible]

instance Verb.instReprOutcomeCardinality : Repr OutcomeCardinality

Equations

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

@[implicit_reducible]

instance Verb.instBEqOutcomeCardinality : BEq OutcomeCardinality

Equations

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

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

Equations

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

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

@[implicit_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