ErrorRates.lean`

62 declarations, 0 contain sorry, 0 declared as axioms

ErrorRates

Realization of block caps, sparse scales, sharp and smoothing budgets, tree tails, fit errors, and uniform polynomial/exponential bounds.

theorem OAI.TraceReconstruction.sourceWindowSize_le line 22

theorem OAI.TraceReconstruction.SourceArithmeticBounds.scheduled_trials line 30

Source comment

We use only positive target scales below.

theorem SourceArithmeticBounds.scheduled_trials {C N F ε : ℝ} {s b ell k : ℕ}
    (H : SourceArithmeticBounds C N F ε s b ell k) (hN : 0 < N) (hC : 0 < C) (hF : 0 < F)
    (j : ℕ) (hj : j+1 < b) :
    N^(scaleKappa b (j+2) ε+ε)/(4800*(C^(2*b)*F)) ≤
      (sourceScheduledTrials (sourceBlockWindows N b ε) (sourceArithmeticTrials C N b ε ell k) (j+1):ℝ) := by
…

Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceBlockWindows, OAI.TraceReconstruction.sourceArithmeticTrials

theorem OAI.TraceReconstruction.SourceArithmeticBounds.binomial_caps line 63
theorem OAI.TraceReconstruction.sourceSparseCount_scale line 94
theorem OAI.TraceReconstruction.sourceLeafCount_succ line 109
theorem OAI.TraceReconstruction.sourceLeafCount_le_length line 113
theorem OAI.TraceReconstruction.sourceArithmeticLength_eq_block line 123
theorem OAI.TraceReconstruction.SourceArithmeticBounds.leaf_bound line 130
theorem OAI.TraceReconstruction.source_sparse_weight_bound line 152
Source documentation
Full sparse degree, with the excluded bottom window and the exact source gap. This is the high-degree geometric gain, before constants.
```
theorem source_sparse_weight_bound (N ε d W w : ℝ) (b s : ℕ) (hN : 0 < N) (hW : 0 ≤ W)
    (hw : w^2 ≤ W*N^(-scaleA b 0 ε*d)) :
    w^2*(sourceSparseCount (sourceBlockWindows N b ε) s (b-1):ℝ) ≤
      W*((2^s:ℕ):ℝ)*N^(-(scaleA b 0 ε*d-sourceInteriorExponent b ε)) := by
…
```
Mentions: OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.sourceBlockWindows, OAI.TraceReconstruction.sourceInteriorExponent
def OAI.TraceReconstruction.sourceBadRoleFactor line 174
def OAI.TraceReconstruction.sourceForcedRoleFactor line 177

theorem OAI.TraceReconstruction.source_sharp_numeric line 183

Source documentation

Explicit finite sharp energy bound. The two undesirable pattern classes are suppressed by eta and a, and the genuine binary forced skeleton pays its full source exponent. The high tail uses the sparse, not dense count.

theorem source_sharp_numeric (T n : ℕ→ℕ) (s b R : ℕ) (ω η a w N ε d K W Q gap : ℝ)
    (hN : 1 ≤ N) (hK : 0 ≤ K) (hW : 0 ≤ W) (_hQ : 0 ≤ Q)
    (hleaves : (SourceLeafCount T (b+1):ℝ) ≤ N) (hwone : w^2 ≤ 1)
    (hw : w^2 ≤ W*N^(-scaleA (b+1) 0 ε*d))
    (hsmall : w^2*((2^s:ℕ):ℝ)*(sourceSparseCount T s b:ℝ) ≤ 1)
    (hhalf : w^2*(sourceSparseCount T s b:ℝ) ≤ 1/2)
    (hsparse : w^2*(sourceSparseCount T s b:ℝ) ≤ Q*N^(-gap))
    (hn : ∀j≤b,hiddenBinomialCap (n j) ω ≤ K*N^(-ε/2))
    (hg : ∀j<b,hiddenBinomialCap (sourceScheduledTrials T n (j+1)) ω ≤
      K*N^(-(scaleKappa (b+1) (j+2) ε+ε)/2)) :
    sourceSharpEnergyBudget T n s b R ω η a w ≤
      sourceBadRoleFactor b R*N^R*(η^2+a^2)+
…

Mentions: OAI.TraceReconstruction.SourceLeafCount, OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenBinomialCap, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.sourceSharpEnergyBudget, OAI.TraceReconstruction.sourceBadRoleFactor

def OAI.TraceReconstruction.sourceSmoothingPrefactor line 264
theorem OAI.TraceReconstruction.hiddenSmoothingBound_scale line 267
theorem OAI.TraceReconstruction.sourceLeafCount_positive line 306
theorem OAI.TraceReconstruction.sourceFitTail_simple line 314
theorem OAI.TraceReconstruction.windowCollection_card_bound line 336
theorem OAI.TraceReconstruction.collectionCount_lower line 352
theorem OAI.TraceReconstruction.sourceEffectiveHiddenTail_simple line 365

theorem OAI.TraceReconstruction.SourceArithmeticBounds.fit_exponent line 394

Source documentation

The literal centering fluctuation has the source epsilon exponent. This does not treat nested window starts as independent.

theorem SourceArithmeticBounds.fit_exponent {C N F ε : ℝ} {s b ell k j : ℕ}
    (H : SourceArithmeticBounds C N F ε s b ell k) (hC : 0<C) (hF : 0<F) (hN : 1 ≤ N) (he : 0 ≤ ε)
    (hκ : ∀v<b,3*ε ≤ scaleKappa b (v+1) ε) (hj : j+1<b) :
    N^ε/512 ≤ 2*((sourceBlockWindows N b ε j:ℝ)/8)^2 /
      (((sourceBlockWindows N b ε (j+1):ℝ)+1)*(sourceArithmeticTrials C N b ε ell k j:ℝ)) := by
…

Mentions: OAI.TraceReconstruction.SourceArithmeticBounds, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.sourceBlockWindows, OAI.TraceReconstruction.sourceArithmeticTrials

def OAI.TraceReconstruction.SourcePolyUpper line 442
Source documentation
A convenience for the manuscript's fixed-B polynomial losses. This predicate is only used to prove bounds on the literal finite constants.
```
def SourcePolyUpper (f : ℕ→ℝ) : Prop :=
…
```
theorem OAI.TraceReconstruction.SourcePolyUpper.const line 445
theorem OAI.TraceReconstruction.SourcePolyUpper.depth line 450
theorem OAI.TraceReconstruction.SourcePolyUpper.mono line 453
theorem OAI.TraceReconstruction.SourcePolyUpper.add line 458
theorem OAI.TraceReconstruction.SourcePolyUpper.mul line 469
theorem OAI.TraceReconstruction.SourcePolyUpper.pow line 480
theorem OAI.TraceReconstruction.sourceEpsilon_inverse_poly line 487
theorem OAI.TraceReconstruction.totalScoreExponent_poly line 494
theorem OAI.TraceReconstruction.SourcePolyUpper.ceil line 502
theorem OAI.TraceReconstruction.sourceCancellationOrder_poly line 508
theorem OAI.TraceReconstruction.sourceCancellationOrder_large line 526
def OAI.TraceReconstruction.SourceExpUpper line 541
Source documentation
Literal finite-block factors are subpower uniformly over the joint deletion regime when their logarithms grow polynomially in the depth.
```
def SourceExpUpper (f : ℕ→ℝ→ℝ) : Prop :=
…
```
theorem OAI.TraceReconstruction.SourcePolyUpper.expUpper line 545
theorem OAI.TraceReconstruction.SourceExpUpper.const line 555
theorem OAI.TraceReconstruction.SourceExpUpper.mono line 558
theorem OAI.TraceReconstruction.SourceExpUpper.mul line 563
theorem OAI.TraceReconstruction.SourceExpUpper.pow_variably line 582
theorem OAI.TraceReconstruction.SourceExpUpper.pow line 596
theorem OAI.TraceReconstruction.sourceOverlapConstant_expUpper line 601
theorem OAI.TraceReconstruction.initialOverlapLower_inverse_expUpper line 608

theorem OAI.TraceReconstruction.SourceExpUpper.uniform line 622

Source documentation

All indices are inside the same physical n,q instance.

theorem SourceExpUpper.uniform (f : ℕ→ℝ→ℝ) (hf : SourceExpUpper f)
    (B : ℕ) (ζ δ : ℝ) (hB : 2 ≤ B) (hζ : ζ∈Set.Ioo 0 1) (hδ : 0<δ)
    {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,f (sourceDepth B ζ ((q t)^3*Real.log (n t))) (q t) ≤
      (sourceTargetScale B (sourceDepth B ζ ((q t)^3*Real.log (n t))) (n t) i)^(
        δ*sourceEpsilon B (sourceDepth B ζ ((q t)^3*Real.log (n t)))) := by
…

Mentions: OAI.TraceReconstruction.SourceExpUpper, OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceEpsilon

def OAI.TraceReconstruction.sourceMomentEnvelope line 645
def OAI.TraceReconstruction.sourceCapEnvelope line 648
def OAI.TraceReconstruction.sourceWeightEnvelope line 651
theorem OAI.TraceReconstruction.sourceMomentEnvelope_pos line 653
theorem OAI.TraceReconstruction.sourceCapEnvelope_pos line 657
theorem OAI.TraceReconstruction.sourceMomentEnvelope_expUpper line 661
theorem OAI.TraceReconstruction.sourceCapEnvelope_expUpper line 672
theorem OAI.TraceReconstruction.sourceWeightEnvelope_expUpper line 683
theorem OAI.TraceReconstruction.sourceMotif_expUpper line 688
theorem OAI.TraceReconstruction.sourceSmoothingPrefactor_expUpper line 692
theorem OAI.TraceReconstruction.sourceSkeletonPrefactor_expUpper line 709
theorem OAI.TraceReconstruction.SourceArithmeticBounds.fit_tail line 731
theorem OAI.TraceReconstruction.SourceArithmeticBounds.metadata_tail line 742

theorem OAI.TraceReconstruction.source_clipping_moment_power line 764

Source documentation

Quantitative clipping without any default-limit increase or limiting interchange: the power is the finite even moment actually used by the oracle.

theorem source_clipping_moment_power (T : ℕ→ℕ) (s b k : ℕ) (N gap L : ℝ)
    (hN : 0<N)
    (hhalf : ((6*(2*k:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤ 1/2)
    (hscale : ((6*(2*k:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤ N^(-gap/2)/8) :
    Real.sqrt (6*(4*sourceCenteredBudget T s b k L)^k) ≤ 3*N^(-gap*(k:ℝ)/4) := by
…

Mentions: OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.sourceCenteredBudget

theorem OAI.TraceReconstruction.SourceExpUpper.add line 799
def OAI.TraceReconstruction.sourceScaleInverseEnvelope line 826
theorem OAI.TraceReconstruction.sourceScaleInverseEnvelope_expUpper line 828
theorem OAI.TraceReconstruction.source_log_scale_lower line 837
theorem OAI.TraceReconstruction.SourceExpUpper.uniform_log line 847

theorem OAI.TraceReconstruction.SourceExpUpper.uniform_tail line 895

Source documentation

Uniform exponential domination at every working scale, with the full depth and the varying known deletion probability retained.

theorem SourceExpUpper.uniform_tail {f g h : ℕ→ℝ→ℝ}
    (hf : SourceExpUpper f) (hg : SourceExpUpper g) (hh : SourceExpUpper h)
    (hf0 : ∀D q,q∈Set.Ioc 0 (1/2:ℝ) → 0<f D q)
    (_hg0 : ∀D q,q∈Set.Ioc 0 (1/2:ℝ) → 0≤g D q)
    (hh0 : ∀D q,q∈Set.Ioc 0 (1/2:ℝ) → 0≤h D q)
    (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,
      g (sourceDepth B ζ ((q t)^3*Real.log (n t))) (q t)*
        Real.exp (-(sourceTargetScale B (sourceDepth B ζ ((q t)^3*Real.log (n t))) (n t) i)^
          (sourceEpsilon B (sourceDepth B ζ ((q t)^3*Real.log (n t))))/
…

Mentions: OAI.TraceReconstruction.SourceExpUpper, OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceEpsilon