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.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.

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

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

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

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