SourceOracle.lean`

127 declarations, 0 contain sorry, 0 declared as axioms

SourceOracle

Actual source mechanisms and posteriors, typical metadata, sparse degrees, common-event clipping, approximate oracles, and mixed Hellinger bounds.

theorem OAI.TraceReconstruction.listTraceOverlap_le_ambient line 25
Source documentation
Ambient finite trace-space choice does not lose any of the genuine complete-trace common mass. The embedding adds only zero-mass points.
```
theorem listTraceOverlap_le_ambient {q : ℝ} (hq : q∈Set.Icc 0 1)
    (x y : List Bool) (M : ℕ) (hx : x.length≤M) (hy : y.length≤M) :
    listTraceOverlap q hq x y≤
      (listTraceLaw q hq x M hx).overlap (listTraceLaw q hq y M hy) := by
…
```
Mentions: OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.listTraceLaw
theorem OAI.TraceReconstruction.listTraceOverlap_ambient line 40
theorem OAI.TraceReconstruction.FiniteLaw.commonPart_le_right line 50
def OAI.TraceReconstruction.tracePairedMechanisms line 63
Source documentation
The paired experiment uses the actual unseparated complete deletion traces, and the actual normalized minimum of their mass functions.
```
def tracePairedMechanisms {m : ℕ} {q ω : ℝ} (hq : q∈Set.Icc 0 1) (hω : 0<ω)
    (U V : Fin m → List Bool) (M : ℕ) (hU : ∀j,(U j).length≤M) (hV : ∀j,(V j).length≤M)
    (hov : ∀j,ω≤listTraceOverlap q hq (U j) (V j)) : PairedMechanisms (BoundedTrace M) m where
…
```
Mentions: OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.BoundedTrace

theorem OAI.TraceReconstruction.sourceTrialWord_overlap line 78

Source documentation

Every literal side pair draws its overlap from the correct height of the source recursion, including reflected global pairs.

theorem sourceTrialWord_overlap {q ω : ℝ} (hq : q∈Set.Icc 0 1)
    (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b : ℕ)
    (hov : ∀j<b,ω≤listTraceOverlap q hq
      (pureAtomRun (sourceBlockWord s P atom j false) (h j))
      (pureAtomRun (sourceBlockWord s P atom j false) (h j+1)))
    (i : WindowTrial T n (sourceScheduledTrials T n) b) :
    ω≤listTraceOverlap q hq (sourceTrialWord s P T n h atom b i false)
      (sourceTrialWord s P T n h atom b i true) := by
…

Mentions: OAI.TraceReconstruction.listTraceOverlap, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourceBlockWord, OAI.TraceReconstruction.WindowTrial, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceTrialWord

theorem OAI.TraceReconstruction.finite_word_bound line 97
Source documentation
A common finite side-trace space exists without changing any word.
```
theorem finite_word_bound {ι : Type*} [Fintype ι] (w : ι → List Bool) :
    ∃M,∀i,(w i).length≤M := by
…
```
def OAI.TraceReconstruction.sourceReportFlags line 110
Source documentation
The actual report flags, in the literal nested trial coordinates.
```
def sourceReportFlags {Side : Type*} (T n : ℕ → ℕ) (b : ℕ)
    (z : Reports Side (SourceTrialCount T n b)) :
    WindowAssignments T n (sourceScheduledTrials T n) (Option Bool) b :=
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials
theorem OAI.TraceReconstruction.source_posterior_code_expect line 117
Source documentation
Exact change of coordinates for the posterior of all hidden bits, not just separate local marginals.
```
theorem source_posterior_code_expect {Side : Type*} (T n : ℕ → ℕ) (b : ℕ)
    (z : Reports Side (SourceTrialCount T n b))
    (F : WindowAssignments T n (sourceScheduledTrials T n) Bool b → ℝ) :
    (PairedMechanisms.orientationsGiven z).expect
      (fun bits => F ((sourceAssignmentCode T n Bool b).symm bits)) =
    (windowPosteriorLaw T n (sourceScheduledTrials T n) b (sourceReportFlags T n b z)).expect F := by
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.PairedMechanisms.orientationsGiven, OAI.TraceReconstruction.sourceAssignmentCode, OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.sourceReportFlags
def OAI.TraceReconstruction.sourceSubsetCode line 132
Source documentation
A monomial is precisely its set of actual leaf addresses.
```
def sourceSubsetCode (T : ℕ → ℕ) (b : ℕ) :
    (Fin (SourceLeafCount T b) → Bool) ≃ Finset (WindowLeaf T b) :=
…
```
Mentions: OAI.TraceReconstruction.SourceLeafCount, OAI.TraceReconstruction.WindowLeaf
theorem OAI.TraceReconstruction.sourceSubsetCode_card line 136
theorem OAI.TraceReconstruction.selectionCoefficient_sign line 142
theorem OAI.TraceReconstruction.source_leaf_selection line 150
theorem OAI.TraceReconstruction.source_canonical_coefficient line 167
Source documentation
The real canonical-oracle coefficient difference is the exact source polynomial coefficient whose forced-tree energy has been proved.
```
theorem source_canonical_coefficient {Side : Type*} (T n : ℕ → ℕ) (s : ℕ)
    (center : ℕ → ℤ) (b : ℕ) (incoming : ℤ)
    (z : Reports Side (SourceTrialCount T n (b+1)))
    (σ : Fin (SourceLeafCount T (b+1)) → Bool) :
    averagedCoefficient (PairedMechanisms.orientationsGiven z)
      (sourceFlatLeafType T n s center (b+1) incoming false) σ -
    averagedCoefficient (PairedMechanisms.orientationsGiven z)
      (sourceFlatLeafType T n s center (b+1) incoming true) σ =
    sourceCoefficient T n (sourceScheduledTrials T n) s center (sourceScheduledShift T n)
      b (sourceReportFlags T n (b+1) z) incoming (sourceSubsetCode T (b+1) σ) := by
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceLeafCount, OAI.TraceReconstruction.averagedCoefficient, OAI.TraceReconstruction.PairedMechanisms.orientationsGiven, OAI.TraceReconstruction.sourceFlatLeafType, OAI.TraceReconstruction.sourceCoefficient, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceScheduledShift, OAI.TraceReconstruction.sourceReportFlags, OAI.TraceReconstruction.sourceSubsetCode

theorem OAI.TraceReconstruction.source_canonical_degree_sum line 189

Source documentation

Reindexing preserves the entire degree-r square sum, including zero and degrees larger than the number of real leaves.

theorem source_canonical_degree_sum {Side : Type*} (T n : ℕ → ℕ) (s : ℕ)
    (center : ℕ → ℤ) (b r : ℕ) (incoming : ℤ)
    (z : Reports Side (SourceTrialCount T n (b+1))) :
    (∑σ : Fin (SourceLeafCount T (b+1)) → Bool, if monomialDegree σ=r then
      (averagedCoefficient (PairedMechanisms.orientationsGiven z)
        (sourceFlatLeafType T n s center (b+1) incoming false) σ -
       averagedCoefficient (PairedMechanisms.orientationsGiven z)
        (sourceFlatLeafType T n s center (b+1) incoming true) σ)^2 else 0) =
    ∑S : DegreeLeafSubset T b r,
      (sourceCoefficient T n (sourceScheduledTrials T n) s center (sourceScheduledShift T n)
        b (sourceReportFlags T n (b+1) z) incoming S.val)^2 := by
…

def OAI.TraceReconstruction.PairedMechanisms.hiddenSubset line 219
theorem OAI.TraceReconstruction.PairedMechanisms.hiddenSubset_mgf line 221
theorem OAI.TraceReconstruction.PairedMechanisms.hiddenSubset_small line 251
Source documentation
A quantitative unconditional bound for failure of a source hidden-count condition. The exponent ω⁴m is sufficient for the uniform scale margins.
```
theorem hiddenSubset_small (S : Finset (Fin m)) {ω : ℝ} (hw : ∀i,M.hiddenWeight i=ω) (hp : ω^2∈Set.Icc 0 1) :
    M.reports.expect (fun z => if (hiddenSubset S z:ℝ)<(S.card:ℝ)*ω^2/2 then 1 else 0)≤
      Real.exp (-(S.card:ℝ)*ω^4/16) := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.hiddenSubset
def OAI.TraceReconstruction.WindowCollection line 287
Source documentation
IDs for precisely one local and one global collection at every genuine nonleaf of the complete source window tree.
```
def WindowCollection (T : ℕ → ℕ) : ℕ → Type
  | 0 => PEmpty
  | b+1 => Bool ⊕ (Fin (T b) × WindowCollection T b)
```
instance OAI.TraceReconstruction.windowCollectionFintype line 291
def OAI.TraceReconstruction.collectionCount line 298
def OAI.TraceReconstruction.collectionTrial line 303
theorem OAI.TraceReconstruction.collectionTrial_injective line 309
def OAI.TraceReconstruction.collectionFlags line 324
theorem OAI.TraceReconstruction.collectionFlags_trial line 331

def OAI.TraceReconstruction.HiddenCollectionConditions line 344

Source documentation

This is the source hidden-count predicate, before any conditioning on fit.

def HiddenCollectionConditions (T n g : ℕ → ℕ) (ω : ℝ) :
    (b : ℕ) → WindowAssignments T n g (Option Bool) b → Prop
  | 0, _ => True
  | b+1, d =>
      (n b:ℝ)*ω^2/2≤∑i,(hiddenTrial (d.1 i):ℝ) ∧
      (g b:ℝ)*ω^2/2≤∑i,(hiddenTrial (d.2.1 i):ℝ) ∧
      ∀u,HiddenCollectionConditions T n g ω b (d.2.2 u)

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.hiddenTrial

theorem OAI.TraceReconstruction.hiddenCollectionConditions_iff line 352
def OAI.TraceReconstruction.sourceCollectionIndex line 372
theorem OAI.TraceReconstruction.sourceCollectionIndex_injective line 376
def OAI.TraceReconstruction.sourceCollectionSet line 380
theorem OAI.TraceReconstruction.sourceCollectionSet_card line 383
theorem OAI.TraceReconstruction.sourceCollection_flags line 388
theorem OAI.TraceReconstruction.sourceCollection_hidden line 398
def OAI.TraceReconstruction.sourceHiddenTail line 411
Source documentation
Exact finite-union metadata cost; it contains no postulated typical event and no independence assertion between different collections.
```
def sourceHiddenTail (T n : ℕ → ℕ) (b : ℕ) (ω : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.source_hidden_conditions_tail line 414
def OAI.TraceReconstruction.hiddenBinomialCap line 454
Source documentation
Numerical cap forced by at least half the mean number of hidden pairs.
```
def hiddenBinomialCap (m : ℕ) (ω : ℝ) : ℝ := Real.sqrt (4/((m:ℝ)*ω^2+2))
```
theorem OAI.TraceReconstruction.hiddenBinomialCap_nonneg line 456
theorem OAI.TraceReconstruction.hidden_binomial_bound line 459
def OAI.TraceReconstruction.hiddenSmoothingBound line 466
theorem OAI.TraceReconstruction.hiddenSmoothingBound_nonneg line 470
theorem OAI.TraceReconstruction.hidden_smoothing_bound line 473
theorem OAI.TraceReconstruction.hiddenConditions_binomialCaps line 493
Source documentation
Hidden-count typicality implies every local/global anchor cap, for the actual source metadata and without a coefficient-dependent event.
```
theorem hiddenConditions_binomialCaps (T n g : ℕ → ℕ) (ω : ℝ) (b : ℕ)
    (d : WindowAssignments T n g (Option Bool) b)
    (h : HiddenCollectionConditions T n g ω b d) :
    MetadataBinomialCaps T n g (fun j => hiddenBinomialCap (n j) ω)
      (fun j => hiddenBinomialCap (g j) ω) b d := by
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.HiddenCollectionConditions, OAI.TraceReconstruction.MetadataBinomialCaps, OAI.TraceReconstruction.hiddenBinomialCap
theorem OAI.TraceReconstruction.hiddenConditions_smoothingCap line 505
theorem OAI.TraceReconstruction.source_noncentral_average line 525
Source documentation
The actual noncentral posterior mass has the unconditional honest fit-error bound. Impossible reports cause no problem in Bayes averaging.
```
theorem source_noncentral_average {Side : Type*} [Fintype Side]
    (T n : ℕ → ℕ) (s b : ℕ) (M : PairedMechanisms Side (SourceTrialCount T n (b+1)))
    (hn : ∀j,j<b → 0<n j) (hne : ∀j,j<b → Even (n j))
    (hT : ∀j≤b,24≤T j) (he : ∀j≤b,Even (T j)) (hL : ∀j≤b,24*2^s≤T j)
    (hroot : 4*(n b+1)≤T b) :
    M.reports.expect (fun z => sourceNoncentralMass T n (sourceScheduledTrials T n) s
      (sourceLocalCenter T n) (sourceScheduledShift T n) (fun j => centralThird (T j))
      (b+1) (sourceReportFlags T n (b+1) z) 0) ≤ sourceFitTail T n (b+1) := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.sourceNoncentralMass, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceLocalCenter, OAI.TraceReconstruction.sourceScheduledShift, OAI.TraceReconstruction.centralThird, OAI.TraceReconstruction.sourceReportFlags, OAI.TraceReconstruction.sourceFitTail

theorem OAI.TraceReconstruction.FiniteLaw.positive_markov line 551

Source documentation

Markov for a genuine finite law, stated for the exact failure indicator.

theorem FiniteLaw.positive_markov {α : Type*} [Fintype α] (P : FiniteLaw α)
    (f : α → ℝ) (hf : ∀x,0≤f x) {a : ℝ} (ha : 0<a) :
    P.expect (fun x => if a≤f x then 1 else 0) ≤ P.expect f/a := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw

def OAI.TraceReconstruction.SourceTypical line 564
Source documentation
One metadata event, fixed before choosing a coefficient, controls local and global smoothing and all internal central-third tests.
```
def SourceTypical {Side : Type*} (T n : ℕ → ℕ) (s b : ℕ) (ω a : ℝ)
    (z : Reports Side (SourceTrialCount T n (b+1))) : Prop :=
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount
theorem OAI.TraceReconstruction.source_typical_failure line 572
theorem OAI.TraceReconstruction.scheduledGlobalShift_plateau_exact line 617
Source documentation
Exact common plateau with integer half-count centering. Unlike the simplified g/2 formula, this identity needs no parity assumption.
```
theorem scheduledGlobalShift_plateau_exact (N t : ℕ)
    (bits : Fin ((N/4)*t) → Bool) (u : Fin N) (hu : u∈centralThird N) :
    scheduledGlobalShift N t bits u = (∑i,(bitIndex (bits i):ℤ))-(N/4:ℕ)*(t/2:ℕ) := by
…
```
Mentions: OAI.TraceReconstruction.centralThird, OAI.TraceReconstruction.scheduledGlobalShift, OAI.TraceReconstruction.bitIndex
def OAI.TraceReconstruction.sourcePlateauCenter line 632
theorem OAI.TraceReconstruction.sourceScheduledShift_hasPlateau line 636
def OAI.TraceReconstruction.sourceForcedBudget line 646
theorem OAI.TraceReconstruction.sourceForcedBudget_nonneg line 653
def OAI.TraceReconstruction.sourceDegreeBudget line 665
Source documentation
Full unabsorbed bound, now with no placeholder anchor-energy hypothesis.
```
def sourceDegreeBudget (T n : ℕ → ℕ) (s b r : ℕ) (ω η a : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.sourceDegreeBudget_nonneg line 670
theorem OAI.TraceReconstruction.source_canonical_degree_bound line 676
theorem OAI.TraceReconstruction.sourceFlatLeafType_window line 709
Source documentation
Pointwise equality of the literal source types and the signed tree types. This holds for every assignment, including overflowing windows.
```
theorem sourceFlatLeafType_window (T n : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (b : ℕ) (incoming : ℤ) (τ : Bool) (bits : Fin (SourceTrialCount T n b) → Bool) :
    sourceFlatLeafType T n s center b incoming τ bits =
      windowFinType T s (sourceTreeAnchors T n (sourceScheduledTrials T n) center
        (sourceScheduledShift T n) b ((sourceAssignmentCode T n Bool b).symm bits) incoming)
        b (boolTypeSign τ) := by
…
```
Mentions: OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.sourceFlatLeafType, OAI.TraceReconstruction.windowFinType, OAI.TraceReconstruction.sourceTreeAnchors, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceScheduledShift, OAI.TraceReconstruction.sourceAssignmentCode, OAI.TraceReconstruction.boolTypeSign
def OAI.TraceReconstruction.sourceSparseCount line 722
theorem OAI.TraceReconstruction.sourceFlatLeafType_sparse line 725
def OAI.TraceReconstruction.sourceOracleCoefficient line 731
theorem OAI.TraceReconstruction.sourceOracleCoefficient_empty line 737
theorem OAI.TraceReconstruction.sourceOracleCoefficient_degree line 741
def OAI.TraceReconstruction.sourceSignedCoefficient line 747
theorem OAI.TraceReconstruction.sourceSignedCoefficient_zero line 751
theorem OAI.TraceReconstruction.sourceSignedCoefficient_degree_geometric line 756
def OAI.TraceReconstruction.sourceEnergyBudget line 772
theorem OAI.TraceReconstruction.source_canonical_energy line 778
Source documentation
Complete signed energy, with finite low-degree forced-tree bound and the geometric high tail. No coefficient estimates remain as hypotheses.
```
theorem source_canonical_energy {Side : Type*} (T n : ℕ → ℕ) (hT : ∀j,0<T j)
    (s b R : ℕ) (ω η a w : ℝ) (ha : 0 ≤ a) (hw : 0 ≤ w)
    (hsmall : w^2*sourceSparseCount T s b<1)
    (hη : ∀j<b+1,hiddenSmoothingBound (n j) s ω ≤ η)
    (z : Reports Side (SourceTrialCount T n (b+1))) (hz : SourceTypical T n s b ω a z) :
    multilinearEnergy (sourceSignedCoefficient T n s b z) w ≤ sourceEnergyBudget T n s b R ω η a w := by
…
```
Mentions: OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenSmoothingBound, OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceTypical, OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.sourceSignedCoefficient, OAI.TraceReconstruction.sourceEnergyBudget
theorem OAI.TraceReconstruction.nonconstant_eq_degreeTail line 799
theorem OAI.TraceReconstruction.source_canonical_centered_energy line 811
Source documentation
The individual density is close to the pure reference without any metadata typicality assumption.
```
theorem source_canonical_centered_energy {Side : Type*} (T n : ℕ → ℕ) (s b : ℕ)
    (z : Reports Side (SourceTrialCount T n (b+1))) (τ : Bool) {w : ℝ} (hw : 0 ≤ w)
    (hsmall : w^2*sourceSparseCount T s b<1) :
    multilinearEnergy (nonconstantCoefficient (sourceOracleCoefficient T n s b z τ)) w ≤
      (w^2*sourceSparseCount T s b)/(1-w^2*sourceSparseCount T s b) := by
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.nonconstantCoefficient, OAI.TraceReconstruction.sourceOracleCoefficient
theorem OAI.TraceReconstruction.FiniteLaw.abs_expect_pow_le line 827
theorem OAI.TraceReconstruction.FiniteLaw.density_score_centered line 838

theorem OAI.TraceReconstruction.FiniteLaw.clipping_mass_difference line 847

Source documentation

Common-event mass difference is controlled by the restricted density difference at every moment, by finite Jensen rather than a pointwise bound.

theorem clipping_mass_difference (R : FiniteLaw α) (f g : α → ℝ)
    (hf : ∀a,0 ≤ f a) (hg : ∀a,0 ≤ g a) (hfm : R.expect f=1) (hgm : R.expect g=1)
    (A : Finset α) (t : ℕ) :
    |(R.withDensity f hf hfm).eventMass A-(R.withDensity g hg hgm).eventMass A|^t ≤
      R.expect (fun a => |if a∈A then g a-f a else 0|^t) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass

theorem OAI.TraceReconstruction.FiniteLaw.clipped_raw_moment_restricted line 861

theorem OAI.TraceReconstruction.FiniteLaw.clipped_score_moment line 883

Source documentation

Explicit normalized clipping, at half of any positive even moment. This constructs the actual conditioned score; no bounded-score hypothesis.

theorem clipped_score_moment (R : FiniteLaw α) (f g : α → ℝ)
    (hf : ∀a,0 ≤ f a) (hg : ∀a,0 ≤ g a) (hfm : R.expect f=1) (hgm : R.expect g=1)
    (A : Finset α) (hAf : ∀a∈A,1/2 ≤ f a)
    (hp : 1/2 ≤ (R.withDensity f hf hfm).eventMass A)
    (hq : 1/2 ≤ (R.withDensity g hg hgm).eventMass A)
    (k : ℕ) (hk : 1 ≤ k) (V : ℝ) (hV : 0 ≤ V)
    (hM : R.expect (fun a => |if a∈A then g a-f a else 0|^(2*k)) ≤ V^k) :
    let p := (R.withDensity f hf hfm).eventMass A
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass

theorem OAI.TraceReconstruction.FiniteLaw.eventMass_indicator line 960
theorem OAI.TraceReconstruction.FiniteLaw.eventMass_compl line 965
theorem OAI.TraceReconstruction.FiniteLaw.density_second_moment_le_six line 975

theorem OAI.TraceReconstruction.FiniteLaw.density_low_event_mass line 986

Source documentation

Cauchy--Schwarz loss on the actual low-reference-density event, for either density. The same clipping event is used for both hypotheses.

theorem density_low_event_mass (R : FiniteLaw α) (f g : α → ℝ)
    (hg : ∀a,0 ≤ g a) (hgm : R.expect g=1) (k : ℕ) (hk : 1 ≤ k) (U : ℝ)
    (hU : 0 ≤ U) (hU1 : U ≤ 1)
    (hfM : R.expect (fun a => |f a-1|^(2*k)) ≤ U^k)
    (hgM : R.expect (fun a => |g a-1|^(2*k)) ≤ U^k) :
    (R.withDensity g hg hgm).eventMass (Finset.univ.filter (fun a => f a<1/2)) ≤
      Real.sqrt (6*(4*U)^k) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass

def OAI.TraceReconstruction.FiniteLaw.commonClipEvent line 1008
theorem OAI.TraceReconstruction.FiniteLaw.commonClipEvent_loss line 1011

theorem OAI.TraceReconstruction.FiniteLaw.commonClipEvent_mass line 1023

Source documentation

Quantitative common clipping on any genuine good event. Both bad-event costs below are measured under the actual normalized laws, not reference mass.

theorem commonClipEvent_mass (R : FiniteLaw α) (f g : α → ℝ)
    (hf : ∀a,0 ≤ f a) (hg : ∀a,0 ≤ g a) (hfm : R.expect f=1) (hgm : R.expect g=1)
    (B : Finset α) (e : ℝ) (hfB : (R.withDensity f hf hfm).eventMass Bᶜ ≤ e)
    (hgB : (R.withDensity g hg hgm).eventMass Bᶜ ≤ e)
    (k : ℕ) (hk : 1 ≤ k) (U : ℝ) (hU : 0 ≤ U) (hU1 : U ≤ 1)
    (hfM : R.expect (fun a => |f a-1|^(2*k)) ≤ U^k)
    (hgM : R.expect (fun a => |g a-1|^(2*k)) ≤ U^k) :
    1-(R.withDensity f hf hfm).eventMass (commonClipEvent B f) ≤ e+Real.sqrt (6*(4*U)^k) ∧
    1-(R.withDensity g hg hgm).eventMass (commonClipEvent B f) ≤ e+Real.sqrt (6*(4*U)^k) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass, OAI.TraceReconstruction.FiniteLaw.commonClipEvent

structure OAI.TraceReconstruction.ClippedOracle line 1046
Source documentation
A pair produced by genuine common-event normalized conditioning. The outcome space and public decoder remain unchanged.
```
structure ClippedOracle {α : Type*} [Fintype α] (P Q : FiniteLaw α) (k : ℕ) (e V : ℝ) where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.FiniteLaw.exists_clippedOracle line 1060
def OAI.TraceReconstruction.sourceEffectiveHiddenTail line 1120
Source documentation
Exact finite-union metadata cost; it contains no postulated typical event and no independence assertion between different collections.
```
def sourceEffectiveHiddenTail (T n : ℕ → ℕ) (b : ℕ) (ω : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.source_hidden_conditions_effective_tail line 1123
theorem OAI.TraceReconstruction.source_typical_effective_failure line 1170
def OAI.TraceReconstruction.sourceOracleDensity line 1214
Source documentation
Literal density of the source's unconditioned finite canonical oracle.
```
def sourceOracleDensity {Side Leaf : Type*} (T n : ℕ → ℕ) (s b : ℕ)
    (Z : Leaf → ℝ) (τ : Bool)
    (zx : Reports Side (SourceTrialCount T n (b+1)) × (Fin (SourceLeafCount T (b+1)) → Leaf)) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceLeafCount
theorem OAI.TraceReconstruction.sourceOracleDensity_expansion line 1220
theorem OAI.TraceReconstruction.sourceOracleDensity_nonneg line 1226
theorem OAI.TraceReconstruction.sourceOracleDensity_mean line 1231
theorem OAI.TraceReconstruction.source_canonical_centered_moment line 1238
theorem OAI.TraceReconstruction.source_canonical_signed_moment line 1257
theorem OAI.TraceReconstruction.degreeForcedRoleEnergy_zero_of_lt line 1283
def OAI.TraceReconstruction.sourceSharpDegreeBudget line 1298
Source documentation
Below the genuine forced binary leaf threshold there is NO forced contribution; retaining even its coarse bound would lose the main exponent.
```
def sourceSharpDegreeBudget (T n : ℕ → ℕ) (s b r : ℕ) (ω η a : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.sourceSharpDegreeBudget_nonneg line 1303
theorem OAI.TraceReconstruction.source_canonical_sharp_degree_bound line 1309
def OAI.TraceReconstruction.sourceSharpEnergyBudget line 1335
theorem OAI.TraceReconstruction.source_canonical_sharp_energy line 1341
Source documentation
Complete signed energy, with finite low-degree forced-tree bound and the geometric high tail. No coefficient estimates remain as hypotheses.
```
theorem source_canonical_sharp_energy {Side : Type*} (T n : ℕ → ℕ) (hT : ∀j,0<T j)
    (s b R : ℕ) (ω η a w : ℝ) (ha : 0 ≤ a) (hw : 0 ≤ w)
    (hsmall : w^2*sourceSparseCount T s b<1)
    (hη : ∀j<b+1,hiddenSmoothingBound (n j) s ω ≤ η)
    (z : Reports Side (SourceTrialCount T n (b+1))) (hz : SourceTypical T n s b ω a z) :
    multilinearEnergy (sourceSignedCoefficient T n s b z) w ≤ sourceSharpEnergyBudget T n s b R ω η a w := by
…
```
Mentions: OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenSmoothingBound, OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceTypical, OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.sourceSignedCoefficient, OAI.TraceReconstruction.sourceSharpEnergyBudget
theorem OAI.TraceReconstruction.sourceSharpEnergyBudget_nonneg line 1362
theorem OAI.TraceReconstruction.source_canonical_sharp_signed_moment line 1384
def OAI.TraceReconstruction.sourceReferenceLaw line 1405
theorem OAI.TraceReconstruction.sourceOracleDensity_total line 1411
theorem OAI.TraceReconstruction.sourceOracle_withDensity line 1419
def OAI.TraceReconstruction.sourceTypicalSet line 1431
theorem OAI.TraceReconstruction.sourceTypicalSet_mass line 1436
def OAI.TraceReconstruction.sourceCenteredBudget line 1453
def OAI.TraceReconstruction.sourceClippingCost line 1457
theorem OAI.TraceReconstruction.sourceCenteredBudget_nonneg line 1461
theorem OAI.TraceReconstruction.sourceCenteredBudget_le_one line 1466
theorem OAI.TraceReconstruction.source_reference_centered_moment line 1473
theorem OAI.TraceReconstruction.source_reference_signed_moment line 1486
theorem OAI.TraceReconstruction.source_reference_clipped_exists line 1511

theorem OAI.TraceReconstruction.source_clippedOracle_exists line 1545

Source documentation

Complete finite quantitative clipping of the actual recursive source oracle. All analytic budgets here are explicit arithmetic in the literal branching/trial counts; no coefficient or oracle-existence premise remains.

theorem source_clippedOracle_exists {Side Leaf : Type*} [Fintype Side] [Fintype Leaf]
    (T n : ℕ → ℕ) (hTpos : ∀j,0<T j) (s b R k : ℕ)
    (M : PairedMechanisms Side (SourceTrialCount T n (b+1))) (P Q : FiniteLaw Leaf)
    (Z : Leaf → ℝ) (hden : ∀a,Q.mass a=P.mass a*(1+Z a)) (hZ : ∀a,0 ≤ 1+Z a)
    (ω a η L : ℝ) (ha : 0<a) (hL : 0<L)
    (hw : ∀i,M.hiddenWeight i=ω) (hp : ω^2∈Set.Icc 0 1)
    (hn : ∀j,j<b → 0<n j) (hne : ∀j,j<b → Even (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) (hk : 1 ≤ k)
    (hMoment : P.expect (fun a => |Z a|^(2*k)) ≤ L^(2*k))
    (hscale : ((6*(2*k:ℕ):ℝ)*L)^2*sourceSparseCount T s b ≤ 1/2)
    (hη : ∀j<b+1,hiddenSmoothingBound (n j) s ω ≤ η)
…

Mentions: OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.sourceSparseCount, OAI.TraceReconstruction.hiddenSmoothingBound

def OAI.TraceReconstruction.ClippedOracle.prod line 1585
theorem OAI.TraceReconstruction.ApproximatesTrace.of_tv line 1607
structure OAI.TraceReconstruction.OracleTracePair line 1618
Source documentation
A finite genuine approximate oracle pair with a common complete-trace decoder. It does not include an overlap or any unproved scale conclusion.
```
structure OracleTracePair (q : ℝ) (x y : List Bool) (k : ℕ) (E V : ℝ) where
…
```

theorem OAI.TraceReconstruction.source_clipped_simulation line 1634

Source documentation

The clipping and independent filler metadata preserve the source's fixed public trace decoder.

theorem source_clipped_simulation {Side Leaf : Type} [Fintype Side] [Fintype Leaf]
    {q E e V : ℝ} (hq : q∈Set.Icc 0 1) (hE : 0≤E)
    (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b k : ℕ)
    (H : SourceLayoutMargins s P T n h b)
    (hP : P b=n b*(2*h b+1)+T b) (hT : Even (T b))
    (hlarge : 4*(n b+1)≤T b) (hmotif : 8*2^s≤T b)
    (hn : ∀j<b,0<n j)
    (M : PairedMechanisms Side (SourceTrialCount T n (b+1)))
    (R : Fin (SourceFillerCount T (b+1)) → FiniteLaw Side) (A B : FiniteLaw Leaf)
    (f : Side → List Bool) (g : Leaf → List Bool)
    (hU : ∀j,SimulatesTrace q (M.first j) f (sourceFlatTrialWord s P T n h atom (b+1) false j))
    (hV : ∀j,SimulatesTrace q (M.second j) f (sourceFlatTrialWord s P T n h atom (b+1) true j))
…

Mentions: OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceFillerCount, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.SimulatesTrace, OAI.TraceReconstruction.sourceFlatTrialWord

theorem OAI.TraceReconstruction.FiniteLaw.expect_nonneg line 1683
theorem OAI.TraceReconstruction.FiniteLaw.evenMomentSq_nonneg line 1686
theorem OAI.TraceReconstruction.FiniteLaw.evenMomentSq_pow line 1689
theorem OAI.TraceReconstruction.FiniteLaw.expect_even_pow_le_of_moment line 1694
theorem OAI.TraceReconstruction.FiniteLaw.secondMoment_le_evenMomentSq line 1700
theorem OAI.TraceReconstruction.FiniteLaw.affinity_coordinateProduct line 1709
theorem OAI.TraceReconstruction.FiniteLaw.one_sub_prod_le_sum line 1721
theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_coordinateProduct_le line 1735
theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_self line 1746
theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_symm line 1749
theorem OAI.TraceReconstruction.FiniteLaw.tv_mixedProduct_le line 1755
Source documentation
Only differing coordinates cost squared Hellinger distance. This estimate does not pay for pure filler coordinates, nor assume independence of traces after their common concatenating decoder.
```
theorem tv_mixedProduct_le {n : ℕ} (P Q : FiniteLaw α) (Z : α → ℝ)
    (hden : ∀a,Q.mass a=P.mass a*(1+Z a)) (k : ℕ) (hk : 1≤k)
    {V : ℝ} (hM : P.evenMomentSq Z k≤V) (τ σ : Fin n → Bool) :
    (coordinateProduct (fun i => if τ i then Q else P)).tv
      (coordinateProduct (fun i => if σ i then Q else P))≤
        Real.sqrt ((∑i,if τ i=σ i then (0:ℝ) else 1)*V) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.tv

theorem OAI.TraceReconstruction.actual_source_oracle line 1784

Source documentation

Literal recursive source oracle with actual complete-trace side laws. All remaining hypotheses here are explicit parameter inequalities, the old leaf oracle, and its genuine repeated-word overlap invariant.

theorem actual_source_oracle {Leaf : Type} [Fintype Leaf]
    {q E : ℝ} (hq : q∈Set.Icc 0 1) (hE : 0≤E)
    (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b R k : ℕ)
    (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 B : FiniteLaw Leaf) (g : Leaf → List Bool) (Z : Leaf → ℝ)
    (hden : ∀a,B.mass a=A.mass a*(1+Z a)) (hZ : ∀a,0≤1+Z a)
    (hA : ApproximatesTrace q A g (atom false) E) (hB : ApproximatesTrace q B g (atom true) E)
    (ω a η L : ℝ) (ha : 0<a) (hL : 0<L) (hω : ω∈Set.Ioo 0 1)
    (hov : ∀j<b+1,ω≤listTraceOverlap q hq
…

Mentions: OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ApproximatesTrace, OAI.TraceReconstruction.listTraceOverlap