Heterogeneous Fiber Misclassification

Abstract

A message fiber with two target values forces a deterministic error.

Theorem 1.1 (A heterogeneous message fiber forces an error).

$$\begin{array}{c}\forall X,M,Y:\mathrm{Type},\\ M_S:X\to M,T:X\to Y,\\ \forall x,y:X,\\ (M_S(x)=M_S(y)\wedge T(x)\ne T(y))\Rightarrow \\ \forall delta:M\to Y,(delta(M_S(x))\ne T(x)\vee delta(M_S(y))\ne T(y)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Communication/HeterogeneousFiberMisclassification.heterogeneous_fiber_forces_misclassification (✓ std3). ∎

Source. Repository-derived.

Commentary.

The message and target are arbitrary readouts on one state carrier. Two named states witness heterogeneity by sharing a message while having different target values.

Every deterministic inference rule is represented by a function from messages to target values. The public conclusion says directly that its inferred value is wrong at the first witness or at the second witness.

Equal messages force equal inferred values. If both inferences were correct, equality transport would contradict the displayed target inequality.

References

• Truth anchor: D5/S3/ConceptDynamics/Communication/HeterogeneousFiberMisclassification.heterogeneous_fiber_forces_misclassification
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition