Mathesis

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

If every candidate's loss is measurable and a.e. valued in [a, b] under Q, every training-generated trajectory is admissible for F, and the resulting uniform-deviation failure event is measurable, then on an i.i.d. panel of size n drawn from Q, measured cumulative empirical-loss progress exceeds population-loss progress by more than 2 · deltaFiniteExperts (card ι) n (b - a) δ with probability at most ENNReal.ofReal δ.

DeclAuditCP.auditBlind_finiteTrajectory_goodhart

∀ {Ωtrain : Type u_1} {Z : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain] [inst_1 : MeasurableSpace Z]
  [inst_2 : Fintype ι] [Nonempty ι] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
  (Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
  0 < n →
    ∀ (a b : ℝ),
      a < b →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (loss : ι → Z → ℝ),
                (∀ (i : ι), Measurable (loss i)) →
                  (∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
                    ∀ (F : Ωtrain → AuditCP.AuditEnvelope ι) (g : Ωtrain → AuditCP.AuditTrajectory ι),
                      (∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)) →
                        MeasurableSet
                            {p |
                              ¬AuditCP.UniformDev (F p.1) (fun i => AuditCP.empiricalLoss loss i p.2)
                                  (fun i => AuditCP.populationLoss Q loss i)
                                  (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)} →
                          ∀ (T : ℕ),
                            (MeasureTheory.Measure.prod μtrain (MeasureTheory.Measure.pi fun x => Q))
                                {p |
                                  AuditCP.cumCP (fun i => AuditCP.empiricalLoss loss i p.2) (g p.1) T >
                                    AuditCP.cumCP (fun i => AuditCP.populationLoss Q loss i) (g p.1) T +
                                      2 * AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ} ≤
                              ENNReal.ofReal δ

TopicAuditing

ThesisStepHypothesisDefinition

DeclAuditCP.auditBlind_finiteTrajectory_goodhartDeclaration kindtheorem

∀ {Ωtrain : Type u_1} {Z : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain] [inst_1 : MeasurableSpace Z]
  [inst_2 : Fintype ι] [Nonempty ι] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
  (Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
  0 < n →
    ∀ (a b : ℝ),
      a < b →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (loss : ι → Z → ℝ),
                (∀ (i : ι), Measurable (loss i)) →
                  (∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
                    ∀ (F : Ωtrain → AuditCP.AuditEnvelope ι) (g : Ωtrain → AuditCP.AuditTrajectory ι),
                      (∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)) →
                        MeasurableSet
                            {p |
                              ¬AuditCP.UniformDev (F p.1) (fun i => AuditCP.empiricalLoss loss i p.2)
                                  (fun i => AuditCP.populationLoss Q loss i)
                                  (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)} →
                          ∀ (T : ℕ),
                            (MeasureTheory.Measure.prod μtrain (MeasureTheory.Measure.pi fun x => Q))
                                {p |
                                  AuditCP.cumCP (fun i => AuditCP.empiricalLoss loss i p.2) (g p.1) T >
                                    AuditCP.cumCP (fun i => AuditCP.populationLoss Q loss i) (g p.1) T +
                                      2 * AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ} ≤
                              ENNReal.ofReal δ

AuditCP.Admissible AuditCP.AuditEnvelope AuditCP.AuditSampleLaw AuditCP.AuditTrajectory AuditCP.UniformDev AuditCP.cumCP AuditCP.deltaFiniteExperts AuditCP.empiricalLoss AuditCP.populationLoss

Uses

AuditCP.auditBlind_randomTrajectory_goodhart
AuditCP.finite_experts_iid_badEvent_le

DeclAuditCP.finite_experts_iid_badEvent_leDeclaration kindtheorem

Under the hypotheses of finite_experts_iid_uniformDev, the ENNReal-valued probability that the panel fails uniform deviation is at most ENNReal.ofReal δ.

∀ {Z : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Z] [inst_1 : Fintype ι] [Nonempty ι]
  (Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
  0 < n →
    ∀ (a b : ℝ),
      a < b →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (loss : ι → Z → ℝ),
                (∀ (i : ι), Measurable (loss i)) →
                  (∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
                    (MeasureTheory.Measure.pi fun x => Q)
                        {panel |
                          ¬AuditCP.UniformDev Set.univ (fun i => AuditCP.empiricalLoss loss i panel)
                              (fun i => AuditCP.populationLoss Q loss i)
                              (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)} ≤
                      ENNReal.ofReal δ

AuditCP.AuditSampleLaw AuditCP.UniformDev AuditCP.deltaFiniteExperts AuditCP.empiricalLoss AuditCP.populationLoss

Uses

AuditCP.finite_experts_iid_uniformDev

Used by

AuditCP.auditBlind_finiteTrajectory_goodhart

DeclAuditCP.finite_experts_iid_uniformDevDeclaration kindtheorem

If every candidate's loss is measurable and a.e. valued in [a, b] under Q, then on an i.i.d. panel of size n drawn from Q, with probability at least 1 − δ the empirical loss empiricalLoss loss i panel and the population loss populationLoss Q loss i agree within deltaFiniteExperts (card ι) n (b - a) δ for every candidate i (hoeffding1963; cesabianchi2006).

∀ {Z : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Z] [inst_1 : Fintype ι] [Nonempty ι]
  (Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
  0 < n →
    ∀ (a b : ℝ),
      a < b →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (loss : ι → Z → ℝ),
                (∀ (i : ι), Measurable (loss i)) →
                  (∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
                    1 - δ ≤
                      (MeasureTheory.Measure.pi fun x => Q).real
                        {panel |
                          AuditCP.UniformDev Set.univ (fun i => AuditCP.empiricalLoss loss i panel)
                            (fun i => AuditCP.populationLoss Q loss i)
                            (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)}

AuditCP.AuditSampleLaw AuditCP.UniformDev AuditCP.deltaFiniteExperts AuditCP.empiricalLoss AuditCP.populationLoss

Uses

AuditCP.finite_experts_subgaussian_uniformDev

Used by

AuditCP.finite_experts_iid_badEvent_le

DeclAuditCP.finite_experts_subgaussian_uniformDevDeclaration kindtheorem

If each Y i j is μ-sub-Gaussian with proxy (L/2)² and, for each candidate i, independent across panel positions j, then with probability at least 1 − δ the panel means (∑ⱼ Y i j) / n all lie within deltaFiniteExperts (card ι) n L δ of 0 (hoeffding1963).

∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : Fintype ι] [Nonempty ι]
  (μ : AuditCP.AuditSampleLaw Ω) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ),
  0 < n →
    ∀ (L : ℝ),
      0 < L →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (Y : ι → Fin n → Ω → ℝ),
                (∀ (i : ι) (j : Fin n), ProbabilityTheory.HasSubgaussianMGF (Y i j) ((‖L‖₊ / 2) ^ 2) μ) →
                  (∀ (i : ι), ProbabilityTheory.iIndepFun (Y i) μ) →
                    1 - δ ≤
                      MeasureTheory.Measure.real μ
                        {ω |
                          AuditCP.UniformDev Set.univ (fun i => (∑ j, Y i j ω) / ↑n) (fun x => 0)
                            (AuditCP.deltaFiniteExperts (Fintype.card ι) n L δ)}

AuditCP.AuditSampleLaw AuditCP.UniformDev AuditCP.deltaFiniteExperts

Used by

AuditCP.finite_experts_iid_uniformDev

DeclAuditCP.auditBlind_randomTrajectory_goodhartDeclaration kindtheorem

If every training-generated trajectory g t is admissible for F t, the uniform-deviation failure event is measurable, and its audit fiber has probability at most δ for μtrain-almost every training history, then measured cumulative compression progress exceeds true progress by more than 2Δ with probability at most δ under μtrain.prod μaudit.

∀ {Ωtrain : Type u_1} {Ωaudit : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain]
  [inst_1 : MeasurableSpace Ωaudit] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
  (μaudit : AuditCP.AuditSampleLaw Ωaudit) [MeasureTheory.IsProbabilityMeasure μaudit]
  (F : Ωtrain → AuditCP.AuditEnvelope ι) (g : Ωtrain → AuditCP.AuditTrajectory ι)
  (Ehat : Ωaudit → AuditCP.AuditPotential ι) (E : AuditCP.AuditPotential ι) (Δ : ℝ) (δ : ENNReal),
  (∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)) →
    MeasurableSet {p | ¬AuditCP.UniformDev (F p.1) (Ehat p.2) E Δ} →
      (∀ᵐ (t : Ωtrain) ∂μtrain, μaudit {a | ¬AuditCP.UniformDev (F t) (Ehat a) E Δ} ≤ δ) →
        ∀ (T : ℕ),
          (MeasureTheory.Measure.prod μtrain μaudit)
              {p | AuditCP.cumCP (Ehat p.2) (g p.1) T > AuditCP.cumCP E (g p.1) T + 2 * Δ} ≤
            δ

AuditCP.Admissible AuditCP.AuditEnvelope AuditCP.AuditPotential AuditCP.AuditSampleLaw AuditCP.AuditTrajectory AuditCP.UniformDev AuditCP.cumCP

Uses

AuditCP.auditBlind_randomClass_badEvent_le
AuditCP.finite_audit_goodhart

Used by

AuditCP.auditBlind_finiteTrajectory_goodhart

DeclAuditCP.finite_audit_goodhartDeclaration kindtheorem
Under UniformDev F Ehat E Δ and Admissible g F, empirical cumulative compression progress is bounded by true cumulative progress plus 2Δ at every horizon T: cumCP Ehat g T ≤ cumCP E g T + 2Δ.
```
∀ {ι : Type u_1} {F : AuditCP.AuditEnvelope ι} {Ehat E : AuditCP.AuditPotential ι} {Δ : ℝ},
  AuditCP.UniformDev F Ehat E Δ →
    ∀ {g : AuditCP.AuditTrajectory ι},
      AuditCP.Admissible g F → ∀ (T : ℕ), AuditCP.cumCP Ehat g T ≤ AuditCP.cumCP E g T + 2 * Δ
```
AuditCP.Admissible AuditCP.AuditEnvelope AuditCP.AuditPotential AuditCP.AuditTrajectory AuditCP.UniformDev AuditCP.cumCP
Uses
- AuditCP.cumCP_telescope
Used by
- AuditCP.auditBlind_randomTrajectory_goodhart
DeclAuditCP.cumCP_telescopeDeclaration kindtheorem
Cumulative signed compression progress telescopes: cumCP E g T = E (g 0) - E (g T).
```
∀ {ι : Type u_1} (E : AuditCP.AuditPotential ι) (g : AuditCP.AuditTrajectory ι) (T : ℕ),
  AuditCP.cumCP E g T = E (g 0) - E (g T)
```
AuditCP.AuditPotential AuditCP.AuditTrajectory AuditCP.cumCP
Used by
- AuditCP.finite_audit_goodhart

DeclAuditCP.auditBlind_randomClass_badEvent_leDeclaration kindtheorem

If the event {p | Bad (Γ p.1) p.2} is measurable and its audit fiber {a | Bad (Γ t) a} has μaudit-probability at most δ for μtrain-almost every training history t, then its probability under the product law μtrain.prod μaudit is at most δ.

∀ {Ωtrain : Type u_1} {Ωaudit : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain]
  [inst_1 : MeasurableSpace Ωaudit] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
  (μaudit : AuditCP.AuditSampleLaw Ωaudit) [MeasureTheory.IsProbabilityMeasure μaudit]
  (Γ : Ωtrain → AuditCP.AuditEnvelope ι) (Bad : AuditCP.AuditEnvelope ι → Ωaudit → Prop) (δ : ENNReal),
  MeasurableSet {p | Bad (Γ p.1) p.2} →
    (∀ᵐ (t : Ωtrain) ∂μtrain, μaudit {a | Bad (Γ t) a} ≤ δ) →
      (MeasureTheory.Measure.prod μtrain μaudit) {p | Bad (Γ p.1) p.2} ≤ δ

AuditCP.AuditEnvelope AuditCP.AuditSampleLaw

Used by

AuditCP.auditBlind_randomTrajectory_goodhart

Hypothesishn
```
0 < n
```
Hypothesishab
```
a < b
```
Hypothesishδ0
```
0 < δ
```
Hypothesishδ1
```
δ ≤ 1
```
Hypothesishmeas
```
∀ (i : ι), Measurable (loss i)
```

Hypothesishbdd

∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b

Hypothesishadm

∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)

HypothesishBad

MeasurableSet
  {p |
    ¬AuditCP.UniformDev (F p.1) (fun i => AuditCP.empiricalLoss loss i p.2) (fun i => AuditCP.populationLoss Q loss i)
        (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)}

DefinitionAuditCP.Admissibledef

Every stage of the trajectory g lies in the envelope F.

{ι : Type u_1} → AuditCP.AuditTrajectory ι → AuditCP.AuditEnvelope ι → Prop

DefinitionAuditCP.AuditEnvelopedef
B4 — AuditEnvelope ι is the type of subsets Set ι of the index ι.
```
AuditCP.AuditIndex → Type u
```
DefinitionAuditCP.AuditPotentialdef
B2 — AuditPotential ι is the type of real-valued readings ι → ℝ of the index ι.
```
AuditCP.AuditIndex → Type u
```
DefinitionAuditCP.AuditSampleLawdef
B7 — AuditSampleLaw Ω is MeasureTheory.Measure Ω, a σ-additive probability law on the measurable space Ω.
```
(Ω : AuditCP.AuditIndex) → [MeasurableSpace Ω] → Type u
```
DefinitionAuditCP.AuditTrajectorydef
B3 — AuditTrajectory ι is the type of stage-indexed selections ℕ → ι of the index ι.
```
AuditCP.AuditIndex → Type u
```

DefinitionAuditCP.UniformDevdef

The potentials Ehat and E agree to within Δ at every point of the envelope F.

{ι : Type u_1} → AuditCP.AuditEnvelope ι → AuditCP.AuditPotential ι → AuditCP.AuditPotential ι → ℝ → Prop

DefinitionAuditCP.cumCPdef
Cumulative signed compression progress of a potential E read along a trajectory g over T stages, ∑_{t < T} (E(g t) − E(g(t+1))) (schmidhuber1991; schmidhuber2010).
```
{ι : Type u_1} → AuditCP.AuditPotential ι → AuditCP.AuditTrajectory ι → ℕ → ℝ
```
DefinitionAuditCP.deltaFiniteExpertsdef
The finite-experts uniform-deviation radius, L·√(log(2N/δ)/(2n)), for N candidates, panel size n, loss range L, and failure probability δ (hoeffding1963).
```
ℕ → ℕ → ℝ → ℝ → ℝ
```
DefinitionAuditCP.empiricalLossdef
The empirical mean loss of candidate i on the panel, (∑ⱼ loss i (panel j)) / n.
```
{Z : Type u_1} → {ι : Type u_2} → {n : ℕ} → (ι → Z → ℝ) → ι → (Fin n → Z) → ℝ
```

DefinitionAuditCP.populationLossdef

The population loss of candidate i under the law Q, ∫ loss i z ∂Q.

{Z : Type u_1} → {ι : Type u_2} → [inst : MeasurableSpace Z] → AuditCP.AuditSampleLaw Z → (ι → Z → ℝ) → ι → ℝ

DOIMTH.R-2026-6015

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