Reachable Behavior Core

Abstract

The reachable future-behavior quotient is reached, separated by future protocols, stable under protocol prefixes, and universal among reachable realizations.

Theorem 1.1 (The reachable behavior quotient has all four core properties).

$$\begin{array}{c}\forall M:\mathrm{Type},X:\mathrm{Type},B:\mathrm{Type},\\ [\mathrm{Monoid}(M)],[\mathrm{MulAction}(M,X)],a:X,O:X\to B,\\ (\mathrm{Surjective}\left((m\mapsto \mathrm{behaviorClass}\left(a,O,m\right))\right))\wedge (\forall z1:\mathrm{ReachableBehaviorQuotient}\left(M,a,O\right),z2:\mathrm{ReachableBehaviorQuotient}\left(M,a,O\right),z1\ne z2\Rightarrow \exists c:M,\mathrm{kerLift}\left(\mathrm{futureBehavior}\left(a,O\right),z1,c\right)\ne \mathrm{kerLift}\left(\mathrm{futureBehavior}\left(a,O\right),z2,c\right))\wedge \\ (\forall p:M,\exists !U:\mathrm{ReachableBehaviorQuotient}\left(M,a,O\right)\to \mathrm{ReachableBehaviorQuotient}\left(M,a,O\right),\forall m:M,U\left(\mathrm{behaviorClass}\left(a,O,m\right)\right)=\mathrm{behaviorClass}\left(a,O,p\cdot m\right))\wedge \\ (\forall Xprime:\mathrm{Type},[\mathrm{MulAction}(M,Xprime)],aprime:Xprime,Oprime:Xprime\to B,\\ (\forall xprime:Xprime,\exists m:M,m\cdot aprime=xprime)\wedge (\forall m:M,\mathrm{Oprime}\left(m\cdot aprime\right)=O\left(m\cdot a\right))\Rightarrow \exists !h:Xprime\to \mathrm{ReachableBehaviorQuotient}\left(M,a,O\right),\mathrm{Surjective}\left(h\right)\wedge (\forall m:M,h\left(m\cdot aprime\right)=\mathrm{behaviorClass}\left(a,O,m\right))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/PredictionFactors/ReachableBehaviorCore.reachable_behavior_core (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a monoid of allowed protocols act on a state carrier from an actual anchor, and let O be the public readout. The target is the existing quotient of reachable states by equality of every future readout.

Every quotient class is produced by an allowed protocol. Injectivity of the kernel lift makes distinct classes differ at some continuation, and left multiplication constructs the unique update induced by each protocol prefix.

For every other reachable action carrier with the same anchor behavior, there is a unique surjection to the quotient, determined on every orbit point by its canonical behavior class.

References

• Truth anchor: D5/S3/ObserverMemory/PredictionFactors/ReachableBehaviorCore.reachable_behavior_core
• Dependency: D5/S3/ObserverMemory/PredictionFactors/CanonicalReachableBehaviorFactor
• Dependency: D5/S3/ObserverMemory/PredictionFactors/ReachableBehaviorClassSurjectivity