Alexandrov Inseparability

Abstract

Upper-Alexandrov inseparability is mutual reachability and antisymmetry.

Theorem 1.1 (Upper-Alexandrov inseparability is mutual relatedness).

$$\begin{gathered} \forall relation:V\to V\to \mathrm{Prop},x,y:V, \\ [\mathrm{Refl}\left(relation\right)][\mathrm{IsTrans}\left(V,relation\right)]\Rightarrow \\ (\mathrm{Inseparable}\left(\mathrm{upperSetTopology}\left(relation\right),x,y\right)⟺relation(x,y)\wedge relation(y,x)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.upper_inseparable_iff_mutual (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equip a carrier with the topology of sets that are upward closed for a reflexive and transitive relation.

The principal upset of either point is open. Inseparability forces each point into the other’s principal upset, giving both relation directions.

Conversely, mutual relatedness transports membership through every upper-open set in both directions, so no open set separates the points.

Theorem 1.2 (Antisymmetry is equality of inseparable points).

$$\begin{gathered} \forall relation:V\to V\to \mathrm{Prop}, \\ [\mathrm{Refl}\left(relation\right)][\mathrm{IsTrans}\left(V,relation\right)]\Rightarrow \\ ((\forall x,y:V,(relation(x,y)\wedge relation(y,x))\Rightarrow x=y)⟺(\forall x,y:V,\mathrm{Inseparable}\left(\mathrm{upperSetTopology}\left(relation\right),x,y\right)\Rightarrow x=y)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.antisymmetric_iff_inseparable_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the displayed reflexivity and transitivity instances, the preceding characterization identifies inseparability with two opposing relation steps.

The relation is antisymmetric exactly when every such mutually related, and hence inseparable, pair is equal.

Theorem 1.3 (Acyclic dependency topology separates distinct points).

$$\begin{gathered} \forall edge:V\to V\to \mathrm{Prop},x,y:V, \\ (\mathrm{AcyclicEdge}\left(edge\right)\wedge \mathrm{Inseparable}\left(\mathrm{dependencyTopology}\left(edge\right),x,y\right))\Rightarrow x=y. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.dependency_inseparable_implies_eq_of_acyclic (✓ std3). ∎

Source. Repository-derived.

Commentary.

Dependency reachability is reflexive and transitive. Acyclicity makes it antisymmetric because opposing nontrivial paths would compose to a cycle.

Therefore two points inseparable in the dependency Alexandrov topology must coincide.

References

• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.antisymmetric_iff_inseparable_eq
• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.dependency_inseparable_implies_eq_of_acyclic
• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovInseparability.upper_inseparable_iff_mutual
• Dependency: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovDependencyTopology