Strict Identity Branch Impossibility

Abstract

Two distinct objects cannot both be strictly identical to one object.

Theorem 1.1 (Strict identity cannot branch).

$$\cdot \ne \cdot \Rightarrow \left(\neg \left(\cdot =\cdot \wedge \cdot =\cdot \right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Identity/StrictIdentityBranchImpossibility.strict_identity_branch_impossible (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier and all three objects are independent source primitives. Strict identity is represented by Lean equality itself.

If y and z both equal x, transitivity with the symmetric second equality gives y equal to z, contradicting their distinction.

No exact repository or pinned Mathlib theorem states this full three-object implication, so the proof applies the core equality operations directly.

References

• Truth anchor: D5/S3/ConceptDynamics/Identity/StrictIdentityBranchImpossibility.strict_identity_branch_impossible