Patterns.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

Patterns

Pattern serialization, motif norms, flag posteriors, signed rank coefficients, translated binomials, and support geometry.

theorem OAI.TraceReconstruction.seriesL2Sq_partial line 23

theorem OAI.TraceReconstruction.period_pattern_norm line 44

Source documentation

The cancellation estimate after disjoint rank clipping, retaining the actual fixed-period kernels and all anchor correlations.

theorem period_pattern_norm {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)
    (hsafe : ∀ j : IncreasingTuple u r, SafeTaggedTuple (periodSlot off ∘ j.val))
    (k : Fin r → GapDifference) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1)
    (hhalf : 1/2 ≤ θ) (hmean : ((u*m:ℕ):ℝ)*θ=l) (hv : 1 ≤ ((u*m:ℕ):ℝ)*θ*(1-θ))
    (a : Fin r) (A : IncreasingTuple u r → ℝ) (w : Fin u → ℝ)
    (hA : ∀ j, A j^2 ≤ w (j.val a)^2)
    (hw : ∀ h, w h ≠ 0 → (u:ℝ)/3 ≤ 2*h.val+1 ∧ (u:ℝ)/3 ≤ 2*u-(2*h.val+1)) :
    (∑ v, (∑ j, if PeriodRankRegion m θ j v then
…

Mentions: OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.PeriodRankRegion

theorem OAI.TraceReconstruction.period_pattern_bounded_norm line 79
theorem OAI.TraceReconstruction.motif_pattern_bounded_gap line 118
Source documentation
Two involved motif positions force a short fixed internal coarse gap. The chosen gap is independent of the actual labels and of the offset law.
```
theorem motif_pattern_bounded_gap {u r : ℕ} (π : IntSeries) (s : ℕ)
    (j : IncreasingTuple u (r+1)) (k : Fin (r+1) → GapDifference)
    (i : Fin r) (b : Fin (r+1)) (hib : i.castSucc < b)
    (hi : k i.castSucc ≠ .unchanged) (hb : k b ≠ .unchanged)
    (hA : motifPatternMultiplier π s (fun a => (j.val a).val) k ≠ 0) :
    coarsePeriodGap j.val i.castSucc.succ ≤ 2*(2^s) := by
…
```
Mentions: OAI.TraceReconstruction.IntSeries, OAI.TraceReconstruction.IncreasingTuple, OAI.TraceReconstruction.GapDifference, OAI.TraceReconstruction.motifPatternMultiplier, OAI.TraceReconstruction.coarsePeriodGap
theorem OAI.TraceReconstruction.centered_window_floor_fit line 139
theorem OAI.TraceReconstruction.centered_window_floor_anchor line 148
theorem OAI.TraceReconstruction.atomString_append line 153
theorem OAI.TraceReconstruction.atomString_three line 159

theorem OAI.TraceReconstruction.template_word_window line 169

Source documentation

A full deterministic template equals a pure prefix, the actual translated window, and a pure suffix. This equality is in unmarked binary strings.

theorem template_word_window (t T z a L : ℕ) (sign : Fin L → Bool) (τ : Bool)
    (w : Bool → List Bool) (hleft : t ≤ a) (hright : a+L ≤ t+T) :
    atomString (t+T+z) w (templateType (t+T+z) a L sign τ) =
      atomString t w (fun _ => false) ++
      atomString T w (templateType T (a-t) L sign τ) ++
      atomString z w (fun _ => false) := by
…

Mentions: OAI.TraceReconstruction.atomString, OAI.TraceReconstruction.templateType

def OAI.TraceReconstruction.pureAtomRun line 186
theorem OAI.TraceReconstruction.atomString_constant line 189
theorem OAI.TraceReconstruction.pureAtomRun_add line 193
theorem OAI.TraceReconstruction.pureAtomRun_partition line 199
Source documentation
Splitting or regrouping a pure region into reported chunks changes no unmarked string. In particular arbitrary fixed chunk IDs are harmless.
```
theorem pureAtomRun_partition (w : List Bool) (ns : List ℕ) :
    (ns.map (pureAtomRun w)).flatten=pureAtomRun w ns.sum := by
…
```
Mentions: OAI.TraceReconstruction.pureAtomRun
def OAI.TraceReconstruction.FiniteLaw.flagPosterior line 214
Source documentation
Exact orientation law after a report: only invisible bits remain random.
```
def flagPosterior (d : Option Bool) : FiniteLaw Bool where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.FiniteLaw.pairedReportMass line 227
theorem OAI.TraceReconstruction.FiniteLaw.pairedFlag_bayes line 232
Source documentation
Pointwise Bayes factorization, valid even at zero probability reports.
```
theorem pairedFlag_bayes (P Q H : FiniteLaw α) (ω : ℝ)
    (z : Option Bool × (α × α)) (b : Bool) :
    (1/2 : ℝ)*pairedFlagMass P Q H ω b z =
      pairedReportMass P Q H ω z * (flagPosterior z.1).mass b := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedFlagMass, OAI.TraceReconstruction.FiniteLaw.pairedReportMass, OAI.TraceReconstruction.FiniteLaw.flagPosterior
theorem OAI.TraceReconstruction.FiniteLaw.pairedReportMass_nonneg line 242
theorem OAI.TraceReconstruction.FiniteLaw.pairedReportMass_total line 249
def OAI.TraceReconstruction.FiniteLaw.pairedReport line 256
theorem OAI.TraceReconstruction.FiniteLaw.pairedFlags_product_bayes line 264
Source documentation
Conditioning solely on exact reports does not correlate mechanisms. This is the actual joint-mass factorization, not an independence hypothesis.
```
theorem pairedFlags_product_bayes {ι : Type*} [Fintype ι]
    (P Q H : ι → FiniteLaw α) (ω : ι → ℝ)
    (z : ι → Option Bool × (α × α)) (b : ι → Bool) :
    (∏ i, (1/2 : ℝ)*pairedFlagMass (P i) (Q i) (H i) (ω i) (b i) (z i)) =
      (∏ i, pairedReportMass (P i) (Q i) (H i) (ω i) (z i)) *
        ∏ i, (flagPosterior (z i).1).mass (b i) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedFlagMass, OAI.TraceReconstruction.FiniteLaw.pairedReportMass, OAI.TraceReconstruction.FiniteLaw.flagPosterior
theorem OAI.TraceReconstruction.FiniteLaw.pairedFlags_report_marginal line 273
def OAI.TraceReconstruction.bitIndex line 287
def OAI.TraceReconstruction.posteriorBitSeries line 289
def OAI.TraceReconstruction.visibleOnes line 292
def OAI.TraceReconstruction.hiddenTrial line 294
theorem OAI.TraceReconstruction.posteriorBitSeries_factor line 296
theorem OAI.TraceReconstruction.posterior_count_series line 306
Source documentation
The count distribution of the literal posterior orientation bits is a translated fair binomial, including reports of probability zero.
```
theorem posterior_count_series {ι : Type*} [Fintype ι] (d : ι → Option Bool) :
    (∑ b : ι → Bool, AddMonoidAlgebra.single (∑ i, (bitIndex (b i):ℤ))
      (∏ i, (FiniteLaw.flagPosterior (d i)).mass (b i))) =
      AddMonoidAlgebra.single (∑ i, (visibleOnes (d i):ℤ)) 1 *
        fairSeries (∑ i, hiddenTrial (d i)) := by
…
```
Mentions: OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.FiniteLaw.flagPosterior, OAI.TraceReconstruction.visibleOnes, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.hiddenTrial
theorem OAI.TraceReconstruction.geomSeries_coeff line 334
theorem OAI.TraceReconstruction.motif_unsigned_convolution line 356
theorem OAI.TraceReconstruction.motifPatternMultiplier_sq_le line 365
theorem OAI.TraceReconstruction.unsigned_motif_energy line 374
theorem OAI.TraceReconstruction.bernoulli_entropy_upper line 388
Source documentation
Elementary chi-square upper bound on the Bernoulli relative entropy. No Stirling estimate is used in the subsequent count overlap.
```
theorem bernoulli_entropy_upper {t p : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp : p ∈ Set.Ioo 0 1) :
    t*Real.log (t/p)+(1-t)*Real.log ((1-t)/(1-p)) ≤
      (t-p)^2/(p*(1-p)) := by
…
```

theorem OAI.TraceReconstruction.binomialMass_likelihood line 401

Source documentation

Exact likelihood change from the mean-matched Bernoulli law.

theorem binomialMass_likelihood (n l : ℕ) {t p : ℝ}
    (ht : t ∈ Set.Ioo 0 1) (hp : p ∈ Set.Ioo 0 1) :
    binomialMass n p l = binomialMass n t l *
      Real.exp (-((l:ℝ)*Real.log (t/p)+((n-l:ℕ):ℝ)*Real.log ((1-t)/(1-p)))) := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.binomialMass_near_mean_lower line 422

Source documentation

Pointwise lower mass at every interior integer, with mean-matched variance at least one. It applies uniformly even as deletion vanishes.

theorem binomialMass_near_mean_lower (n l : ℕ) {t p : ℝ}
    (ht : t ∈ Set.Ioo 0 1) (hp : p ∈ Set.Ioo 0 1)
    (hl : l ≤ n) (hmean : (n:ℝ)*t=l) (hv : 1 ≤ (n:ℝ)*t*(1-t)) :
    Real.exp (-((l:ℝ)-(n:ℝ)*p)^2/((n:ℝ)*p*(1-p))) /
      (12*Real.sqrt ((n:ℝ)*t*(1-t))) ≤ binomialMass n p l := by
…

Mentions: OAI.TraceReconstruction.binomialMass

def OAI.TraceReconstruction.signedPeriodDefects line 458
theorem OAI.TraceReconstruction.signedPeriodDefects_strictMono line 464
theorem OAI.TraceReconstruction.SafeTaggedTuple.comp line 469
theorem OAI.TraceReconstruction.shiftedTag_comp line 474
def OAI.TraceReconstruction.signedRankCoefficient line 483
Source documentation
Exact degree-r coefficient difference of the actual randomized motif in the marked central run, prior to any rank clipping.
```
def signedRankCoefficient {u m l r : ℕ} (hl : l ≤ u*m) (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u := u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.signedRankCoefficient_expansion line 490
def OAI.TraceReconstruction.translateSeries line 538
theorem OAI.TraceReconstruction.translateSeries_coeff line 541
theorem OAI.TraceReconstruction.translateSeries_L2Sq line 546
theorem OAI.TraceReconstruction.translateSeries_L1 line 552
theorem OAI.TraceReconstruction.mul_translateSeries line 558
theorem OAI.TraceReconstruction.fairSeries_support line 563
theorem OAI.TraceReconstruction.fairSeries_reflect line 574
theorem OAI.TraceReconstruction.affine_reflected_binomial line 591
Source documentation
Reflection in the posterior count is exactly an ordinary translated fair binomial; it does not change the smoothing channel.
```
theorem affine_reflected_binomial (g : ℕ) (c z : ℤ) :
    (fairSeries g).coeff (c-z)=
      (translateSeries (c-g) (fairSeries g)).coeff z := by
…
```
Mentions: OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.translateSeries
theorem OAI.TraceReconstruction.translated_binomial_nonneg line 597
theorem OAI.TraceReconstruction.translated_binomial_support line 602
theorem OAI.TraceReconstruction.translated_binomial_smoothing line 609
theorem OAI.TraceReconstruction.linearPattern_order line 622
theorem OAI.TraceReconstruction.first_second_counts_linear line 630
theorem OAI.TraceReconstruction.odd_pattern_pair line 651
theorem OAI.TraceReconstruction.odd_nonlinear_order line 671

theorem OAI.TraceReconstruction.motif_convolution_support line 679

Source documentation

An actual convolution witness, retaining the common motif offset.

theorem motif_convolution_support (f π : IntSeries) (L : ℕ)
    (hf : ∀z, f.coeff z≠0 → 0≤z ∧ z<L) (z : ℤ) (hz : (f*π).coeff z≠0) :
    ∃X∈π.coeff.support, X≤z ∧ z<X+L := by
…

Mentions: OAI.TraceReconstruction.IntSeries

def OAI.TraceReconstruction.CentralMotifSupport line 688
Source documentation
A support criterion obtained from the actual side-count range.
```
def CentralMotifSupport (u s : ℕ) (π : IntSeries) : Prop :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.motif_convolution_central line 692
theorem OAI.TraceReconstruction.prouhet_convolution_central line 703
theorem OAI.TraceReconstruction.unsigned_convolution_central line 713