OAI/Probability/TraceReconstruction/Induction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TraceReconstruction.SourceLevelPair line 25

   Source documentation

   The literal induction invariant, including the depth-dependent moment, actual complete-trace simulator, distinct words, length, and power overlap.

   abbrev SourceLevelPair (B D : ℕ) (n q : ℝ) (hq : q∈Set.Icc 0 1) (i : ℕ) :=
   …

2. theorem OAI.TraceReconstruction.source_level_geometry line 30
3. theorem OAI.TraceReconstruction.SourceArithmeticBounds.copies_positive line 56
4. theorem OAI.TraceReconstruction.SourceArithmeticBounds.trials_positive line 65
5. theorem OAI.TraceReconstruction.source_level_exponent_margins line 72
6. theorem OAI.TraceReconstruction.sourceEffectiveHiddenTail_one line 116
7. theorem OAI.TraceReconstruction.sourceEffectiveHiddenTail_step line 125
8. theorem OAI.TraceReconstruction.sourceEffectiveHiddenTail_two_ge_one line 141
9. theorem OAI.TraceReconstruction.sourceSparseCount_motif_le line 151
10. theorem OAI.TraceReconstruction.source_level_tail_budget line 166
11. theorem OAI.TraceReconstruction.source_level_all_budgets line 201
12. theorem OAI.TraceReconstruction.source_old_variance_scale line 263
13. theorem OAI.TraceReconstruction.source_old_variance_square line 270
14. theorem OAI.TraceReconstruction.source_level_dense_overlap line 277
15. theorem OAI.TraceReconstruction.source_level_warmup_second line 321

    Source documentation

    The second warmup lift is produced from the one-window oracle, whose quadratic energy gain is essential before the main-block regime.

    theorem source_level_warmup_second {B D i : ℕ} {n q : ℝ} {hq : q∈Set.Icc 0 1}
        (U : SourceLevelPair B D n q hq i) (hB : 2 ≤ B) (hi : i<D) (hn : 4 ≤ n)
        (hq' : q∈Set.Ioc 0 (1/2:ℝ)) (hiw : i<warmupBlocks B)
        (H : SourceNumericMargins B D q (sourceTargetScale B D n (i+1)))
        (htail : 2*(B:ℝ)*Real.exp
          (-(sourceTargetScale B D n (i+1))^(sourceEpsilon B D)/sourceTailDenominator B D q) ≤
            n^(-sourceTailExponent B D)) :
        let N := sourceTargetScale B D n (i+1)
    …

    Mentions: OAI.TraceReconstruction.SourceLevelPair, OAI.TraceReconstruction.warmupBlocks, OAI.TraceReconstruction.SourceNumericMargins, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTailDenominator, OAI.TraceReconstruction.sourceTailExponent

16. theorem OAI.TraceReconstruction.source_level_overlap line 440
17. theorem OAI.TraceReconstruction.source_level_step line 540

    Source documentation

    The exact manuscript block is now a producer: no new level invariant or overlap is assumed. All hypotheses besides the old actual pair are literal scalar schedule margins.

    theorem source_level_step {B D i : ℕ} {n q : ℝ} {hq : q∈Set.Icc 0 1}
        (U : SourceLevelPair B D n q hq i) (hB : 2 ≤ B) (hi : i<D) (hn : 4 ≤ n)
        (hq' : q∈Set.Ioc 0 (1/2:ℝ))
        (H : SourceNumericMargins B D q (sourceTargetScale B D n (i+1)))
        (htail : 2*(B:ℝ)*Real.exp
          (-(sourceTargetScale B D n (i+1))^(sourceEpsilon B D)/sourceTailDenominator B D q) ≤
            n^(-sourceTailExponent B D)) :
        Nonempty (SourceLevelPair B D n q hq (i+1)) := by
    …

    Mentions: OAI.TraceReconstruction.SourceLevelPair, OAI.TraceReconstruction.SourceNumericMargins, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTailDenominator, OAI.TraceReconstruction.sourceTailExponent

18. theorem OAI.TraceReconstruction.source_all_levels_eventually line 660

    Source documentation

    Full source construction at every scheduled level, uniformly in the joint deletion regime. No level witnesses are assumed.

    theorem source_all_levels_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,∀i ≤ sourceDepth B ζ ((q t)^3*Real.log (n t)),
          Nonempty (SourceLevelPair B (sourceDepth B ζ ((q t)^3*Real.log (n t)))
            (n t) (q t) ⟨(hq t).1.le,by linarith [(hq t).2]⟩ i) := by
    …

    Mentions: OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.SourceLevelPair

19. theorem OAI.TraceReconstruction.source_final_pair_eventually line 681

    Source documentation

    The final source pair has actual length in [n/2,n], an exact common complete-trace simulator, prescribed high moment and inductively obtained power overlap. This is the construction theorem, before statistical transfer.

    theorem source_final_pair_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,Nonempty (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))))) := by
    …

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