LeafOracle.lean`

101 declarations, 0 contain sorry, 0 declared as axioms

LeafOracle

Recursive leaf oracles, sparse high tails, occupied shapes, posterior smoothing, source bit trees, and singleton cancellation.

def OAI.TraceReconstruction.WindowLeaf line 25
Source documentation
Complete window-tree leaf indices, with counts numbered from the bottom. The tree is fixed before any occupied subset or orientation is selected.
```
def WindowLeaf (T : ℕ → ℕ) : ℕ → Type
  | 0 => Fin 1
  | b+1 => Fin (T b) × WindowLeaf T b
```
instance OAI.TraceReconstruction.windowLeafFintype line 29
def OAI.TraceReconstruction.motifChildSign line 36
Source documentation
A motif's actual outgoing type, allowing every integer displacement.
```
def motifChildSign (s : ℕ) (X : ℤ) (h : ℕ) (τ : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.motifChildSign_isSign line 39
theorem OAI.TraceReconstruction.motifChildSign_negative_active line 43
def OAI.TraceReconstruction.windowLeafSign line 53
Source documentation
Literal top-down type recursion in the source's unconditioned surrogate. X path is the root anchor or w_j-Y_path. Dependence of different paths through the same global jitter is retained by this single full-tree map.
```
def windowLeafSign (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ) :
    (b : ℕ) → List ℕ → ℝ → WindowLeaf T b → ℝ
  | 0, _, τ, _ => τ
  | b+1, path, τ, v => windowLeafSign T s X b (path++[v.1.val])
      (motifChildSign s (X path) v.1.val τ) v.2
```
Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.motifChildSign
theorem OAI.TraceReconstruction.windowLeafSign_isSign line 59
def OAI.TraceReconstruction.windowLeafType line 66
theorem OAI.TraceReconstruction.windowLeafType_weight line 70
def OAI.TraceReconstruction.windowFinType line 79
Source documentation
A finite indexing of all leaves, not just the active or fitted leaves.
```
def windowFinType (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (τ : ℝ) (i : Fin (Fintype.card (WindowLeaf T b))) : Bool :=
…
```
Mentions: OAI.TraceReconstruction.WindowLeaf
def OAI.TraceReconstruction.recursiveLeafLaw line 85
Source documentation
The actual mixed leaf oracle at arbitrary exact metadata. The one latent law governs the whole map X; no independent-anchor law is substituted.
```
def recursiveLeafLaw {Ω α : Type*} [Fintype Ω] [Fintype α]
    (R : FiniteLaw Ω) (X : Ω → List ℕ → ℤ) (T : ℕ → ℕ) (s b : ℕ)
    (P Q : FiniteLaw α) (τ : ℝ) :
    FiniteLaw (Fin (Fintype.card (WindowLeaf T b)) → α) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.WindowLeaf
theorem OAI.TraceReconstruction.recursiveLeafLaw_density line 91

theorem OAI.TraceReconstruction.recursive_selectionCoefficient line 102

Source documentation

Pointwise recursive coefficient before averaging over the actual bits.

theorem recursive_selectionCoefficient {Ω : Type*} [Fintype Ω]
    (X : Ω → List ℕ → ℤ) (T : ℕ → ℕ) (s b : ℕ) (ω : Ω)
    {τ : ℝ} (hτ : IsTypeSign τ) (σ : Fin (Fintype.card (WindowLeaf T b)) → Bool) :
    selectionCoefficient (windowFinType T s (X ω) b τ) σ =
      ∏i, if σ i then
        (1-windowLeafSign T s (X ω) b [] τ ((Fintype.equivFin (WindowLeaf T b)).symm i))/2 else 1 := by
…

Mentions: OAI.TraceReconstruction.IsTypeSign, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.selectionCoefficient, OAI.TraceReconstruction.windowFinType, OAI.TraceReconstruction.windowLeafSign

theorem OAI.TraceReconstruction.motif_negative_count line 115
def OAI.TraceReconstruction.windowMinusCount line 134
Source documentation
Exact number of minus leaves in a fixed realization, without a fit condition.
```
def windowMinusCount (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (τ : ℝ) : ℕ :=
…
```
theorem OAI.TraceReconstruction.windowMinusCount_succ line 138
theorem OAI.TraceReconstruction.windowMinusCount_bound line 150
Source documentation
Source the block layout high-degree budget, bottom motif length times all upper window counts. It holds for every latent realization, typical or not.
```
theorem windowMinusCount_bound (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (τ : ℝ) :
    windowMinusCount T s X (b+1) path τ ≤
      2^s * ∏j∈Finset.range b, T (j+1) := by
…
```
Mentions: OAI.TraceReconstruction.windowMinusCount
def OAI.TraceReconstruction.boolSupport line 176
theorem OAI.TraceReconstruction.boolSupport_injective line 179
theorem OAI.TraceReconstruction.selectionCoefficient_eq_support line 186
theorem OAI.TraceReconstruction.selection_degree_sum_le line 205
Source documentation
Uniform cardinality bound for the actual selected monomials of a sparse 0/1 coefficient vector; mixing does not add a squared-cardinality loss.
```
theorem selection_degree_sum_le {n : ℕ} (θ : Fin n → Bool) (r : ℕ) :
    (∑σ : Fin n → Bool, if monomialDegree σ=r then selectionCoefficient θ σ else 0) ≤
      ((monomialDegree θ).choose r:ℝ) := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.selectionCoefficient
theorem OAI.TraceReconstruction.averaged_sparse_degree line 225
theorem OAI.TraceReconstruction.windowFinType_degree line 257
Source documentation
Genuine sparse complete-tree leaf count in the exact Fin indexing used by the independent-product reference law.
```
theorem windowFinType_degree (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (τ : ℝ) :
    monomialDegree (windowFinType T s X b τ) = windowMinusCount T s X b [] τ := by
…
```
Mentions: OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.windowFinType, OAI.TraceReconstruction.windowMinusCount
theorem OAI.TraceReconstruction.recursive_degree_bound line 265
def OAI.TraceReconstruction.degreeTail line 275
theorem OAI.TraceReconstruction.degreeTail_degree line 278
theorem OAI.TraceReconstruction.averaged_sparse_tail_energy line 292
Source documentation
Geometric high-degree energy of an actual mixed sparse leaf law.
```
theorem averaged_sparse_tail_energy {Ω : Type*} [Fintype Ω] {n A₀ : ℕ}
    (R : FiniteLaw Ω) (θ : Ω → Fin n → Bool)
    (hA : ∀ω, monomialDegree (θ ω) ≤ A₀) (k : ℕ) {w : ℝ}
    (hw : 0 ≤ w) (ha : w^2*A₀ < 1) :
    multilinearEnergy (degreeTail (averagedCoefficient R θ) k) w ≤
      (w^2*A₀)^k/(1-w^2*A₀) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.monomialDegree, OAI.TraceReconstruction.multilinearEnergy, OAI.TraceReconstruction.degreeTail, OAI.TraceReconstruction.averagedCoefficient

theorem OAI.TraceReconstruction.recursive_high_moment line 315

Source documentation

Actual recursive-oracle high tail, including arbitrary correlated latent bits and displacements. This supplies the block layout's unconditioned high-degree input; low degrees still require the signed occupied-tree cancellation.

theorem recursive_high_moment {Ω α : Type*} [Fintype Ω] [Fintype α]
    (R : FiniteLaw Ω) (X : Ω → List ℕ → ℤ) (T : ℕ → ℕ) (s b r₀ k : ℕ) (τ : ℝ)
    (P : FiniteLaw α) (Z : α → ℝ) (hk : 1 ≤ k) (hcenter : P.expect Z=0)
    {L : ℝ} (hL : 0 < L) (hMoment : P.expect (fun a => |Z a|^(2*k)) ≤ L^(2*k))
    (ha : ((6*(2*k:ℕ):ℝ)*L)^2 * (2^s*∏j∈Finset.range b,T (j+1):ℕ) < 1) :
    (P.product (Fintype.card (WindowLeaf T (b+1)))).evenMomentSq
      (multilinear (degreeTail (averagedCoefficient R
        (fun ω => windowFinType T s (X ω) (b+1) τ)) r₀) Z) k ≤
      (((6*(2*k:ℕ):ℝ)*L)^2*(2^s*∏j∈Finset.range b,T (j+1):ℕ))^r₀/
        (1-((6*(2*k:ℕ):ℝ)*L)^2*(2^s*∏j∈Finset.range b,T (j+1):ℕ)) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.multilinear, OAI.TraceReconstruction.degreeTail, OAI.TraceReconstruction.averagedCoefficient, OAI.TraceReconstruction.windowFinType

def OAI.TraceReconstruction.selectedChildren line 339
def OAI.TraceReconstruction.selectedChildLeaves line 342
theorem OAI.TraceReconstruction.selected_prod_children line 347
theorem OAI.TraceReconstruction.selected_prod_index line 365

def OAI.TraceReconstruction.occupiedWindowShape line 374

Source documentation

Occupied shape of an actual subset of a complete window tree. Only occupied children are enumerated, so its leaves are exactly the selected monomial variables, not the other complete-tree leaves.

def occupiedWindowShape (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ) :
    (b : ℕ) → (path : List ℕ) → Finset (WindowLeaf T (b+1)) → CoefficientShape b
  | 0, path, S => .bottom S.card
      (fun i => motifIndicator s (((S.equivFin.symm i).val.1.val:ℤ)-X path))
      (fun i => (prouhetSeries s).coeff (((S.equivFin.symm i).val.1.val:ℤ)-X path))
  | b+1, path, S => .node (selectedChildren S).card
      (fun i => motifIndicator s ((((selectedChildren S).equivFin.symm i).val.val:ℤ)-X path))
      (fun i => (prouhetSeries s).coeff ((((selectedChildren S).equivFin.symm i).val.val:ℤ)-X path))
      (fun i => occupiedWindowShape T s X b
        (path++[((selectedChildren S).equivFin.symm i).val.val])
        (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val))

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.CoefficientShape, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.selectedChildren, OAI.TraceReconstruction.selectedChildLeaves

theorem OAI.TraceReconstruction.occupiedWindowShape_admissible line 386
theorem OAI.TraceReconstruction.occupiedWindowShape_eval line 395
Source documentation
The literal coefficient product equals the evaluation of its occupied shape; this is before any averaging or parity cancellation.
```
theorem occupiedWindowShape_eval (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (S : Finset (WindowLeaf T (b+1))) (τ : ℝ) :
    (occupiedWindowShape T s X b path S).eval τ =
      ∏v∈S, (1-windowLeafSign T s X (b+1) path τ v)/2 := by
…
```
Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.occupiedWindowShape, OAI.TraceReconstruction.windowLeafSign
theorem OAI.TraceReconstruction.selected_children_card line 419
theorem OAI.TraceReconstruction.selectedChildLeaves_nonempty line 425
theorem OAI.TraceReconstruction.occupiedWindowShape_leafCount line 431
theorem OAI.TraceReconstruction.occupiedWindowShape_occupied line 443

theorem OAI.TraceReconstruction.occupiedWindowShape_forced_count line 455

Source documentation

Forced-leaf count for a term of an actual selected monomial.

theorem occupiedWindowShape_forced_count (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (S : Finset (WindowLeaf T (b+1)))
    (a : (occupiedWindowShape T s X b path S).Choice)
    (hw : (occupiedWindowShape T s X b path S).weight a ≠ 0)
    (ho : ((occupiedWindowShape T s X b path S).termTree a).isOdd)
    (hn : ((occupiedWindowShape T s X b path S).termTree a).noSingleton) :
    2^(b+1) ≤ S.card := by
…

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.occupiedWindowShape

def OAI.TraceReconstruction.OccupiedWindowChoice line 467
Source documentation
The role choices depend only on the selected subset, not on any hidden orientation. This common index type permits averaging before norm estimates.
```
def OccupiedWindowChoice (T : ℕ → ℕ) :
    (b : ℕ) → Finset (WindowLeaf T (b+1)) → Type
  | 0, S => Fin S.card → Fin 3
  | b+1, S =>
      ((i : Fin (selectedChildren S).card) → OccupiedWindowChoice T b
        (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val)) ×
      (Fin (selectedChildren S).card → Fin 3)
```
Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.selectedChildren, OAI.TraceReconstruction.selectedChildLeaves
instance OAI.TraceReconstruction.occupiedWindowChoiceFintype line 475
def OAI.TraceReconstruction.occupiedWindowChoiceEquiv line 485

def OAI.TraceReconstruction.occupiedWindowTerm line 496

Source documentation

The parity tree of a role choice is independent of all displacement bits.

noncomputable def occupiedWindowTerm (T : ℕ → ℕ) :
    (b : ℕ) → (S : Finset (WindowLeaf T (b+1))) →
      OccupiedWindowChoice T b S → OccupiedParityTree (b+1)
  | 0, S, a => .node S.card (fun _ => .leaf) a
  | b+1, S, a => .node (selectedChildren S).card
      (fun i => occupiedWindowTerm T b
        (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val) (a.1 i)) a.2

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.selectedChildren, OAI.TraceReconstruction.selectedChildLeaves

theorem OAI.TraceReconstruction.occupiedWindowTerm_eq line 504
def OAI.TraceReconstruction.occupiedWindowWeight line 517
theorem OAI.TraceReconstruction.occupiedWindow_difference line 525
Source documentation
Exact source parity formula for the actual selected leaves, using a single role index independent of the latent map. No fit conditioning.
```
theorem occupiedWindow_difference (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (S : Finset (WindowLeaf T (b+1))) :
    (∏v∈S, (1-windowLeafSign T s X (b+1) path 1 v)/2) -
      (∏v∈S, (1-windowLeafSign T s X (b+1) path (-1) v)/2) =
      2*∑a : OccupiedWindowChoice T b S,
        if (occupiedWindowTerm T b S a).isOdd then occupiedWindowWeight T s X b path S a else 0 := by
…
```
Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.windowLeafSign, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.occupiedWindowWeight

theorem OAI.TraceReconstruction.occupiedWindow_averaged_difference line 542

Source documentation

Averaging the complete exact expansion keeps all correlations of the common hidden map. The indicator of an odd root is deterministic.

theorem occupiedWindow_averaged_difference {Ω : Type*} [Fintype Ω]
    (R : FiniteLaw Ω) (T : ℕ → ℕ) (s : ℕ) (X : Ω → List ℕ → ℤ)
    (b : ℕ) (path : List ℕ) (S : Finset (WindowLeaf T (b+1))) :
    R.expect (fun ω => ∏v∈S, (1-windowLeafSign T s (X ω) (b+1) path 1 v)/2) -
      R.expect (fun ω => ∏v∈S, (1-windowLeafSign T s (X ω) (b+1) path (-1) v)/2) =
      2*∑a : OccupiedWindowChoice T b S,
        if (occupiedWindowTerm T b S a).isOdd then
          R.expect (fun ω => occupiedWindowWeight T s (X ω) b path S a) else 0 := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.windowLeafSign, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.occupiedWindowWeight

theorem OAI.TraceReconstruction.posterior_count_average line 571

Source documentation

Arbitrary functions of the actual posterior count have the translated fair-binomial law, not only its generating polynomial.

theorem posterior_count_average {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (F : ℤ → ℝ) :
    (∑ b : ι → Bool, (∏i, (flagPosterior (d i)).mass (b i)) *
      F (∑i, (bitIndex (b i):ℤ))) =
    ∑k∈Finset.range ((∑i, hiddenTrial (d i))+1),
      fairBinomial (∑i, hiddenTrial (d i)) k * F ((∑i,(visibleOnes (d i):ℤ))+k) := by
…

Mentions: OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.hiddenTrial, OAI.TraceReconstruction.fairBinomial, OAI.TraceReconstruction.visibleOnes

theorem OAI.TraceReconstruction.fairBinomial_reflect line 585

theorem OAI.TraceReconstruction.posterior_count_average_reflected line 591

Source documentation

Reflection of the remaining hidden count. The known visible contribution is kept, and no positivity assumption on the metadata mass is needed.

theorem posterior_count_average_reflected {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (F : ℤ → ℝ) :
    (∑ b : ι → Bool, (∏i, (flagPosterior (d i)).mass (b i)) *
      F (∑i, (bitIndex (b i):ℤ))) =
    ∑k∈Finset.range ((∑i, hiddenTrial (d i))+1),
      fairBinomial (∑i, hiddenTrial (d i)) k *
        F ((∑i,(visibleOnes (d i):ℤ))+(∑i,hiddenTrial (d i))-k) := by
…

Mentions: OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.hiddenTrial, OAI.TraceReconstruction.fairBinomial, OAI.TraceReconstruction.visibleOnes

theorem OAI.TraceReconstruction.posterior_signed_motif line 609
Source documentation
The actual local signed motif averaged over posterior orientations is exactly a translated smoothed Prouhet polynomial.
```
theorem posterior_signed_motif {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (s : ℕ) (z : ℤ) :
    (∑b : ι → Bool, (∏i,(flagPosterior (d i)).mass (b i)) *
      (prouhetSeries s).coeff (z+∑i,(bitIndex (b i):ℤ))) =
      (prouhetSeries s * fairSeries (∑i,hiddenTrial (d i))).coeff
        (z+(∑i,(visibleOnes (d i):ℤ))+(∑i,hiddenTrial (d i))) := by
…
```
Mentions: OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.hiddenTrial, OAI.TraceReconstruction.visibleOnes

theorem OAI.TraceReconstruction.posterior_signed_motif_bound line 627

Source documentation

Singleton smoothing for literal hidden orientation bits. Other mechanisms can now be conditioned on without changing this bound.

theorem posterior_signed_motif_bound {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (s : ℕ) (z : ℤ) :
    |∑b : ι → Bool, (∏i,(flagPosterior (d i)).mass (b i)) *
      (prouhetSeries s).coeff (z+∑i,(bitIndex (b i):ℤ))| ≤
      (2:ℝ)^(s*s)*((2*binomialBound ((∑i,hiddenTrial (d i))/(s+1)))^s *
        binomialBound ((∑i,hiddenTrial (d i))/(s+1))) := by
…

Mentions: OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.binomialBound, OAI.TraceReconstruction.hiddenTrial

theorem OAI.TraceReconstruction.windowKernel_binomial line 645
Source documentation
The literal unsigned window evaluated at an affine fair-binomial shift.
```
theorem windowKernel_binomial (n L : ℕ) (z : ℤ) :
    windowKernel n L z =
      ∑k∈Finset.range (n+1), fairBinomial n k *
        (if 0 ≤ z+(k:ℤ) ∧ z+(k:ℤ)<L then (1:ℝ) else 0) := by
…
```
Mentions: OAI.TraceReconstruction.windowKernel, OAI.TraceReconstruction.fairBinomial
theorem OAI.TraceReconstruction.posterior_unsigned_motif line 669
Source documentation
Exact local anchor kernel for the actual posterior bits, with the known visible contribution retained as a translation.
```
theorem posterior_unsigned_motif {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (s : ℕ) (z : ℤ) :
    (∑b : ι → Bool, (∏i,(flagPosterior (d i)).mass (b i)) *
      motifIndicator s (z+∑i,(bitIndex (b i):ℤ))) =
      windowKernel (∑i,hiddenTrial (d i)) (2^s) (z+∑i,(visibleOnes (d i):ℤ)) := by
…
```
Mentions: OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.windowKernel, OAI.TraceReconstruction.hiddenTrial, OAI.TraceReconstruction.visibleOnes

theorem OAI.TraceReconstruction.posterior_count_support line 680

Source documentation

The finite-series functional form of the posterior count identity.

theorem posterior_count_support {ι : Type*} [Fintype ι]
    (d : ι → Option Bool) (F : ℤ → ℝ) :
    (∑b : ι → Bool, (∏i,(flagPosterior (d i)).mass (b i))*F (∑i,(bitIndex (b i):ℤ))) =
    ∑v∈(fairSeries (∑i,hiddenTrial (d i))).coeff.support,
      (fairSeries (∑i,hiddenTrial (d i))).coeff v * F ((∑i,(visibleOnes (d i):ℤ))+v) := by
…

Mentions: OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.hiddenTrial, OAI.TraceReconstruction.visibleOnes

def OAI.TraceReconstruction.posteriorJointAnchors line 695

Source documentation

The actual two-sibling anchor multiplier. Global bits are shared by the two siblings until AFTER averaging; their local bits are independent.

def posteriorJointAnchors {ιg ι₁ ι₂ : Type*} [Fintype ιg] [Fintype ι₁] [Fintype ι₂]
    (dg : ιg → Option Bool) (d₁ : ι₁ → Option Bool) (d₂ : ι₂ → Option Bool)
    (s : ℕ) (z₁ z₂ : ℤ) : ℝ :=
…

theorem OAI.TraceReconstruction.posteriorJointAnchors_eq line 704

theorem OAI.TraceReconstruction.posterior_sibling_anchor_energy line 728

Source documentation

Quantitative sibling summation now directly bounds genuine posterior bits, not an independent-anchor surrogate.

theorem posterior_sibling_anchor_energy {ιg ι₁ ι₂ : Type*}
    [Fintype ιg] [Fintype ι₁] [Fintype ι₂]
    (dg : ιg → Option Bool) (d₁ : ι₁ → Option Bool) (d₂ : ι₂ → Option Bool)
    (s : ℕ) (A B C D : Finset ℤ) (c₁ c₂ : ℤ) :
    (∑a∈A, ∑b∈B, ∑_c∈closeLabels C (2^s) a, ∑_d∈closeLabels D (2^s) b,
      (posteriorJointAnchors dg d₁ d₂ s (a-c₁) (b-c₂))^2) ≤
    4*((2^s:ℕ):ℝ)^6*binomialBound (∑i,hiddenTrial (dg i))*
      binomialBound (∑i,hiddenTrial (d₂ i)) := by
…

Mentions: OAI.TraceReconstruction.closeLabels, OAI.TraceReconstruction.posteriorJointAnchors, OAI.TraceReconstruction.binomialBound, OAI.TraceReconstruction.hiddenTrial

theorem OAI.TraceReconstruction.FiniteLaw.expect_mul_const line 755
theorem OAI.TraceReconstruction.FiniteLaw.expect_const_mul line 760
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_product line 765
theorem OAI.TraceReconstruction.FiniteLaw.expect_prod_split line 772
def OAI.TraceReconstruction.WindowAssignments line 785
Source documentation
All local and global orientation collections on the complete index tree, including unoccupied vertices and paths which do not fit. The type is fixed before any selected monomial or role choices. n is the local trial count, g the number of global paired trials, and T the full window counts.
```
def WindowAssignments (T n g : ℕ → ℕ) (A : Type) : ℕ → Type
  | 0 => PUnit
  | b+1 => (Fin (n b) → A) × (Fin (g b) → A) ×
      (Fin (T b) → WindowAssignments T n g A b)
```
instance OAI.TraceReconstruction.windowAssignmentsFintype line 790
def OAI.TraceReconstruction.posteriorArray line 798

def OAI.TraceReconstruction.windowPosteriorLaw line 803

Source documentation

Actual independent posterior orientations at exact non-leaf metadata. The common global bits in a group are drawn only once.

def windowPosteriorLaw (T n g : ℕ → ℕ) : (b : ℕ) →
    WindowAssignments T n g (Option Bool) b → FiniteLaw (WindowAssignments T n g Bool b)
  | 0, _ => ⟨fun _ => 1,fun _ => by norm_num,by change (∑_ : PUnit,(1:ℝ))=1; simp⟩
  | b+1, d => (posteriorArray d.1).prod ((posteriorArray d.2.1).prod
      (coordinateProduct (fun i => windowPosteriorLaw T n g b (d.2.2 i))))

/-- Displacements from the jointly generated bit tree. The ancestor global
map may vary off its plateau. No independent jitter per child is introduced.
The fixed center includes the deterministic half-trial corrections. -/

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.posteriorArray

def OAI.TraceReconstruction.sourceTreeAnchors line 812

Source documentation

Displacements from the jointly generated bit tree. The ancestor global map may vary off its plateau. No independent jitter per child is introduced. The fixed center includes the deterministic half-trial corrections.

def sourceTreeAnchors (T n g : ℕ → ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ) :
    (b : ℕ) → WindowAssignments T n g Bool b → ℤ → List ℕ → ℤ
  | 0, _, _, _ => 0
  | b+1, bits, incoming, [] => center b - (∑i,(bitIndex (bits.1 i):ℤ))-incoming
  | b+1, bits, _, h::tail => if hh : h<T b then
      sourceTreeAnchors T n g center globalShift b (bits.2.2 ⟨h,hh⟩)
        (globalShift b bits.2.1 ⟨h,hh⟩) tail else 0

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.bitIndex

theorem OAI.TraceReconstruction.sourceTreeAnchors_root line 821
theorem OAI.TraceReconstruction.sourceTreeAnchors_child line 827

theorem OAI.TraceReconstruction.windowLeafSign_prefix line 837

Source documentation

Moving the origin of a subtree preserves the literal type recursion.

theorem windowLeafSign_prefix (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (pre path : List ℕ) (τ : ℝ) (v : WindowLeaf T b) :
    windowLeafSign T s X b (pre++path) τ v =
      windowLeafSign T s (fun tail => X (pre++tail)) b path τ v := by
…

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.windowLeafSign

def OAI.TraceReconstruction.sourceTreeLeafSign line 850

Source documentation

Exact recursive leaf signs for the complete bit tree, with one joint parent-global shift supplied to each sibling's local mechanism.

def sourceTreeLeafSign (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ) :
    (b : ℕ) → WindowAssignments T n g Bool b → ℤ → ℝ → WindowLeaf T b → ℝ
  | 0, _, _, τ, _ => τ
  | b+1, bits, incoming, τ, v =>
      sourceTreeLeafSign T n g s center globalShift b (bits.2.2 v.1)
        (globalShift b bits.2.1 v.1)
        (motifChildSign s (center b-(∑i,(bitIndex (bits.1 i):ℤ))-incoming) v.1.val τ) v.2

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.motifChildSign, OAI.TraceReconstruction.bitIndex

theorem OAI.TraceReconstruction.sourceTreeLeafSign_eq line 859

def OAI.TraceReconstruction.occupiedRootWeight line 888

Source documentation

The factor at the current vertex of a fixed actual occupied role choice. It only uses that vertex's displacement, never any descendant mechanism.

def occupiedRootWeight (T : ℕ → ℕ) (s : ℕ) :
    (b : ℕ) → (S : Finset (WindowLeaf T (b+1))) →
      OccupiedWindowChoice T b S → ℤ → ℝ
  | 0, S, a, X => ∏i : Fin S.card,
      bottomRoleWeight (motifIndicator s (((S.equivFin.symm i).val.1.val:ℤ)-X))
        ((prouhetSeries s).coeff (((S.equivFin.symm i).val.1.val:ℤ)-X)) (a i)
  | b+1, S, a, X => ∏i : Fin (selectedChildren S).card,
      @internalRoleWeight (occupiedWindowTerm T b
        (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val) (a.1 i)).isOdd
        (Classical.propDecidable _)
        (motifIndicator s ((((selectedChildren S).equivFin.symm i).val.val:ℤ)-X))
        ((prouhetSeries s).coeff ((((selectedChildren S).equivFin.symm i).val.val:ℤ)-X)) (a.2 i)

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.bottomRoleWeight, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.selectedChildren, OAI.TraceReconstruction.internalRoleWeight, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.selectedChildLeaves

theorem OAI.TraceReconstruction.occupiedWindowWeight_zero line 901
theorem OAI.TraceReconstruction.occupiedWindowWeight_succ line 905

theorem OAI.TraceReconstruction.occupiedWindowWeight_prefix line 928

Source documentation

Moving a subtree's path origin does not change any of its role factors.

theorem occupiedWindowWeight_prefix (T : ℕ → ℕ) (s : ℕ) (X : List ℕ → ℤ)
    (b : ℕ) (pre path : List ℕ) (S : Finset (WindowLeaf T (b+1)))
    (a : OccupiedWindowChoice T b S) :
    occupiedWindowWeight T s X b (pre++path) S a =
      occupiedWindowWeight T s (fun tail => X (pre++tail)) b path S a := by
…

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowWeight

theorem OAI.TraceReconstruction.bottomRoleWeight_abs_le_one line 942
theorem OAI.TraceReconstruction.internalRoleWeight_abs_le_one line 947
theorem OAI.TraceReconstruction.occupiedRootWeight_abs_le_one line 953
theorem OAI.TraceReconstruction.occupiedWindowWeight_abs_le_one line 966
theorem OAI.TraceReconstruction.bottom_singleton_factor line 979
Source documentation
A singleton signed role factors off its signed motif with a scalar independent of all displacements. Bottom zero-role terms really vanish.
```
theorem bottom_singleton_factor {n : ℕ} (a : Fin n → Fin 3) (i : Fin n)
    (hi : a i=2) (hrest : ∀j,j≠i → a j=0) :
    ∃c : ℝ, |c|≤1 ∧ ∀χ σ : Fin n → ℝ,
      (∏j,bottomRoleWeight (χ j) (σ j) (a j)) = c*σ i := by
…
```
Mentions: OAI.TraceReconstruction.bottomRoleWeight
theorem OAI.TraceReconstruction.internal_singleton_factor line 1005
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_subtype line 1021
Source documentation
Unoccupied independent coordinates integrate to one.
```
theorem coordinateProduct_expect_subtype {α : Type*} [Fintype α] {n : ℕ}
    (P : Fin n → FiniteLaw α) (S : Finset (Fin n)) (f : S → α → ℝ) :
    (coordinateProduct P).expect (fun x => ∏i : S, f i (x i.val)) =
      ∏i : S, (P i.val).expect (f i) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.expect
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_selected line 1049
theorem OAI.TraceReconstruction.FiniteLaw.expect_prod_selected line 1064
theorem OAI.TraceReconstruction.FiniteLaw.abs_expect_le_const line 1074
def OAI.TraceReconstruction.sourceRoleTerm line 1083
Source documentation
A fixed real coefficient term evaluated on the actual complete bit tree. The selected role choice is fixed independently of these bits.
```
def sourceRoleTerm (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (bits : WindowAssignments T n g Bool (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) (a : OccupiedWindowChoice T b S) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice
def OAI.TraceReconstruction.sourceRoleAverage line 1090
theorem OAI.TraceReconstruction.sourceRoleTerm_zero line 1097
theorem OAI.TraceReconstruction.sourceRoleTerm_succ line 1104
theorem OAI.TraceReconstruction.sourceRoleAverage_zero line 1126
theorem OAI.TraceReconstruction.sourceRoleAverage_succ line 1143
theorem OAI.TraceReconstruction.sourceRoleAverage_abs_le_one line 1166
def OAI.TraceReconstruction.posteriorSmoothingCost line 1176
Source documentation
The exact signed smoothing cost read off the visible metadata alone.
```
def posteriorSmoothingCost {ι : Type*} [Fintype ι] (s : ℕ) (d : ι → Option Bool) : ℝ :=
…
```
def OAI.TraceReconstruction.MetadataSmoothingCap line 1182
Source documentation
A purely numerical typical-metadata condition on every local collection. It includes unoccupied vertices and is fixed before a coefficient is chosen.
```
def MetadataSmoothingCap (T n g : ℕ → ℕ) (s : ℕ) (η : ℝ) :
    (b : ℕ) → WindowAssignments T n g (Option Bool) b → Prop
  | 0, _ => True
  | b+1, d => posteriorSmoothingCost s d.1 ≤ η ∧
      ∀h, MetadataSmoothingCap T n g s η b (d.2.2 h)
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.posteriorSmoothingCost
def OAI.TraceReconstruction.occupiedRootHasSingleton line 1188
theorem OAI.TraceReconstruction.occupiedRoot_singleton_factor line 1193
theorem OAI.TraceReconstruction.occupiedRoot_singleton_average line 1213
theorem OAI.TraceReconstruction.abs_prod_le_coordinate line 1239
theorem OAI.TraceReconstruction.sourceRoleAverage_singleton line 1249
Source documentation
Literal singleton cancellation for the complete posterior bit tree. No successful-fit event is conditioned on, and the common parent-global jitter is retained until after the child factors have averaged.
```
theorem sourceRoleAverage_singleton (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ)
    (S : Finset (WindowLeaf T (b+1))) (a : OccupiedWindowChoice T b S)
    (η : ℝ) (hcap : MetadataSmoothingCap T n g s η (b+1) d)
    (hsing : ¬(occupiedWindowTerm T b S a).noSingleton) :
    |sourceRoleAverage T n g s center globalShift b d incoming S a|≤η := by
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.MetadataSmoothingCap, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage