Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

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 / 2

TopicAuditing

ThesisStepDefinition

DeclAuditCP.auditSealed_iff_no_binary_decision_advantageDeclaration kindtheorem

∀ {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 / 2

AuditCP.AuditChannel AuditCP.AuditSealed AuditCP.equalPriorBayesError

Uses

AuditCP.equalPriorBayesError_eq_half_iff

DeclAuditCP.equalPriorBayesError_eq_half_iffDeclaration kindtheorem
F3b — equalPriorBayesError p q = 1/2 ↔ p = q.
```
∀ {Y : Type uY} [inst : Fintype Y] (p q : PMF Y), AuditCP.equalPriorBayesError p q = 1 / 2 ↔ p = q
```
AuditCP.equalPriorBayesError AuditCP.finiteTotalVariation
Uses
- AuditCP.equalPriorBayesError_eq_half_one_sub_tv
- AuditCP.finiteTotalVariation_eq_zero_iff
Used by
- AuditCP.auditSealed_iff_no_binary_decision_advantage
DeclAuditCP.finiteTotalVariation_eq_zero_iffDeclaration kindtheorem
finiteTotalVariation p q = 0 ↔ p = q.
```
∀ {Y : Type uY} [inst : Fintype Y] (p q : PMF Y), AuditCP.finiteTotalVariation p q = 0 ↔ p = q
```
AuditCP.finiteTotalVariation AuditCP.pmfMass
Used by
- AuditCP.equalPriorBayesError_eq_half_iff
DeclAuditCP.equalPriorBayesError_eq_half_one_sub_tvDeclaration kindtheorem
F3a — equalPriorBayesError p q = (1 - finiteTotalVariation p q) / 2.
```
∀ {Y : Type uY} [inst : Fintype Y] (p q : PMF Y),
  AuditCP.equalPriorBayesError p q = (1 - AuditCP.finiteTotalVariation p q) / 2
```
AuditCP.equalPriorBayesError AuditCP.finiteTotalVariation AuditCP.pmfMass
Uses
- AuditCP.min_eq_add_sub_abs_div_two
- AuditCP.sum_pmfMass_eq_one
Used by
- AuditCP.equalPriorBayesError_eq_half_iff
DeclAuditCP.sum_pmfMass_eq_oneDeclaration kindtheorem
On a finite type, the real point masses of p sum to 1.
```
∀ {Y : Type uY} [inst : Fintype Y] (p : PMF Y), ∑ y, AuditCP.pmfMass p y = 1
```
AuditCP.pmfMass
Used by
- AuditCP.equalPriorBayesError_eq_half_one_sub_tv
DeclAuditCP.min_eq_add_sub_abs_div_twoDeclaration kindtheorem
min x y = (x + y - |x - y|) / 2.
```
∀ (x y : ℝ), min x y = (x + y - |x - y|) / 2
```
Used by
- AuditCP.equalPriorBayesError_eq_half_one_sub_tv
DefinitionAuditCP.AuditChanneldef
B6 — AuditChannel S A Y is AuditExperiment (S × A) Y, an experiment whose parameter is split into a public coordinate S and an audit coordinate A.
```
AuditCP.AuditIndex → AuditCP.AuditIndex → AuditCP.AuditIndex → Type (max u v w)
```
DefinitionAuditCP.AuditSealeddef
The channel K is audit-sealed: its output law at fixed public state s does not depend on the audit state a.
```
{S : Type uS} → {A : Type uA} → {Y : Type uY} → AuditCP.AuditChannel S A Y → Prop
```
DefinitionAuditCP.equalPriorBayesErrordef
The equal-prior Bayes error between p and q, (1/2) * ∑ y, min (pmfMass p y) (pmfMass q y).
```
{Y : Type uY} → [Fintype Y] → PMF Y → PMF Y → ℝ
```
DefinitionAuditCP.finiteTotalVariationdef
The total variation distance between p and q, half the ℓ¹ distance of their point masses, (1/2) * ∑ y, |pmfMass p y - pmfMass q y|.
```
{Y : Type uY} → [Fintype Y] → PMF Y → PMF Y → ℝ
```
DefinitionAuditCP.pmfMassdef
The real-valued point mass of y under the Mathlib PMF p, (p y).toReal.
```
{Y : Type uY} → PMF Y → Y → ℝ
```

DOIMTH.R-2026-6017

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 2b5c97530787
Verified: 2026-09-24T00:00:00Z