Public Recovery Criterion

Abstract

Public recovery through an additive observation is equivalent to kernel containment and to vanishing covert transport; adding a ledger can only shrink the covert image.

Theorem 1.1 (Public recovery, kernel containment, and ledger refinement).

$$\begin{array}{c}\forall U,P,\mathcal{K},\Lambda :Type,\\ \mathrm{AddGroup}\left(U\right)\wedge \mathrm{AddGroup}\left(P\right)\wedge \mathrm{AddGroup}\left(\mathcal{K}\right)\wedge \mathrm{AddGroup}\left(\Lambda \right)\wedge \\ H:\mathrm{AddMonoidHom}\left(U,P\right)\wedge K:\mathrm{AddMonoidHom}\left(U,\mathcal{K}\right)\wedge L:\mathrm{AddMonoidHom}\left(U,\Lambda \right)\Rightarrow \\ \left(\left(\exists \overline{K}:\mathrm{AddMonoidHom}\left(\mathrm{im}\left(H\right),\mathcal{K}\right),K=\overline{K}\circ H\iff \ker \left(H\right)\subseteq \ker \left(K\right)\right)\wedge \left(\left(\ker \left(H\right)\subseteq \ker \left(K\right)\iff \mathrm{image}\left(K,\ker \left(H\right)\right)=0\right)\wedge \left(\mathrm{image}\left(K,\ker \left(H\right)\right)=0\iff \exists \overline{K}:\mathrm{AddMonoidHom}\left(\mathrm{im}\left(H\right),\mathcal{K}\right),K=\overline{K}\circ H\right)\right)\right)\wedge \mathrm{image}\left(K,\mathrm{intersection}\left(\ker \left(H\right),\ker \left(L\right)\right)\right)\subseteq \mathrm{image}\left(K,\ker \left(H\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Agency/PublicRecoveryCriterion.public_recovery_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The control, public, hidden, and ledger carriers are additive groups. The public observation H, hidden transport K, and ledger L are additive homomorphisms, matching the source’s uses of kernels, zero, intersection, and kernel image.

A recovery homomorphism on the realized public image exists exactly when every publicly silent control is also hidden-silent. The covert throat is represented by the additive image K(ker H), so its vanishing is the same kernel condition.

Adding the ledger replaces ker H by ker H intersect ker L. This is a subgroup of ker H, and monotonicity of additive image proves that the remaining covert transport can only shrink.

References

• Truth anchor: D5/S3/Observer/Agency/PublicRecoveryCriterion.public_recovery_criterion