Amplification.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Amplification

Oracle products, mixed powers, padding, warmup and nested template Hellinger estimates, overlap, and block assembly.

theorem OAI.TraceReconstruction.OracleTracePair.mixed_tv line 24

Source documentation

The literal product/concatenation decoder charges only coordinates at which the two deterministic input templates differ.

theorem OracleTracePair.mixed_tv {q E V : ℝ} {x y : List Bool} {k n : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1) (hk : 1≤k)
    (τ σ : Fin n → Bool) (M : ℕ)
    (hτ : (coordinateWord (fun i => if τ i then y else x)).length≤M)
    (hσ : (coordinateWord (fun i => if σ i then y else x)).length≤M) :
    (listTraceLaw q hq (coordinateWord (fun i => if τ i then y else x)) M hτ).tv
      (listTraceLaw q hq (coordinateWord (fun i => if σ i then y else x)) M hσ) ≤
      Real.sqrt ((∑i,if τ i=σ i then (0:ℝ) else 1)*V)+2*(n:ℝ)*E := by
…

Mentions: OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.coordinateWord, OAI.TraceReconstruction.listTraceLaw

theorem OAI.TraceReconstruction.coordinateWord_constant line 48

theorem OAI.TraceReconstruction.OracleTracePair.power_tv line 57

Source documentation

Tensorization of a genuine approximate oracle, on actual word powers.

theorem OracleTracePair.power_tv {q E V : ℝ} {x y : List Bool} {k : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1) (hk : 1≤k)
    (n M : ℕ) (hx : (pureAtomRun x n).length≤M) (hy : (pureAtomRun y n).length≤M) :
    (listTraceLaw q hq (pureAtomRun x n) M hx).tv
      (listTraceLaw q hq (pureAtomRun y n) M hy) ≤
      Real.sqrt ((n:ℝ)*V)+2*(n:ℝ)*E := by
…

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

theorem OAI.TraceReconstruction.listTraceOverlap_lift line 70

Source documentation

Genuine lifting for complete traces, with no auxiliary overlap hypothesis.

theorem listTraceOverlap_lift {F k R : ℕ} {C p q : ℝ}
    (hk : 1≤k) (hR : 1≤R) (hp : p∈Set.Ioc 0 (1/8)) (hq : q∈Set.Icc 0 1)
    (hC : 1073741824≤p*C) (hF : C*k*R≤F) (w : List Bool)
    (hov : p≤listTraceOverlap q hq (pureAtomRun w k) (pureAtomRun w (k+1))) :
    (2/3:ℝ)≤listTraceOverlap q hq (pureAtomRun w (F*R)) (pureAtomRun w (F*R+R)) := by
…

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

theorem OAI.TraceReconstruction.pureAtomRun_mul line 84

theorem OAI.TraceReconstruction.OracleTracePair.lifted_power_overlap line 98

Source documentation

Quantitative overlap transfer used for the initial pure comparison and the small-dimensional warmup refinement. All three laws are ordinary traces.

theorem OracleTracePair.lifted_power_overlap {q E V p C₀ : ℝ} {w z : List Bool}
    {k h P F : ℕ} (O : OracleTracePair q (pureAtomRun w P) z k E V)
    (hq : q∈Set.Icc 0 1) (hk : 1≤k) (hh : 1≤h) (hP : 1≤P)
    (hp : p∈Set.Ioc 0 (1/8)) (hC : 1073741824≤p*C₀) (hF : C₀*h*P≤F)
    (hov : p≤listTraceOverlap q hq (pureAtomRun w h) (pureAtomRun w (h+1))) :
    (2/3:ℝ)-(Real.sqrt ((F:ℝ)*V)+2*(F:ℝ)*E)-
      (Real.sqrt (((F+1:ℕ):ℝ)*V)+2*((F+1:ℕ):ℝ)*E) ≤
      listTraceOverlap q hq (pureAtomRun z F) (pureAtomRun z (F+1)) := by
…

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

theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_mixedProduct_le line 142
theorem OAI.TraceReconstruction.ApproximatesTrace.power line 158

theorem OAI.TraceReconstruction.OracleTracePair.mixed_power_tv line 171

Source documentation

Repeated mixed templates pay only for the differing leaves in squared Hellinger, while approximate leaf simulation is charged linearly.

theorem OracleTracePair.mixed_power_tv {q E V : ℝ} {x y : List Bool} {k n : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1) (hk : 1 ≤ k)
    (τ σ : Fin n → Bool) (F M : ℕ)
    (hτ : (pureAtomRun (coordinateWord (fun i => if τ i then y else x)) F).length ≤ M)
    (hσ : (pureAtomRun (coordinateWord (fun i => if σ i then y else x)) F).length ≤ M) :
    (listTraceLaw q hq (pureAtomRun (coordinateWord (fun i => if τ i then y else x)) F) M hτ).tv
      (listTraceLaw q hq (pureAtomRun (coordinateWord (fun i => if σ i then y else x)) F) M hσ) ≤
      Real.sqrt ((F:ℝ)*(∑i,if τ i=σ i then (0:ℝ) else 1)*V)+2*(F:ℝ)*(n:ℝ)*E := by
…

Mentions: OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.coordinateWord, OAI.TraceReconstruction.listTraceLaw

def OAI.TraceReconstruction.OracleTracePair.pad line 215
Source documentation
An exact common prefix and suffix are observed as ordinary independent complete traces. They neither change the score moment nor cost simulation error. This is the source's deterministic residual convention.
```
def OracleTracePair.pad {q E V : ℝ} {x y : List Bool} {k : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1) (u v : List Bool) :
    OracleTracePair q (u++x++v) (u++y++v) k E V := by
…
```
Mentions: OAI.TraceReconstruction.OracleTracePair

theorem OAI.TraceReconstruction.complementaryWords_pad line 249

Source documentation

Literal template equality under deterministic pure residual padding.

theorem complementaryWords_pad (L P R a len : ℕ) (sign : Fin len → Bool)
    (w : Bool → List Bool) (τ : Bool) (hfit : a+len ≤ P) :
    complementaryWords (L+P+R) (L+a) len sign w τ =
      pureAtomRun (w false) L++complementaryWords P a len sign w τ++pureAtomRun (w false) R := by
…

Mentions: OAI.TraceReconstruction.complementaryWords, OAI.TraceReconstruction.pureAtomRun

def OAI.TraceReconstruction.centeredLeftResidual line 277
def OAI.TraceReconstruction.centeredRightResidual line 278
theorem OAI.TraceReconstruction.centeredResidual_geometry line 280
theorem OAI.TraceReconstruction.centeredComplementaryWords_pad line 288
Source documentation
The auxiliary one-window oracle is centered at the same actual source motif after appending pure residuals, also for odd ambient atom counts.
```
theorem centeredComplementaryWords_pad (N P s : ℕ) (w : Bool → List Bool) (τ : Bool)
    (hP : 2 ≤ P) (hN : P ≤ N) (hfit : P/2-1+2^s ≤ P) :
    complementaryWords N (N/2-1) (2^s) (prouhetBool s) w τ =
      pureAtomRun (w false) (centeredLeftResidual N P)++
      complementaryWords P (P/2-1) (2^s) (prouhetBool s) w τ++
      pureAtomRun (w false) (centeredRightResidual N P) := by
…
```
Mentions: OAI.TraceReconstruction.complementaryWords, OAI.TraceReconstruction.prouhetBool, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.centeredLeftResidual, OAI.TraceReconstruction.centeredRightResidual

theorem OAI.TraceReconstruction.actual_one_window_oracle line 310

Source documentation

The source's special one-window warmup observation. The ambient word need not have the root's arithmetic divisibility: exact pure residuals restore its literal center, at no additional statistical error.

theorem actual_one_window_oracle {q E V : ℝ} {x y : List Bool} {k : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1) (hE : 0 ≤ E)
    (s N T t h R : ℕ) (hT : 24 ≤ T) (he : Even T)
    (hMotif : 24*2^s ≤ T) (hroot : 4*(t+1) ≤ T)
    (hfit : t*(2*h+1)+T ≤ N)
    (ω a η L : ℝ) (ha : 0 < a) (hL : 0 < L) (hω : ω∈Set.Ioo 0 1)
    (hov : ω ≤ listTraceOverlap q hq (pureAtomRun x h) (pureAtomRun x (h+1)))
    (hk : 1 ≤ k) (hV : V ≤ L^2)
    (hscale : ((6*(2*k:ℕ):ℝ)*L)^2*sourceSparseCount (fun _ => T) s 0 ≤ 1/2)
    (hη : hiddenSmoothingBound t s ω ≤ η)
    (herror : sourceClippingCost (fun _ => T) (fun _ => t) s 0 k ω a L ≤ 1/2) :
    Nonempty (OracleTracePair q
…

Mentions: OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenSmoothingBound, OAI.TraceReconstruction.sourceClippingCost

theorem OAI.TraceReconstruction.sourceLeafCount_one line 374
theorem OAI.TraceReconstruction.sourceSharpEnergyBudget_one_window line 381
Source documentation
Exact two-degree cutoff for the one-window warmup refinement. In particular the remaining geometric term is quadratic in the old energy.
```
theorem sourceSharpEnergyBudget_one_window (T n : ℕ → ℕ) (s : ℕ) (ω η a w : ℝ) :
    sourceSharpEnergyBudget T n s 0 2 ω η a w =
      36*(T 0:ℝ)*w^2*(η^2+a^2)+4*(w^2*2^s)^2/(1-w^2*2^s) := by
…
```
Mentions: OAI.TraceReconstruction.sourceSharpEnergyBudget
theorem OAI.TraceReconstruction.sourceSharpEnergyBudget_warmup line 388
theorem OAI.TraceReconstruction.templateType_difference_count line 410
Source documentation
The number of differing labels of complementary templates is bounded by the actual motif length, without any assumption that it fills the word.
```
theorem templateType_difference_count (N a L : ℕ) (sign : Fin L → Bool) (τ σ : Bool) :
    (∑i : Fin N,if templateType N a L sign τ i=templateType N a L sign σ i then (0:ℝ) else 1) ≤ L := by
…
```
Mentions: OAI.TraceReconstruction.templateType
structure OAI.TraceReconstruction.HellingerTracePair line 440
Source documentation
Actual paired finite observations with a common complete-trace decoder and a squared Hellinger bound. This auxiliary structure is constructed from the source score oracle and closed under literal template substitution.
```
structure HellingerTracePair (q : ℝ) (x y : List Bool) (E V : ℝ) where
…
```
def OAI.TraceReconstruction.OracleTracePair.hellinger line 450
def OAI.TraceReconstruction.HellingerTracePair.mix line 464
def OAI.TraceReconstruction.HellingerTracePair.weaken line 491
def OAI.TraceReconstruction.HellingerTracePair.template line 495
theorem OAI.TraceReconstruction.HellingerTracePair.power_tv line 505
theorem OAI.TraceReconstruction.templateType_one_count line 526
def OAI.TraceReconstruction.HellingerTracePair.pure_template line 536
theorem OAI.TraceReconstruction.bool_word_eta line 548

def OAI.TraceReconstruction.sourceDensePair line 555

Source documentation

Literal dense substitution of the old auxiliary laws, used only for overlap comparison. Statistical cost is paid only for differing motif leaves, not the filler atoms.

def sourceDensePair {q E V : ℝ} (hq : q∈Set.Icc 0 1) (s : ℕ) (P : ℕ → ℕ)
    (atom : Bool → List Bool) (C : HellingerTracePair q (atom false) (atom true) E V) :
    (j : ℕ) → HellingerTracePair q (sourceBlockWord s P atom j false)
      (sourceBlockWord s P atom j true) ((sourceBlockLength P 1 j:ℝ)*E) (((2^s:ℕ):ℝ)^j*V)
  | 0 => by simpa only [sourceBlockWord,sourceBlockLength,Nat.cast_one,pow_zero,one_mul] using C
  | j+1 => by
      have D := (sourceDensePair hq s P atom C j).template hq (P j) (P j/2-1) (2^s) (prouhetBool s)
…

Mentions: OAI.TraceReconstruction.HellingerTracePair, OAI.TraceReconstruction.sourceBlockWord, OAI.TraceReconstruction.sourceBlockLength, OAI.TraceReconstruction.prouhetBool

theorem OAI.TraceReconstruction.HellingerTracePair.lifted_power_overlap line 566
theorem OAI.TraceReconstruction.HellingerTracePair.lifted_overlap_quarter line 600

theorem OAI.TraceReconstruction.source_nested_overlap line 621

Source documentation

Finite nested overlap induction at the main (post-warmup) dimensions. Every closeness premise is an explicit scalar estimate on the old oracle; the repeated-word overlaps themselves are proved, not assumed.

theorem source_nested_overlap {q E V p C₀ : ℝ} (hq : q∈Set.Icc 0 1)
    (hE : 0 ≤ E) (s : ℕ) (P h : ℕ → ℕ) (atom : Bool → List Bool)
    (C : HellingerTracePair q (atom false) (atom true) E V) (b : ℕ)
    (hp : p∈Set.Ioc 0 (1/8)) (hC : 1073741824 ≤ p*C₀)
    (hcount : ∀j ≤ b,1 ≤ h j) (hP : ∀j < b,1 ≤ P j)
    (hlift : ∀j < b,C₀*h j*P j ≤ h (j+1))
    (hsmall : ∀j < b,
      Real.sqrt (((h (j+1)+1:ℕ):ℝ)*(((2^s:ℕ):ℝ)^(j+1)*V))+
        2*((h (j+1)+1:ℕ):ℝ)*((sourceBlockLength P 1 (j+1):ℝ)*E) ≤ 1/4)
    (hbase : p ≤ listTraceOverlap q hq (pureAtomRun (atom false) (h 0))
      (pureAtomRun (atom false) (h 0+1))) :
    ∀j ≤ b,p ≤ listTraceOverlap q hq (pureAtomRun (sourceBlockWord s P atom j false) (h j))
…

Mentions: OAI.TraceReconstruction.HellingerTracePair, OAI.TraceReconstruction.sourceBlockLength, OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourceBlockWord

theorem OAI.TraceReconstruction.sourceFitTail_nonneg line 656
theorem OAI.TraceReconstruction.sourceEffectiveHiddenTail_nonneg line 664
theorem OAI.TraceReconstruction.sourceClippingCost_nonneg line 670

theorem OAI.TraceReconstruction.source_warmup_nested_overlap line 678

Source documentation

The two-dimensional warmup uses the actual one-window cancellation oracle at its second nested overlap step. No unproved side overlap is inserted into the recursive source observation.

theorem source_warmup_nested_overlap {q E V p C₀ : ℝ} (hq : q∈Set.Icc 0 1)
    (hE : 0 ≤ E) (s k : ℕ) (P h : ℕ → ℕ) (atom : Bool → List Bool)
    (C : OracleTracePair q (atom false) (atom true) k E V)
    (hp : p∈Set.Ioc 0 (1/8)) (hC : 1073741824 ≤ p*C₀)
    (hcount : ∀j ≤ 1,1 ≤ h j) (hP : ∀j < 2,1 ≤ P j)
    (hlift : ∀j < 2,C₀*h j*P j ≤ h (j+1))
    (hfirst : Real.sqrt (((h 1+1:ℕ):ℝ)*((2^s:ℕ):ℝ)*V)+
      2*((h 1+1:ℕ):ℝ)*((P 0:ℝ)*E) ≤ 1/4)
    (hbase : p ≤ listTraceOverlap q hq (pureAtomRun (atom false) (h 0))
      (pureAtomRun (atom false) (h 0+1)))
    (T t : ℕ) (hT : 24 ≤ T) (he : Even T) (hMotif : 24*2^s ≤ T)
    (hroot : 4*(t+1) ≤ T) (hfit : t*(2*h 0+1)+T ≤ P 0)
…

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

theorem OAI.TraceReconstruction.OracleTracePair.error_nonneg line 734

theorem OAI.TraceReconstruction.actual_main_block line 743

Source documentation

Finite main-block production: actual oracle, complete trace projection, and all side overlaps follow from arithmetic budgets and the OLD invariant. In particular none of the new side laws or their overlap are hypotheses.

theorem actual_main_block {q E V ω C₀ : ℝ} (hq : q∈Set.Icc 0 1)
    (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b R k : ℕ)
    (C : OracleTracePair q (atom false) (atom true) k E V)
    (H : SourceLayoutMargins s P T n h b)
    (hTpos : ∀j,0 < T j) (hP : P b=n b*(2*h b+1)+T b)
    (hn : ∀j < b,0 < n j) (hT : ∀j ≤ b,24 ≤ T j) (he : ∀j ≤ b,Even (T j))
    (hMotif : ∀j ≤ b,24*2^s ≤ T j) (hroot : 4*(n b+1) ≤ T b)
    (a η L : ℝ) (ha : 0 < a) (hL : 0 < L) (hω : ω∈Set.Ioc 0 (1/8))
    (hk : 1 ≤ k) (hV : V ≤ L^2)
    (hscale : ((6*(2*k:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤ 1/2)
    (hη : ∀j < b+1,hiddenSmoothingBound (n j) s ω ≤ η)
    (herror : sourceClippingCost T n s b k ω a L ≤ 1/2)
…

Mentions: OAI.TraceReconstruction.OracleTracePair, OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenSmoothingBound, OAI.TraceReconstruction.sourceClippingCost

def OAI.TraceReconstruction.OracleTracePair.toConcrete line 784

Source documentation

Conversion of a produced genuine oracle into the manuscript invariant. The scalar bounds here are exactly those to be discharged by scale margins.

def OracleTracePair.toConcrete {q E V N Δ d ω F : ℝ} {x y : List Bool} {k i h : ℕ}
    (C : OracleTracePair q x y k E V) (hq : q∈Set.Icc 0 1)
    (hlen : x.length=y.length) (hne : x≠y) (hlo : N/2 ≤ (x.length:ℝ))
    (hhi : (x.length:ℝ) ≤ N) (herror : E/(x.length:ℝ) ≤ ((i:ℝ)+1)*Δ)
    (hV : V ≤ N^(-d)) (hhlo : x.length ≤ h) (hhhi : (h:ℝ) ≤ F*(x.length:ℝ))
    (hov : ω ≤ listTraceOverlap q hq (pureAtomRun x h) (pureAtomRun x (h+1))) :
    ConcreteLevelPair q hq N Δ d ω F i k := {
…

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