Epistemic Change Trichotomy

Abstract

Fixed-world conclusion changes expose an admission, evidence, or inference change.

Theorem 1.1 (Changed conclusions expose an epistemic component).

$$\forall x5\in \cdot ,\forall x6\in \cdot ,\forall x7\in \left(\forall x7\in \cdot ,\mathrm{Type}\right),\forall x8\in \left(\forall x8\in \cdot ,\mathrm{Type}\right),\forall x9\in \left(\forall x9\in \cdot ,\cdot \right),\forall x10\in \left(\forall x10\in \cdot ,\cdot \right),\forall x11\in \left(\forall x11\in \cdot ,\cdot \right),\forall x12\in \left(\forall x12\in \cdot ,\cdot \right),\forall x13\in \left(\forall x13\in \left(\forall x13\in \cdot ,\mathrm{Type}\right),\forall x14\in \left(\forall x14\in \cdot ,\cdot \right),\forall x15\in \left(\forall x15\in \cdot ,\cdot \right),\forall x16\in \cdot ,\cdot \right),x5=x6\Rightarrow \left(x13\left(x7,x9,x11,x5\right)\ne x13\left(x8,x10,x12,x6\right)\Rightarrow \left(x7\ne x8\vee \left(x9\ne x10\vee x11\ne x12\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Epistemic/EpistemicChangeTrichotomy.changed_conclusion_exposes_epistemic_component (✓ std3). ∎

Source. Repository-derived.

Commentary.

The admission predicates, evidence concepts, inference rules, worlds, and conclusion evaluator are independent source primitives.

The public fixed-world premise holds the underlying state constant. If every component were also equal, deterministic evaluation would force equal conclusions, contradicting the other premise.

The three public alternatives directly audit a change to admissible worlds, evidence distinctions, or the inference rule; no target-defined state structure or private classification is used.

References

• Truth anchor: D5/S3/ConceptDynamics/Epistemic/EpistemicChangeTrichotomy.changed_conclusion_exposes_epistemic_component