OAI/Probability/TraceReconstruction/InitialRates.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

InitialRates

Initial geometric parameters, moment depths, error and overlap rates, and production of the base induction pair.

  1. theorem OAI.TraceReconstruction.initialPrefactor_rate line 28

    Source documentation

    Exact power of the sharp initial rank prefactor; all channel losses are subpower at the source's smallest scale.

    theorem initialPrefactor_rate (hN : Tendsto N atTop atTop)
    {α β : ℝ} (hu : PowerRate N (fun t=>(u t:ℝ)) α)
    (hm : PowerRate N (fun t=>(m t:ℝ)) β) (hq : PowerRate N q 0) (r d : ℕ) :
    PowerRate N (fun t=>initialPrefactorCap (u t) (m t) r d (q t))
      (α/2-β*((d:ℝ)+(r:ℝ)/2)) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialPrefactorCap

  2. theorem OAI.TraceReconstruction.periodCentral_rate line 45
  3. theorem OAI.TraceReconstruction.periodBounded_rate line 56
  4. theorem OAI.TraceReconstruction.hiddenSigned_rate line 67
  5. theorem OAI.TraceReconstruction.hiddenUnsigned_rate line 78
  6. theorem OAI.TraceReconstruction.initial_central_rate line 89

    Source documentation

    The two eliminated large gaps are quantitatively visible in this exponent.

    theorem initial_central_rate (hN : Tendsto N atTop atTop)
    (hu : PowerRate N (fun t=>(u t:ℝ)) (123/250))
    (hm : PowerRate N (fun t=>(m t:ℝ)) (62/125)) (hq : PowerRate N q 0)
    {r : ℕ} (hr : 0<r) (d : ℕ) :
    PowerRate N (fun t=>initialPrefactorCap (u t) (m t) r d (q t)*periodCentralSumConstant (u t) r)
      (-123/250-(62/125)*(d:ℝ)-(1/500)*(r:ℝ)) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialPrefactorCap, OAI.TraceReconstruction.periodCentralSumConstant

  7. theorem OAI.TraceReconstruction.initial_bounded_rate line 97
  8. theorem OAI.TraceReconstruction.initial_signed_pattern_upper line 106

    Source documentation

    Fixed low degrees already beat the signed and pure source score exponents.

    theorem initial_signed_pattern_upper (hN : Tendsto N atTop atTop)
    (hu : PowerRate N (fun t=>(u t:ℝ)) (123/250))
    (hm : PowerRate N (fun t=>(m t:ℝ)) (62/125)) (hq : PowerRate N q 0)
    (hJ : PowerRate N (fun t=>(J t:ℝ)) (1/125)) (hω : PowerRate N ω 0)
    {r : ℕ} (hr : 0<r) (k : Fin r→GapDifference) (hk : Odd (firstDifferenceCount k)) :
    PowerUpper N (fun t=>initialSignedPatternCap (J t) (u t) (m t) r 300 (q t) (ω t) k) (-223/100) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.firstDifferenceCount, OAI.TraceReconstruction.PowerUpper, OAI.TraceReconstruction.initialSignedPatternCap

  9. theorem OAI.TraceReconstruction.initial_pure_pattern_upper line 130
  10. theorem OAI.TraceReconstruction.increasingTuple_card_le line 152
  11. theorem OAI.TraceReconstruction.initialRankTail_upper line 156
  12. theorem OAI.TraceReconstruction.initialMomentRatio_rate line 178
  13. theorem OAI.TraceReconstruction.initial_fixed_high_tail_rate line 189
  14. theorem OAI.TraceReconstruction.initialSignedDegree_upper line 203
  15. theorem OAI.TraceReconstruction.initialPureDegree_upper line 224
  16. theorem OAI.TraceReconstruction.initialSignedCap_upper line 245
  17. theorem OAI.TraceReconstruction.initialPureCap_upper line 257
  18. theorem OAI.TraceReconstruction.initial_score_caps_eventually line 271

    Source documentation

    Actual scalar budgets, not assumed coefficient bounds: all report- and count-independent caps are strictly below the source clipping allowances.

    theorem initial_score_caps_eventually (hN : Tendsto N atTop atTop)
    (hu : PowerRate N (fun t=>(u t:ℝ)) (123/250))
    (hm : PowerRate N (fun t=>(m t:ℝ)) (62/125)) (hq : PowerRate N q 0)
    (hJ : PowerRate N (fun t=>(J t:ℝ)) (1/125)) (hω : PowerRate N ω 0) (hw : PowerRate N w 0) :
    ∀ᶠt in atTop,
      64*initialSignedCap (J t) (u t) (m t) 3000 300 (q t) (ω t) (w t) ≤ (N t)^(-11/5:ℝ) ∧
      64*initialPureCap (J t) (u t) (m t) 3000 300 (q t) (ω t) (w t) ≤ (N t)^(-7/5:ℝ) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialSignedCap, OAI.TraceReconstruction.initialPureCap

  19. theorem OAI.TraceReconstruction.PowerRate.sub_lower line 294
  20. theorem OAI.TraceReconstruction.PowerRate.nat_sub_lower line 305
  21. def OAI.TraceReconstruction.sourceInitialM line 316

    Source documentation

    Literal integer choices of the initial-pair construction, including the outer floors.

    def sourceInitialM (N : ℝ) : ℕ := ⌊N^(62/125:ℝ)⌋₊
  22. def OAI.TraceReconstruction.sourceInitialK line 317
  23. def OAI.TraceReconstruction.sourceInitialPeriodSize line 318
  24. def OAI.TraceReconstruction.sourceInitialCapacity line 319
  25. def OAI.TraceReconstruction.sourceInitialJ line 320
  26. def OAI.TraceReconstruction.sourceInitialP line 323
  27. def OAI.TraceReconstruction.sourceInitialAnchor line 326

    Source documentation

    One-based manuscript anchors translated once to zero-based list indices.

    def sourceInitialAnchor (q N : ℝ) : ℤ := ((sourceInitialP q N/2:ℕ):ℤ)-1

    Mentions: OAI.TraceReconstruction.sourceInitialP

  28. theorem OAI.TraceReconstruction.sourceInitialM_rate line 328
  29. theorem OAI.TraceReconstruction.sourceInitialK_rate line 333
  30. theorem OAI.TraceReconstruction.sourceInitialPeriodSize_rate line 338
  31. theorem OAI.TraceReconstruction.sourceInitialCapacity_rate line 344
  32. theorem OAI.TraceReconstruction.sourceInitialSide_rate line 351
  33. theorem OAI.TraceReconstruction.sourceInitialJ_rate line 357
  34. theorem OAI.TraceReconstruction.initialOverlap_rate line 368
  35. theorem OAI.TraceReconstruction.deletion_rate_zero line 382
  36. theorem OAI.TraceReconstruction.source_initial_score_caps line 403

    Source documentation

    Mechanical realization of the base scalar score budgets from the actual integer choices and the unchanged known channel.

    theorem source_initial_score_caps {q w : ℕ→ℝ} (hN : Tendsto N atTop atTop)
    (hq : ∀t,q t∈Set.Ioc 0 1)
    (hΛ : Tendsto (fun t=>(q t)^(-3:ℤ)/Real.log (N t)) atTop (𝓝 0))
    (hw : PowerRate N w 0) :
    ∀ᶠt in atTop,
      64*initialSignedCap (sourceInitialJ (q t) (N t)) (sourceInitialK (N t))
        (sourceInitialM (N t)) 3000 300 (q t) (initialOverlapLower (q t)) (w t) ≤ (N t)^(-11/5:ℝ) ∧
      64*initialPureCap (sourceInitialJ (q t) (N t)) (sourceInitialK (N t))
        (sourceInitialM (N t)) 3000 300 (q t) (initialOverlapLower (q t)) (w t) ≤ (N t)^(-7/5:ℝ) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialSignedCap, OAI.TraceReconstruction.sourceInitialJ, OAI.TraceReconstruction.sourceInitialK, OAI.TraceReconstruction.sourceInitialM, OAI.TraceReconstruction.initialOverlapLower, OAI.TraceReconstruction.initialPureCap

  37. def OAI.TraceReconstruction.sourceInitialOffset line 425

    Source documentation

    The manuscript's one-based middle defect, translated to a list index.

    def sourceInitialOffset (m : ℕ) (hm : 4 ≤ m) : Fin m :=
…
  38. theorem OAI.TraceReconstruction.sourceInitialOffset_interior line 428
  39. theorem OAI.TraceReconstruction.sourceInitialOffset_middle line 432
  40. theorem OAI.TraceReconstruction.sourceInitialOffset_safe line 443
  41. theorem OAI.TraceReconstruction.initial_anchor_geometry line 449

    Source documentation

    A literal arithmetic margin implies every base window placement condition.

    theorem initial_anchor_geometry (J K t s : ℕ) (hK : 12*(J+2^s+1) ≤ K) :
    let a : ℤ := (((J*(2*t+1)+K)/2:ℕ):ℤ)-1
…
  42. theorem OAI.TraceReconstruction.prouhetSeries_coeff_zero line 475
  43. theorem OAI.TraceReconstruction.motifPeriodWord_ne line 483

    Source documentation

    Literal source initial words really are different, not only their formal templates.

    theorem motifPeriodWord_ne {m : ℕ} (off : Fin m) (hi : 1 ≤ off.val ∧ off.val+1 < m)
    (u s : ℕ) (a : ℤ) (ha : 0 ≤ a) (hau : a<u) :
    motifPeriodWord off hi u s a (-1) ≠ motifPeriodWord off hi u s a 1 := by
…

    Mentions: OAI.TraceReconstruction.motifPeriodWord

  44. theorem OAI.TraceReconstruction.initial_period_count_bounds line 496

    Source documentation

    Floors in the initial construction waste no more than one long slot.

    theorem initial_period_count_bounds {N : ℝ} {m K t : ℕ}
    (hL : 0<2*m-1) (hN : 0 ≤ N) (hK : (K:ℝ) ≤ ⌊N/(2*m-1:ℕ)⌋₊) :
    let F : ℕ := ⌊N/(2*m-1:ℕ)⌋₊
…
  45. def OAI.TraceReconstruction.sourceHalfMoment line 538

    Source documentation

    Source moment order is twice this integer.

    def sourceHalfMoment (B D : ℕ) (n : ℝ) (i : ℕ) : ℕ :=
…
  46. theorem OAI.TraceReconstruction.sourceEpsilon_le_one line 542
  47. theorem OAI.TraceReconstruction.sourceTargetScale_tendsto line 548
  48. theorem OAI.TraceReconstruction.source_uniform_log_absorption line 566
  49. theorem OAI.TraceReconstruction.totalScoreExponent_bounds line 580
  50. theorem OAI.TraceReconstruction.sourceHalfMoment_bounds line 601
  51. theorem OAI.TraceReconstruction.PowerRate.eventually_lt line 640
  52. theorem OAI.TraceReconstruction.PowerRate.log_base line 647
  53. structure OAI.TraceReconstruction.SourceInitialGeometry line 657

    Source documentation

    Only arithmetic predicates on the literal source integers.

    structure SourceInitialGeometry (q N : ℝ) : Prop where
…
  54. theorem OAI.TraceReconstruction.source_initial_geometry line 670

    Source documentation

    All floor, seed, count, placement and length restrictions are automatic in the actual joint regime; no change of the deletion rate at the base scale.

    theorem source_initial_geometry {q : ℕ→ℝ} (hN : Tendsto N atTop atTop)
    (hq : ∀t,q t∈Set.Ioc 0 1)
    (hΛ : Tendsto (fun t=>(q t)^(-3:ℤ)/Real.log (N t)) atTop (𝓝 0)) :
    ∀ᶠt in atTop,SourceInitialGeometry (q t) (N t) := by
…

    Mentions: OAI.TraceReconstruction.SourceInitialGeometry

  55. theorem OAI.TraceReconstruction.sourceHalfMoment_rate line 729

    Source documentation

    The exact varying even moment order is subpower at EVERY working scale.

    theorem sourceHalfMoment_rate (B : ℕ) (ζ : ℝ) (hB : 2 ≤ B) (hζ : ζ∈Set.Ioo 0 1)
    {n Λ H : ℕ→ℝ} (i : ℕ→ℕ) (hn : Tendsto n atTop atTop) (hH : Tendsto H atTop atTop)
    (hΛ : ∀t,1 ≤ Λ t) (hrel : ∀t,Real.log (n t)=Λ t*H t) :
    PowerRate (fun t=>sourceTargetScale B (sourceDepth B ζ (H t)) (n t) (i t))
      (fun t=>(sourceHalfMoment B (sourceDepth B ζ (H t)) (n t) (i t):ℝ)) 0 := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceHalfMoment

  56. def OAI.TraceReconstruction.sourceInitialWeight line 773

    Source documentation

    Actual primitive-score weight at the base scale.

    def sourceInitialWeight (q : ℝ) (k : ℕ) : ℝ := (6*(2*k:ℕ):ℝ)*(2/q)
  57. theorem OAI.TraceReconstruction.sourceInitialWeight_rate line 775
  58. def OAI.TraceReconstruction.initialClipFactor line 796
  59. theorem OAI.TraceReconstruction.initialClipFactor_rate line 800
  60. theorem OAI.TraceReconstruction.initial_clip_exp_bound line 809

    Source documentation

    The source moment is genuinely used in clipping: the exponent is linear in that moment, not a fixed negative power of the intermediate length.

    theorem initial_clip_exp_bound (hN : Tendsto N atTop atTop)
    (hq : PowerRate N q 0) (hw : PowerRate N w 0) (hk : ∀ᶠt in atTop,1 ≤ k t) :
    ∀ᶠt in atTop,
      Real.sqrt (6*(initialClipFactor (N t) (q t) (w t))^(k t)) ≤
        Real.exp (-(k t:ℝ)*Real.log (N t)/2000) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialClipFactor

  61. theorem OAI.TraceReconstruction.initial_metadata_exp_bound line 838

    Source documentation

    The fixed metadata tails also beat the varying moment times log-scale. Their exponents have orders .988 and .008 respectively, while k log N has order zero.

    theorem initial_metadata_exp_bound (hN : Tendsto N atTop atTop)
    (hq : PowerRate N q 0) (hω : PowerRate N (fun t=>initialOverlapLower (q t)) 0)
    (hk : PowerRate N (fun t=>(k t:ℝ)) 0) :
    ∀ᶠt in atTop,
      2*Real.exp (-((sourceInitialK (N t)*sourceInitialM (N t):ℕ):ℝ)*(q t)^4/64)+
        Real.exp (-(sourceInitialJ (q t) (N t):ℝ)*(initialOverlapLower (q t))^4/16) ≤
        3*Real.exp (-(k t:ℝ)*Real.log (N t)) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialOverlapLower, OAI.TraceReconstruction.sourceInitialK, OAI.TraceReconstruction.sourceInitialM, OAI.TraceReconstruction.sourceInitialJ

  62. theorem OAI.TraceReconstruction.initial_error_eventually line 859

    Source documentation

    A completely quantitative sufficient moment inequality for the actual initial error. This is later discharged by the literal ceiling r_0/2.

    theorem initial_error_eventually {n A : ℕ→ℝ} (hN : Tendsto N atTop atTop)
    (hn : Tendsto n atTop atTop) (hA : ∀ᶠt in atTop,1 ≤ A t)
    (hq : ∀t,q t∈Set.Ioc 0 1)
    (hΛ : Tendsto (fun t=>(q t)^(-3:ℤ)/Real.log (N t)) atTop (𝓝 0))
    (hk : PowerRate N (fun t=>(k t:ℝ)) 0) (hk1 : ∀ᶠt in atTop,1 ≤ k t)
    (hmoment : ∀ᶠt in atTop, 10^6*A t*Real.log (n t) ≤ (k t:ℝ)*Real.log (N t)) :
    ∀ᶠt in atTop,
      initialErrorCap (sourceInitialJ (q t) (N t)) (sourceInitialK (N t))
        (sourceInitialM (N t)) (k t) (q t) (initialOverlapLower (q t))
        (sourceInitialWeight (q t) (k t)) ≤ (n t)^(-100*A t) := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialErrorCap, OAI.TraceReconstruction.sourceInitialJ, OAI.TraceReconstruction.sourceInitialK, OAI.TraceReconstruction.sourceInitialM, OAI.TraceReconstruction.initialOverlapLower, OAI.TraceReconstruction.sourceInitialWeight

  63. theorem OAI.TraceReconstruction.PowerRate.add_lower line 910
  64. theorem OAI.TraceReconstruction.PowerRate.nat_ceil line 921
  65. def OAI.TraceReconstruction.sourceOverlapConstant line 926
  66. def OAI.TraceReconstruction.sourceInitialCount line 927
  67. theorem OAI.TraceReconstruction.sourceInitialP_rate line 930
  68. theorem OAI.TraceReconstruction.sourceOverlapConstant_rate line 942
  69. theorem OAI.TraceReconstruction.sourceInitialCount_rate line 948
  70. theorem OAI.TraceReconstruction.sourceOverlapConstant_pos line 957
  71. theorem OAI.TraceReconstruction.sourceOverlapConstant_large line 961
  72. def OAI.TraceReconstruction.sourceInitialWord line 979
  73. def OAI.TraceReconstruction.sourceInitialPure line 985
  74. def OAI.TraceReconstruction.sourceInitialError line 988
  75. theorem OAI.TraceReconstruction.sourceInitialWord_length line 992
  76. theorem OAI.TraceReconstruction.sourceInitialWord_different line 997
  77. theorem OAI.TraceReconstruction.source_initial_oracles_eventually line 1018

    Source documentation

    The actual initial proof, with no oracle or coefficient-bound hypothesis. The only moment restriction is the quantitative source ceiling inequality.

    theorem source_initial_oracles_eventually {N q n A : ℕ→ℝ} {k : ℕ→ℕ}
    (hN : Tendsto N atTop atTop) (hn : Tendsto n atTop atTop)
    (hA : ∀ᶠt in atTop,1 ≤ A t) (hq : ∀t,q t∈Set.Ioc 0 (1/2:ℝ))
    (hΛ : Tendsto (fun t=>(q t)^(-3:ℤ)/Real.log (N t)) atTop (𝓝 0))
    (hk : PowerRate N (fun t=>(k t:ℝ)) 0) (hk1 : ∀ᶠt in atTop,1 ≤ k t)
    (hmoment : ∀ᶠt in atTop,10^6*A t*Real.log (n t) ≤ (k t:ℝ)*Real.log (N t)) :
    ∀ᶠt in atTop,
      SourceInitialGeometry (q t) (N t) ∧
      sourceInitialError (q t) (N t) (k t) ≤ (n t)^(-100*A t) ∧
      Nonempty (OracleTracePair (q t) (sourceInitialWord (q t) (N t) (-1))
        (sourceInitialWord (q t) (N t) 1) (k t) (sourceInitialError (q t) (N t) (k t)) ((N t)^(-11/5:ℝ))) ∧
      Nonempty (OracleTracePair (q t) (sourceInitialPure (q t) (N t))
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.SourceInitialGeometry, OAI.TraceReconstruction.sourceInitialError, OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.sourceInitialWord, OAI.TraceReconstruction.sourceInitialPure

  78. theorem OAI.TraceReconstruction.sourceInitialCount_bounds line 1076

    Source documentation

    Literal count instantiation; the harmless ceiling is included.

    theorem sourceInitialCount_bounds {q N : ℝ} (hq : q ∈ Set.Ioc 0 (1/2:ℝ))
    (H : SourceInitialGeometry q N) :
    sourceInitialP q N*sourceInitialPeriodSize N  ≤  sourceInitialCount q N ∧
    (sourceInitialCount q N:ℝ)  ≤  (sourceOverlapConstant q)^2*
      ((sourceInitialP q N*sourceInitialPeriodSize N:ℕ):ℝ) := by
…

    Mentions: OAI.TraceReconstruction.SourceInitialGeometry, OAI.TraceReconstruction.sourceInitialP, OAI.TraceReconstruction.sourceInitialPeriodSize, OAI.TraceReconstruction.sourceInitialCount, OAI.TraceReconstruction.sourceOverlapConstant

  79. theorem OAI.TraceReconstruction.OracleTracePair.transfer_power_overlap line 1134

    Source documentation

    Genuine overlap stability for complete traces of powers.

    theorem OracleTracePair.transfer_power_overlap {q E V p : ℝ} {x y : List Bool} {k F : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q ∈ Set.Icc 0 1) (hk : 1 ≤ k)
    (hov : p ≤ listTraceOverlap q hq (pureAtomRun y F) (pureAtomRun y (F+1))) :
    p-(Real.sqrt ((F:ℝ)*V)+2*(F:ℝ)*E)-
      (Real.sqrt (((F+1:ℕ):ℝ)*V)+2*((F+1:ℕ):ℝ)*E)  ≤ 
      listTraceOverlap q hq (pureAtomRun x F) (pureAtomRun x (F+1)) := by
…

    Mentions: OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.pureAtomRun

  80. theorem OAI.TraceReconstruction.powerTransferBudget_mono line 1168
  81. theorem OAI.TraceReconstruction.source_initial_power_overlap line 1176
  82. theorem OAI.TraceReconstruction.source_initial_overlap_budget_eventually line 1219

    Source documentation

    The exact initial overlap error is negligible, including channel-dependent count factors. This is a consequence, not a hypothesis of the initial pair.

    theorem source_initial_overlap_budget_eventually {q N E : ℕ→ℝ}
    (hN : Tendsto N atTop atTop) (hq : PowerRate N q 0)
    (hω : PowerRate N (fun t=>initialOverlapLower (q t)) 0)
    (hE : ∀ᶠt in atTop,0 ≤ E t ∧ E t ≤ (N t)^(-100:ℝ)) :
    ∀ᶠt in atTop,Real.sqrt (((sourceInitialCount (q t) (N t)+1:ℕ):ℝ)*((N t)^(-7/5:ℝ)))+
      2*((sourceInitialCount (q t) (N t)+1:ℕ):ℝ)*E t ≤ 1/16 := by
…

    Mentions: OAI.TraceReconstruction.PowerRate, OAI.TraceReconstruction.initialOverlapLower, OAI.TraceReconstruction.sourceInitialCount

  83. theorem OAI.TraceReconstruction.source_initial_level_eventually line 1248
  84. theorem OAI.TraceReconstruction.sourceScaleProduct_le_one line 1292

    Source documentation

    All backwards targets are no larger than n, with the source epsilon.

    theorem sourceScaleProduct_le_one (B D i : ℕ) (hB : 2 ≤ B) : sourceScaleProduct B D i ≤ 1 := by
…

    Mentions: OAI.TraceReconstruction.sourceScaleProduct

  85. theorem OAI.TraceReconstruction.sourceTargetScale_le line 1315
  86. theorem OAI.TraceReconstruction.sourceHalfMoment_sufficient line 1319
  87. theorem OAI.TraceReconstruction.source_initial_at_smallest_scale line 1347

    Source documentation

    The source base invariant, with literal target scales, moment ceiling, error threshold, count and overlap, uniformly in the joint deletion regime.

    theorem source_initial_at_smallest_scale (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]⟩
      (sourceTargetScale B (sourceDepth B ζ ((q t)^3*Real.log (n t))) (n t) 0)
      ((n t)^(-100*(totalScoreExponent B (sourceDepth B ζ ((q t)^3*Real.log (n t)))+B+1)))
      (11/5) (initialOverlapLower (q t)) ((sourceOverlapConstant (q t))^2) 0
      (sourceHalfMoment B (sourceDepth B ζ ((q t)^3*Real.log (n t))) (n t) 0)) := by
…

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