Control Identity Refines Passive Identity

Abstract

Adding control actions refines action-induced identity, while passive identity need not recover the full control identity.

Theorem 1.1 (Control identity refines passive identity).

$$\begin{gathered} \forall A,X,Y:Type,P,C:\mathrm{Set}\left(A\right), \\ act:A\to X\to X,obs:X\to Y, \\ P\subseteq C\Rightarrow \mathrm{Refines}\left(I_P,I_C\right)\wedge {\sim }_C\subseteq {\sim }_P. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Control/ControlIdentityRefinesPassive.control_identity_refines_passive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The action identity of a state is the complete family of observed outcomes obtained after applying every action in the chosen set. When every passive action is also a control action, restricting that family from control coordinates to passive coordinates provides the required factor map.

Thus the full-control identity refines the passive identity. Equally, states that agree after every control action must agree after every passive action, so control indistinguishability is contained in passive indistinguishability.

Lemma 1.2 (Passive identity need not recover control identity).

$$\begin{gathered} A=X=Y=Bool,P=\{false\},C=\{false,true\}, \\ act(a,x)=\mathrm{ite}\left(a,x,false\right),obs=id, \\ \Rightarrow P\subseteq C\wedge \mathrm{Refines}\left(I_P,I_C\right)\wedge \neg \mathrm{Refines}\left(I_C,I_P\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Control/ControlIdentityRefinesPassive.reverse_control_refinement_can_fail (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the two-state Boolean system, the sole passive action resets every state to false, whereas the additional control action preserves the state. The passive readout therefore identifies false and true, but the control readout separates them. Forward refinement still holds, while no factor map can reconstruct the control identity from the passive one.

References

• Truth anchor: D5/S3/ConceptDynamics/Control/ControlIdentityRefinesPassive.control_identity_refines_passive
• Truth anchor: D5/S3/ConceptDynamics/Control/ControlIdentityRefinesPassive.reverse_control_refinement_can_fail
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/OperationalOntology/ActionExpansionIndistinguishability