Anchors.lean`

72 declarations, 0 contain sorry, 0 declared as axioms

Anchors

Forced anchors, extra-leaf closeness, and correlated group square-sum estimates.

theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_two line 26
Source documentation
Two distinct actual child coordinates are independent. This does not assert independence of their shared parent-global jitter.
```
theorem coordinateProduct_expect_two {α : Type*} [Fintype α] {n : ℕ}
    (P : Fin n → FiniteLaw α) (a c : Fin n) (hne : a≠c) (f h : α → ℝ) :
    (coordinateProduct P).expect (fun x => f (x a)*h (x c)) = (P a).expect f*(P c).expect h := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.expect

theorem OAI.TraceReconstruction.FiniteLaw.expect_prod_two line 49

Source documentation

Exact local/global/children factorization with the parent-global draw outside the product of child expectations.

theorem expect_prod_two {α β γ : Type*} [Fintype α] [Fintype β] [Fintype γ]
    {n : ℕ} (P : FiniteLaw α) (Q : FiniteLaw β) (R : Fin n → FiniteLaw γ)
    (a c : Fin n) (hne : a≠c) (f : α → ℝ) (h k : β → γ → ℝ) :
    (P.prod (Q.prod (coordinateProduct R))).expect (fun x =>
      f x.1 * (h x.2.1 (x.2.2 a)*k x.2.1 (x.2.2 c))) =
      P.expect f * Q.expect (fun z => (R a).expect (h z)*(R c).expect (k z)) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.expect

def OAI.TraceReconstruction.BinaryWindowLabels line 61
Source documentation
A concrete binary selection of labels in the complete index tree. Unlike a free abstract shape this retains every actual column label.
```
def BinaryWindowLabels (T : ℕ → ℕ) : ℕ → Type
  | 0 => PUnit
  | b+1 => Fin (T b) × Fin (T b) × BinaryWindowLabels T b × BinaryWindowLabels T b
```
instance OAI.TraceReconstruction.binaryWindowLabelsFintype line 65

def OAI.TraceReconstruction.BinaryWindowLabels.distinct line 74

Source documentation

The forced children are distinct at every split. Central restrictions are separate deterministic predicates, not conditioning events.

def BinaryWindowLabels.distinct (T : ℕ → ℕ) : (b : ℕ) → BinaryWindowLabels T b → Prop
  | 0, _ => True
  | b+1, p => p.1≠p.2.1 ∧ distinct T b p.2.2.1 ∧ distinct T b p.2.2.2

/-- Product of the first-child unsigned anchor at every forced nonleaf,
evaluated using the literal complete-tree orientation assignment. -/

Mentions: OAI.TraceReconstruction.BinaryWindowLabels

def OAI.TraceReconstruction.binaryAnchorKernel line 80

Source documentation

Product of the first-child unsigned anchor at every forced nonleaf, evaluated using the literal complete-tree orientation assignment.

def binaryAnchorKernel (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ) :
    (b : ℕ) → BinaryWindowLabels T b → WindowAssignments T n g Bool b → ℤ → ℝ
  | 0, _, _, _ => 1
  | b+1, p, bits, incoming =>
      motifIndicator s ((p.1.val:ℤ)-center b+(∑i,(bitIndex (bits.1 i):ℤ))+incoming) *
      (binaryAnchorKernel T n g s center globalShift b p.2.2.1 (bits.2.2 p.1)
        (globalShift b bits.2.1 p.1) *
       binaryAnchorKernel T n g s center globalShift b p.2.2.2 (bits.2.2 p.2.1)
        (globalShift b bits.2.1 p.2.1))

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

def OAI.TraceReconstruction.binaryAnchorAverage line 91
theorem OAI.TraceReconstruction.binaryAnchorAverage_zero line 98
theorem OAI.TraceReconstruction.binaryAnchorAverage_succ line 104
def OAI.TraceReconstruction.localAnchorAverage line 125
Source documentation
Local unsigned anchor averaged against its actual known/hidden flags.
```
def localAnchorAverage {m : ℕ} (d : Fin m → Option Bool) (s : ℕ) (z : ℤ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.localAnchorAverage_kernel line 128

def OAI.TraceReconstruction.binaryAnchorBelow line 139

Source documentation

Product of all lower sibling-group factors. Each group still averages its own single common global draw, not two independent global draws.

def binaryAnchorBelow (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ) :
    (b : ℕ) → BinaryWindowLabels T (b+1) → WindowAssignments T n g (Option Bool) (b+1) → ℝ
  | 0, _, _ => 1
  | b+1, p, d =>
      (posteriorArray d.2.1).expect (fun glob =>
        localAnchorAverage (d.2.2 p.1).1 s
          ((p.2.2.1.1.val:ℤ)-center b+globalShift (b+1) glob p.1) *
        localAnchorAverage (d.2.2 p.2.1).1 s
          ((p.2.2.2.1.val:ℤ)-center b+globalShift (b+1) glob p.2.1)) *
      (binaryAnchorBelow T n g s center globalShift b p.2.2.1 (d.2.2 p.1) *
       binaryAnchorBelow T n g s center globalShift b p.2.2.2 (d.2.2 p.2.1))

Mentions: OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.posteriorArray, OAI.TraceReconstruction.localAnchorAverage

theorem OAI.TraceReconstruction.binaryAnchorAverage_factor line 154

Source documentation

Exact factorization of the forced anchor expectation into its root kernel and all correlated sibling groups, at the real metadata/labels.

theorem binaryAnchorAverage_factor (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (p : BinaryWindowLabels T (b+1)) (d : WindowAssignments T n g (Option Bool) (b+1))
    (incoming : ℤ) (hd : BinaryWindowLabels.distinct T (b+1) p) :
    binaryAnchorAverage T n g s center globalShift (b+1) p d incoming =
      localAnchorAverage d.1 s ((p.1.val:ℤ)-center b+incoming) *
        binaryAnchorBelow T n g s center globalShift b p d := by
…

Mentions: OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.BinaryWindowLabels.distinct, OAI.TraceReconstruction.binaryAnchorAverage, OAI.TraceReconstruction.localAnchorAverage, OAI.TraceReconstruction.binaryAnchorBelow

theorem OAI.TraceReconstruction.localAnchor_pair_plateau line 203

Source documentation

One plateau group's local means are the genuine shared-global joint anchor, with exactly the affine shift appearing in the layout.

theorem localAnchor_pair_plateau {mg m₁ m₂ : ℕ}
    (dg : Fin mg → Option Bool) (d₁ : Fin m₁ → Option Bool) (d₂ : Fin m₂ → Option Bool)
    (s : ℕ) (z₁ z₂ shift : ℤ) :
    (posteriorArray dg).expect (fun glob =>
      localAnchorAverage d₁ s (z₁+(∑i,(bitIndex (glob i):ℤ))-shift) *
      localAnchorAverage d₂ s (z₂+(∑i,(bitIndex (glob i):ℤ))-shift)) =
    posteriorJointAnchors dg d₁ d₂ s (z₁-shift) (z₂-shift) := by
…

Mentions: OAI.TraceReconstruction.posteriorArray, OAI.TraceReconstruction.localAnchorAverage, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.posteriorJointAnchors

def OAI.TraceReconstruction.forcedWindowLabels line 230

Source documentation

A role-selected forced subtree remembers the actual complete-tree labels, not merely its abstract binary shape.

def forcedWindowLabels (T : ℕ → ℕ) : (b : ℕ) →
    (S : Finset (WindowLeaf T (b+1))) → (a : OccupiedWindowChoice T b S) →
    (occupiedWindowTerm T b S a).Forced → BinaryWindowLabels T (b+1)
  | 0, S, _, .node i j _ _ _ _ _ =>
      ((S.equivFin.symm i).val.1,(S.equivFin.symm j).val.1,PUnit.unit,PUnit.unit)
  | b+1, S, a, .node i j _ _ _ left right =>
      (((selectedChildren S).equivFin.symm i).val,
       ((selectedChildren S).equivFin.symm j).val,
       forcedWindowLabels T b (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val)
         (a.1 i) left,
       forcedWindowLabels T b (selectedChildLeaves S ((selectedChildren S).equivFin.symm j).val)
         (a.1 j) right)

Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.selectedChildren, OAI.TraceReconstruction.selectedChildLeaves

theorem OAI.TraceReconstruction.forcedWindowLabels_distinct line 243
theorem OAI.TraceReconstruction.motifIndicator_nonneg line 264
theorem OAI.TraceReconstruction.motifIndicator_le_one line 268
theorem OAI.TraceReconstruction.binaryAnchorKernel_nonneg line 272
theorem OAI.TraceReconstruction.bottomRoleWeight_abs_le_indicator line 281
theorem OAI.TraceReconstruction.internalRoleWeight_active_abs_le_indicator line 286
theorem OAI.TraceReconstruction.occupiedRootWeight_bottom_anchor line 292
theorem OAI.TraceReconstruction.occupiedRootWeight_internal_anchor line 300
theorem OAI.TraceReconstruction.abs_prod_le_two line 309

theorem OAI.TraceReconstruction.sourceRoleTerm_forced_anchor line 331

Source documentation

The real role term is pointwise dominated by its selected unsigned anchors. No independence assumption is used in this domination.

theorem sourceRoleTerm_forced_anchor (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)
    (F : (occupiedWindowTerm T b S a).Forced) :
    |sourceRoleTerm T n g s center globalShift b bits incoming S a|≤
      binaryAnchorKernel T n g s center globalShift (b+1) (forcedWindowLabels T b S a F) bits incoming := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleTerm, OAI.TraceReconstruction.binaryAnchorKernel, OAI.TraceReconstruction.forcedWindowLabels

theorem OAI.TraceReconstruction.sourceRoleAverage_forced_anchor line 375

Source documentation

Therefore the coefficient average is bounded by the actual forced anchor average, with the true posterior law and shared jitter retained.

theorem sourceRoleAverage_forced_anchor (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)
    (F : (occupiedWindowTerm T b S a).Forced) :
    |sourceRoleAverage T n g s center globalShift b d incoming S a|≤
      binaryAnchorAverage T n g s center globalShift (b+1) (forcedWindowLabels T b S a F) d incoming := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage, OAI.TraceReconstruction.binaryAnchorAverage, OAI.TraceReconstruction.forcedWindowLabels

theorem OAI.TraceReconstruction.sourceRoleTerm_valid line 386
theorem OAI.TraceReconstruction.sourceRoleAverage_valid line 398

theorem OAI.TraceReconstruction.sourceRoleAverage_alternative line 416

Source documentation

The source's two alternatives now apply to actual posterior coefficient terms: signed singleton smoothing, or domination by a genuine forced tree.

theorem sourceRoleAverage_alternative (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)
    (η : ℝ) (hη : 0≤η) (hcap : MetadataSmoothingCap T n g s η (b+1) d)
    (ho : (occupiedWindowTerm T b S a).isOdd) :
    |sourceRoleAverage T n g s center globalShift b d incoming S a|≤η ∨
    ∃F : (occupiedWindowTerm T b S a).Forced,
      BinaryWindowLabels.distinct T (b+1) (forcedWindowLabels T b S a F) ∧
      |sourceRoleAverage T n g s center globalShift b d incoming S a|≤
        binaryAnchorAverage T n g s center globalShift (b+1) (forcedWindowLabels T b S a F) d incoming := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.MetadataSmoothingCap, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage, OAI.TraceReconstruction.BinaryWindowLabels.distinct, OAI.TraceReconstruction.forcedWindowLabels, OAI.TraceReconstruction.binaryAnchorAverage

def OAI.TraceReconstruction.sourceBottomIndicator line 444

Source documentation

The unsigned bottom constraint at one literal complete-tree leaf.

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

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

def OAI.TraceReconstruction.sourceLeafProduct line 452
theorem OAI.TraceReconstruction.sourceBottomIndicator_zero_one line 458
theorem OAI.TraceReconstruction.prod_zero_one line 468
theorem OAI.TraceReconstruction.sourceLeafProduct_zero_one line 478
theorem OAI.TraceReconstruction.binaryAnchorKernel_zero_one line 486
theorem OAI.TraceReconstruction.sourceLeafProduct_succ line 501

theorem OAI.TraceReconstruction.sourceRoleTerm_all_leaf_constraints line 521

Source documentation

Every selected leaf is active in the bottom expansion, including those outside the forced tree. Their absolute constraints are not lost.

theorem sourceRoleTerm_all_leaf_constraints (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) :
    |sourceRoleTerm T n g s center globalShift b bits incoming S a|≤
      sourceLeafProduct T n g s center globalShift b bits incoming S := by
…

theorem OAI.TraceReconstruction.sourceLeafProduct_antitone line 556
theorem OAI.TraceReconstruction.le_mul_of_zero_one line 568

theorem OAI.TraceReconstruction.sourceRoleAverage_forced_extra line 575

Source documentation

Actual forced anchor AND extra-leaf constraints in one bit expectation. In particular E can be precisely the nonforced leaves; keeping it arbitrary here permits the later label summation without any conditioning gates.

theorem sourceRoleAverage_forced_extra (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 E : Finset (WindowLeaf T (b+1))) (hES : E⊆S) (a : OccupiedWindowChoice T b S)
    (F : (occupiedWindowTerm T b S a).Forced) :
    |sourceRoleAverage T n g s center globalShift b d incoming S a|≤
      (windowPosteriorLaw T n g (b+1) d).expect (fun bits =>
        binaryAnchorKernel T n g s center globalShift (b+1) (forcedWindowLabels T b S a F) bits incoming *
        sourceLeafProduct T n g s center globalShift b bits incoming E) := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage, OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.binaryAnchorKernel, OAI.TraceReconstruction.forcedWindowLabels, OAI.TraceReconstruction.sourceLeafProduct

def OAI.TraceReconstruction.BinaryWindowLabels.close line 605
Source documentation
Deterministic closeness of each forced split; it is a restriction on labels, never an additional conditioning event for the random bits.
```
def BinaryWindowLabels.close (T : ℕ → ℕ) (s : ℕ) : (b : ℕ) → BinaryWindowLabels T b → Prop
  | 0, _ => True
  | b+1, p => |(p.1.val:ℤ)-p.2.1.val|<(2^s:ℕ) ∧ close T s b p.2.2.1 ∧ close T s b p.2.2.2
```
Mentions: OAI.TraceReconstruction.BinaryWindowLabels
theorem OAI.TraceReconstruction.motifIndicator_pair_close line 609
theorem OAI.TraceReconstruction.nonzero_of_abs_le line 620
theorem OAI.TraceReconstruction.sourceRoleTerm_forced_close line 627
Source documentation
A nonzero literal role multiplier enforces all close-child restrictions of every forced subtree chosen from its fixed role pattern.
```
theorem sourceRoleTerm_forced_close (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)
    (F : (occupiedWindowTerm T b S a).Forced)
    (h : sourceRoleTerm T n g s center globalShift b bits incoming S a≠0) :
    BinaryWindowLabels.close T s (b+1) (forcedWindowLabels T b S a F) := by
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleTerm, OAI.TraceReconstruction.BinaryWindowLabels.close, OAI.TraceReconstruction.forcedWindowLabels

theorem OAI.TraceReconstruction.sourceRoleAverage_forced_close line 666

Source documentation

Closeness remains a pure label condition after averaging, without conditioning on it.

theorem sourceRoleAverage_forced_close (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)
    (F : (occupiedWindowTerm T b S a).Forced)
    (h : sourceRoleAverage T n g s center globalShift b d incoming S a≠0) :
    BinaryWindowLabels.close T s (b+1) (forcedWindowLabels T b S a F) := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.OccupiedWindowChoice, OAI.TraceReconstruction.occupiedWindowTerm, OAI.TraceReconstruction.sourceRoleAverage, OAI.TraceReconstruction.BinaryWindowLabels.close, OAI.TraceReconstruction.forcedWindowLabels

def OAI.TraceReconstruction.finIntegerLabels line 691
Source documentation
The literal finite child labels embedded in the integer line.
```
def finIntegerLabels (N : ℕ) : Finset ℤ := Finset.univ.image (fun i : Fin N => (i.val:ℤ))
```
theorem OAI.TraceReconstruction.sum_finIntegerLabels line 693
theorem OAI.TraceReconstruction.sum_close_finIntegerLabels line 701

theorem OAI.TraceReconstruction.localAnchor_finite_energy line 708

Source documentation

Any deterministic plateau/distinctness restriction can be retained in child-pair summation. Only closeness is used to upper bound its cost.

theorem localAnchor_finite_energy {m N : ℕ} (d : Fin m → Option Bool) (s : ℕ)
    (c : ℤ) (R : Fin N → Fin N → Prop) [DecidableRel R]
    (hR : ∀a b,R a b → |(b.val:ℤ)-a.val|<(2^s:ℕ)) :
    (∑a : Fin N, ∑b : Fin N, if R a b then localAnchorAverage d s ((a.val:ℤ)-c)^2 else 0) ≤
      2*((2^s:ℕ):ℝ)^3*binomialBound (∑i,hiddenTrial (d i)) := by
…

Mentions: OAI.TraceReconstruction.localAnchorAverage, OAI.TraceReconstruction.binomialBound, OAI.TraceReconstruction.hiddenTrial

theorem OAI.TraceReconstruction.posteriorJoint_finite_energy line 736

Source documentation

Actual shared-jitter energy over two finite sibling pairs. Parent-label plateau restrictions are discharged before applying this lemma; arbitrary restrictions on these child pairs are kept, not conditioned on.

theorem posteriorJoint_finite_energy {mg m₁ m₂ N : ℕ}
    (dg : Fin mg → Option Bool) (d₁ : Fin m₁ → Option Bool) (d₂ : Fin m₂ → Option Bool)
    (s : ℕ) (c₁ c₂ : ℤ) (R : Fin N → Fin N → Prop) [DecidableRel R]
    (hR : ∀a b,R a b → |(b.val:ℤ)-a.val|<(2^s:ℕ)) :
    (∑a : Fin N, ∑c : Fin N, ∑b : Fin N, ∑d : Fin N,
      if R a c ∧ R b d then
        posteriorJointAnchors dg d₁ d₂ s ((a.val:ℤ)-c₁) ((b.val:ℤ)-c₂)^2 else 0) ≤
       4*((2^s:ℕ):ℝ)^6*binomialBound (∑i,hiddenTrial (dg i))*binomialBound (∑i,hiddenTrial (d₂ i)) := by
…

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

def OAI.TraceReconstruction.anchorPairAllowed line 789
Source documentation
The actual finite central domain, distinctness and close-label restriction. It is purely deterministic and is never added to the orientation posterior.
```
def anchorPairAllowed (T : ℕ → ℕ) (A : (b : ℕ) → Finset (Fin (T b))) (s b : ℕ)
    (a c : Fin (T b)) : Prop := a∈A b ∧ c∈A b ∧ a≠c ∧ |(c.val:ℤ)-a.val|<(2^s:ℕ)
```
def OAI.TraceReconstruction.HasGlobalPlateau line 794
Source documentation
The source global plateau identity is required pointwise for bits, not just in distribution and not after conditioning on successful layout.
```
def HasGlobalPlateau (T g : ℕ → ℕ) (A : (b : ℕ) → Finset (Fin (T b))) (shift : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ) : Prop :=
…
```

def OAI.TraceReconstruction.MetadataBinomialCaps line 800

Source documentation

Numerical binomial caps extracted from the literal known/hidden metadata. In applications these are proved using the source hidden-trial lower bounds.

def MetadataBinomialCaps (T n g : ℕ → ℕ) (B C : ℕ → ℝ) :
    (b : ℕ) → WindowAssignments T n g (Option Bool) b → Prop
  | 0, _ => True
  | b+1, d => binomialBound (∑i, hiddenTrial (d.1 i)) ≤ B b ∧
      binomialBound (∑i, hiddenTrial (d.2.1 i)) ≤ C b ∧
      ∀u, MetadataBinomialCaps T n g B C b (d.2.2 u)

/-- One correlated sibling-group anchor, using the actual child metadata
and their parent's one shared global orientation collection. -/

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

def OAI.TraceReconstruction.binarySiblingAnchor line 809

Source documentation

One correlated sibling-group anchor, using the actual child metadata and their parent's one shared global orientation collection.

def binarySiblingAnchor (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1+1))
    (u v : Fin (T (b+1))) (a c : Fin (T b)) : ℝ :=
…

Mentions: OAI.TraceReconstruction.WindowAssignments

theorem OAI.TraceReconstruction.binarySiblingAnchor_plateau line 817

def OAI.TraceReconstruction.binaryDescendantEnergy line 842

Source documentation

Exact dynamic sum of squared group anchors over the allowed finite labels below a fixed forced split. Distinct groups retain their own metadata.

def binaryDescendantEnergy (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) :
    (b : ℕ) → WindowAssignments T n g (Option Bool) (b+1) → Fin (T b) → Fin (T b) → ℝ
  | 0, _, _, _ => 1
  | b+1, d, u, v =>
      ∑a : Fin (T b),∑c : Fin (T b),∑e : Fin (T b),∑f : Fin (T b),
        if anchorPairAllowed T A s b a c ∧ anchorPairAllowed T A s b e f then
          binarySiblingAnchor T n g s center globalShift b d u v a e ^ 2 *
            binaryDescendantEnergy T n g s center globalShift A b (d.2.2 u) a c *
            binaryDescendantEnergy T n g s center globalShift A b (d.2.2 v) e f
        else 0

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.anchorPairAllowed, OAI.TraceReconstruction.binarySiblingAnchor

theorem OAI.TraceReconstruction.binaryDescendantEnergy_nonneg line 855

theorem OAI.TraceReconstruction.binarySiblingAnchor_energy line 876

Source documentation

True common-jitter energy at one group, with its exact finite domains.

theorem binarySiblingAnchor_energy (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (shift : ℕ → ℤ)
    (hplat : HasGlobalPlateau T g A shift globalShift)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1+1))
    (u v : Fin (T (b+1))) (hu : u∈A (b+1)) (hv : v∈A (b+1)) :
    (∑a : Fin (T b),∑c : Fin (T b),∑e : Fin (T b),∑f : Fin (T b),
        if anchorPairAllowed T A s b a c ∧ anchorPairAllowed T A s b e f then
          binarySiblingAnchor T n g s center globalShift b d u v a e ^ 2 else 0) ≤
      4*((2^s:ℕ):ℝ)^6*binomialBound (∑i,hiddenTrial (d.2.1 i))*
        binomialBound (∑i,hiddenTrial ((d.2.2 v).1 i)) := by
…

Mentions: OAI.TraceReconstruction.HasGlobalPlateau, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.anchorPairAllowed, OAI.TraceReconstruction.binarySiblingAnchor, OAI.TraceReconstruction.binomialBound, OAI.TraceReconstruction.hiddenTrial

theorem OAI.TraceReconstruction.binaryDescendantEnergy_le line 895

Source documentation

The complete bottom-up forced-label energy estimate. Its only numerical inputs are actual metadata hidden-count binomial caps. The group bound keeps one shared global kernel until AFTER squaring.

theorem binaryDescendantEnergy_le (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (shift : ℕ → ℤ)
    (hplat : HasGlobalPlateau T g A shift globalShift)
    (B C : ℕ → ℝ) (hB : ∀b,0≤B b) (hC : ∀b,0≤C b)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1))
    (hcap : MetadataBinomialCaps T n g B C (b+1) d)
    (u v : Fin (T b)) (hu : u∈A b) (hv : v∈A b) :
    binaryDescendantEnergy T n g s center globalShift A b d u v ≤
      binaryTreeBudget (fun j => 4*((2^s:ℕ):ℝ)^6*C (j+1)*B j) b := by
…

Mentions: OAI.TraceReconstruction.HasGlobalPlateau, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.MetadataBinomialCaps, OAI.TraceReconstruction.binaryDescendantEnergy, OAI.TraceReconstruction.binaryTreeBudget

def OAI.TraceReconstruction.BinaryWindowLabels.allowed line 952
theorem OAI.TraceReconstruction.BinaryWindowLabels.allowed_distinct line 958
def OAI.TraceReconstruction.joinBinaryLabels line 966
Source documentation
Regroup the two real top child labels, without changing the actual finite label type or declaration order.
```
def joinBinaryLabels {T : ℕ → ℕ} {b : ℕ} (a : Fin (T b) × Fin (T b))
    (p : BinaryWindowLabels T b × BinaryWindowLabels T b) : BinaryWindowLabels T (b+1) :=
…
```
Mentions: OAI.TraceReconstruction.BinaryWindowLabels
theorem OAI.TraceReconstruction.sum_binary_labels line 970

theorem OAI.TraceReconstruction.sum_pair_tensor line 984

Source documentation

Exact finite tensor summation after preserving both deterministically allowed label domains. No probabilistic independence is asserted here.

theorem sum_pair_tensor {α β σ τ : Type*} [Fintype α] [Fintype β] [Fintype σ] [Fintype τ]
    (R : α → Prop) (S : β → Prop) (P : σ → Prop) (Q : τ → Prop)
    [DecidablePred R] [DecidablePred S] [DecidablePred P] [DecidablePred Q]
    (K : α → β → ℝ) (f : α → σ → ℝ) (h : β → τ → ℝ) :
    (∑a,∑x,∑b,∑y, if R a ∧ P x ∧ S b ∧ Q y then K a b*f a x*h b y else 0) =
      ∑a,∑b,if R a ∧ S b then K a b*(∑x,if P x then f a x else 0)*
        (∑y,if Q y then h b y else 0) else 0 := by
…

theorem OAI.TraceReconstruction.binaryAnchorBelow_sum line 1013

Source documentation

Literal sum over all descendant labels is the recursively compiled sibling-group energy. This is the bridge from the actual anchor average to bottom-up summation; no coefficient estimate is supplied as a hypothesis.

theorem binaryAnchorBelow_sum (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (u v : Fin (T b)) :
    (∑p : BinaryWindowLabels T b × BinaryWindowLabels T b,
      if BinaryWindowLabels.allowed T A s b p.1 ∧ BinaryWindowLabels.allowed T A s b p.2 then
        binaryAnchorBelow T n g s center globalShift b (joinBinaryLabels (u,v) p) d ^ 2 else 0) =
      binaryDescendantEnergy T n g s center globalShift A b d u v := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.BinaryWindowLabels.allowed, OAI.TraceReconstruction.binaryAnchorBelow, OAI.TraceReconstruction.joinBinaryLabels, OAI.TraceReconstruction.binaryDescendantEnergy

theorem OAI.TraceReconstruction.binaryAnchorAverage_sum line 1053

Source documentation

The square-sum of actual anchor averages over all admissible forced indices, including the root local smoothing cost exactly once.

theorem binaryAnchorAverage_sum (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (b : ℕ)
    (d : WindowAssignments T n g (Option Bool) (b+1)) (incoming : ℤ) :
    (∑p : BinaryWindowLabels T (b+1), if BinaryWindowLabels.allowed T A s (b+1) p then
      binaryAnchorAverage T n g s center globalShift (b+1) p d incoming ^ 2 else 0) =
      ∑u : Fin (T b),∑v : Fin (T b), if anchorPairAllowed T A s b u v then
        localAnchorAverage d.1 s ((u.val:ℤ)-center b+incoming)^2 *
          binaryDescendantEnergy T n g s center globalShift A b d u v else 0 := by
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.BinaryWindowLabels.allowed, OAI.TraceReconstruction.binaryAnchorAverage, OAI.TraceReconstruction.anchorPairAllowed, OAI.TraceReconstruction.localAnchorAverage, OAI.TraceReconstruction.binaryDescendantEnergy

theorem OAI.TraceReconstruction.binaryAnchorAverage_energy line 1093

Source documentation

Full finite forced-anchor squared coefficient budget, with the source power of one local root cost and one correlated global/local cost per group. This conclusion is about literal posterior averages and actual labels.

theorem binaryAnchorAverage_energy (T n g : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ)
    (globalShift : (b : ℕ) → (Fin (g b) → Bool) → Fin (T b) → ℤ)
    (A : (b : ℕ) → Finset (Fin (T b))) (shift : ℕ → ℤ)
    (hplat : HasGlobalPlateau T g A shift globalShift)
    (B C : ℕ → ℝ) (hB : ∀b,0≤B b) (hC : ∀b,0≤C b)
    (b : ℕ) (d : WindowAssignments T n g (Option Bool) (b+1))
    (hcap : MetadataBinomialCaps T n g B C (b+1) d) (incoming : ℤ) :
    (∑p : BinaryWindowLabels T (b+1), if BinaryWindowLabels.allowed T A s (b+1) p then
      binaryAnchorAverage T n g s center globalShift (b+1) p d incoming ^ 2 else 0) ≤
        (2*((2^s:ℕ):ℝ)^3*B b) *
          binaryTreeBudget (fun j => 4*((2^s:ℕ):ℝ)^6*C (j+1)*B j) b := by
…

Mentions: OAI.TraceReconstruction.HasGlobalPlateau, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.MetadataBinomialCaps, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.BinaryWindowLabels.allowed, OAI.TraceReconstruction.binaryAnchorAverage, OAI.TraceReconstruction.binaryTreeBudget

theorem OAI.TraceReconstruction.motifIndicator_finite_sum line 1138
Source documentation
A literal unsigned length-L translated motif admits at most L child labels in any finite window, even when the intended motif does not fit.
```
theorem motifIndicator_finite_sum (s N : ℕ) (X : ℤ) :
    (∑h : Fin N,motifIndicator s ((h.val:ℤ)-X)) ≤ (2^s:ℕ) := by
…
```
Mentions: OAI.TraceReconstruction.motifIndicator
def OAI.TraceReconstruction.extraLabelAverage line 1165
Source documentation
The complete bits law is arbitrary. All extra-leaf offsets may be mutually correlated and correlated with the retained forced-anchor kernel. Only the extra leaf label variables themselves are summed here.
```
def extraLabelAverage {Ω : Type*} [Fintype Ω] (P : FiniteLaw Ω)
    (s N e : ℕ) (f : Ω → ℝ) (X : Ω → Fin e → ℤ) (h : Fin e → Fin N) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.extraLabelAverage_nonneg line 1169
theorem OAI.TraceReconstruction.extraLabelAverage_sum line 1179
Source documentation
Source the correlated-anchor estimate, extra leaf l1 cost before squaring. No free T_1 cost and no invalid decoupling of global displacements enter.
```
theorem extraLabelAverage_sum {Ω : Type*} [Fintype Ω] (P : FiniteLaw Ω)
    (s N e : ℕ) (f : Ω → ℝ) (hf : ∀ω,0≤f ω) (X : Ω → Fin e → ℤ) :
    (∑h : Fin e → Fin N,extraLabelAverage P s N e f X h) ≤
      ((2^s:ℕ):ℝ)^e*P.expect f := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.extraLabelAverage
theorem OAI.TraceReconstruction.extraLabelAverage_energy line 1205
Source documentation
The squared extra-leaf cost follows from nonnegativity AFTER the whole shared-bit average, exactly as in the source (not from independence).
```
theorem extraLabelAverage_energy {Ω : Type*} [Fintype Ω] (P : FiniteLaw Ω)
    (s N e : ℕ) (f : Ω → ℝ) (hf : ∀ω,0≤f ω) (X : Ω → Fin e → ℤ) :
    (∑h : Fin e → Fin N,extraLabelAverage P s N e f X h ^ 2) ≤
      ((2^s:ℕ):ℝ)^(2*e)*(P.expect f)^2 := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.extraLabelAverage