Metadata.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Metadata

Hidden metadata, fair jitter, heterogeneous emissions, independent window trials, concentration, and fit.

theorem OAI.TraceReconstruction.FiniteLaw.pairedReportMass_none line 25
theorem OAI.TraceReconstruction.FiniteLaw.pairedReport_hidden_expect line 30

theorem OAI.TraceReconstruction.FiniteLaw.pairedReport_hidden_mgf line 50

Source documentation

Centered hidden-flag MGF, derived from the literal paired experiment.

theorem pairedReport_hidden_mgf (P Q H : FiniteLaw α) {ω t : ℝ} (hω : 0≤ω)
    (hP : ∀a,ω*H.mass a≤P.mass a) (hQ : ∀a,ω*H.mass a≤Q.mass a)
    (hp : ω^2∈Set.Icc 0 1) (ht : |t|≤1) :
    (pairedReport P Q H hω hP hQ).expect (fun z =>
      Real.exp (t*((hiddenTrial z.1:ℕ)-ω^2)))≤Real.exp (t^2) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedReport, OAI.TraceReconstruction.FiniteLaw.expect, OAI.TraceReconstruction.hiddenTrial

def OAI.TraceReconstruction.PairedMechanisms.hiddenCount line 65
theorem OAI.TraceReconstruction.PairedMechanisms.hiddenCount_mgf line 69
Source documentation
No independence of displacements is presumed: only the flags of the distinct literal paired mechanisms are independent.
```
theorem hiddenCount_mgf {ω t : ℝ} (hw : ∀i,M.hiddenWeight i=ω)
    (hp : ω^2∈Set.Icc 0 1) (ht : |t|≤1) :
    M.reports.expect (fun z => Real.exp (t*((hiddenCount z:ℕ)-(m:ℝ)*ω^2)))≤
      Real.exp ((m:ℝ)*t^2) := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.hiddenCount
theorem OAI.TraceReconstruction.PairedMechanisms.hiddenCount_small line 99
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 hiddenCount_small {ω : ℝ} (hw : ∀i,M.hiddenWeight i=ω) (hp : ω^2∈Set.Icc 0 1) :
    M.reports.expect (fun z => if (hiddenCount z:ℝ)<(m:ℝ)*ω^2/2 then 1 else 0)≤
      Real.exp (-(m:ℝ)*ω^4/16) := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.hiddenCount
theorem OAI.TraceReconstruction.PairedMechanisms.posterior_average line 125
Source documentation
Exact Bayes averaging under all metadata, including impossible reports.
```
theorem posterior_average (F : (Fin m → Bool) → ℝ) :
    M.reports.expect (fun z => (orientationsGiven z).expect F)=
      (fairOrientations m).expect F := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.orientationsGiven, OAI.TraceReconstruction.PairedMechanisms.fairOrientations
theorem OAI.TraceReconstruction.PairedMechanisms.posterior_bad_mass line 145
Source documentation
Markov's inequality for the actual conditional failure probability. This does not condition any orientation averages on fitting paths.
```
theorem posterior_bad_mass {a : ℝ} (_ha : 0<a) (bad : (Fin m → Bool) → Prop)
    [DecidablePred bad] :
    a*M.reports.expect (fun z => if a≤(orientationsGiven z).expect (fun b => if bad b then 1 else 0)
      then 1 else 0) ≤ (fairOrientations m).expect (fun b => if bad b then 1 else 0) := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.orientationsGiven, OAI.TraceReconstruction.PairedMechanisms.fairOrientations
theorem OAI.TraceReconstruction.FiniteLaw.indexedProduct_expect_product line 168
def OAI.TraceReconstruction.fairField line 176
Source documentation
The unconditional orientation distribution on any actual finite trial ID set.
```
def fairField (ι : Type*) [Fintype ι] : FiniteLaw (ι → Bool) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.fairLinearSum line 179
theorem OAI.TraceReconstruction.fairBit_mgf line 183
Source documentation
Exact MGF calculation for each paired orientation bit.
```
theorem fairBit_mgf (t : ℝ) :
    (FiniteLaw.flagPosterior none).expect (fun b => Real.exp (t*((bitIndex b:ℝ)-1/2)))=
      Real.cosh (t/2) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw.flagPosterior, OAI.TraceReconstruction.bitIndex
theorem OAI.TraceReconstruction.fairLinearSum_mgf line 193
Source documentation
Hoeffding's exponential estimate for the actual independently fair bits, allowing deterministic zero coefficients for completed/nonactive global pairs.
```
theorem fairLinearSum_mgf {ι : Type*} [Fintype ι] (c : ι → ℝ) (t : ℝ) :
    (fairField ι).expect (fun bits => Real.exp (t*fairLinearSum c bits))≤
      Real.exp ((∑i,(c i)^2)*t^2/8) := by
…
```
Mentions: OAI.TraceReconstruction.fairField, OAI.TraceReconstruction.fairLinearSum
theorem OAI.TraceReconstruction.fairLinearSum_mgf_card line 221

theorem OAI.TraceReconstruction.fairLinearSum_tail_variance line 238

Source documentation

Two-sided finite Hoeffding bound with the source's sharp quadratic scale.

theorem fairLinearSum_tail_variance {ι : Type*} [Fintype ι] (c : ι → ℝ)
    {V : ℝ} (hV : 0<V) (hc : (∑i,(c i)^2)≤V) {a : ℝ} (ha : 0≤a) :
    (fairField ι).expect (fun bits => if a≤|fairLinearSum c bits| then 1 else 0)≤
      2*Real.exp (-2*a^2/V) := by
…

Mentions: OAI.TraceReconstruction.fairField, OAI.TraceReconstruction.fairLinearSum

theorem OAI.TraceReconstruction.fairLinearSum_tail line 289

Source documentation

Cardinal specialization, without imposing any extra computation limits.

theorem fairLinearSum_tail {ι : Type*} [Fintype ι] (c : ι → ℝ)
    (hc : ∀i,|c i|≤1) (hn : 0<Fintype.card ι) {a : ℝ} (ha : 0≤a) :
    (fairField ι).expect (fun bits => if a≤|fairLinearSum c bits| then 1 else 0)≤
      2*Real.exp (-2*a^2/(Fintype.card ι:ℝ)) := by
…

Mentions: OAI.TraceReconstruction.fairField, OAI.TraceReconstruction.fairLinearSum

def OAI.TraceReconstruction.FiniteLaw.dependentProduct line 313
Source documentation
Independent observations at literal slot IDs, allowing different outcome types (side traces and old leaf oracles carry genuinely different data).
```
def dependentProduct (P : ∀i,FiniteLaw (A i)) : FiniteLaw (∀i,A i) where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.FiniteLaw.dependentProduct_expect_product line 318
theorem OAI.TraceReconstruction.FiniteLaw.expect_dependentProduct_succ line 323
theorem OAI.TraceReconstruction.FiniteLaw.dependentProduct_expect_equiv line 334
Source documentation
A genuine dependent Pi-law is invariant under a fixed bijective relabeling of slots. No observation is duplicated and no random order is transmitted.
```
theorem dependentProduct_expect_equiv {κ : Type*} [Fintype κ] [DecidableEq κ] (P : ∀i,FiniteLaw (A i))
    (e : κ ≃ ι) (F : (∀i,A i) → ℝ) :
    (dependentProduct P).expect F=(dependentProduct (fun j => P (e j))).expect
      (fun x => F (fun i => cast (congrArg A (e.apply_symm_apply i)) (x (e.symm i)))) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.dependentProduct, OAI.TraceReconstruction.FiniteLaw.expect

theorem OAI.TraceReconstruction.dependentCoordinate_approximates line 362

Source documentation

Independent heterogeneous emissions in a literal finite chronological order accumulate precisely the sum of their trace approximation costs.

theorem dependentCoordinate_approximates {n : ℕ} {A : Fin n → Type*}
    [∀i,Fintype (A i)] {q : ℝ} (hq : q∈Set.Icc 0 1)
    (P : ∀i,FiniteLaw (A i)) (f : ∀i,A i → List Bool)
    (w : Fin n → List Bool) (E : Fin n → ℝ)
    (h : ∀i,ApproximatesTrace q (P i) (f i) (w i) (E i)) :
    ApproximatesTrace q (FiniteLaw.dependentProduct P)
      (fun x => coordinateWord (fun i => f i (x i))) (coordinateWord w) (∑i,E i) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ApproximatesTrace, OAI.TraceReconstruction.FiniteLaw.dependentProduct, OAI.TraceReconstruction.coordinateWord

def OAI.TraceReconstruction.WindowTrial line 397

Source documentation

Actual IDs of every local or global paired trial on the whole window tree.

def WindowTrial (T n g : ℕ → ℕ) : ℕ → Type
  | 0 => PEmpty
  | b+1 => Fin (n b) ⊕ (Fin (g b) ⊕ (Fin (T b) × WindowTrial T n g b))

instance OAI.TraceReconstruction.windowTrialFintype line 401
def OAI.TraceReconstruction.windowAssignmentEquiv line 409
Source documentation
A fixed bijection, independent of every bit, reveal and hypothesis.
```
def windowAssignmentEquiv (T n g : ℕ → ℕ) (A : Type) :
    (b : ℕ) → WindowAssignments T n g A b ≃ (WindowTrial T n g b → A)
  | 0 =>
    { toFun := fun _ i => PEmpty.elim i
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowTrial
theorem OAI.TraceReconstruction.windowPosterior_mass_flat line 438
theorem OAI.TraceReconstruction.windowPosterior_expect_flat line 466
Source documentation
Exact flat posterior distribution, including all paths and zero-mass metadata. This is the same independent bit law, not a new assumption.
```
theorem windowPosterior_expect_flat (T n g : ℕ → ℕ) (b : ℕ)
    (d : WindowAssignments T n g (Option Bool) b)
    (F : WindowAssignments T n g Bool b → ℝ) :
    (windowPosteriorLaw T n g b d).expect F=
      (FiniteLaw.indexedProduct (fun i : WindowTrial T n g b => FiniteLaw.flagPosterior
        (windowAssignmentEquiv T n g (Option Bool) b d i))).expect
          (fun bits => F ((windowAssignmentEquiv T n g Bool b).symm bits)) := by
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.FiniteLaw.indexedProduct, OAI.TraceReconstruction.WindowTrial, OAI.TraceReconstruction.FiniteLaw.flagPosterior, OAI.TraceReconstruction.windowAssignmentEquiv
def OAI.TraceReconstruction.noReveals line 480
theorem OAI.TraceReconstruction.windowPosterior_fair_flat line 483
def OAI.TraceReconstruction.globalTrialEquiv line 499
Source documentation
The literal global schedule is indexed by a fixed pair/block bijection.
```
def globalTrialEquiv (N t : ℕ) : (Fin (N/4) × Fin t) ≃ Fin ((N/4)*t) :=
…
```
def OAI.TraceReconstruction.sourceGlobalCoefficient line 502
def OAI.TraceReconstruction.sourceGroupCoefficient line 506
theorem OAI.TraceReconstruction.even_half_cast line 513
theorem OAI.TraceReconstruction.scheduledGlobalShift_linear line 518
theorem OAI.TraceReconstruction.sourceDisplacement_linear line 536
theorem OAI.TraceReconstruction.sourceGroupCoefficient_variance line 575

theorem OAI.TraceReconstruction.sourceDisplacement_tail line 602

Source documentation

Actual per-window unconditional fit tail under the full tree's fair law. No independence between different window displacements is asserted.

theorem sourceDisplacement_tail (T n : ℕ → ℕ) (b : ℕ) (ht : Even (n b))
    (hn : 0<n b) (u : Fin (T (b+1))) {a : ℝ} (ha : 0≤a) :
    (windowPosteriorLaw T n (sourceScheduledTrials T n) (b+2)
      (noReveals T n (sourceScheduledTrials T n) (b+2))).expect
      (fun bits => if a≤|(sourceDisplacement (T (b+1)) (n b)
        (fun v => (bits.2.2 v).1) bits.2.1 u:ℝ)| then 1 else 0)≤
      2*Real.exp (-2*a^2/(((T (b+1):ℝ)+1)*(n b:ℝ))) := by
…

Mentions: OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.noReveals, OAI.TraceReconstruction.sourceDisplacement

theorem OAI.TraceReconstruction.FiniteLaw.expect_fintype_sum line 623
theorem OAI.TraceReconstruction.FiniteLaw.expect_add line 628
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_eval line 632
theorem OAI.TraceReconstruction.noReveals_succ line 646
theorem OAI.TraceReconstruction.windowPosterior_child line 649
theorem OAI.TraceReconstruction.failure_forall_le_sum line 661
def OAI.TraceReconstruction.sourceFitTail line 678
Source documentation
Explicit finite tree union bound. The source's scale estimates will make this number exponentially small; no independence of sibling shifts is used.
```
def sourceFitTail (T n : ℕ → ℕ) : ℕ → ℝ
  | 0 => 0
  | 1 => 0
  | b+2 => (T (b+1):ℝ)*(2*Real.exp (-2*((T b:ℝ)/8)^2/(((T (b+1):ℝ)+1)*(n b:ℝ)))+
      sourceFitTail T n (b+1))
```
theorem OAI.TraceReconstruction.sourceTreeFit_tail line 684