F3 — AuditSealed K ↔ ∀ s a a', equalPriorBayesError (K (s, a)) (K (s, a')) = 1/2.
DeclAuditCP.auditSealed_iff_no_binary_decision_advantage
∀ {S : Type uS} {A : Type uA} {Y : Type uY} [inst : Fintype Y] (K : AuditCP.AuditChannel S A Y),
AuditCP.AuditSealed K ↔ ∀ (s : S) (a a' : A), AuditCP.equalPriorBayesError (K (s, a)) (K (s, a')) = 1 / 2TopicAuditing
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6017 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6017
Cite
Verification
- Library
- AuditCP.FiniteBlackwellDecision
- Statement digest
- 739b86a5fd24
- First verified
- 2026-09-24T00:00:00Z