Two Sources of Path Dependence

Abstract

Word order and transition incompatibility independently produce path dependence.

Theorem 1.1 (Word order and gluing supply independent residuals).

$$\begin{array}{r}u:Bool\to \mathrm{Prod}\left(Unit,Bool\right)\to \mathrm{Prod}\left(Unit,Bool\right),\\ \mathrm{apply}\left(u,a,\mathrm{pair}\left(star,b\right)\right)=\mathrm{pair}\left(star,\mathrm{if}\left(a,false,\mathrm{not}\left(b\right)\right)\right),\\ \mathrm{Run}\left(u,\mathrm{word}\left(false,true\right),\mathrm{pair}\left(star,false\right)\right)\ne \mathrm{Run}\left(u,\mathrm{word}\left(true,false\right),\mathrm{pair}\left(star,false\right)\right),\\ addFalse,addTrue:\mathrm{ClosureOperator}\left(\mathrm{Set}\left(Bool\right)\right),transition:\mathrm{OrderIso}\left(\mathrm{Set}\left(Bool\right),\mathrm{Set}\left(Bool\right)\right),\\ \mathrm{apply}\left(addFalse,S\right)=\mathrm{union}\left(S,\mathrm{singleton}\left(false\right)\right),\mathrm{apply}\left(addTrue,S\right)=\mathrm{union}\left(S,\mathrm{singleton}\left(true\right)\right),\\ \mathrm{apply}\left(transition,S\right)=\mathrm{image}\left(\mathrm{swap}\left(false,true\right),S\right),\\ \mathrm{Commute}\left(addFalse,addTrue\right)\wedge \mathrm{apply}\left(transition,\mathrm{apply}\left(addFalse,empty\right)\right)\ne \mathrm{apply}\left(addFalse,\mathrm{apply}\left(transition,empty\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Gluing/PathDependenceSources.path_dependence_has_two_sources (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first witness uses one global product carrier Unit x Bool. Its two actions are applied by the canonical finite-word evaluator, and reversing the two-letter word changes the resulting state.

The second witness uses the powerset of Bool. Adding false and adding true are distinct bundled closure operators and commute locally. The Boolean swap induces a bijective order isomorphism on sets, but it does not intertwine the add-false closure.

References

• Truth anchor: D5/S3/ConceptDynamics/Gluing/PathDependenceSources.path_dependence_has_two_sources
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality