Mathesis

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

F2 — given A nonempty, BlackwellEquivalent (learnerExperiment K) publicOnlyExperiment ↔ AuditSealed K (blackwell1953).

DeclAuditCP.blackwellEquivalent_publicOnly_iff_auditSealed

∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellEquivalent (AuditCP.learnerExperiment K) AuditCP.publicOnlyExperiment ↔ AuditCP.AuditSealed K

TopicAuditing

ThesisStepDefinition

DeclAuditCP.blackwellEquivalent_publicOnly_iff_auditSealedDeclaration kindtheorem
```
∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellEquivalent (AuditCP.learnerExperiment K) AuditCP.publicOnlyExperiment ↔ AuditCP.AuditSealed K
```
AuditCP.AuditChannel AuditCP.AuditSealed AuditCP.BlackwellBelow AuditCP.BlackwellEquivalent AuditCP.learnerExperiment AuditCP.publicOnlyExperiment
Uses
- AuditCP.learner_blackwellBelow_publicOnly_iff_auditSealed
- AuditCP.publicOnly_blackwellBelow_learner
DeclAuditCP.publicOnly_blackwellBelow_learnerDeclaration kindtheorem
F2a — public information is Blackwell-below the complete learner view: BlackwellBelow publicOnlyExperiment (learnerExperiment K).
```
∀ {S : Type uS} {A : Type uA} {Y : Type uY} (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellBelow AuditCP.publicOnlyExperiment (AuditCP.learnerExperiment K)
```
AuditCP.AuditChannel AuditCP.AuditExperiment AuditCP.BlackwellBelow AuditCP.learnerExperiment AuditCP.publicOnlyExperiment
Used by
- AuditCP.blackwellEquivalent_publicOnly_iff_auditSealed
DeclAuditCP.learner_blackwellBelow_publicOnly_iff_auditSealedDeclaration kindtheorem
F2b — given A nonempty, BlackwellBelow (learnerExperiment K) publicOnlyExperiment ↔ AuditSealed K (blackwell1953).
```
∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellBelow (AuditCP.learnerExperiment K) AuditCP.publicOnlyExperiment ↔ AuditCP.AuditSealed K
```
AuditCP.AuditChannel AuditCP.AuditExperiment AuditCP.AuditSealed AuditCP.BlackwellBelow AuditCP.FactorsThroughPublic AuditCP.learnerExperiment AuditCP.publicOnlyExperiment
Uses
- AuditCP.auditSealed_iff_factorsThroughPublic
- AuditCP.pmf_map_publicTag_injective
Used by
- AuditCP.blackwellEquivalent_publicOnly_iff_auditSealed
DeclAuditCP.pmf_map_publicTag_injectiveDeclaration kindtheorem
Pushing a PMF on Y through the tag y ↦ (s, y) is injective.
```
∀ {S : Type uS} {Y : Type uY} (s : S), Function.Injective fun p => PMF.map (fun y => (s, y)) p
```
Used by
- AuditCP.learner_blackwellBelow_publicOnly_iff_auditSealed
DeclAuditCP.auditSealed_iff_factorsThroughPublicDeclaration kindtheorem
F1 — given A nonempty, AuditSealed K ↔ FactorsThroughPublic K.
```
∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.AuditSealed K ↔ AuditCP.FactorsThroughPublic K
```
AuditCP.AuditChannel AuditCP.AuditExperiment AuditCP.AuditSealed AuditCP.FactorsThroughPublic
Used by
- AuditCP.learner_blackwellBelow_publicOnly_iff_auditSealed
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.AuditExperimentdef
B5 — AuditExperiment Θ X is the type of parameter-indexed discrete observation laws Θ → PMF X.
```
AuditCP.AuditIndex → AuditCP.AuditIndex → Type (max u v)
```
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.BlackwellBelowdef
E₀ is Blackwell-below E₁ when some garbling G of E₁'s output reproduces E₀: ∃ G, ∀ θ, E₀ θ = (E₁ θ).bind G (blackwell1953).
```
{Θ : Type uΘ} → {X₀ : Type uX₀} → {X₁ : Type uX₁} → AuditCP.AuditExperiment Θ X₀ → AuditCP.AuditExperiment Θ X₁ → Prop
```

DefinitionAuditCP.BlackwellEquivalentdef

E₀ and E₁ are Blackwell-equivalent when each is Blackwell-below the other (blackwell1953).

{Θ : Type uΘ} → {X₀ : Type uX₀} → {X₁ : Type uX₁} → AuditCP.AuditExperiment Θ X₀ → AuditCP.AuditExperiment Θ X₁ → Prop

DefinitionAuditCP.FactorsThroughPublicdef
The channel K factors through the public coordinate: ∃ H, ∀ s a, K (s, a) = H s.
```
{S : Type uS} → {A : Type uA} → {Y : Type uY} → AuditCP.AuditChannel S A Y → Prop
```
DefinitionAuditCP.learnerExperimentdef
The channel revealing the public state together with K's output, fun sa => (K sa).map (fun y => (sa.1, y)).
```
{S : Type uS} → {A : Type uA} → {Y : Type uY} → AuditCP.AuditChannel S A Y → AuditCP.AuditChannel S A (S × Y)
```
DefinitionAuditCP.publicOnlyExperimentdef
The channel revealing exactly the public state s and nothing else, fun (s, a) => PMF.pure s.
```
{S : Type uS} → {A : Type uA} → AuditCP.AuditChannel S A S
```

DOIMTH.R-2026-6016

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: 304b019f2077
Verified: 2026-09-24T00:00:00Z