Differences.lean`

151 declarations, 0 contain sorry, 0 declared as axioms

Differences

Tensor gap differences, positional shifts, two-gap elimination, central clipping, disjoint rank regions, and weighted period sums.

def OAI.TraceReconstruction.binomialLengthDifference line 23
Source documentation
Forward length differences of the actual binomial probability polynomial, before imposing the conditional rank total.
```
def binomialLengthDifference (g s : ℕ) (p : ℝ) : IntSeries :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.binomialLengthDifference_succ line 28
Source documentation
Increasing the number of trials corresponds exactly to multiplying by the Bernoulli step polynomial.
```
theorem binomialLengthDifference_succ (g s : ℕ) (p : ℝ) :
    binomialLengthDifference g (s+1) p =
      binomialLengthDifference (g+1) s p - binomialLengthDifference g s p := by
…
```
Mentions: OAI.TraceReconstruction.binomialLengthDifference
theorem OAI.TraceReconstruction.biasedSeries_step_sub_one line 35
theorem OAI.TraceReconstruction.binomialLengthDifference_eq line 48
theorem OAI.TraceReconstruction.seriesL2Sq_smul line 54

theorem OAI.TraceReconstruction.binomialLengthDifference_bounds line 62

Source documentation

Pointwise and square-sum bounds for every forward length difference. The quotient form keeps every order and every channel factor explicit.

theorem binomialLengthDifference_bounds (g s : ℕ) {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :
    (∀ z : ℤ, |(binomialLengthDifference g s p).coeff z| ≤
      (2*biasedBinomialBound (g/(s+1)) p)^s * biasedBinomialBound (g/(s+1)) p) ∧
    (seriesL2Sq (binomialLengthDifference g s p) ≤
      ((2*biasedBinomialBound (g/(s+1)) p)^s)^2 * biasedBinomialBound (g/(s+1)) p) := by
…

Mentions: OAI.TraceReconstruction.binomialLengthDifference, OAI.TraceReconstruction.biasedBinomialBound, OAI.TraceReconstruction.seriesL2Sq

def OAI.TraceReconstruction.lengthDifferenceConstant line 81
Source documentation
Explicit fixed-order smoothing constant; no asymptotic hypothesis is hidden.
```
def lengthDifferenceConstant (s : ℕ) (p : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.lengthDifferenceConstant_pos line 84
theorem OAI.TraceReconstruction.biasedBinomialBound_length_le line 89

theorem OAI.TraceReconstruction.binomialLengthDifference_numeric line 104

Source documentation

Squared supremum and squared L2 smoothing estimates in a form suitable for exact constrained rank profiles.

theorem binomialLengthDifference_numeric (g s : ℕ) {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :
    (∀ z : ℤ, (binomialLengthDifference g s p).coeff z ^ 2 ≤
      (lengthDifferenceConstant s p)^(2*s+2) / ((g:ℝ)+1)^(s+1)) ∧
    (seriesL2Sq (binomialLengthDifference g s p) ≤
      (lengthDifferenceConstant s p)^(2*s+1) /
        (((g:ℝ)+1)^s * Real.sqrt ((g:ℝ)+1))) := by
…

Mentions: OAI.TraceReconstruction.binomialLengthDifference, OAI.TraceReconstruction.lengthDifferenceConstant, OAI.TraceReconstruction.seriesL2Sq

theorem OAI.TraceReconstruction.series_finite_sum_sq_le line 142
def OAI.TraceReconstruction.signedRankProduct line 151
Source documentation
Product coefficients of signed gap series, including an arbitrary translation of each observed rank gap.
```
def signedRankProduct {l r : ℕ} (f : Fin (r+1) → IntSeries)
    (shift : Fin (r+1) → ℤ) (v : IncreasingTuple l r) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.IncreasingTuple
theorem OAI.TraceReconstruction.signedRankProduct_square_sum_le line 158
Source documentation
Largest-gap elimination also holds for signed finite-difference series. The fixed sum of the observed gaps supplies the missing square-root factor; translations are unrestricted and the estimate contains no omitted ranks.
```
theorem signedRankProduct_square_sum_le {l r : ℕ}
    (f : Fin (r+1) → IntSeries) (shift : Fin (r+1) → ℤ)
    (e : Fin (r+1)) (M : ℝ) (hM : 0 ≤ M)
    (hbound : ∀ z : ℤ, (f e).coeff z ^ 2 ≤ M) :
    (∑ v : IncreasingTuple l r, signedRankProduct f shift v ^ 2) ≤
      M * ∏ i : Fin r, seriesL2Sq (f (Equiv.swap 0 e i.succ)) := by
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.signedRankProduct, OAI.TraceReconstruction.seriesL2Sq
theorem OAI.TraceReconstruction.rank_mixture_square_sum_le line 198
Source documentation
Finite mixtures of signed rank products can be estimated termwise. This is the exact Cauchy--Schwarz form used when expanding positional finite-difference operators into gap derivatives.
```
theorem rank_mixture_square_sum_le {α V : Type*} [Fintype α] [Fintype V]
    (c : α → ℝ) (F : α → V → ℝ) (B : α → ℝ)
    (hB : ∀ a, (∑ v, F a v ^ 2) ≤ B a) :
    (∑ v, (∑ a, c a * F a v)^2) ≤ (∑ a, |c a|) * ∑ a, |c a| * B a := by
…
```
def OAI.TraceReconstruction.tensorSeries line 226
Source documentation
The tensor product of finitely supported one-dimensional coefficient series, represented on its literal vector-valued exponents.
```
def tensorSeries {ι : Type*} [Fintype ι] (f : ι → IntSeries) :
    AddMonoidAlgebra ℝ (ι → ℤ) :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.tensorSeries_coeff line 237
theorem OAI.TraceReconstruction.tensorSeries_support line 240
theorem OAI.TraceReconstruction.tensorSeries_mul line 248
Source documentation
Literal tensor multiplication is coordinatewise convolution.
```
theorem tensorSeries_mul {ι : Type*} [Fintype ι] (f g : ι → IntSeries) :
    tensorSeries (fun i => f i*g i) = tensorSeries f * tensorSeries g := by
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.tensorSeries
theorem OAI.TraceReconstruction.tensorSeries_one line 261
def OAI.TraceReconstruction.coordinateExponent line 277
Source documentation
Embedding one integral exponent into its own gap coordinate.
```
def coordinateExponent {ι : Type*} [DecidableEq ι] (i : ι) : ℤ →+ (ι → ℤ) where
…
```
def OAI.TraceReconstruction.coordinateSeriesHom line 286
theorem OAI.TraceReconstruction.coordinateExponent_injective line 290
theorem OAI.TraceReconstruction.tensorSeries_coordinate line 296
theorem OAI.TraceReconstruction.tensorSeries_prod line 329
theorem OAI.TraceReconstruction.tensorSeries_eq_prod line 341
Source documentation
The literal product of the coordinate embeddings has precisely the independent product coefficients, with no external tensor-product axioms.
```
theorem tensorSeries_eq_prod {ι : Type*} [Fintype ι] [DecidableEq ι]
    (f : ι → IntSeries) :
    tensorSeries f = ∏ i, coordinateSeriesHom i (f i) := by
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.tensorSeries, OAI.TraceReconstruction.coordinateSeriesHom

theorem OAI.TraceReconstruction.rank_gap_derivatives_bound line 358

Source documentation

Explicit fixed-order gap derivative bound, uniformly over translated rank restrictions and the choice of the eliminated gap.

theorem rank_gap_derivatives_bound {l r : ℕ}
    (g s : Fin (r+1) → ℕ) (shift : Fin (r+1) → ℤ)
    {p : ℝ} (hp : p ∈ Set.Ioo 0 1) (e : Fin (r+1)) :
    (∑ v : IncreasingTuple l r,
      signedRankProduct (fun i => binomialLengthDifference (g i) (s i) p) shift v ^ 2) ≤
    (lengthDifferenceConstant (s e) p)^(2*s e+2) / ((g e:ℝ)+1)^(s e+1) *
      ∏ i : Fin r,
        (lengthDifferenceConstant (s (Equiv.swap 0 e i.succ)) p)^(2*s (Equiv.swap 0 e i.succ)+1) /
        (((g (Equiv.swap 0 e i.succ):ℝ)+1)^(s (Equiv.swap 0 e i.succ)) *
          Real.sqrt ((g (Equiv.swap 0 e i.succ):ℝ)+1)) := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.signedRankProduct, OAI.TraceReconstruction.binomialLengthDifference, OAI.TraceReconstruction.lengthDifferenceConstant

theorem OAI.TraceReconstruction.lengthDifferenceConstant_mono line 377
Source documentation
Increasing an order increases only its explicit smoothing constant.
```
theorem lengthDifferenceConstant_mono {s t : ℕ} (hst : s ≤ t)
    {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :
    lengthDifferenceConstant s p ≤ lengthDifferenceConstant t p := by
…
```
Mentions: OAI.TraceReconstruction.lengthDifferenceConstant
inductive OAI.TraceReconstruction.GapDifference line 390
def OAI.TraceReconstruction.GapDifference.order line 394
def OAI.TraceReconstruction.adjacentGap line 397
def OAI.TraceReconstruction.gapTermWeight line 400
def OAI.TraceReconstruction.gapTermOrder line 406
def OAI.TraceReconstruction.gapTermExtra line 414
def OAI.TraceReconstruction.gapOperator line 423
Source documentation
Polynomial of a centered positional operator after removing from both incident gaps the one unit needed for either direction of movement.
```
def gapOperator {r : ℕ} (h : Fin r) (k : GapDifference) (p : ℝ) :
    AddMonoidAlgebra ℝ (Fin (r+1) → ℤ) :=
…
```
Mentions: OAI.TraceReconstruction.GapDifference
theorem OAI.TraceReconstruction.tensorSeries_two_coordinates line 432
theorem OAI.TraceReconstruction.gapLocalTerm_factor line 443
theorem OAI.TraceReconstruction.gapOperator_expansion line 460
Source documentation
Exact four-term assignment of positional differences to the adjacent binomial gap lengths, including all signs and all bounded shifts.
```
theorem gapOperator_expansion {r : ℕ} (h : Fin r) (k : GapDifference) (p : ℝ) :
    gapOperator h k p = ∑ a : Bool × Bool, gapTermWeight k a •
      tensorSeries (fun i => (biasedSeries 1 p-1)^gapTermOrder h k a i *
        (biasedSeries 1 p)^gapTermExtra h k a i) := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.gapOperator, OAI.TraceReconstruction.gapTermWeight, OAI.TraceReconstruction.tensorSeries, OAI.TraceReconstruction.biasedSeries, OAI.TraceReconstruction.gapTermOrder, OAI.TraceReconstruction.gapTermExtra
theorem OAI.TraceReconstruction.gapTermWeight_l1 line 472
theorem OAI.TraceReconstruction.gapTermOrder_total line 476
theorem OAI.TraceReconstruction.gapOperators_expansion line 481
Source documentation
Exact global expansion inside the unconstrained vector of gap counts.
```
theorem gapOperators_expansion {r : ℕ} (g : Fin (r+1) → ℕ)
    (k : Fin r → GapDifference) (p : ℝ) :
    tensorSeries (fun i => biasedSeries (g i) p) * (∏ h, gapOperator h (k h) p) =
      ∑ a : Fin r → Bool × Bool, (∏ h, gapTermWeight (k h) (a h)) •
        tensorSeries (fun i => binomialLengthDifference
          (g i + ∑ h, gapTermExtra h (k h) (a h) i)
          (∑ h, gapTermOrder h (k h) (a h) i) p) := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.tensorSeries, OAI.TraceReconstruction.biasedSeries, OAI.TraceReconstruction.gapOperator, OAI.TraceReconstruction.gapTermWeight, OAI.TraceReconstruction.binomialLengthDifference, OAI.TraceReconstruction.gapTermExtra, OAI.TraceReconstruction.gapTermOrder
theorem OAI.TraceReconstruction.gapOperators_weight_l1 line 502
theorem OAI.TraceReconstruction.prod_eliminate_fin line 520

theorem OAI.TraceReconstruction.lengthDifference_uniform line 530

Source documentation

Uniform smoothing with the individual gap scale retained, and a common lower gap scale reserved for every derivative order.

theorem lengthDifference_uniform (g b s : ℕ) {p C G : ℝ}
    (hp : p ∈ Set.Ioo 0 1) (hC : lengthDifferenceConstant s p ≤ C)
    (hG : 0 < G) (hb : b ≤ g) (hGg : G ≤ (g:ℝ)+1) :
    (∀ z : ℤ, (binomialLengthDifference g s p).coeff z^2 ≤
      (C/Real.sqrt ((b:ℝ)+1)) * (C^(2*s+1)/(G^s*Real.sqrt ((b:ℝ)+1)))) ∧
    seriesL2Sq (binomialLengthDifference g s p) ≤
      C^(2*s+1)/(G^s*Real.sqrt ((b:ℝ)+1)) := by
…

Mentions: OAI.TraceReconstruction.lengthDifferenceConstant, OAI.TraceReconstruction.binomialLengthDifference, OAI.TraceReconstruction.seriesL2Sq

theorem OAI.TraceReconstruction.rank_derivatives_uniform line 567

Source documentation

A single translated signed rank product, with every smoothing scale and the largest-gap constraint exposed.

theorem rank_derivatives_uniform {l r : ℕ}
    (g b s : Fin (r+1) → ℕ) (shift : Fin (r+1) → ℤ)
    {p C G : ℝ} (hp : p ∈ Set.Ioo 0 1)
    (hC : ∀ i, lengthDifferenceConstant (s i) p ≤ C) (hG : 0 < G)
    (hb : ∀ i, b i ≤ g i) (hGg : ∀ i, G ≤ (g i:ℝ)+1) (e : Fin (r+1)) :
    (∑ v : IncreasingTuple l r,
      signedRankProduct (fun i => binomialLengthDifference (g i) (s i) p) shift v ^ 2) ≤
      C^(2*(∑ i, s i)+r+2) /
        (G^(∑ i, s i) * Real.sqrt ((b e:ℝ)+1) * ∏ i, Real.sqrt ((b i:ℝ)+1)) := by
…

Mentions: OAI.TraceReconstruction.lengthDifferenceConstant, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.signedRankProduct, OAI.TraceReconstruction.binomialLengthDifference

def OAI.TraceReconstruction.SafeTaggedTuple line 608
Source documentation
Enough vacant slots for independent one-step displacements of every tag.
```
def SafeTaggedTuple {n r : ℕ} (p : Fin r → Fin n) : Prop :=
…
```
def OAI.TraceReconstruction.shiftedTag line 612
theorem OAI.TraceReconstruction.shiftedTag_strictMono line 619
def OAI.TraceReconstruction.gapIncidence line 629
def OAI.TraceReconstruction.shiftGapExtra line 632
def OAI.TraceReconstruction.localShiftExtra line 637
Source documentation
Literal adjacent-gap allocation of the units used by a displacement. Value zero means translate left, one leave fixed, two translate right.
```
def localShiftExtra {r : ℕ} (h : Fin r) (a : Fin 3) (i : Fin (r+1)) : ℕ :=
…
```
theorem OAI.TraceReconstruction.sum_castSucc_indicator line 640
theorem OAI.TraceReconstruction.sum_succ_indicator line 646
theorem OAI.TraceReconstruction.shiftGapExtra_eq_sum line 652
theorem OAI.TraceReconstruction.gapIncidence_le line 658
theorem OAI.TraceReconstruction.tupleGap_shifted line 685
Source documentation
The exact geometric identity relating translated tag positions to nonnegative binomial-gap lengths.
```
theorem tupleGap_shifted {n r : ℕ} (p : Fin r → Fin n) (hp : SafeTaggedTuple p)
    (a : Fin r → Fin 3) (i : Fin (r+1)) :
    tupleGap (shiftedTag p hp a) i =
      tupleGap p i - gapIncidence r i + shiftGapExtra a i := by
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.shiftedTag, OAI.TraceReconstruction.gapIncidence, OAI.TraceReconstruction.shiftGapExtra
def OAI.TraceReconstruction.positionalWeight line 724
Source documentation
Coefficients of the unchanged, centered first, and centered second one-step positional operators.
```
def positionalWeight (k : GapDifference) (a : Fin 3) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.GapDifference
theorem OAI.TraceReconstruction.localShift_factor line 730
theorem OAI.TraceReconstruction.gapOperator_positional_expansion line 744
theorem OAI.TraceReconstruction.shifted_gap_series_expansion line 756
Source documentation
Literal centered differences of all rank kernels are coefficients of the adjacent-gap operator product, with no formal negative trial lengths.
```
theorem shifted_gap_series_expansion {n r : ℕ} (p : Fin r → Fin n)
    (hp : SafeTaggedTuple p) (k : Fin r → GapDifference) (θ : ℝ) :
    (∑ a : Fin r → Fin 3, (∏ h, positionalWeight (k h) (a h)) •
      tensorSeries (fun i => biasedSeries (tupleGap (shiftedTag p hp a) i) θ)) =
    tensorSeries (fun i => biasedSeries (tupleGap p i-gapIncidence r i) θ) *
      ∏ h, gapOperator h (k h) θ := by
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.positionalWeight, OAI.TraceReconstruction.tensorSeries, OAI.TraceReconstruction.biasedSeries, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.shiftedTag, OAI.TraceReconstruction.gapIncidence, OAI.TraceReconstruction.gapOperator
def OAI.TraceReconstruction.positionalRankDifference line 778
Source documentation
Simultaneous literal positional operators applied to the actual conditional retained-subset kernel.
```
def positionalRankDifference {n l r : ℕ} (hl : l ≤ n) (p : Fin r → Fin n)
    (hp : SafeTaggedTuple p) (k : Fin r → GapDifference) (v : IncreasingTuple l r) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.IncreasingTuple
theorem OAI.TraceReconstruction.positionalRankDifference_expansion line 783
theorem OAI.TraceReconstruction.gap_global_order line 813
Source documentation
The total derivative order is the source value |D|+2|V|.
```
theorem gap_global_order {r : ℕ} (k : Fin r → GapDifference) (a : Fin r → Bool × Bool) :
    (∑ i : Fin (r+1), ∑ h, gapTermOrder h (k h) (a h) i) = ∑ h, (k h).order := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.gapTermOrder
theorem OAI.TraceReconstruction.gapTermOrder_sum_le_global line 825
theorem OAI.TraceReconstruction.positionalRankDifference_square_sum_le line 836
Source documentation
Literal mixed centered positional differences of a conditional rank kernel, with a single explicit constant depending only on the total order and the Bernoulli parameter. Every gap scale remains available for summing over the period tuples in the signed initial construction.
```
theorem positionalRankDifference_square_sum_le {n l r : ℕ} (hl : l ≤ n)
    (p : Fin r → Fin n) (hp : SafeTaggedTuple p) (k : Fin r → GapDifference)
    {θ G : ℝ} (hθ : θ ∈ Set.Ioo 0 1) (hG : 0 < G)
    (hgap : ∀ i, G ≤ (tupleGap p i-gapIncidence r i : ℕ)+1)
    (e : Fin (r+1)) :
    (∑ v : IncreasingTuple l r, positionalRankDifference hl p hp k v ^ 2) ≤
      (θ^r / binomialMass n θ l)^2 * (2:ℝ)^(2*r) *
        (lengthDifferenceConstant (∑ h, (k h).order) θ)^(2*(∑ h, (k h).order)+r+2) /
      (G^(∑ h, (k h).order) * Real.sqrt ((tupleGap p e-gapIncidence r e:ℕ)+1) *
        ∏ i, Real.sqrt ((tupleGap p i-gapIncidence r i:ℕ)+1)) := by
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapIncidence, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.positionalRankDifference, OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.lengthDifferenceConstant
theorem OAI.TraceReconstruction.gapIncidence_le_two line 892
theorem OAI.TraceReconstruction.constant_period_safe line 901
Source documentation
Constant middle-period tags admit every independent left/unchanged/right choice without violating slot order or either end boundary.
```
theorem constant_period_safe {u m r : ℕ} (off : Fin m)
    (hoff₁ : 1 ≤ off.val) (hoff₂ : off.val+1 < m) (hm : 3 ≤ m)
    (j : Fin r → Fin u) (hj : StrictMono j) :
    SafeTaggedTuple (periodSlot (fun _ => off) ∘ j) := by
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.period_derivative_base_lower line 922

Source documentation

Removing both incident displacement units still leaves a fixed fraction of each actual coarse gap. Doubled coarse gaps are used to keep all combinatorial labels integer-valued.

theorem period_derivative_base_lower {u m r : ℕ} (hm : 32 ≤ m) (hr : 0 < r)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (j : Fin r → Fin u) (hj : StrictMono j)
    (hsafe : SafeTaggedTuple (periodSlot off ∘ j)) (i : Fin (r+1)) :
    (m:ℝ)*coarsePeriodGap j i/4 ≤
      ((tupleGap (periodSlot off ∘ j) i-gapIncidence r i:ℕ):ℝ)+1 := by
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.coarsePeriodGap, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapIncidence

theorem OAI.TraceReconstruction.period_derivative_common_lower line 938

theorem OAI.TraceReconstruction.period_derivative_largest_lower line 951

Source documentation

A largest coarse gap supplies the additional square-root improvement coming from the fixed sum of the observed ranks.

theorem period_derivative_largest_lower {u m r : ℕ} (hm : 32 ≤ m) (hr : 0 < r)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (j : Fin r → Fin u) (hj : StrictMono j)
    (hsafe : SafeTaggedTuple (periodSlot off ∘ j)) (e : Fin (r+1))
    (he : 2*u ≤ (r+1)*coarsePeriodGap j e) :
    (u:ℝ)*m/(2*(r+1:ℝ)) ≤
      ((tupleGap (periodSlot off ∘ j) e-gapIncidence r e:ℕ):ℝ)+1 := by
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.coarsePeriodGap, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapIncidence

theorem OAI.TraceReconstruction.binomial_rank_normalization line 972

theorem OAI.TraceReconstruction.positionalRankDifference_scale_bound line 988

Source documentation

The exact mean-count version, with arbitrary proven positive lower scales for all gaps; no asymptotic or analytic estimate is assumed.

theorem positionalRankDifference_scale_bound {n l r : ℕ} (hl : l ≤ n)
    (p : Fin r → Fin n) (hp : SafeTaggedTuple p) (k : Fin r → GapDifference)
    {θ G H : ℝ} (hθ : θ ∈ Set.Ioo 0 1) (hG : 0 < G) (hH : 0 < H)
    (hmean : (n:ℝ)*θ=l) (hv : 1 ≤ (n:ℝ)*θ*(1-θ))
    (B : Fin (r+1) → ℝ) (hB : ∀ i, 0 < B i)
    (hgap : ∀ i, G ≤ (tupleGap p i-gapIncidence r i:ℕ)+1)
    (hscale : ∀ i, B i ≤ (tupleGap p i-gapIncidence r i:ℕ)+1)
    (e : Fin (r+1)) (hlarge : H ≤ Real.sqrt ((tupleGap p e-gapIncidence r e:ℕ)+1)) :
    (∑ v : IncreasingTuple l r, positionalRankDifference hl p hp k v ^ 2) ≤
      144*(n:ℝ)*(2:ℝ)^(2*r)*
        (lengthDifferenceConstant (∑ h, (k h).order) θ)^(2*(∑ h, (k h).order)+r+2) /
      (G^(∑ h, (k h).order)*H*∏ i, Real.sqrt (B i)) := by
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.gapIncidence, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.positionalRankDifference, OAI.TraceReconstruction.lengthDifferenceConstant

def OAI.TraceReconstruction.periodDifferencePrefactor line 1018
Source documentation
Explicit source rank-difference prefactor. It depends on the period count, slot length, derivative order and Bernoulli parameter, not the selected period tuple.
```
def periodDifferencePrefactor (u m r d : ℕ) (θ : ℝ) : ℝ :=
…
```

theorem OAI.TraceReconstruction.period_positionalRankDifference_bound line 1026

Source documentation

The finite-difference estimate for actual translated tagged slots in periodic words. The tuple dependence is exactly the product of inverse square roots of its doubled coarse gaps.

theorem period_positionalRankDifference_bound {u m l r : ℕ}
    (hm : 32 ≤ m) (hr : 0 < r) (hl : l ≤ u*m)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (j : IncreasingTuple u r) (hsafe : SafeTaggedTuple (periodSlot off ∘ j.val))
    (k : Fin r → GapDifference) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1)
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ)) :
    (∑ v : IncreasingTuple l r,
      positionalRankDifference hl (periodSlot off ∘ j.val) hsafe k v ^ 2) ≤
      periodDifferencePrefactor u m r (∑ h, (k h).order) θ *
        ∏ i, (Real.sqrt (coarsePeriodGap j.val i))⁻¹ := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.positionalRankDifference, OAI.TraceReconstruction.periodDifferencePrefactor, OAI.TraceReconstruction.coarsePeriodGap

theorem OAI.TraceReconstruction.two_sums_determine line 1071

Source documentation

Two independent exact sum constraints determine a missing coordinate on each side of a fixed cut. This is the second-gap elimination needed when a period label has been fixed.

theorem two_sums_determine {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Finset ι) {e d : ι} (he : e∈A) (hd : d∉A)
    (x y : ι → ℕ) (hA : ∑ i∈A, x i = ∑ i∈A, y i)
    (ht : ∑ i, x i = ∑ i, y i)
    (hxy : ∀ i, i≠e → i≠d → x i=y i) : x=y := by
…

abbrev OAI.TraceReconstruction.RemainingCoordinates line 1104

theorem OAI.TraceReconstruction.two_sums_restrict_injective line 1108

Source documentation

Restricting an injective gap profile to all but the two eliminated coordinates is still injective on two fixed-sum fibers.

theorem two_sums_restrict_injective {α ι : Type*} [Fintype ι] [DecidableEq ι]
    {U L V : ℕ} (A : Finset ι) {e d : ι} (he : e∈A) (hd : d∉A)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V) :
    Function.Injective (fun a => fun i : RemainingCoordinates e d => p a i.val) := by
…

Mentions: OAI.TraceReconstruction.RemainingCoordinates

theorem OAI.TraceReconstruction.two_sums_product_bound line 1126

Source documentation

Once the two coordinates are eliminated all remaining gap weights sum independently; any additional constraints may be dropped.

theorem two_sums_product_bound {α ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι]
    {U L V : ℕ} (A : Finset ι) {e d : ι} (he : e∈A) (hd : d∉A)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V)
    (w : ι → Fin (U+1) → ℝ) (hw : ∀ i k, 0≤w i k) :
    (∑ a, ∏ i : RemainingCoordinates e d, w i.val (p a i.val)) ≤
      ∏ i : RemainingCoordinates e d, ∑ k, w i.val k := by
…

Mentions: OAI.TraceReconstruction.RemainingCoordinates

theorem OAI.TraceReconstruction.coarsePeriodGap_prefix line 1145
Source documentation
The sum of doubled coarse gaps to a specified period label is exact, including the half endpoint cells in the source convention.
```
theorem coarsePeriodGap_prefix {u r : ℕ} (j : Fin r → Fin u) (hj : StrictMono j)
    (i : Fin r) : (∑ g∈Finset.Iic i.castSucc, coarsePeriodGap j g) = 2*(j i).val+1 := by
…
```
Mentions: OAI.TraceReconstruction.coarsePeriodGap
theorem OAI.TraceReconstruction.fin_sum_inverse_sqrt line 1180
Source documentation
The full inverse-square-root sum, including the zero cell (whose value is zero), has the same elementary integral bound.
```
theorem fin_sum_inverse_sqrt (U : ℕ) :
    (∑ k : Fin (U+1), (Real.sqrt (k.val:ℝ))⁻¹) ≤ 2*Real.sqrt U := by
…
```
theorem OAI.TraceReconstruction.prod_two_coordinates line 1188
theorem OAI.TraceReconstruction.inverse_sqrt_pair line 1200

theorem OAI.TraceReconstruction.two_large_gaps_inverse_sum line 1211

Source documentation

Explicit two-gap summation on a fixed-sum fiber. Both large gaps contribute R^(-1), rather than losing a free label factor.

theorem two_large_gaps_inverse_sum {α ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι]
    {U L V : ℕ} (A : Finset ι) {e d : ι} (he : e∈A) (hd : d∉A)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V)
    {R : ℝ} (hR : 0<R) (heR : ∀ a, R≤(p a e).val) (hdR : ∀ a, R≤(p a d).val) :
    (∑ a, ∏ i, (Real.sqrt ((p a i).val:ℝ))⁻¹) ≤
      R⁻¹*(2*Real.sqrt U)^Fintype.card (RemainingCoordinates e d) := by
…

Mentions: OAI.TraceReconstruction.RemainingCoordinates

def OAI.TraceReconstruction.FixedPeriodTuple line 1240
Source documentation
The fixed involved label is a genuine geometric fiber, not an extra analytic hypothesis on the rank kernel.
```
def FixedPeriodTuple (u r : ℕ) (a : Fin r) (h : Fin u) :=
…
```
instance OAI.TraceReconstruction.fixedPeriodTupleFintype line 1243
def OAI.TraceReconstruction.fixedPeriodProfile line 1248
theorem OAI.TraceReconstruction.fixedPeriodProfile_injective line 1253
theorem OAI.TraceReconstruction.fixedPeriodProfile_prefix line 1262
theorem OAI.TraceReconstruction.fixedPeriodProfile_total line 1268
theorem OAI.TraceReconstruction.binomialMass_centered_mgf line 1279
Source documentation
An elementary centered MGF bound valid on both sides of the mean, with constants independent of the Bernoulli parameter.
```
theorem binomialMass_centered_mgf (n : ℕ) {p t : ℝ}
    (hp : p∈Set.Icc 0 1) (ht : |t|≤1) :
    (∑ k∈Finset.range (n+1), binomialMass n p k*Real.exp (t*((k:ℝ)-n*p))) ≤
      Real.exp ((n:ℝ)*t^2) := by
…
```
Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.binomialMass_signed_tail line 1305

Source documentation

Either signed deviation has the same Chernoff estimate.

theorem binomialMass_signed_tail (n : ℕ) {p t a ε : ℝ}
    (hp : p∈Set.Icc 0 1) (ht : t∈Set.Icc 0 1) (hε : ε=1 ∨ ε= -1) :
    (∑ k∈(Finset.range (n+1)).filter (fun k : ℕ => a≤ε*((k:ℝ)-n*p)), binomialMass n p k) ≤
      Real.exp (-t*a+(n:ℝ)*t^2) := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.binomialMass_abs_tail line 1322
Source documentation
A uniform two-sided tail at any finite cutoff. Unlike a quoted concentration theorem, this follows here from the finite binomial MGF.
```
theorem binomialMass_abs_tail (n : ℕ) {p t a : ℝ}
    (hp : p∈Set.Icc 0 1) (ht : t∈Set.Icc 0 1) :
    (∑ k∈(Finset.range (n+1)).filter (fun k : ℕ => a≤|(k:ℝ)-n*p|), binomialMass n p k) ≤
      2*Real.exp (-t*a+(n:ℝ)*t^2) := by
…
```
Mentions: OAI.TraceReconstruction.binomialMass
theorem OAI.TraceReconstruction.remainingCoordinates_card line 1352
Source documentation
Cardinality bookkeeping for the two eliminated gap coordinates.
```
theorem remainingCoordinates_card {ι : Type*} [Fintype ι] [DecidableEq ι]
    {e d : ι} (hed : e≠d) :
    Fintype.card (RemainingCoordinates e d)=Fintype.card ι-2 := by
…
```
Mentions: OAI.TraceReconstruction.RemainingCoordinates

theorem OAI.TraceReconstruction.exists_large_in_subset line 1367

Source documentation

A finite sum's largest entry on a nonempty set controls its average, with the full number of coordinates in place of the subset cardinality.

theorem exists_large_in_subset {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Finset ι) (hA : A.Nonempty) (x : ι → ℝ) (hx : ∀ i, 0≤x i)
    {R : ℝ} (hR : R*Fintype.card ι ≤ ∑ i∈A, x i) :
    ∃ e∈A, R≤x e := by
…

theorem OAI.TraceReconstruction.two_sided_large_gaps_sum line 1385

Source documentation

Covering the fixed-sum profile by its selected largest coordinates costs only the square of its (fixed) dimension.

theorem two_sided_large_gaps_sum {α ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι]
    {U L V : ℕ} (A : Finset ι)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V)
    {R : ℝ} (hR : 0<R)
    (hleft : ∀ a, ∃ e∈A, R≤(p a e).val)
    (hright : ∀ a, ∃ d∉A, R≤(p a d).val) :
    (∑ a, ∏ i, (Real.sqrt ((p a i).val:ℝ))⁻¹) ≤
      (Fintype.card ι:ℝ)^2*R⁻¹*(2*Real.sqrt U)^(Fintype.card ι-2) := by
…

theorem OAI.TraceReconstruction.fixedPeriodProfile_central_sum line 1425

Source documentation

The fixed central label leaves a macroscopic sum on both sides.

theorem fixedPeriodProfile_central_sum {u r : ℕ} (a : Fin r) (h : Fin u)
    (hleft : (u:ℝ)/3≤2*h.val+1)
    (hright : (u:ℝ)/3≤2*u-(2*h.val+1)) :
    (∑ j : FixedPeriodTuple u r a h,
      ∏ i, (Real.sqrt (coarsePeriodGap j.val.val i))⁻¹) ≤
      ((r+1:ℕ):ℝ)^2 * ((u:ℝ)/(3*(r+1:ℝ)))⁻¹ *
        (2*Real.sqrt (2*u:ℕ))^(r-1) := by
…

Mentions: OAI.TraceReconstruction.FixedPeriodTuple, OAI.TraceReconstruction.coarsePeriodGap

theorem OAI.TraceReconstruction.binomialMass_cutoff_filter_le line 1474

Source documentation

Any finite cutoff only removes nonnegative mass from the full binomial support, even if the cutoff extends beyond that support.

theorem binomialMass_cutoff_filter_le (n U : ℕ) {p : ℝ} (hp : p∈Set.Icc 0 1)
    (P : ℕ → Prop) [DecidablePred P] :
    (∑ k : Fin (U+1), if P k.val then binomialMass n p k.val else 0) ≤
      ∑ k∈(Finset.range (n+1)).filter P, binomialMass n p k := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.profile_coordinate_event_le line 1494

Source documentation

A single-coordinate event for any injective family of profiles is bounded by the corresponding full product marginal.

theorem profile_coordinate_event_le {α ι κ : Type*} [Fintype α] [Fintype ι] [Fintype κ]
    [DecidableEq ι] (p : α → ι → κ) (hp : Function.Injective p)
    (w : ι → κ → ℝ) (hw : ∀ i k, 0≤w i k)
    (hs : ∀ i, ∑ k, w i k≤1) (e : ι) (P : κ → Prop) [DecidablePred P]
    {T : ℝ} (_hT : 0≤T) (ht : (∑ k, if P k then w e k else 0)≤T) :
    (∑ a, if P (p a e) then ∏ i, w i (p a i) else 0) ≤ T := by
…

theorem OAI.TraceReconstruction.subsetRankKernel_gap_tail line 1536

Source documentation

Exponentially small clipping loss for a single gap of the actual conditional retained-subset rank kernel.

theorem subsetRankKernel_gap_tail {n l r : ℕ} (hl : l≤n)
    (p : Fin r → Fin n) (hp : StrictMono p) (e : Fin (r+1))
    {θ t a : ℝ} (hθ : θ∈Set.Ioo 0 1) (ht : t∈Set.Icc 0 1) :
    (∑ v : IncreasingTuple l r,
      if a≤|(tupleGap v.val e:ℝ)-(tupleGap p e:ℝ)*θ|
      then subsetRankKernel hl p v.val else 0) ≤
      θ^r / binomialMass n θ l *
        (2*Real.exp (-t*a+(tupleGap p e:ℝ)*t^2)) := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.subsetRankKernel_outside_region line 1577

Source documentation

A coordinatewise rank region has a union-bound clipping estimate.

theorem subsetRankKernel_outside_region {n l r : ℕ} (hl : l≤n)
    (p : Fin r → Fin n) (hp : StrictMono p)
    {θ t a : ℝ} (hθ : θ∈Set.Ioo 0 1) (ht : t∈Set.Icc 0 1) :
    (∑ v : IncreasingTuple l r,
      if ∃ i, a≤|(tupleGap v.val i:ℝ)-(tupleGap p i:ℝ)*θ|
      then subsetRankKernel hl p v.val else 0) ≤
      ((r+1:ℕ):ℝ)*θ^r / binomialMass n θ l *
        (2*Real.exp (-t*a+(n:ℝ)*t^2)) := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.inverse_sqrt_nat_le_one line 1631
Source documentation
An inverse square root at an integer, extended by zero at zero, never exceeds one.
```
theorem inverse_sqrt_nat_le_one (k : ℕ) : (Real.sqrt (k:ℝ))⁻¹≤1 := by
…
```
theorem OAI.TraceReconstruction.fin_bounded_inverse_sqrt line 1640
Source documentation
A bounded gap costs a constant depending only on that bound, rather than an additional square root of the ambient period count.
```
theorem fin_bounded_inverse_sqrt (U M : ℕ) :
    (∑ k : Fin (U+1), if k.val≤M then (Real.sqrt (k.val:ℝ))⁻¹ else 0) ≤ M+1 := by
…
```
theorem OAI.TraceReconstruction.prod_one_special line 1661

theorem OAI.TraceReconstruction.two_large_bounded_gap_sum line 1675

Source documentation

Refined two-gap elimination when a third gap has bounded size.

theorem two_large_bounded_gap_sum {α ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι]
    {U L V M : ℕ} (A : Finset ι) {e d c : ι} (he : e∈A) (hd : d∉A)
    (hce : c≠e) (hcd : c≠d)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V)
    {R : ℝ} (hR : 0<R) (heR : ∀ a, R≤(p a e).val) (hdR : ∀ a, R≤(p a d).val)
    (hcM : ∀ a, (p a c).val≤M) :
    (∑ a, ∏ i, (Real.sqrt ((p a i).val:ℝ))⁻¹) ≤
      R⁻¹*(M+1)*(2*Real.sqrt U)^(Fintype.card ι-3) := by
…

theorem OAI.TraceReconstruction.two_sided_bounded_gaps_sum line 1722

Source documentation

A small internal gap cannot be either selected macroscopic gap. The bound retains the extra factor u^(-1/2) needed for nonlinear terms.

theorem two_sided_bounded_gaps_sum {α ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι]
    {U L V M : ℕ} (A : Finset ι) (c : ι)
    (p : α → ι → Fin (U+1)) (hp : Function.Injective p)
    (hA : ∀ a, ∑ i∈A, (p a i).val=L) (ht : ∀ a, ∑ i, (p a i).val=V)
    {R : ℝ} (hR : 0<R) (hMR : (M:ℝ)<R)
    (hleft : ∀ a, ∃ e∈A, R≤(p a e).val)
    (hright : ∀ a, ∃ d∉A, R≤(p a d).val)
    (hcM : ∀ a, (p a c).val≤M) :
    (∑ a, ∏ i, (Real.sqrt ((p a i).val:ℝ))⁻¹) ≤
      (Fintype.card ι:ℝ)^2*R⁻¹*(M+1)*(2*Real.sqrt U)^(Fintype.card ι-3) := by
…

def OAI.TraceReconstruction.PeriodRankRegion line 1775
Source documentation
The literal rank-clipping rectangles used in the manuscript, with doubled coarse gaps to avoid half-integer natural indices. Only the first and internal gaps are needed to determine the period tuple.
```
def PeriodRankRegion {u l r : ℕ} (m : ℕ) (θ : ℝ)
    (j : IncreasingTuple u r) (v : IncreasingTuple l r) : Prop :=
…
```
Mentions: OAI.TraceReconstruction.IncreasingTuple

theorem OAI.TraceReconstruction.nearby_gap_centers_equal line 1781

Source documentation

Enough accuracy to distinguish two integer gap lengths.

theorem nearby_gap_centers_equal {x y : ℕ} {z θ m : ℝ}
    (hθ : 1 / 2 ≤ θ) (hm : 0 < m)
    (hx : |z - θ * m * x / 2| < m / 8) (hy : |z - θ * m * y / 2| < m / 8) : x = y := by
…

theorem OAI.TraceReconstruction.periodRankRegion_unique line 1798
Source documentation
Regions for distinct tagged period tuples are genuinely disjoint, before any coefficient or orientation averaging.
```
theorem periodRankRegion_unique {u l r m : ℕ} (hm : 0 < m) {θ : ℝ} (hθ : 1 / 2 ≤ θ)
    {j k : IncreasingTuple u r} {v : IncreasingTuple l r}
    (hj : PeriodRankRegion m θ j v) (hk : PeriodRankRegion m θ k v) : j=k := by
…
```
Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.PeriodRankRegion

theorem OAI.TraceReconstruction.disjoint_support_sum_sq line 1817

Source documentation

Orthogonality of a finite family with pointwise disjoint supports.

theorem disjoint_support_sum_sq {α β : Type*} [Fintype α] [Fintype β]
    (f : α → β → ℝ) (hf : ∀ a b, a≠b → ∀ v, f a v*f b v=0) :
    (∑ v, (∑ a, f a v)^2) = ∑ a, ∑ v, f a v^2 := by
…

theorem OAI.TraceReconstruction.period_clipped_square_sum line 1837

Source documentation

Squared norm of the clipped sum is at most the sum of the original squared norms, with arbitrary signed multipliers on each tuple.

theorem period_clipped_square_sum {u l r m : ℕ} (hm : 0 < m) {θ : ℝ} (hθ : 1 / 2 ≤ θ)
    (W : IncreasingTuple u r → IncreasingTuple l r → ℝ)
    (a : IncreasingTuple u r → ℝ) :
    (∑ v, (∑ j, if PeriodRankRegion m θ j v then a j*W j v else 0)^2) ≤
      ∑ j, a j^2*∑ v, W j v^2 := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.PeriodRankRegion

instance OAI.TraceReconstruction.(instance at line 1866) line 1866
theorem OAI.TraceReconstruction.sum_gapDifference line 1869
def OAI.TraceReconstruction.motifShift line 1875
Source documentation
The sign-dependent displacement in {-1,0,1}, represented by Fin 3.
```
def motifShift (χ β τ : ℝ) : Fin 3 :=
…
```

def OAI.TraceReconstruction.motifDifferenceWeight line 1879

Source documentation

Coefficients of 1 + χ V + τ β D.

def motifDifferenceWeight (χ β τ : ℝ) : GapDifference → ℝ
  | .unchanged => 1 | .first => τ*β | .second => χ

/-- The centered operator expansion is an exact displacement, not an
 approximation of the trace kernel. -/

Mentions: OAI.TraceReconstruction.GapDifference

theorem OAI.TraceReconstruction.motif_positional_identity line 1884
Source documentation
The centered operator expansion is an exact displacement, not an approximation of the trace kernel.
```
theorem motif_positional_identity {χ β τ : ℝ} (hβ : IsMotifValue χ β)
    (hτ : IsTypeSign τ) (a : Fin 3) :
    (∑ k, motifDifferenceWeight χ β τ k * positionalWeight k a)=
      if a=motifShift χ β τ then 1 else 0 := by
…
```
Mentions: OAI.TraceReconstruction.IsMotifValue, OAI.TraceReconstruction.IsTypeSign, OAI.TraceReconstruction.motifDifferenceWeight, OAI.TraceReconstruction.positionalWeight, OAI.TraceReconstruction.motifShift
theorem OAI.TraceReconstruction.product_function_delta line 1893
theorem OAI.TraceReconstruction.motif_shift_expansion line 1905
Source documentation
Tensorization of the exact local shift identity, with an arbitrary array W (in particular any literal retained-subset rank kernel).
```
theorem motif_shift_expansion {r : ℕ} (χ β : Fin r → ℝ) (τ : ℝ)
    (hβ : ∀ h, IsMotifValue (χ h) (β h)) (hτ : IsTypeSign τ)
    (W : (Fin r → Fin 3) → ℝ) :
    W (fun h => motifShift (χ h) (β h) τ)=
      ∑ k : Fin r → GapDifference,
        (∏ h, motifDifferenceWeight (χ h) (β h) τ (k h))*
        (∑ a : Fin r → Fin 3, (∏ h, positionalWeight (k h) (a h))*W a) := by
…
```
Mentions: OAI.TraceReconstruction.IsMotifValue, OAI.TraceReconstruction.IsTypeSign, OAI.TraceReconstruction.motifShift, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.motifDifferenceWeight, OAI.TraceReconstruction.positionalWeight
def OAI.TraceReconstruction.firstDifferenceCount line 1933
def OAI.TraceReconstruction.secondDifferenceCount line 1936
theorem OAI.TraceReconstruction.motifDifferenceWeight_product line 1940
Source documentation
Every factor of the hypothesis sign comes precisely from a D operator.
```
theorem motifDifferenceWeight_product {r : ℕ} (χ β : Fin r → ℝ) (τ : ℝ)
    (k : Fin r → GapDifference) :
    (∏ h, motifDifferenceWeight (χ h) (β h) τ (k h))=
      τ^firstDifferenceCount k *∏ h, motifDifferenceWeight (χ h) (β h) 1 (k h) := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.motifDifferenceWeight, OAI.TraceReconstruction.firstDifferenceCount

theorem OAI.TraceReconstruction.motif_signed_shift_expansion line 1956

Source documentation

The signed difference retains exactly the patterns having an odd number of centered first differences, with the source's factor two.

theorem motif_signed_shift_expansion {r : ℕ} (χ β : Fin r → ℝ)
    (hβ : ∀ h, IsMotifValue (χ h) (β h)) (W : (Fin r → Fin 3) → ℝ) :
    W (fun h => motifShift (χ h) (β h) 1)-
      W (fun h => motifShift (χ h) (β h) (-1))=
      ∑ k : Fin r → GapDifference,
        (if Odd (firstDifferenceCount k) then
          2*∏ h, motifDifferenceWeight (χ h) (β h) 1 (k h) else 0)*
        (∑ a : Fin r → Fin 3, (∏ h, positionalWeight (k h) (a h))*W a) := by
…

Mentions: OAI.TraceReconstruction.IsMotifValue, OAI.TraceReconstruction.motifShift, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.firstDifferenceCount, OAI.TraceReconstruction.motifDifferenceWeight, OAI.TraceReconstruction.positionalWeight

theorem OAI.TraceReconstruction.difference_order_eq_counts line 1973
theorem OAI.TraceReconstruction.odd_pattern_linear_or_order_three line 1983
Source documentation
The only signed pattern of order below three is the singleton D term.
```
theorem odd_pattern_linear_or_order_three {r : ℕ} (k : Fin r → GapDifference)
    (hk : Odd (firstDifferenceCount k)) :
    (firstDifferenceCount k=1 ∧ secondDifferenceCount k=0) ∨
      3≤∑ h, (k h).order := by
…
```
Mentions: OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.firstDifferenceCount, OAI.TraceReconstruction.secondDifferenceCount
theorem OAI.TraceReconstruction.shiftGapExtra_le line 1998
theorem OAI.TraceReconstruction.tupleGap_shifted_close line 2014
Source documentation
A unit positional shift changes each actual rank gap by at most two.
```
theorem tupleGap_shifted_close {n r : ℕ} (p : Fin r → Fin n)
    (hp : SafeTaggedTuple p) (a : Fin r → Fin 3) (i : Fin (r+1)) :
    |(tupleGap (shiftedTag p hp a) i:ℝ)-(tupleGap p i:ℝ)| ≤ 2 := by
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.tupleGap, OAI.TraceReconstruction.shiftedTag
theorem OAI.TraceReconstruction.period_shifted_gap_rounding line 2024
theorem OAI.TraceReconstruction.coarse_outside_implies_gap_tail line 2038

theorem OAI.TraceReconstruction.period_shifted_outside_region line 2050

Source documentation

The manuscript's rank rectangles lose exponentially little mass for every bounded shift of a tagged tuple.

theorem period_shifted_outside_region {u m l r : ℕ}
    (hu : 0 < u) (hm : 128 ≤ m) (hr : 0 < r) (hl : l ≤ u*m)
    (off : Fin u → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (j : IncreasingTuple u r) (hsafe : SafeTaggedTuple (periodSlot off ∘ j.val))
    (a : Fin r → Fin 3) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1) :
    (∑ v : IncreasingTuple l r,
      if PeriodRankRegion m θ j v then 0 else
        subsetRankKernel hl (shiftedTag (periodSlot off ∘ j.val) hsafe a) v.val)  ≤ 
      ((r+1:ℕ):ℝ)*θ^r /binomialMass (u*m) θ l *
        (2*Real.exp (-(m:ℝ)/(1024*u))) := by
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.PeriodRankRegion, OAI.TraceReconstruction.subsetRankKernel, OAI.TraceReconstruction.shiftedTag, OAI.TraceReconstruction.binomialMass

def OAI.TraceReconstruction.motifIndicator line 2104
Source documentation
The literal support indicator of the length-2^s signed block.
```
def motifIndicator (s : ℕ) (z : ℤ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.prouhet_motif_value line 2107
theorem OAI.TraceReconstruction.motif_weight_abs_le line 2119
theorem OAI.TraceReconstruction.motif_weight_abs_le_indicator line 2124
def OAI.TraceReconstruction.motifPatternMultiplier line 2132
Source documentation
A kernel-pattern multiplier averaged over the actual finitely supported anchor law. No independence of its involved positions is asserted.
```
def motifPatternMultiplier {r : ℕ} (π : IntSeries) (s : ℕ)
    (j : Fin r → ℤ) (k : Fin r → GapDifference) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.GapDifference
def OAI.TraceReconstruction.linearPattern line 2138
theorem OAI.TraceReconstruction.motif_linear_multiplier line 2141
theorem OAI.TraceReconstruction.motifPatternMultiplier_abs_le line 2157
theorem OAI.TraceReconstruction.motif_multiplier_nonzero_support line 2182
Source documentation
A nonzero averaged pattern requires every involved tagged position to lie in one common translate of the motif; correlations are retained.
```
theorem motif_multiplier_nonzero_support {r : ℕ} (π : IntSeries) (s : ℕ)
    (j : Fin r → ℤ) (k : Fin r → GapDifference)
    (hm : motifPatternMultiplier π s j k ≠ 0) :
    ∃ X ∈ π.coeff.support, ∀ h, k h ≠ .unchanged →
      0 ≤ j h-X ∧ j h-X < (2^s : ℕ) := by
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.motifPatternMultiplier
theorem OAI.TraceReconstruction.motif_multiplier_bounded_separation line 2199

theorem OAI.TraceReconstruction.mixed_signed_shift_expansion line 2210

Source documentation

Mixing commutes with the exact signed positional expansion.

theorem mixed_signed_shift_expansion {r : ℕ} (π : IntSeries) (s : ℕ)
    (j : Fin r → ℤ) (W : (Fin r → Fin 3) → ℝ) :
    (∑ X ∈ π.coeff.support, π.coeff X *
      (W (fun h => motifShift (motifIndicator s (j h-X)) ((prouhetSeries s).coeff (j h-X)) 1)-
       W (fun h => motifShift (motifIndicator s (j h-X)) ((prouhetSeries s).coeff (j h-X)) (-1))))=
      ∑ k : Fin r → GapDifference,
        (if Odd (firstDifferenceCount k) then 2*motifPatternMultiplier π s j k else 0)*
        (∑ a : Fin r → Fin 3, (∏ h, positionalWeight (k h) (a h))*W a) := by
…

Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.motifShift, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.firstDifferenceCount, OAI.TraceReconstruction.motifPatternMultiplier, OAI.TraceReconstruction.positionalWeight

theorem OAI.TraceReconstruction.weighted_fiber_sum_le line 2254

Source documentation

A general weighted fiber sum, including multipliers which vanish on inadmissible anchor labels.

theorem weighted_fiber_sum_le {α β : Type*} [Fintype α] [Fintype β]
    (f : α → β) (a : α → ℝ) (w : β → ℝ) (P : α → ℝ) (C : ℝ)
    (hP : ∀ x, 0 ≤ P x) (ha : ∀ x, a x^2 ≤ w (f x)^2)
    (hC : ∀ y, w y ≠ 0 → (∑ x : {x // f x=y}, P x.val) ≤ C) :
    (∑ x, a x^2*P x) ≤ C*∑ y, w y^2 := by
…

def OAI.TraceReconstruction.periodCentralSumConstant line 2280
Source documentation
Explicit central-anchor summation constant for doubled period gaps.
```
def periodCentralSumConstant (u r : ℕ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.weighted_period_gap_sum line 2283

theorem OAI.TraceReconstruction.fixedPeriodProfile_large_sides line 2304

Source documentation

The two largest gaps exist even after arbitrary restrictions on the tuple, provided its anchor label is central.

theorem fixedPeriodProfile_large_sides {u r : ℕ} (a : Fin r) (h : Fin u)
    (hleft : (u:ℝ)/3 ≤ 2*h.val+1)
    (hright : (u:ℝ)/3 ≤ 2*u-(2*h.val+1)) (j : FixedPeriodTuple u r a h) :
    (∃ e ∈ Finset.Iic a.castSucc, (u:ℝ)/(3*(r+1:ℝ)) ≤ (fixedPeriodProfile a h j e).val) ∧
    (∃ d ∉ Finset.Iic a.castSucc, (u:ℝ)/(3*(r+1:ℝ)) ≤ (fixedPeriodProfile a h j d).val) := by
…

Mentions: OAI.TraceReconstruction.FixedPeriodTuple, OAI.TraceReconstruction.fixedPeriodProfile

theorem OAI.TraceReconstruction.fixedPeriodProfile_bounded_central_sum line 2338

Source documentation

Source's bounded gap refinement at a prescribed central label.

theorem fixedPeriodProfile_bounded_central_sum {u r M : ℕ} (a : Fin r) (h : Fin u)
    (c : Fin (r+1)) (hleft : (u:ℝ)/3 ≤ 2*h.val+1)
    (hright : (u:ℝ)/3 ≤ 2*u-(2*h.val+1)) (hM : (M:ℝ) < (u:ℝ)/(3*(r+1:ℝ))) :
    (∑ j : FixedPeriodTuple u r a h,
      if coarsePeriodGap j.val.val c ≤ M then ∏ i, (Real.sqrt (coarsePeriodGap j.val.val i))⁻¹ else 0) ≤
      ((r+1:ℕ):ℝ)^2*((u:ℝ)/(3*(r+1:ℝ)))⁻¹*(M+1)*(2*Real.sqrt (2*u:ℕ))^(r-2) := by
…

Mentions: OAI.TraceReconstruction.FixedPeriodTuple, OAI.TraceReconstruction.coarsePeriodGap

def OAI.TraceReconstruction.periodBoundedSumConstant line 2365
theorem OAI.TraceReconstruction.weighted_period_bounded_gap_sum line 2368
def OAI.TraceReconstruction.childWindowIndex line 2403
Source documentation
A displaced child window as an actual interval of the deterministic parent template. t is the realized count of atoms before the window.
```
def childWindowIndex {P T : ℕ} (t : ℕ) (hfit : t+T ≤ P) (h : Fin T) : Fin P :=
…
```
theorem OAI.TraceReconstruction.templateType_inside_window line 2406
theorem OAI.TraceReconstruction.templateType_outside_window line 2426
Source documentation
When the motif fits its assigned window, every atom outside that window has the default pure type, including pieces crossing nominal cuts.
```
theorem templateType_outside_window {P T a L t : ℕ}
    (sign : Fin L → Bool) (τ : Bool) (hleft : t ≤ a) (hright : a+L ≤ t+T)
    (i : Fin P) (hi : i.val < t ∨ t+T ≤ i.val) :
    templateType P a L sign τ i=false := by
…
```
Mentions: OAI.TraceReconstruction.templateType
theorem OAI.TraceReconstruction.centered_window_fit line 2436
Source documentation
A literal centered window remains within its own nominal parent unit, and contains the motif, whenever its jitter has the source fit bound. This elementary statement is independent of the distribution of the jitter.
```
theorem centered_window_fit (P T L a A t : ℕ) (Y : ℤ)
    (hP : 2*T ≤ P) (hA : 2*A=P-T) (ha : 2*a=P)
    (hL : 8*L ≤ T) (hY : |8*Y| ≤ (T:ℤ)) (ht : (t:ℤ)=A+Y) :
    t+T ≤ P ∧ t ≤ a ∧ a+L ≤ t+T := by
…
```
def OAI.TraceReconstruction.parentGroupType line 2444
Source documentation
Flattened deterministic parent type, before any random partition.
```
def parentGroupType {R P L : ℕ} (a : ℕ) (sign : Fin L → Bool)
    (τ : Fin R → Bool) (u : Fin R) (h : Fin P) : Bool :=
…
```
theorem OAI.TraceReconstruction.parentGroup_window_types line 2448