Action Graph Communication Bound

Abstract

Cumulative cost on a finite deterministic action graph is bounded exactly when every closed action word has zero cost.

Definition 1.1 (Finite action words determine terminal states).

$$\begin{array}{c}\forall Q,\mathcal{F},T:\mathcal{F}\to \left(Q\to Q\right),\\ \forall m\in Q,\mathrm{runWord}(T,[],m)=m,\\ \forall f\in \mathcal{F},\forall u\in \mathrm{List}(\mathcal{F}),\mathrm{runWord}(T,\mathrm{cons}(f,u),m)=\mathrm{runWord}(T,u,T(f,m)).\end{array}$$

Formalization. D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality.runWord (✓ std3).

Source. Repository-derived.

Commentary.

Starting at m, the empty word leaves the state unchanged. Executing a word whose first action is f first applies the deterministic transition T_f and then executes the remaining word.

Definition 1.2 (Finite-word communication is the sum of step costs).

$$\begin{array}{c}\forall Q,\mathcal{F},T:\mathcal{F}\to \left(Q\to Q\right),w:Q\to \left(\mathcal{F}\to \mathbb{N}\right),\\ \forall m\in Q,\mathrm{Comm}(T,w,m,[])=0,\\ \forall f\in \mathcal{F},\forall u\in \mathrm{List}(\mathcal{F}),\mathrm{Comm}(T,w,m,\mathrm{cons}(f,u))=w(m,f)+\mathrm{Comm}(T,w,T(f,m),u).\end{array}$$

Formalization. D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.Comm (✓ std3).

Source. Repository-derived.

Commentary.

The empty word costs zero. A nonempty word pays the cost of its first labelled edge and then pays the cost of the remaining execution from the successor state.

Definition 1.3 (Infinite-word communication is a prefix supremum).

$$\begin{gathered} \forall Q,\mathcal{F},T:\mathcal{F}\to \left(Q\to Q\right),w:Q\to \left(\mathcal{F}\to \mathbb{N}\right), \\ \forall m\in Q,\forall \omega :\mathbb{N}\to \mathcal{F}, \\ \mathrm{InfiniteComm}(T,w,m,\omega )={\sup }_{n\ge 0}\mathrm{Comm}(T,w,m,\mathrm{prefix}(\omega ,n))\in \mathrm{ENat}. \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.InfiniteComm (✓ std3).

Source. Repository-derived.

Commentary.

The total cost of an infinite action word is the supremum in the extended natural numbers of the costs of all its finite prefixes.

Definition 1.4 (The finite supremum of edge costs).

$$\begin{gathered} \forall Q,\mathcal{F},[\mathrm{Fintype}Q],[\mathrm{Fintype}\mathcal{F}],w:Q\to \left(\mathcal{F}\to \mathbb{N}\right), \\ \mathrm{maxEdgeCost}(w)={\sup }_{m\in Q,f\in \mathcal{F}}w(m,f). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.maxEdgeCost (✓ std3).

Source. Repository-derived.

Commentary.

For finite state and action carriers, W_max is the finite supremum of all labelled-edge costs; its value is zero if either carrier is empty.

Theorem 1.5 (Cumulative communication criterion).

$$\begin{array}{c}\forall Q,\mathcal{F}:\mathrm{Type},[\mathrm{Fintype}Q],[\mathrm{Nonempty}Q],\\ [\mathrm{Fintype}\mathcal{F}],[\mathrm{Nonempty}\mathcal{F}],I:\mathrm{Set}(Q),\\ T:\mathcal{F}\to \left(Q\to Q\right),w:Q\to \left(\mathcal{F}\to \mathbb{N}\right),\\ \forall m\in Q,\exists m_0\in I,\exists p\in \mathrm{List}(\mathcal{F}),\mathrm{runWord}(T,p,m_0)=m,\\ W_{max}=\mathrm{maxEdgeCost}(w),\\ a:\forall m_0\in I,\forall \omega :\mathbb{N}\to \mathcal{F},\mathrm{InfiniteComm}(T,w,m_0,\omega )\ne \infty ,\\ b:\exists B\in \mathbb{N},\forall m_0\in I,\forall u\in \mathrm{List}(\mathcal{F}),\mathrm{Comm}(T,w,m_0,u)\le B,\\ c:\forall m\in Q,\forall v\in \mathrm{List}(\mathcal{F}),v\ne []\wedge \mathrm{runWord}(T,v,m)=m\Rightarrow \mathrm{Comm}(T,w,m,v)=0,\\ List.TFAE([a,b,c])\wedge \\ (c\Rightarrow \forall m_0\in I,\forall u\in \mathrm{List}(\mathcal{F}),\mathrm{Comm}(T,w,m_0,u)\le (\mathrm{card}(Q)-1)W_{max}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.cumulative_communication_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Q and the action alphabet be finite and nonempty. Let I be a set of initial states, and assume every state is reached from I by some finite action word; since the state type is nonempty, I is then nonempty. Then finite total cost for every infinite execution, one common bound for all finite executions from I, and zero cost for every nonempty closed action word are equivalent.

If the cycle condition holds, remove a closed segment whenever an execution repeats a state. The segment has zero cost and its deletion preserves the state from which the suffix runs. Iteration leaves a path with no repeated state, hence at most card(Q)-1 edges, and each edge costs at most W_max.

Conversely, a reachable positive-cost cycle can be repeated after a prefix leading to it. Determinism returns to the same state after each copy, so its prefix costs are unbounded. A common finite-word bound directly bounds every infinite-word prefix supremum.

References

• Truth anchor: D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.Comm
• Truth anchor: D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.InfiniteComm
• Truth anchor: D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.cumulative_communication_criterion
• Truth anchor: D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound.maxEdgeCost
• Truth anchor: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality.runWord
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality