Agency Residual Witness

Abstract

A hidden strategy difference is a concrete witness of agency residual.

Theorem 1.1 (A hidden strategy difference is residual).

$$\begin{gathered} \forall current:H\to M,profile:H\to P,x,y:H, \\ (\mathrm{current}\left(x\right)=\mathrm{current}\left(y\right)\wedge \mathrm{profile}\left(x\right)\ne \mathrm{profile}\left(y\right))\Rightarrow \mathrm{AgencyResidual}\left(current,profile,x,y\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencySelf/AgencyResidualWitness.hidden_strategy_difference_is_residual (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume two histories have the same current-memory value but different strategy-profile values.

These two displayed facts are exactly the defining components of an agency-residual witness for that pair.

Theorem 1.2 (A residual pair is separated by the paired readout).

$$\begin{gathered} \forall current:H\to M,profile:H\to P,x,y:H, \\ \mathrm{AgencyResidual}\left(current,profile,x,y\right)\Rightarrow \mathrm{pair}\left(\mathrm{current}\left(x\right),\mathrm{profile}\left(x\right)\right)\ne \mathrm{pair}\left(\mathrm{current}\left(y\right),\mathrm{profile}\left(y\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencySelf/AgencyResidualWitness.residual_separated_by_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume the displayed pair lies in the agency residual.

Equality of the paired memory-profile values would imply equality of their profile components, contradicting the residual witness.

References

• Truth anchor: D5/S3/Observer/AgencySelf/AgencyResidualWitness.hidden_strategy_difference_is_residual
• Truth anchor: D5/S3/Observer/AgencySelf/AgencyResidualWitness.residual_separated_by_pair