Worst-Case Byzantine Recovery Impossibility

Abstract

When no strict honest majority is guaranteed, report vectors cannot deterministically identify a Boolean truth under every allowed attack.

Theorem 1.1 (No deterministic recovery at or below half).

$$\begin{array}{c}\forall n,f\in \mathbb{N},n\le 2\times f\\ \Rightarrow \neg \exists recovery:(\mathrm{Fin}\left(n\right)\to Bool)\to Bool,\\ \forall truth:Bool,reports:\mathrm{Fin}\left(n\right)\to Bool,\\ \mathrm{byzantineCount}\left(reports,truth\right)\le f\Rightarrow recovery(reports)=truth.\end{array}$$

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

Source. Repository-derived.

Commentary.

The report population is indexed by Fin n. The imported byzantineCount primitive counts reports that disagree with the common honest Boolean truth.

Under n at most two f, the proof constructs one report vector within the allowed f disagreements of both truth values. A deterministic rule would have to return false and true on that same vector.

References

• Truth anchor: D5/S3/ConceptDynamics/InstitutionalCapture/ByzantineRecoveryImpossibility.deterministic_recovery_impossible
• Dependency: D5/S3/ConceptDynamics/InstitutionalCapture/ByzantineMajorityRecovery