LayoutRates.lean`

75 declarations, 0 contain sorry, 0 declared as axioms

LayoutRates

Integer block schedules, rounding, length and trial margins, sparse gaps, and forced-anchor decay.

def OAI.TraceReconstruction.sourceWindowSize line 23
Source documentation
The source integer window size, with zero-based nesting index.
```
def sourceWindowSize (N : ℝ) (b : ℕ) (ε : ℝ) (j : ℕ) : ℕ :=
…
```
def OAI.TraceReconstruction.sourceLocalTrials line 27
Source documentation
At a nonroot node the source trial count is an even integer.
```
def sourceLocalTrials (P h : ℕ) : ℕ := 2*(P/(100*(2*h+1)))
```
def OAI.TraceReconstruction.sourceRootTrials line 30
Source documentation
The root schedule count: the literal floor after subtracting its window.
```
def sourceRootTrials (N : ℝ) (S T h : ℕ) : ℕ :=
…
```
structure OAI.TraceReconstruction.SourceArithmeticStage line 35
Source documentation
Literal length and overlap-count state of one nested source block. copies and trials refer to the transition into this state.
```
structure SourceArithmeticStage where
…
```
def OAI.TraceReconstruction.sourceArithmeticStages line 41
def OAI.TraceReconstruction.sourceArithmeticP line 53
def OAI.TraceReconstruction.sourceArithmeticTrials line 56
def OAI.TraceReconstruction.sourceArithmeticLength line 59
def OAI.TraceReconstruction.sourceArithmeticCount line 62
theorem OAI.TraceReconstruction.sourceLocalTrials_even line 65
theorem OAI.TraceReconstruction.sourceLocalTrials_budget line 68
theorem OAI.TraceReconstruction.sourceLocalTrials_reserves line 74
theorem OAI.TraceReconstruction.sourceWindowSize_even line 92
theorem OAI.TraceReconstruction.sourceArithmeticLength_step line 97
theorem OAI.TraceReconstruction.sourceArithmeticCount_step line 101
theorem OAI.TraceReconstruction.sourceArithmetic_inner_trials line 105
theorem OAI.TraceReconstruction.sourceArithmetic_root_copies line 110
theorem OAI.TraceReconstruction.sourceArithmetic_count_lift line 117

theorem OAI.TraceReconstruction.sourceWindowSize_bounds line 129

Source documentation

Rounding the source windows loses at most a factor two.

theorem sourceWindowSize_bounds {N ε : ℝ} {b j : ℕ}
    (h : 8 ≤ N^(scaleKappa b (j+1) ε)) :
    N^(scaleKappa b (j+1) ε)/2 ≤ (sourceWindowSize N b ε j:ℝ) ∧
      (sourceWindowSize N b ε j:ℝ) ≤ N^(scaleKappa b (j+1) ε) := by
…

Mentions: OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.sourceWindowSize

theorem OAI.TraceReconstruction.sourceLocalTrials_bounds line 141
Source documentation
The nonroot even trial count is between one and two times its unrounded quotient once the quotient is at least two.
```
theorem sourceLocalTrials_bounds (P h : ℕ) (hlarge : (200:ℝ)*(2*h+1) ≤ P) :
    (P:ℝ)/(100*(2*h+1)) ≤ (sourceLocalTrials P h:ℝ) ∧
      (sourceLocalTrials P h:ℝ) ≤ (P:ℝ)/(50*(2*h+1)) := by
…
```
Mentions: OAI.TraceReconstruction.sourceLocalTrials
theorem OAI.TraceReconstruction.source_floor_length_bounds line 159
theorem OAI.TraceReconstruction.sourceRootTrials_floor line 173
Source documentation
The real floor and integer division versions of the root are identical whenever its remaining ambient count is nonnegative.
```
theorem sourceRootTrials_floor {N : ℝ} {S T h : ℕ}
    (hT : T ≤ ⌊N/(S:ℝ)⌋₊) :
    sourceRootTrials N S T h=⌊((⌊N/(S:ℝ)⌋₊:ℝ)-T)/(2*h+1)⌋₊ := by
…
```
Mentions: OAI.TraceReconstruction.sourceRootTrials
theorem OAI.TraceReconstruction.source_root_length_bounds line 180
theorem OAI.TraceReconstruction.source_ceil_count_bounds line 211
theorem OAI.TraceReconstruction.source_scale_target_step line 237
theorem OAI.TraceReconstruction.sourceWindowSize_le_previous line 245

theorem OAI.TraceReconstruction.source_root_margins line 261

Source documentation

The root's subtraction and rounding margins follow from the one subpower comparison N^epsilon >= 8F.

theorem source_root_margins {N X u F : ℝ} {S h T : ℕ}
    (hS : 1 ≤ S) (hX : (S:ℝ) ≤ X) (hF : 1 ≤ F) (hu : 8*F ≤ u)
    (hh : (h:ℝ) ≤ F*S) (hT : (T:ℝ) ≤ X) (hrel : X^2*u=N) :
    T ≤ ⌊N/(S:ℝ)⌋₊ ∧ (2*(h:ℝ)+2)*S ≤ N/2 := by
…

theorem OAI.TraceReconstruction.source_arithmetic_inner_copies line 282
theorem OAI.TraceReconstruction.source_arithmetic_root_copies line 287

theorem OAI.TraceReconstruction.source_arithmetic_lengths line 303

Source documentation

All nested lengths and overlap counts for the literal floors/ceilings. Only the scalar subpower margin is needed for every rounding step.

theorem source_arithmetic_lengths {C N F ε : ℝ} {b ell k : ℕ}
    (hC : 2 ≤ C) (hN : 1 ≤ N) (hF : 1 ≤ F) (he : 0 ≤ ε)
    (ha : ∀j ≤ b,0 ≤ scaleA b j ε)
    (hsmall : 8*C^(2*b)*F ≤ N^ε)
    (hell : N^(scaleA b 0 ε)/2 ≤ (ell:ℝ)) (hell' : (ell:ℝ) ≤ N^(scaleA b 0 ε))
    (hk : ell ≤ k) (hk' : (k:ℝ) ≤ F*ell) :
    ∀j ≤ b,
      N^(scaleA b j ε)/2 ≤ (sourceArithmeticLength C N b ε ell k j:ℝ) ∧
      (sourceArithmeticLength C N b ε ell k j:ℝ) ≤ N^(scaleA b j ε) ∧
      sourceArithmeticLength C N b ε ell k j ≤ sourceArithmeticCount C N b ε ell k j ∧
      (sourceArithmeticCount C N b ε ell k j:ℝ) ≤
        C^(2*j)*F*sourceArithmeticLength C N b ε ell k j := by
…

Mentions: OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.sourceArithmeticLength, OAI.TraceReconstruction.sourceArithmeticCount

theorem OAI.TraceReconstruction.source_copies_bounds line 381
theorem OAI.TraceReconstruction.source_inner_trials_scale line 391
theorem OAI.TraceReconstruction.source_root_trials_scale line 420
def OAI.TraceReconstruction.sourceDegreeCutoff line 452
def OAI.TraceReconstruction.sourceCancellationOrder line 454
def OAI.TraceReconstruction.sourceChannelLogConstant line 457
theorem OAI.TraceReconstruction.sourceChannelLogConstant_pos line 459
theorem OAI.TraceReconstruction.deletion_inverse_cube_ge_one line 463
theorem OAI.TraceReconstruction.deletion_inverse_le_cube line 468
theorem OAI.TraceReconstruction.sourceOverlapConstant_log_bound line 477
theorem OAI.TraceReconstruction.sourceOverlapConstant_ge_two line 497
theorem OAI.TraceReconstruction.source_count_factor_exp_bound line 506
Source documentation
The whole block-count loss, including every nesting and every earlier block, is bounded by a single exp(O_B((D+1)Lambda)).
```
theorem source_count_factor_exp_bound {q : ℝ} (hq : q∈Set.Ioc 0 (1/2:ℝ))
    (B D b i : ℕ) (hb : b ≤ B) (hi : i ≤ D) :
    8*(sourceOverlapConstant q)^(2*b)*(sourceOverlapConstant q)^(2*B*i+2) ≤
      Real.exp ((8+sourceChannelLogConstant*(2*B+2))*((D:ℝ)+1)*q^(-3:ℤ)) := by
…
```
Mentions: OAI.TraceReconstruction.sourceOverlapConstant, OAI.TraceReconstruction.sourceChannelLogConstant
theorem OAI.TraceReconstruction.source_uniform_count_margin line 539
theorem OAI.TraceReconstruction.sourceEpsilon_power_small line 565
Source documentation
Tiny epsilon estimates are uniform in the varying block depth.
```
theorem sourceEpsilon_power_small (B D m : ℕ) (hm : m ≤ 4*B+100) :
    (2:ℝ)^m*sourceEpsilon B D ≤ 1 := by
…
```
Mentions: OAI.TraceReconstruction.sourceEpsilon
theorem OAI.TraceReconstruction.scaleA_mono_index line 574
theorem OAI.TraceReconstruction.scaleA_le_geometric line 581
theorem OAI.TraceReconstruction.sourceKappa_three_epsilon line 592
theorem OAI.TraceReconstruction.sourceA_nonneg line 622
def OAI.TraceReconstruction.sourceInteriorExponent line 632
Source documentation
The interior scale mass excludes the bottom window, as required by the sparse role count rather than the much larger total leaf count.
```
def sourceInteriorExponent (b : ℕ) (ε : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.two_power_sum_shift line 635
theorem OAI.TraceReconstruction.sourceInteriorExponent_upper line 641
theorem OAI.TraceReconstruction.scaleA_zero_simple_lower line 662
theorem OAI.TraceReconstruction.source_sparse_gap line 670
Source documentation
Quantitative sparse gap, keeping its growth in d. Both the two-dimensional warmup and the post-warmup dimension satisfy this common estimate.
```
theorem source_sparse_gap (B D b : ℕ) (d : ℝ) (hb1 : 1 ≤ b) (_hb : b ≤ B)
    (hd : 11/5 ≤ d) (hcases : b=2 ∨ (b=B ∧ (2:ℝ)^B+2 ≤ d)) :
    (d+1)/(128*(2:ℝ)^(2*B)) ≤
      scaleA b 0 (sourceEpsilon B D)*d-sourceInteriorExponent b (sourceEpsilon B D) := by
…
```
Mentions: OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceInteriorExponent
theorem OAI.TraceReconstruction.totalScoreExponent_step line 724
theorem OAI.TraceReconstruction.totalScoreExponent_after_warmup line 730
theorem OAI.TraceReconstruction.source_level_sparse_gap line 739
def OAI.TraceReconstruction.sourceBlockWindows line 761
Source documentation
Levels outside the finite source block are irrelevant. Their harmless positive extension permits the global-index API of the finite tree lemmas.
```
def sourceBlockWindows (N : ℝ) (b : ℕ) (ε : ℝ) (j : ℕ) : ℕ :=
…
```
structure OAI.TraceReconstruction.SourceArithmeticBounds line 764

theorem OAI.TraceReconstruction.source_arithmetic_geometry line 780

Source documentation

Exact layout inequalities for the literal recursive integer construction. The hypotheses are just two scalar subpower margins and the exact scale identities, not any probabilistic producer or new overlap premise.

theorem source_arithmetic_geometry {C N F ε : ℝ} {s b ell k : ℕ}
    (hC : 2 ≤ C) (hN : 1 ≤ N) (hF : 1 ≤ F) (he : 0 ≤ ε)
    (ha : ∀j ≤ b,0 ≤ scaleA b j ε) (hκ : ∀j<b,3*ε ≤ scaleKappa b (j+1) ε)
    (hsmall : 1200*C^(2*b)*F ≤ N^ε) (hmotif : 48*((2^s:ℕ):ℝ) ≤ N^ε)
    (hell : N^(scaleA b 0 ε)/2 ≤ (ell:ℝ)) (hell' : (ell:ℝ) ≤ N^(scaleA b 0 ε))
    (hk : ell ≤ k) (hk' : (k:ℝ) ≤ F*ell) :
    SourceArithmeticBounds C N F ε s b ell k := by
…

Mentions: OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.SourceArithmeticBounds

theorem OAI.TraceReconstruction.SourceArithmeticBounds.layout line 855
theorem OAI.TraceReconstruction.SourceArithmeticBounds.window_positive line 884
def OAI.TraceReconstruction.binaryTreeExponent line 902
Source documentation
Exact exponent of the full binary forced skeleton, in the same bottom-up order as binaryTreeBudget.
```
def binaryTreeExponent (e : ℕ → ℝ) : ℕ → ℝ
  | 0 => 0
  | b+1 => e b+2*binaryTreeExponent e b
```
theorem OAI.TraceReconstruction.binaryTreeExponent_sum line 906
theorem OAI.TraceReconstruction.binaryTreeBudget_mono line 922
theorem OAI.TraceReconstruction.binaryTreeBudget_scaled line 937
theorem OAI.TraceReconstruction.binaryTreeBudget_const line 955
theorem OAI.TraceReconstruction.source_interior_product line 966

theorem OAI.TraceReconstruction.sourceForcedBudget_degree_factor line 974

Source documentation

Pull all extra selected leaves into the sparse-degree small factor. Only the mandatory 2^(b+1) bottom leaves pay the old score exponent.

theorem sourceForcedBudget_degree_factor (T n : ℕ → ℕ) (s b r : ℕ) (ω w : ℝ)
    (hr : 2^(b+1) ≤ r) :
    w^(2*r)*sourceForcedBudget T n s b r ω=
      (OccupiedParityTree.shapeRoleConstant r (b+1):ℝ)*
      (w^2*((2^s:ℕ):ℝ)*(sourceSparseCount T s b:ℝ))^(r-2^(b+1))*
      (w^2)^(2^(b+1))*
      ((2*((2^s:ℕ):ℝ)^3*hiddenBinomialCap (n b) ω)*
        binaryTreeBudget (fun j => 4*((2^s:ℕ):ℝ)^6*
          hiddenBinomialCap (sourceScheduledTrials T n (j+1)) ω*hiddenBinomialCap (n j) ω) b) := by
…

Mentions: OAI.TraceReconstruction.sourceForcedBudget, OAI.TraceReconstruction.OccupiedParityTree.shapeRoleConstant, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenBinomialCap, OAI.TraceReconstruction.binaryTreeBudget, OAI.TraceReconstruction.sourceScheduledTrials

theorem OAI.TraceReconstruction.sourceForcedBudget_degree_le line 993

Source documentation

The remaining extra-degree factor costs no scale power.

theorem sourceForcedBudget_degree_le (T n : ℕ → ℕ) (s b r : ℕ) (ω w : ℝ)
    (hr : 2^(b+1) ≤ r)
    (hsmall : w^2*((2^s:ℕ):ℝ)*(sourceSparseCount T s b:ℝ) ≤ 1) :
    w^(2*r)*sourceForcedBudget T n s b r ω ≤
      (OccupiedParityTree.shapeRoleConstant r (b+1):ℝ)*(w^2)^(2^(b+1))*
      ((2*((2^s:ℕ):ℝ)^3*hiddenBinomialCap (n b) ω)*
        binaryTreeBudget (fun j => 4*((2^s:ℕ):ℝ)^6*
          hiddenBinomialCap (sourceScheduledTrials T n (j+1)) ω*hiddenBinomialCap (n j) ω) b) := by
…

Mentions: OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.sourceForcedBudget, OAI.TraceReconstruction.OccupiedParityTree.shapeRoleConstant, OAI.TraceReconstruction.hiddenBinomialCap, OAI.TraceReconstruction.binaryTreeBudget, OAI.TraceReconstruction.sourceScheduledTrials

theorem OAI.TraceReconstruction.hiddenBinomialCap_rpow line 1021
theorem OAI.TraceReconstruction.forcedDecay_binary line 1049
Source documentation
The exact exponent in the skeleton budget equals the manuscript's forcedDecay, not an arbitrary favorable surrogate.
```
theorem forcedDecay_binary (b : ℕ) (ε d : ℝ) (hb : 1 ≤ b) :
    forcedDecay b ε d=ε/2+
      binaryTreeExponent (fun j=>scaleKappa b (j+2) ε/2+ε) (b-1)+
      (2:ℝ)^b*scaleA b 0 ε*d := by
…
```
Mentions: OAI.TraceReconstruction.forcedDecay, OAI.TraceReconstruction.binaryTreeExponent, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.scaleA
def OAI.TraceReconstruction.sourceSkeletonPrefactor line 1064
theorem OAI.TraceReconstruction.sourceSkeletonPrefactor_nonneg line 1067
theorem OAI.TraceReconstruction.source_forced_core_bound line 1073

theorem OAI.TraceReconstruction.source_forced_degree_decay line 1128

Source documentation

The sharp forced degree has the full decay gain, after all actual source caps and the old-score factor have been multiplied.

theorem source_forced_degree_decay (T n : ℕ → ℕ) (s b r : ℕ) (ω N ε d K W w : ℝ)
    (hN : 0 < N) (hK : 0 ≤ K) (hW : 0 ≤ W) (hr : 2^(b+1) ≤ r)
    (hsmall : w^2*((2^s:ℕ):ℝ)*(sourceSparseCount T s b:ℝ) ≤ 1)
    (hw : w^2 ≤ W*N^(-scaleA (b+1) 0 ε*d))
    (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)) :
    w^(2*r)*sourceForcedBudget T n s b r ω ≤
      (OccupiedParityTree.shapeRoleConstant r (b+1):ℝ)*W^(2^(b+1))*
        sourceSkeletonPrefactor s b K*N^(-forcedDecay (b+1) ε d) := by
…

Mentions: OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.scaleA, OAI.TraceReconstruction.hiddenBinomialCap, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.scaleKappa, OAI.TraceReconstruction.sourceForcedBudget, OAI.TraceReconstruction.OccupiedParityTree.shapeRoleConstant, OAI.TraceReconstruction.sourceSkeletonPrefactor, OAI.TraceReconstruction.forcedDecay