Evidential — derived properties

[Aik04]

Derived predicates and the Aikhenvald-cell mapping that lets typological classifications be DERIVED from declared inventories rather than hardcoded per-language. Mirrors the Determiner.Inventory.markingStrategy pattern at Semantics/Definiteness/Determiner.lean: typological classifications are theorems about the declared inventory, not stipulations.

Main declarations

• Entry.Cell — the cells of [Aik04] Ch 2's paradigm space, distinct evidence-source categories a paradigm can carve out.
• Entry.cell : Entry → Cell — projection from a typed entry to its Aikhenvald cell. Direct entries map via DirectSource (visual, auditory, etc.), inferential entries via InferentialBasis (from-result, from-assumption), reportative entries via ReportativeSource (unidentified, identified).

inductive Semantics.Evidential.Entry.Cell : Type

A cell in [Aik04] Ch 2's paradigm space. Each Entry covers one cell; AikhenvaldSystem.fromInventory then classifies a paradigm by inspecting which cells are filled.

• firsthand : Cell

  Generic firsthand, no sensory channel specified (A1's catch-all).

• visual : Cell

  Specifically visual evidence.

• nonvisualSensory : Cell

  Non-visual sensory (touch, smell, taste, generic non-visual).

• auditory : Cell

  Specifically auditory (A5; Kashaya's distinctive split).

• inferred : Cell

  Inference from an observable result.

• assumed : Cell

  Inference from general knowledge or reasoning.

• reported : Cell

  Hearsay from an unidentified source.

• quotative : Cell

  Hearsay from a specifically identified source.

@[instance_reducible]

instance Semantics.Evidential.Entry.instDecidableEqCell : DecidableEq Cell

Equations

• Semantics.Evidential.Entry.instDecidableEqCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Evidential.Entry.instBEqCell : BEq Cell

Equations

• Semantics.Evidential.Entry.instBEqCell = { beq := Semantics.Evidential.Entry.instBEqCell.beq }

def Semantics.Evidential.Entry.instBEqCell.beq : Cell → Cell → Bool

Equations

• Semantics.Evidential.Entry.instBEqCell.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Semantics.Evidential.Entry.instReprCell : Repr Cell

Equations

• Semantics.Evidential.Entry.instReprCell = { reprPrec := Semantics.Evidential.Entry.instReprCell.repr }

def Semantics.Evidential.Entry.instReprCell.repr : Cell → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Evidential.Entry.instInhabitedCell : Inhabited Cell

Equations

• Semantics.Evidential.Entry.instInhabitedCell = { default := Semantics.Evidential.Entry.instInhabitedCell.default }

def Semantics.Evidential.Entry.cell : Entry → Cell

Project a typed Entry to its Aikhenvald paradigm cell.

Equations

• One or more equations did not get rendered due to their size.
• (Semantics.Evidential.Entry.direct { toEvidential := toEvidential, exponent := exponent }).cell = Semantics.Evidential.Entry.Cell.firsthand
• (Semantics.Evidential.Entry.direct { toEvidential := toEvidential, exponent := exponent, source := Semantics.Evidential.DirectSource.visual }).cell = Semantics.Evidential.Entry.Cell.visual
• (Semantics.Evidential.Entry.inferential { toEvidential := toEvidential, exponent := exponent }).cell = Semantics.Evidential.Entry.Cell.inferred
• (Semantics.Evidential.Entry.reportative { toEvidential := toEvidential, exponent := exponent }).cell = Semantics.Evidential.Entry.Cell.reported

Coarse source and perspective

def Semantics.Evidential.Entry.Cell.toCoarseSource : Cell → CoarseSource

Collapse an Aikhenvald cell to its [willett-1988] coarse source.

Equations

• Semantics.Evidential.Entry.Cell.firsthand.toCoarseSource = Semantics.Evidential.CoarseSource.direct
• Semantics.Evidential.Entry.Cell.visual.toCoarseSource = Semantics.Evidential.CoarseSource.direct
• Semantics.Evidential.Entry.Cell.nonvisualSensory.toCoarseSource = Semantics.Evidential.CoarseSource.direct
• Semantics.Evidential.Entry.Cell.auditory.toCoarseSource = Semantics.Evidential.CoarseSource.direct
• Semantics.Evidential.Entry.Cell.inferred.toCoarseSource = Semantics.Evidential.CoarseSource.inference
• Semantics.Evidential.Entry.Cell.assumed.toCoarseSource = Semantics.Evidential.CoarseSource.inference
• Semantics.Evidential.Entry.Cell.reported.toCoarseSource = Semantics.Evidential.CoarseSource.hearsay
• Semantics.Evidential.Entry.Cell.quotative.toCoarseSource = Semantics.Evidential.CoarseSource.hearsay

def Semantics.Evidential.Entry.toCoarseSource : Entry → CoarseSource

The coarse source of an entry: the three Entry kinds are exactly the [willett-1988] tripartition.

Equations

• (Semantics.Evidential.Entry.direct e).toCoarseSource = Semantics.Evidential.CoarseSource.direct
• (Semantics.Evidential.Entry.reportative e).toCoarseSource = Semantics.Evidential.CoarseSource.hearsay
• (Semantics.Evidential.Entry.inferential e).toCoarseSource = Semantics.Evidential.CoarseSource.inference

theorem Semantics.Evidential.Entry.cell_toCoarseSource (e : Entry) : e.cell.toCoarseSource = e.toCoarseSource

The taxonomy tower commutes: collapsing an entry's Aikhenvald cell gives its coarse source.

@[instance_reducible]

instance Semantics.Evidential.instHasCoarseSourceEntry : HasCoarseSource Entry

Inventory entries declare their coarse source; the evidential perspective derives via the canonical source mapping.

Equations

• Semantics.Evidential.instHasCoarseSourceEntry = { toCoarseSource := fun (e : Semantics.Evidential.Entry) => some e.toCoarseSource }

theorem Semantics.Evidential.Entry.isNonfuture (e : Entry) : IsNonfuture e

Every inventory entry is nonfuture: all three coarse sources are causally downstream of the described event (T ≤ A) under the canonical mapping.