Empirical Identifiability

Abstract

Protocol outcomes determine exactly which model properties descend uniquely.

Theorem 1.1 (Empirical quotient descent and residual obstruction).

$\forall P, T h e t a, Y, O u t : P \to T h e t a \to Type, T : T h e t a \to Y, ((\exists! d : T h e t a_{e m p} \to Y, T (t h e t a) = d (c l a ss (t h e t a))) ⟺ (\forall t h e t a, t h e t a P r im e, (\forall P, O u t (P) (t h e t a) = O u t (P) (t h e t a P r im e)) \Rightarrow T (t h e t a) = T (t h e t a P r im e))) \land ((\exists t h e t a, t h e t a P r im e, (\forall P, O u t (P) (t h e t a) = O u t (P) (t h e t a P r im e)) \land T (t h e t a) \neq = T (t h e t a P r im e)) \Rightarrow \neg\exists d : T h e t a_{e m p} \to Y, T (t h e t a) = d \circ c l a ss) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/EmpiricalIdentifiability.empirical_identifiability (✓ std3). ∎

Source. Repository-derived.

Commentary.

The empirical setoid is constructed from equality of every allowed protocol outcome, and the quotient and class map are the canonical ones for that source relation.

A property descends to exactly one quotient map precisely when it is constant on every empirical-equivalence fiber. An empirically equivalent pair with different property values rules out every possible quotient factor.

Pinned quotient constructors were applied directly; no source object is defined as the target conclusion.

References

Truth anchor: D5/S3/ConceptDynamics/EmpiricalIdentifiability.empirical_identifiability

Keyboard shortcuts

trureturing Blueprint

Empirical Identifiability

Abstract

References