Complete Inputs Exclude Deterministic Disagreement

Abstract

Deterministic disagreement exposes a difference in at least one complete input.

Theorem 1.1 (Complete input agreement excludes deterministic disagreement).

$$\begin{gathered} I_l=(C_l,b_l,A_l,{\beta }_l,V_l,U_l,s_l,x_l), \\ {I}_r=(C_r,b_r,A_r,{\beta }_r,V_r,U_r,s_r,x_r), \\ \forall I,u,v,(D(I,u)\wedge D(I,v))\Rightarrow u=v, \\ D(I_l,u_l)\wedge D(I_r,u_r) \\ \Rightarrow [((C_l=C_r\wedge b_l=b_r\wedge A_l=A_r\wedge {\beta }_l={\beta }_r\wedge V_l=V_r\wedge U_l=U_r\wedge s_l=s_r\wedge x_l=x_r)\Rightarrow u_l=u_r) \\ \wedge (u_l\ne u_r\Rightarrow C_l\ne C_r\vee b_l\ne b_r\vee A_l\ne A_r\vee {\beta }_l\ne {\beta }_r\vee V_l\ne V_r\vee U_l\ne U_r\vee s_l\ne s_r\vee x_l\ne x_r)]. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValue/CompleteInputDeterminism.complete_input_agreement_excludes_deterministic_disagreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each decision input is constructed from the evidence concept and value, admission predicate, inference relation, value channel, action set, random seed, and actual anchor supplied by the source.

The decisioner is a relation whose right uniqueness is a public premise. Thus determinism is not installed by defining the decisioner as a function or by defining its inputs through the conclusion.

Right uniqueness proves agreement when all eight components coincide. The second public conjunct is its componentwise contrapositive: unequal related decisions identify at least one unequal input layer.

The qualitative remark about ease of resolving disagreement has no source predicate and is not asserted as a universal theorem.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValue/CompleteInputDeterminism.complete_input_agreement_excludes_deterministic_disagreement
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition