Action Loop Requires Memory

Abstract

A policy-visible loop effect requires nontrivial memory transport.

Theorem 1.1 (Policy change implies memory change).

$$\forall x3\in \left(\forall x3\in \cdot ,\forall x4\in \cdot ,\cdot \right),\forall x4\in \cdot ,\forall x5\in \left(\forall x5\in \cdot ,\cdot \right),\forall x6\in \cdot ,x3\left(x4,x5\left(x6\right)\right)\ne x3\left(x4,x6\right)\Rightarrow x5\left(x6\right)\ne x6$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/ActionLoopRequiresMemory.policy_change_implies_memory_change (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a question, memory state, memory transport, and policy. Assume the transport changes the policy’s selected action.

If the transported memory were unchanged, the two policy evaluations would coincide. The visible action change therefore forces a memory change.

Theorem 1.2 (An injective policy coordinate detects memory change).

$$\begin{gathered} \forall policy:Q\to \left(M\to A\right),q:Q,h:M\to M,m:M, \\ (\mathrm{Injective}\left(\mathrm{policy}\left(q\right)\right)\wedge h\left(m\right)\ne m)\Rightarrow \mathrm{policy}\left(q,h\left(m\right)\right)\ne \mathrm{policy}\left(q,m\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/ActionLoopRequiresMemory.injective_policy_detects_memory_change (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the converse direction, assume the policy at the chosen question is injective as a function of memory.

A nontrivial memory transport must then change the selected action at that memory state. No injectivity is assumed at other questions.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/ActionLoopRequiresMemory.injective_policy_detects_memory_change
• Truth anchor: D5/S3/Observer/AgencyHolonomy/ActionLoopRequiresMemory.policy_change_implies_memory_change