TraceReconstruction.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Bounds

Restored construction and final scales; quantitative sample lower bound and both fixed-channel superpolynomial endpoints.

theorem OAI.TraceReconstruction.source_final_error_eventually line 25

Source documentation

The exact source error is negligible compared to the squared score energy.

theorem source_final_error_eventually (B : ℕ) (ζ : ℝ) (hB : 2≤B) (hζ : ζ∈Set.Ioo 0 1)
    {n q : ℕ→ℝ} (hn : Tendsto n atTop atTop) (hq : ∀t,q t∈Set.Ioc 0 (1/2:ℝ))
    (hH : Tendsto (fun t=>(q t)^3*Real.log (n t)) atTop atTop) :
    ∀ᶠt in atTop,∀ (U : ConcreteLevelPair (q t) ⟨(hq t).1.le,by linarith [(hq t).2]⟩ (n t)
      ((n t)^(-100*(totalScoreExponent B (sourceDepth B ζ ((q t)^3*Real.log (n t)))+B+1)))
      (totalScoreExponent B (sourceDepth B ζ ((q t)^3*Real.log (n t))))
      (initialOverlapLower (q t))
      ((sourceOverlapConstant (q t))^(2*B*sourceDepth B ζ ((q t)^3*Real.log (n t))+2))
      (sourceDepth B ζ ((q t)^3*Real.log (n t)))
      (sourceHalfMoment B (sourceDepth B ζ ((q t)^3*Real.log (n t))) (n t)
        (sourceDepth B ζ ((q t)^3*Real.log (n t))))),
      U.error≤(n t)^(-2*totalScoreExponent B (sourceDepth B ζ ((q t)^3*Real.log (n t)))) := by
…

Mentions: OAI.TraceReconstruction.ConcreteLevelPair, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.initialOverlapLower, OAI.TraceReconstruction.sourceOverlapConstant, OAI.TraceReconstruction.sourceHalfMoment

theorem OAI.TraceReconstruction.exists_source_slope line 66

theorem OAI.TraceReconstruction.subdivided_working_scale line 94

Source documentation

Constant-size subdivision and larger deletion preserve the joint regime. The factor 16 includes the factor eight of the working deletion cube.

theorem subdivided_working_scale {n q : ℕ→ℝ} (hn : Tendsto n atTop atTop)
    (hq : ∀t,q t∈Set.Ioo 0 1)
    (hH : Tendsto (fun t=>(q t)^3*Real.log (n t)) atTop atTop)
    {G : ℝ} (hG : 0<G) :
    Tendsto (fun t=>n t/G) atTop atTop ∧
    Tendsto (fun t=>(workingDeletion (q t))^3*Real.log (n t/G)) atTop atTop ∧
    ∀ᶠt in atTop,(q t)^3*Real.log (n t)/16 ≤
      (workingDeletion (q t))^3*Real.log (n t/G) := by
…

Mentions: OAI.TraceReconstruction.workingDeletion

theorem OAI.TraceReconstruction.workingDeletion_Ioc line 118

theorem OAI.TraceReconstruction.source_restored_exponent_margin line 132

Source documentation

Full sharp slope restoration after fixed gadget packing. Both deletion probability and length may vary; the working channel is only internal.

theorem source_restored_exponent_margin (B : ℕ) (ζ c G a : ℝ)
    (hB : 2≤B) (hζ : ζ∈Set.Ioo 0 1) (hc : 0<c) (hα : c<finalSlope B ζ)
    (hG : 0<G) (ha : 0<a) {n q : ℕ→ℝ} (hn : Tendsto n atTop atTop)
    (hq : ∀t,q t∈Set.Ioo 0 1)
    (hH : Tendsto (fun t=>(q t)^3*Real.log (n t)) atTop atTop) :
    ∀ᶠt in atTop,(n t)^(c*Real.log ((q t)^3*Real.log (n t))) ≤
      a*(n t/G)^(totalScoreExponent B
        (sourceDepth B ζ ((workingDeletion (q t))^3*Real.log (n t/G)))) := by
…

Mentions: OAI.TraceReconstruction.finalSlope, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.workingDeletion

theorem OAI.TraceReconstruction.sample_tv_small line 182
theorem OAI.TraceReconstruction.quantitative_sample_lower_bound line 213
Source documentation
Source Theorem 1: all fixed positive success levels, not only binary testing above one half, with complete independent traces and known channel.
Distinct definitions of this name: ComparatorChallenges/TraceReconstruction.lean:62 (same statement text; different proof or body). Qualify references as OAI.TraceReconstruction.quantitative_sample_lower_bound@path.
```
theorem quantitative_sample_lower_bound
    (s c : ℝ) (hs : s ∈ Set.Ioc 0 1)
    (hc : c ∈ Set.Ioo 0 (1 / (4 * Real.log 2)))
    (n : ℕ → ℕ) (q : ℕ → ℝ)
    (hn : Tendsto n atTop atTop)
    (hq : ∀ k, q k ∈ Set.Ioo 0 1)
    (hscale : Tendsto (fun k => (q k) ^ 3 * Real.log (n k)) atTop atTop) :
    ∀ᶠ k in atTop,
      ENNReal.ofReal ((n k : ℝ) ^ (c * Real.log ((q k) ^ 3 * Real.log (n k))))  ≤ 
        sampleComplexity (n k) (q k) s := by
…
```
Mentions: OAI.TraceReconstruction.sampleComplexity
theorem OAI.TraceReconstruction.FiniteLaw.tv_product_one line 286
theorem OAI.TraceReconstruction.totalScoreExponent_two line 291
theorem OAI.TraceReconstruction.minTraceTV_nonneg_of_pair line 295
theorem OAI.TraceReconstruction.minTraceTV_le_pair line 302
theorem OAI.TraceReconstruction.one_trace_power_bound line 307
theorem OAI.TraceReconstruction.superpolynomial_one_trace line 332
Source documentation
Source Theorem 2, first conclusion, over all integer lengths and at the same fixed channel for every power.
Distinct definitions of this name: ComparatorChallenges/TraceReconstruction.lean:74 (different declaration text). Qualify references as OAI.TraceReconstruction.superpolynomial_one_trace@path.
```
theorem superpolynomial_one_trace
    (q : ℝ) (hq : q ∈ Set.Ioo 0 1) (C : ℝ) (hC : 0<C) :
    Tendsto (fun n : ℕ=>(n:ℝ)^C*minTraceTV n q) atTop (𝓝 0) := by
…
```
theorem OAI.TraceReconstruction.superpolynomial_sample_complexity line 378
Source documentation
Source Theorem 2's sample conclusion at the same fixed deletion channel.
Distinct definitions of this name: ComparatorChallenges/TraceReconstruction.lean:79 (same statement text; different proof or body). Qualify references as OAI.TraceReconstruction.superpolynomial_sample_complexity@path.
```
theorem superpolynomial_sample_complexity
    (q : ℝ) (hq : q ∈ Set.Ioo 0 1) (s : ℝ) (hs : s ∈ Set.Ioc 0 1)
    (C : ℝ) (hC : 0 < C) :
    Tendsto
      (fun n : ℕ => sampleComplexity n q s / ENNReal.ofReal ((n : ℝ) ^ C))
      atTop (𝓝 ⊤) := by
…
```
Mentions: OAI.TraceReconstruction.sampleComplexity