InitialOverlap.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

InitialOverlap

Literal periods, count overlap, initial low/high energies, genuine densities, and centered moment bounds.

theorem OAI.TraceReconstruction.primitive_one_add_score_nonneg line 23
theorem OAI.TraceReconstruction.conditionalPeriodLaw_density line 30
Source documentation
Exact conditional law of the genuine periodic primitive observation.
```
theorem conditionalPeriodLaw_density {u m l : ℕ} (hl : l ≤ u*m)
    {q : ℝ} (hq : q ∈ Set.Ioo 0 1) (off : Fin u → Fin m) (x : Fin l → PrimitiveMark) :
    (conditionalPrimitiveLaw hl q hq (defectTypes (periodSlot off))).mass x =
      ((primitiveMarkLaw q hq false).product l).mass x *
        averagedDensity (uniformSubsetLaw l (by simpa using hl))
          (defectAtRank (Finset.univ.image (periodSlot off))) (primitiveScore q) x := by
…
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.conditionalPrimitiveLaw, OAI.TraceReconstruction.defectTypes, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.primitiveMarkLaw, OAI.TraceReconstruction.averagedDensity, OAI.TraceReconstruction.uniformSubsetLaw, OAI.TraceReconstruction.defectAtRank, OAI.TraceReconstruction.primitiveScore
def OAI.TraceReconstruction.primitivePeriodConstant line 42
Source documentation
Absolute constant in the conditional second-moment exponent.
```
def primitivePeriodConstant : ℝ := 36*rankSchurConstant^2
```
Mentions: OAI.TraceReconstruction.rankSchurConstant
theorem OAI.TraceReconstruction.primitivePeriodConstant_nonneg line 44
theorem OAI.TraceReconstruction.conditionalPeriod_second_moment line 48

theorem OAI.TraceReconstruction.conditionalPeriod_overlap line 78

Source documentation

Association converts the two actual conditional period-laws into common mass. The two original block totals may differ; only the retained count agrees.

theorem conditionalPeriod_overlap {u v m l : ℕ}
    (hl : l ≤ u*m) (hl' : l ≤ v*m) (hm : 32 ≤ m) (hum : u ≤ m) (hvm : v ≤ m)
    {q θ θ' : ℝ} (hq : q ∈ Set.Ioc 0 (1/2:ℝ))
    (hθ : θ ∈ Set.Icc (1-q^2) (1-q^2/4))
    (hθ' : θ' ∈ Set.Icc (1-q^2) (1-q^2/4))
    (hmean : ((u*m:ℕ):ℝ)*θ=l) (hmean' : ((v*m:ℕ):ℝ)*θ'=l)
    (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ)) (hv' : 1 ≤ ((v*m:ℕ):ℝ)*θ'*(1-θ'))
    (off : Fin u → Fin m) (off' : Fin v → Fin m)
    (hoff : ∀ j, |((off j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hoff' : ∀ j, |((off' j).val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hdiff : ∀ j k, |((off j).val:ℝ)-(off k).val| ≤ 2)
    (hdiff' : ∀ j k, |((off' j).val:ℝ)-(off' k).val| ≤ 2) :
…

theorem OAI.TraceReconstruction.primitive_count_window line 154

Source documentation

The common count window is admissible for every genuine period count in the base case. All hypotheses are elementary size/location inequalities.

theorem primitive_count_window {q θ : ℝ} {m n l : ℕ}
    (hq : q ∈ Set.Ioc 0 (1/2:ℝ)) (hm : 32 ≤ m)
    (hscale : 16 ≤ q^3*(m:ℝ))
    (hnlo : q*(m:ℝ)^2/2 ≤ (n:ℝ)) (hnhi : (n:ℝ) ≤ (m:ℝ)^2)
    (hmean : (n:ℝ)*θ=l)
    (hdev : |(l:ℝ)-(n:ℝ)*(1-q^2/2)| ≤ 2*(m:ℝ)) :
    θ ∈ Set.Icc (1-q^2) (1-q^2/4) ∧
    1 ≤ (n:ℝ)*θ*(1-θ) ∧
    Real.sqrt ((n:ℝ)*θ*(1-θ)) ≤ (m:ℝ) ∧
    ((l:ℝ)-(n:ℝ)*(1-q^2/2))^2 / ((n:ℝ)*(1-q^2/2)*(q^2/2)) ≤ 32/q^3 := by
…

theorem OAI.TraceReconstruction.primitive_count_mass_lower line 218

Source documentation

Genuine binomial count mass in the window, uniformly in the vanishing working deletion rate, with an absolute explicit exponential cost.

theorem primitive_count_mass_lower {q : ℝ} {m n l : ℕ}
    (hq : q ∈ Set.Ioc 0 (1/2:ℝ)) (hm : 32 ≤ m)
    (hscale : 16 ≤ q^3*(m:ℝ))
    (hnlo : q*(m:ℝ)^2/2 ≤ (n:ℝ)) (hnhi : (n:ℝ) ≤ (m:ℝ)^2)
    (hdev : |(l:ℝ)-(n:ℝ)*(1-q^2/2)| ≤ 2*(m:ℝ)) :
    Real.exp (-32/q^3)/(12*(m:ℝ)) ≤ binomialMass n (1-primitiveErasure q) l := by
…

Mentions: OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.primitiveErasure

def OAI.TraceReconstruction.initialSideCount line 253
Source documentation
The actual base count, with no redefinition of the working channel.
```
def initialSideCount (q : ℝ) (m : ℕ) : ℕ := ⌊q*(m:ℝ)⌋₊
```
theorem OAI.TraceReconstruction.initialSideCount_bounds line 255
def OAI.TraceReconstruction.commonCountIndex line 278
Source documentation
An injective enumeration of m common integer counts; no asymptotic cardinality argument is left implicit.
```
def commonCountIndex {m : ℕ} (k : ℕ) (p : ℝ) (hp : p ∈ Set.Icc 0 1) (j : Fin m) :
    Fin ((k+1)*m+1) :=
…
```
theorem OAI.TraceReconstruction.commonCountIndex_injective line 289
theorem OAI.TraceReconstruction.commonCountIndex_deviation line 296
theorem OAI.TraceReconstruction.ordinaryRun_replicate line 323
theorem OAI.TraceReconstruction.primitive_period_word line 331
Source documentation
Unique primitive parsing identifies the rank model with the literal period words in the manuscript, not just a law on unlabeled locations.
```
theorem primitive_period_word {m : ℕ} (off : Fin m) :
    (List.ofFn (fun j : Fin m => primitiveBlock (decide (j=off)))).flatten =
      initialPeriod m off.val := by
…
```
Mentions: OAI.TraceReconstruction.primitiveBlock, OAI.TraceReconstruction.initialPeriod
theorem OAI.TraceReconstruction.periodSlot_range_iff line 349
Source documentation
Membership in the true periodic defect set is exactly the within-period slot test, uniformly for all deterministic period types.
```
theorem periodSlot_range_iff {u m : ℕ} (off : Fin u → Fin m) (i : Fin u) (j : Fin m) :
    (⟨i.val*m+j.val,by
      have hi := Nat.mul_le_mul_right m (Nat.succ_le_of_lt i.isLt)
…
```
theorem OAI.TraceReconstruction.periodic_primitive_word line 373
Source documentation
The simulator's actual primitive list is the unpadded source gadget.
```
theorem periodic_primitive_word {u m : ℕ} (off : Fin u → Fin m) :
    (((List.ofFn (defectTypes (periodSlot off))).map primitiveBlock).flatten) =
      periodString m u off := by
…
```
Mentions: OAI.TraceReconstruction.defectTypes, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.primitiveBlock, OAI.TraceReconstruction.periodString
theorem OAI.TraceReconstruction.periodString_constant line 393
theorem OAI.TraceReconstruction.primitive_count_admissible line 405
def OAI.TraceReconstruction.initialOverlapLower line 426
Source documentation
The common-mass constant depends only on the working deletion rate.
```
def initialOverlapLower (q : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.initialOverlapLower_pos line 429
theorem OAI.TraceReconstruction.initialOverlapLower_lt_eighth line 433
theorem OAI.TraceReconstruction.initial_counted_overlap line 445
Source documentation
Unconditioned common mass of the two genuine count-and-mark simulators. This includes all retained counts, not a conditioned or changed channel.
```
theorem initial_counted_overlap {q : ℝ} {m : ℕ}
    (hq : q ∈ Set.Ioc 0 (1/2:ℝ)) (hm : 32 ≤ m)
    (hscale : 16 ≤ q^3*(m:ℝ)) (off : Fin m)
    (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 3) :
    let k := initialSideCount q m
…
```
Mentions: OAI.TraceReconstruction.initialSideCount
theorem OAI.TraceReconstruction.simulations_overlap_le line 552
Source documentation
Data processing for common exact simulators, stated as a common-mass inequality and allowing unequal original lengths.
```
theorem simulations_overlap_le {α : Type*} [Fintype α] {q : ℝ}
    (hq : q ∈ Set.Icc 0 1) (P Q : FiniteLaw α) (decode : α → List Bool)
    (x y : List Bool) (hP : SimulatesTrace q P decode x)
    (hQ : SimulatesTrace q Q decode y) :
    P.overlap Q ≤ listTraceOverlap q hq x y := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.SimulatesTrace, OAI.TraceReconstruction.listTraceOverlap
theorem OAI.TraceReconstruction.initial_pure_trace_overlap line 567
Source documentation
The initial hidden-bit overlap for ordinary complete deletion traces of consecutive pure runs. This is the unconditioned original channel.
```
theorem initial_pure_trace_overlap {q : ℝ} {m : ℕ}
    (hq : q ∈ Set.Ioc 0 (1/2:ℝ)) (hm : 32 ≤ m)
    (hscale : 16 ≤ q^3*(m:ℝ)) (off : Fin m)
    (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 3) :
    let k := initialSideCount q m
…
```
Mentions: OAI.TraceReconstruction.initialSideCount
def OAI.TraceReconstruction.oneStepOffset line 598
Source documentation
An interior period slot admits the three literal shifts.
```
def oneStepOffset {m : ℕ} (off : Fin m)
    (hi : 1  ≤  off.val ∧ off.val + 1 < m) (a : Fin 3) : Fin m :=
…
```
theorem OAI.TraceReconstruction.oneStepOffset_add_one line 602
theorem OAI.TraceReconstruction.oneStepOffset_distance line 608
theorem OAI.TraceReconstruction.constantPeriod_safe line 618
theorem OAI.TraceReconstruction.shifted_constantPeriod line 631
theorem OAI.TraceReconstruction.signedPeriod_geometry line 644
Source documentation
Arbitrary deterministic motif orientations remain genuine one-defect periods with the exact geometry used in the high-degree rank bound.
```
theorem signedPeriod_geometry {u m : ℕ} (off : Fin m)
    (hi : 1  ≤  off.val ∧ off.val + 1 < m)
    (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.primitive_score_evenMoment line 671
Source documentation
Every moment of the actual primitive score has the source uniform bound.
```
theorem primitive_score_evenMoment {q : ℝ} (hq : q∈Set.Ioo 0 1) (k : ℕ) :
    (primitiveMarkLaw q hq false).expect (fun z => |primitiveScore q z|^(2*k))  ≤ 
      (2/q)^(2*k) := by
…
```
Mentions: OAI.TraceReconstruction.primitiveMarkLaw, OAI.TraceReconstruction.primitiveScore
theorem OAI.TraceReconstruction.initial_moment_of_energy line 684
Source documentation
Hypercontractivity now applies directly to the actual signed initial density difference under its ordinary-mark reference law.
```
theorem initial_moment_of_energy {u m l : ℕ} (hl : l ≤ u*m) (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.degree_square_mixture_le line 699

Source documentation

Jensen's inequality on each homogeneous degree.

theorem degree_square_mixture_le {Ω : Type*} [Fintype Ω] {n : ℕ}
    (P : FiniteLaw Ω) (A : Ω → (Fin n → Bool) → ℝ) (r : ℕ) :
    (∑σ : Fin n → Bool, if monomialDegree σ=r then
      (P.expect (fun ω => A ω σ))^2 else 0)  ≤ 
    P.expect (fun ω => ∑σ : Fin n → Bool,
      if monomialDegree σ=r then (A ω σ)^2 else 0) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.monomialDegree

theorem OAI.TraceReconstruction.degree_square_sub_le line 716
theorem OAI.TraceReconstruction.mixedMotifCoefficient_expect line 725
theorem OAI.TraceReconstruction.mixedMotifCoefficient_empty line 736

theorem OAI.TraceReconstruction.mixedMotif_degree_le line 743

Source documentation

Uniform high-degree estimate after the real hidden-anchor mixture.

theorem mixedMotif_degree_le {u m l r : ℕ} (hl : l ≤ u*m) (hr : 0 < r)
    (hru : r ≤ u) (hm : 32 ≤ m) (hum : u ≤ m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.mixedMotif_degree_vanish line 768
Source documentation
There are never more selected ranks than actual defect periods, even in the hidden-anchor mixture.
```
theorem mixedMotif_degree_vanish {u m l r : ℕ} (hl : l ≤ u*m) (hru : u < r) (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.signedMotif_degree_zero line 782
Source documentation
The signed difference has no constant term.
```
theorem signedMotif_degree_zero {u m l : ℕ} (hl : l ≤ u*m) (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.signedMotif_degree_cancellation line 793
Source documentation
Low-degree cancellation is for exactly the coefficients of the conditional motif densities, without a rank surrogate at the boundary.
```
theorem signedMotif_degree_cancellation {u m l r : ℕ}
    (hu : 0 < u) (hm : 128 ≤ m) (hr : 0 < r) (hl : l ≤ u*m)
    (off : Fin m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 3)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.finite_geometric_tail_le line 824

Source documentation

A finite tail is no larger than the full geometric tail.

theorem finite_geometric_tail_le {a : ℝ} (ha : 0 ≤ a) (ha1 : a < 1) (N R : ℕ) :
    (∑r ∈ Finset.range N, if R ≤ r then a^r else 0) ≤ a^R/(1-a) := by
…

theorem OAI.TraceReconstruction.multilinearEnergy_low_high line 849

Source documentation

Splitting the exact homogeneous expansion, not a surrogate polynomial.

theorem multilinearEnergy_low_high {n R : ℕ} (A : (Fin n → Bool) → ℝ)
    (w a K : ℝ) (hw : 0 ≤ w) (ha : 0 ≤ a) (ha1 : a < 1) (hK : 0 ≤ K)
    (L : ℕ → ℝ)
    (hlow : ∀r < R, (∑σ : Fin n → Bool, if monomialDegree σ=r then A σ^2 else 0) ≤ L r)
    (hhigh : ∀r, R ≤ r → w^(2*r)*(∑σ : Fin n → Bool,
      if monomialDegree σ=r then A σ^2 else 0) ≤ K*a^r)
    (hL : ∀r, 0 ≤ L r) :
    multilinearEnergy A w ≤ (∑r ∈ Finset.range R, w^(2*r)*L r)+K*a^R/(1-a) := by
…

Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.multilinearEnergy

theorem OAI.TraceReconstruction.signedMotif_degree_geometric line 885

Source documentation

The signed high-degree bound includes the true anchor mixture.

theorem signedMotif_degree_geometric {u m l r : ℕ} (hl : l ≤ u*m) (hr : 0 < r)
    (hm : 32 ≤ m) (hum : u ≤ m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

def OAI.TraceReconstruction.signedInitialDegreeBound line 928
Source documentation
Explicit low-degree majorant from the signed finite-difference estimate.
```
def signedInitialDegreeBound (u m r s : ℕ) (π : IntSeries) (θ : ℝ) (l : ℕ) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.signedInitialDegreeBound_nonneg line 936
theorem OAI.TraceReconstruction.signed_initial_full_energy line 954
Source documentation
A fully finite norm estimate for the actual low and high degree pieces. Only numerical admissible-count and geometric conditions remain to be chosen.
```
theorem signed_initial_full_energy {u m l R : ℕ} (hu : 0 < u) (hm : 128 ≤ m)
    (hum : u ≤ m) (hR : 0 < R) (hl : l ≤ u*m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.primitive_reference_mass_pos line 1002
theorem OAI.TraceReconstruction.primitive_product_mass_pos line 1008
def OAI.TraceReconstruction.initialMotifDensity line 1015
Source documentation
The density in the actual base experiment, not an independent model.
```
def initialMotifDensity {u m l : ℕ} (hl : l ≤ u*m) (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.initialMotifDensity_nonneg line 1020
theorem OAI.TraceReconstruction.initialMotifDensity_mean line 1029
theorem OAI.TraceReconstruction.initialMotifLaw_withDensity line 1037
theorem OAI.TraceReconstruction.multilinear_sub line 1050
def OAI.TraceReconstruction.nonconstantCoefficient line 1056
Source documentation
The constant-term deletion of a polynomial.
```
def nonconstantCoefficient {l : ℕ} (A : (Fin l → Bool) → ℝ) (σ : Fin l → Bool) : ℝ :=
…
```
theorem OAI.TraceReconstruction.nonconstant_multilinear line 1059
theorem OAI.TraceReconstruction.nonconstant_degree_zero line 1069
theorem OAI.TraceReconstruction.nonconstant_degree_pos line 1073
theorem OAI.TraceReconstruction.mixedMotif_degree_geometric line 1091

theorem OAI.TraceReconstruction.initial_centered_energy line 1121

Source documentation

Clipping input: the actual conditional density is close to one.

theorem initial_centered_energy {u m l : ℕ} (hl : l ≤ u*m)
    (hm : 32 ≤ m) (hum : u ≤ m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…

Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot

theorem OAI.TraceReconstruction.initial_centered_moment line 1147