Cycle Collapse Projection

Abstract

Cyclic realization paths collapse to one logical node under an antisymmetric monotone projection.

Theorem 1.1 (Mutual realization paths collapse in a partial order).

$$\begin{array}{c}\forall realEdge:Real\to Real\to Prop,projection:Real\to Logical,first,second:Real,\\ [\mathrm{PartialOrder}\left(Logical\right)],\\ (\mathrm{EdgeMonotoneProjection}\left(realEdge,le,projection\right)\wedge \mathrm{ReflTransGen}\left(realEdge,first,second\right)\wedge \\ \mathrm{ReflTransGen}\left(realEdge,second,first\right))\Rightarrow \\ \mathrm{projection}\left(first\right)=\mathrm{projection}\left(second\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagSemantics/CycleCollapseProjection.cycle_segment_collapses_in_partialOrder (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a partially ordered logical carrier and a projection that sends every realization edge to a nondecreasing logical step. Supply reachable paths in both directions between two realization states.

The projected endpoints are then ordered in both directions, so partial-order antisymmetry identifies them. The theorem does not identify the original states unless projection injectivity is separately assumed.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/CycleCollapseProjection.cycle_segment_collapses_in_partialOrder