OAI/Probability/TraceReconstruction/Propagation.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Propagation

Moment restriction, scale margins, sharp budget closure, clipping and error propagation, and dense/warmup overlap.

  1. theorem OAI.TraceReconstruction.FiniteLaw.evenMomentSq_mono_order line 25
  2. def OAI.TraceReconstruction.OracleTracePair.restrict line 48
  3. def OAI.TraceReconstruction.ConcreteLevelPair.oracle line 56

    Source documentation

    Null-mass outcomes are assigned zero score. This proves, rather than assumes, the pointwise positivity needed by the finite simulation API.

    def ConcreteLevelPair.oracle {q N Δ d ω F : ℝ} {hq : q∈Set.Icc 0 1} {i k : ℕ}
    (C : ConcreteLevelPair q hq N Δ d ω F i k) :
    OracleTracePair q C.left C.right k C.error (N^(-d)) := by
…

    Mentions: OAI.TraceReconstruction.ConcreteLevelPair, OAI.TraceReconstruction.OracleTracePair

  4. theorem OAI.TraceReconstruction.sourceScaleProduct_step_le line 101
  5. theorem OAI.TraceReconstruction.sourceHalfMoment_step line 117
  6. def OAI.TraceReconstruction.sourceGapFloor line 138
  7. theorem OAI.TraceReconstruction.sourceGapFloor_pos line 140
  8. theorem OAI.TraceReconstruction.sourceGapFloor_le_one line 142
  9. theorem OAI.TraceReconstruction.sourceEpsilon_gap_small line 148
  10. theorem OAI.TraceReconstruction.sourceHalfMoment_strong line 162
  11. theorem OAI.TraceReconstruction.source_clipping_power_delta line 170
  12. def OAI.TraceReconstruction.sourceWorkSize line 212
  13. theorem OAI.TraceReconstruction.sourceWorkSize_pos line 215
  14. theorem OAI.TraceReconstruction.sourceCancellationOrder_lower line 222
  15. theorem OAI.TraceReconstruction.source_smoothing_absorb line 226
  16. theorem OAI.TraceReconstruction.sparse_power_absorb line 250

    Source documentation

    The actual sparse count controls both extra forced roles and clipping.

    theorem sparse_power_absorb {N ε gap W L x : ℝ}
    (hN : 1≤ N) (he : 0≤ε) (hg : 2*ε≤ gap) (hW : 0≤ W) (hL : 1≤ L)
    (hx : x≤ W*L*N^(-gap)) (hfac : 8*W*L^2≤ N^ε) :
    x≤ N^(-gap/2)/8 ∧ x≤1/2 ∧ x*L≤1 := by
…
  17. theorem OAI.TraceReconstruction.source_weight_square line 276
  18. theorem OAI.TraceReconstruction.source_high_tail_margin line 289
  19. theorem OAI.TraceReconstruction.rpow_coefficient_absorb line 321
  20. theorem OAI.TraceReconstruction.sharp_energy_absorb line 331

    Source documentation

    Closing the three explicit sharp classes, with the source's fixed finite degree cutoff and no hidden dependence on N in their constants.

    theorem sharp_energy_absorb {N ε d M Fdec gap Cr Cf E : ℝ} {R : ℕ}
    (hN : 1≤ N) (he : ε≤1) (hM : d+(R:ℝ)+1≤ M) (hd : 0≤ d) (_hR : 0≤(R:ℝ))
    (hbad : 384*Cr≤ N^ε) (hforce : 192*Cf≤ N^ε) (htail : 1536≤ N^ε)
    (hfdec : d+ε≤ Fdec) (hgap : d+ε≤ gap*(R:ℝ))
    (hE : E ≤ Cr*N^R*((N^(-20*M))^2+(N^(-20*M))^2)+Cf*N^(-Fdec)+8*N^(-gap*(R:ℝ))) :
    64*E≤ N^(-d) := by
…
  21. theorem OAI.TraceReconstruction.sourceDimension_bounds line 364
  22. theorem OAI.TraceReconstruction.totalScoreExponent_mono line 369
  23. theorem OAI.TraceReconstruction.sourceTargetScale_bounds line 375
  24. theorem OAI.TraceReconstruction.ConcreteLevelPair.error_le line 382
  25. theorem OAI.TraceReconstruction.source_warmup_score_margin line 389
  26. theorem OAI.TraceReconstruction.source_main_score_margin line 404
  27. theorem OAI.TraceReconstruction.sourceSparseCount_ge_one line 438
  28. theorem OAI.TraceReconstruction.source_block_energy_close line 446

    Source documentation

    Scalar closure of the exact sparse/forced block budget. All assumptions here are explicit elementary coefficient bounds, not oracle conclusions.

    theorem source_block_energy_close (T n : ℕ→ℕ) (s b R : ℕ) (ω N ε d dnew K W M gap : ℝ)
    (hN : 1 ≤ N) (he : 0 ≤ ε) (he1 : ε ≤ 1) (hK : 0 ≤ K) (hW : 0 ≤ W)
    (hd : 0 ≤ dnew) (hM : dnew+(R:ℝ)+1 ≤ M) (hg : 2*ε ≤ gap)
    (hf : dnew+ε ≤ forcedDecay (b+1) ε d) (hR : dnew+ε ≤ gap/2*(R:ℝ))
    (hfac : 8*W*((2^s:ℕ):ℝ)^2 ≤ N^ε)
    (hbad : 384*sourceBadRoleFactor b R ≤ N^ε)
    (hforce : 192*(sourceForcedRoleFactor b R*W^(2^(b+1))*sourceSkeletonPrefactor s b K) ≤ N^ε)
    (htail : 1536 ≤ N^ε)
    (hleaf : (SourceLeafCount T (b+1):ℝ) ≤ N)
    (hcount : 1 ≤ sourceSparseCount T s b)
    (k : ℕ) (L : ℝ)
    (hw : ((6*(2*k:ℕ):ℝ)*L)^2 ≤ W*N^(-scaleA (b+1) 0 ε*d))
…

    Mentions: OAI.TraceReconstruction.forcedDecay, OAI.TraceReconstruction.sourceBadRoleFactor, OAI.TraceReconstruction.sourceForcedRoleFactor, OAI.TraceReconstruction.sourceSkeletonPrefactor, OAI.TraceReconstruction.SourceLeafCount, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.scaleA

  29. theorem OAI.TraceReconstruction.source_level_energy line 496

    Source documentation

    Instantiation at the manuscript's literal block dimension, integer schedules, source cutoff, moment envelope, and full next score exponent.

    theorem source_level_energy (B D i ell h k : ℕ) (C N F ω K : ℝ)
    (hB : 2 ≤ B) (hi : i<D) (hN : 1 ≤ N) (hC : 1 ≤ C) (hF : 1 ≤ F) (hω : 0<ω)
    (H : SourceArithmeticBounds C N F (sourceEpsilon B D) (sourceCancellationOrder B D)
      (sourceDimension B i) ell h)
    (hk : (k:ℝ) ≤ sourceMomentEnvelope B D)
    (hK : 200*(C^(2*sourceDimension B i)*F)/ω ≤ K)
    (hfac : 8*sourceWeightEnvelope B D*((2^(sourceCancellationOrder B D):ℕ):ℝ)^2 ≤ N^(sourceEpsilon B D))
    (hbad : 384*sourceBadRoleFactor (sourceDimension B i-1) (sourceDegreeCutoff B) ≤ N^(sourceEpsilon B D))
    (hforce : 192*(sourceForcedRoleFactor (sourceDimension B i-1) (sourceDegreeCutoff B)*
        (sourceWeightEnvelope B D)^(2^(sourceDimension B i))*
        sourceSkeletonPrefactor (sourceCancellationOrder B D) (sourceDimension B i-1) K) ≤ N^(sourceEpsilon B D))
    (htail : 1536 ≤ N^(sourceEpsilon B D))
…

    Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceCancellationOrder, OAI.TraceReconstruction.sourceDimension, OAI.TraceReconstruction.sourceMomentEnvelope, OAI.TraceReconstruction.sourceWeightEnvelope, OAI.TraceReconstruction.sourceBadRoleFactor, OAI.TraceReconstruction.sourceDegreeCutoff, OAI.TraceReconstruction.sourceForcedRoleFactor, OAI.TraceReconstruction.sourceSkeletonPrefactor

  30. structure OAI.TraceReconstruction.SourceNumericMargins line 608
  31. theorem OAI.TraceReconstruction.sourceWeightEnvelope_nonneg line 621
  32. theorem OAI.TraceReconstruction.sourceForcedRoleFactor_nonneg line 625
  33. theorem OAI.TraceReconstruction.source_forced_prefactor_expUpper line 629
  34. theorem OAI.TraceReconstruction.source_overlap_prefactor_expUpper line 644
  35. theorem OAI.TraceReconstruction.source_numeric_margins_eventually line 657
  36. theorem OAI.TraceReconstruction.source_count_envelope line 710
  37. theorem OAI.TraceReconstruction.source_cap_envelope line 719
  38. theorem OAI.TraceReconstruction.source_local_envelope line 728
  39. theorem OAI.TraceReconstruction.SourceArithmeticBounds.count_bound line 740
  40. theorem OAI.TraceReconstruction.sourceErrorUnit_small line 755
  41. def OAI.TraceReconstruction.sourceTailDenominator line 780
  42. def OAI.TraceReconstruction.sourceTailExponent line 783
  43. theorem OAI.TraceReconstruction.sourceTailDenominator_pos line 786
  44. theorem OAI.TraceReconstruction.sourceTailDenominator_expUpper line 791
  45. theorem OAI.TraceReconstruction.sourceWorkSize_poly line 798
  46. theorem OAI.TraceReconstruction.sourceTailExponent_expUpper line 802
  47. theorem OAI.TraceReconstruction.source_tails_eventually line 811
  48. theorem OAI.TraceReconstruction.source_exponential_error_budget line 830

    Source documentation

    Turning the common uniform exponential bound into the two exact scheduled-error terms, including the division by the clipping threshold.

    theorem source_exponential_error_budget {B D b s ell k : ℕ} {C N F ω f n : ℝ}
    (H : SourceArithmeticBounds C N F (sourceEpsilon B D) s b ell k)
    (hB : 2 ≤ B) (hb : b ≤ B) (hC : 0<C) (hF : 0<F) (hω : 0<ω)
    (hn : 1 ≤ n) (hN : 1 ≤ N) (hNn : N ≤ n)
    (hf512 : 512 ≤ f) (hfmeta : 9600*(C^(2*b)*F)/ω^4 ≤ f)
    (htail : 2*(B:ℝ)*Real.exp (-(N^(sourceEpsilon B D)/f)) ≤ n^(-sourceTailExponent B D)) :
    sourceEffectiveHiddenTail (sourceBlockWindows N b (sourceEpsilon B D))
      (sourceArithmeticTrials C N b (sourceEpsilon B D) ell k) b ω ≤ n^(-200*(totalScoreExponent B D+B+1)) ∧
    sourceFitTail (sourceBlockWindows N b (sourceEpsilon B D))
      (sourceArithmeticTrials C N b (sourceEpsilon B D) ell k) b /
      N^(-20*sourceWorkSize B D) ≤ n^(-200*(totalScoreExponent B D+B+1)) ∧
    sourceFitTail (sourceBlockWindows N b (sourceEpsilon B D))
…

    Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTailExponent, OAI.TraceReconstruction.sourceEffectiveHiddenTail, OAI.TraceReconstruction.sourceBlockWindows, OAI.TraceReconstruction.sourceArithmeticTrials, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceFitTail, OAI.TraceReconstruction.sourceWorkSize

  49. theorem OAI.TraceReconstruction.rpow_constant_absorb line 899
  50. theorem OAI.TraceReconstruction.overlap_sqrt_budget line 909
  51. theorem OAI.TraceReconstruction.source_dense_variance_budget line 916

    Source documentation

    Generic dense-template estimate, used for the first warmup step and every step of a post-warmup block.

    theorem source_dense_variance_budget {N ε e a K L V h : ℝ} {j : ℕ}
    (hN : 1 ≤ N) (_hK : 0 ≤ K) (hL : 0 ≤ L) (hh : 0 ≤ h)
    (hcount : h ≤ (K+1)*N^a) (hV : V ≤ N^(-e))
    (hc : 4096*(K+1)*L^j ≤ N^ε) (he : ε+a ≤ e) :
    h*(L^j*V) ≤ 1/4096 := by
…
  52. theorem OAI.TraceReconstruction.source_warmup_variance_budget line 934

    Source documentation

    Exact scalar one-window refinement. Its quadratic sparse term is what makes the second warmup overlap possible at old score exponent 11/5.

    theorem source_warmup_variance_budget {N ε e M K W L w T h E : ℝ}
    (hN : 1 ≤ N) (hK : 0 ≤ K) (hW : 0 ≤ W) (hL : 0 ≤ L)
    (hT : 0 ≤ T) (hh : 0 ≤ h) (hcount : h ≤ (K+1)*N)
    (hwindow : T ≤ N) (hw : w^2 ≤ W*N^(-e))
    (henergy : E ≤ 64*(72*T*w^2*(N^(-20*M))^2+8*(w^2*L)^2))
    (hbad : 8192*(4608*(K+1)*L*W) ≤ N^ε)
    (hquad : 8192*(512*(K+1)*W^2*L^3) ≤ N^ε)
    (hebad : ε+2-e-40*M ≤ 0) (hequad : ε+1-2*e ≤ 0) :
    h*(L*E) ≤ 1/4096 := by
…
  53. theorem OAI.TraceReconstruction.sourceBlockLength_factor line 981
  54. theorem OAI.TraceReconstruction.source_delta_power_budget line 994
  55. theorem OAI.TraceReconstruction.source_repeated_error_budget line 1009

    Source documentation

    Uniform repeated old simulation error; this is the error term in every dense nested-overlap estimate.

    theorem source_repeated_error_budget {n N ε K E t h : ℝ} {B D : ℕ}
    (hB : 2 ≤ B) (hn : 1 ≤ n) (hN : 1 ≤ N) (hNn : N ≤ n)
    (he : 0 ≤ ε) (he1 : ε ≤ 1) (hh : 0 ≤ h) (_hK : 0 ≤ K)
    (hcount : h ≤ (K+1)*N)
    (hcost : t*E ≤ ((D:ℝ)+1)*n^(-100*(totalScoreExponent B D+B+1))*N)
    (hmargin : 64*(K+1)*((D:ℝ)+1) ≤ N^ε) : 2*h*(t*E) ≤ 1/32 := by
…

    Mentions: OAI.TraceReconstruction.totalScoreExponent

  56. theorem OAI.TraceReconstruction.source_old_error_cost line 1035
  57. theorem OAI.TraceReconstruction.normalized_block_error line 1056

    Source documentation

    The normalized error invariant propagates through actual leaf products, with one fresh delta paid by clipping and fitting.

    theorem normalized_block_error {E Δ clip fit : ℝ} {ell newell leaves i : ℕ}
    (hell : 1 ≤ newell) (hE : E ≤ ((i:ℝ)+1)*Δ*ell) (hΔ : 0 ≤ Δ)
    (hleaf : leaves*ell ≤ newell) (hnew : clip+fit ≤ Δ) :
    (clip+(leaves:ℝ)*E+fit)/(newell:ℝ) ≤ ((i:ℝ)+2)*Δ := by
…
  58. theorem OAI.TraceReconstruction.source_level_clipping line 1075

    Source documentation

    All three genuine clipping losses, and fitting, share the same global error unit. The reference power is the actual half-moment at this scale.

    theorem source_level_clipping (B D j s b : ℕ) (T t : ℕ→ℕ) (n ω a gap L : ℝ)
    (hB : 2 ≤ B) (hn : 4 ≤ n) (hg : sourceGapFloor B ≤ gap)
    (hmeta : sourceEffectiveHiddenTail T t (b+1) ω ≤ n^(-200*(totalScoreExponent B D+B+1)))
    (hfit : sourceFitTail T t (b+1)/a ≤ n^(-200*(totalScoreExponent B D+B+1)))
    (hfit' : sourceFitTail T t (b+1) ≤ n^(-200*(totalScoreExponent B D+B+1)))
    (hhalf : ((6*(2*sourceHalfMoment B D n j:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤ 1/2)
    (hscale : ((6*(2*sourceHalfMoment B D n j:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤
      (sourceTargetScale B D n j)^(-gap/2)/8) :
    sourceClippingCost T t s b (sourceHalfMoment B D n j) ω a L ≤ 1/2 ∧
    sourceClippingCost T t s b (sourceHalfMoment B D n j) ω a L+sourceFitTail T t (b+1) ≤
      n^(-100*(totalScoreExponent B D+B+1)) := by
…

    Mentions: OAI.TraceReconstruction.sourceGapFloor, OAI.TraceReconstruction.sourceEffectiveHiddenTail, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceFitTail, OAI.TraceReconstruction.sourceHalfMoment, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceClippingCost

  59. theorem OAI.TraceReconstruction.source_one_window_clipping line 1096

    Source documentation

    At one window the root metadata can still fail; only the fitting loss vanishes. We charge the root metadata rather than discard it.

    theorem source_one_window_clipping (B D j s : ℕ) (T t : ℕ) (n ω a gap L : ℝ)
    (hB : 2 ≤ B) (hn : 4 ≤ n) (hg : sourceGapFloor B ≤ gap)
    (hmeta : sourceEffectiveHiddenTail (fun _=>T) (fun _=>t) 1 ω ≤ n^(-200*(totalScoreExponent B D+B+1)))
    (hhalf : ((6*(2*sourceHalfMoment B D n j:ℕ):ℝ)*L)^2*(2:ℝ)^s ≤ 1/2)
    (hscale : ((6*(2*sourceHalfMoment B D n j:ℕ):ℝ)*L)^2*(2:ℝ)^s ≤
      (sourceTargetScale B D n j)^(-gap/2)/8) :
    sourceClippingCost (fun _=>T) (fun _=>t) s 0 (sourceHalfMoment B D n j) ω a L ≤ 1/2 ∧
    sourceClippingCost (fun _=>T) (fun _=>t) s 0 (sourceHalfMoment B D n j) ω a L ≤
      n^(-100*(totalScoreExponent B D+B+1)) := by
…

    Mentions: OAI.TraceReconstruction.sourceGapFloor, OAI.TraceReconstruction.sourceEffectiveHiddenTail, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceHalfMoment, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceClippingCost

  60. theorem OAI.TraceReconstruction.source_overlap_prefactors line 1118
  61. theorem OAI.TraceReconstruction.source_literal_dense_overlap line 1149

    Source documentation

    Complete dense-overlap numerical criterion for the literal schedules, including the error carried by the old exact simulator.

    theorem source_literal_dense_overlap {C N F ε E Δ V K W L n e : ℝ}
    {s b ell k j i D B : ℕ} (H : SourceArithmeticBounds C N F ε s b ell k)
    (hB : 2 ≤ B) (hb : b ≤ B) (hC : 1 ≤ C) (hF : 0 ≤ F)
    (hn : 1 ≤ n) (hN : 1 ≤ N) (hNn : N ≤ n) (he : 0 ≤ ε) (he1 : ε ≤ 1)
    (hK : 0 ≤ K) (hW : 0 ≤ W) (hL : 1 ≤ L) (hLdef : L=(2:ℝ)^s)
    (hG : C^(2*b)*F ≤ K) (hi : i ≤ D) (hj : j ≤ b)
    (ha : 0 ≤ scaleA b j ε) (ha1 : scaleA b j ε ≤ 1)
    (hE : E ≤ ((i:ℝ)+1)*Δ*ell) (hΔ : Δ=n^(-100*(totalScoreExponent B D+B+1)))
    (hV : V ≤ N^(-e)) (hgap : ε+scaleA b j ε ≤ e)
    (hmargin : 64*(K+1)*((D:ℝ)+1) ≤ N^ε)
    (hoverlap : 1099511627776*(K+1)*(W+1)^2*L^(B+2) ≤ N^ε) :
    Real.sqrt (((sourceArithmeticCount C N b ε ell k j+1:ℕ):ℝ)*
…

    Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceArithmeticCount

  62. theorem OAI.TraceReconstruction.SourceArithmeticBounds.length_positive line 1187
  63. theorem OAI.TraceReconstruction.SourceArithmeticBounds.copies_le_target line 1195
  64. theorem OAI.TraceReconstruction.source_warmup_error_budget line 1209

    Source documentation

    Both contributions to the error in the second warmup overlap are paid by the common delta margin. The old term uses T₀ ≤ P₀, not an independent full-block overlap hypothesis.

    theorem source_warmup_error_budget {C N F ε E Δ clip K n : ℝ} {s ell k i D B : ℕ}
    (H : SourceArithmeticBounds C N F ε s 2 ell k)
    (hB : 2 ≤ B) (hC : 1 ≤ C) (hF : 0 ≤ F) (hn : 1 ≤ n) (hN : 1 ≤ N) (hNn : N ≤ n)
    (he : 0 ≤ ε) (he1 : ε ≤ 1) (hK : 0 ≤ K) (hG : C^4*F ≤ K) (hi : i ≤ D)
    (hE : E ≤ ((i:ℝ)+1)*Δ*ell) (hE0 : 0 ≤ E) (hΔ : Δ=n^(-100*(totalScoreExponent B D+B+1)))
    (hclip : clip ≤ Δ) (hmargin : 64*(K+1)*((D:ℝ)+1) ≤ N^ε) :
    2*((sourceArithmeticCount C N 2 ε ell k 2+1:ℕ):ℝ)*
      ((sourceArithmeticP C N 2 ε ell k 1:ℝ)*
        (clip+(sourceBlockWindows N 2 ε 0:ℝ)*E)) ≤ 1/8 := by
…

    Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.totalScoreExponent, OAI.TraceReconstruction.sourceArithmeticCount, OAI.TraceReconstruction.sourceArithmeticP, OAI.TraceReconstruction.sourceBlockWindows