Agency Completion Minimality

Abstract

Componentwise recoverability induces recoverability of the paired agency completion.

Theorem 1.1 (Component factorizations induce a paired factorization).

$$\begin{gathered} \forall current:H\to M,profile:H\to P, \\ summary:H\to S,currentFactor:S\to M, \\ profileFactor:S\to P, \\ (\forall h:H,\mathrm{current}\left(h\right)=\mathrm{currentFactor}\left(\mathrm{summary}\left(h\right)\right)\wedge \forall h:H,\mathrm{profile}\left(h\right)=\mathrm{profileFactor}\left(\mathrm{summary}\left(h\right)\right))\Rightarrow \exists pairFactor:S\to \mathrm{Prod}\left(M,P\right),h\mapsto (\mathrm{current}\left(h\right),\mathrm{profile}\left(h\right))=pairFactor\circ summary. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Assume both the current-memory readout and the strategy profile factor pointwise through the same summary.

Pair the two supplied factor maps. This yields a factor from summaries to memory-profile pairs through which the paired completion equals the composite with the summary.

The conclusion asserts existence of that paired factor; it does not claim uniqueness or a converse factorization.

Theorem 1.2 (The paired completion recovers both components).

$$\forall current:H\to M,profile:H\to P,(h\mapsto \mathrm{fst}\left(\mathrm{pair}\left(\mathrm{current}\left(h\right),\mathrm{profile}\left(h\right)\right)\right)=current\wedge h\mapsto \mathrm{snd}\left(\mathrm{pair}\left(\mathrm{current}\left(h\right),\mathrm{profile}\left(h\right)\right)\right)=profile).$$

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

Source. Repository-derived.

Commentary.

For arbitrary current and profile readouts, pair their values at each history.

The first and second product projections recover the current and profile functions respectively, with no extra assumptions.

References

• Truth anchor: D5/S3/Observer/AgencySelf/AgencyCompletionMinimality.paired_completion_factors_through_summary
• Truth anchor: D5/S3/Observer/AgencySelf/AgencyCompletionMinimality.paired_completion_recovers_components