Public Unlinkability and Accountability Incompatibility

Abstract

Nontrivial identity makes public unlinkability incompatible with complete accountability.

Theorem 1.1 (Public unlinkability and complete accountability are incompatible).

$$\begin{gathered} \forall X,B_P,B_I:\mathrm{Type}, \\ P:X\to B_P,I:X\to B_I, \\ \exists x,y:X,I(x)\ne I(y)\Rightarrow \\ \neg \mathrm{commonCoreRelation}(P,I)=top\wedge \mathrm{Refines}(I,P). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InstitutionalCapture/PublicUnlinkabilityAccountabilityIncompatibility.public_unlinkability_accountability_incompatible (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let P be a public transcript and I an identity readout on the same source carrier. Identity is nontrivial when two source states have different identity readouts.

Structural public unlinkability says the canonical common-core relation of P and I is the top setoid, so its common coarsening is trivial. Complete public accountability says I factors through P via the canonical Refines relation.

The displayed conclusion publicly negates the conjunction of these two clauses. It imports the existing common-core construction and applies its obstruction theorem without redeclaring either family primitive.

References

• Truth anchor: D5/S3/ConceptDynamics/InstitutionalCapture/PublicUnlinkabilityAccountabilityIncompatibility.public_unlinkability_accountability_incompatible
• Dependency: D5/S3/ConceptDynamics/Interventions/CommonCoreForgettingObstruction