Simulation.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

Simulation

Canonical and filled simulations, central fit, root words, chronology, slots, finite codes, and complete-trace decoding.

theorem OAI.TraceReconstruction.dependentProduct_approximates line 25

Source documentation

Heterogeneous emissions retain their actual outcome type while moving to the one fixed public chronological order.

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

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

abbrev OAI.TraceReconstruction.EmissionSlot line 47
Source documentation
Each paired mechanism owns two distinct side slots; fillers and old leaf oracles have their own IDs. This type is independent of every orientation.
```
abbrev EmissionSlot (m k n : ℕ) := (Fin m × Bool) ⊕ (Fin k ⊕ Fin n)
```
def OAI.TraceReconstruction.EmissionOutcome line 49
instance OAI.TraceReconstruction.emissionOutcomeFintype line 54
def OAI.TraceReconstruction.emissionAssignmentEquiv line 63
Source documentation
Actual arrays and slot observations are bijective, not a lossy interface.
```
def emissionAssignmentEquiv (Side Leaf : Type) (m k n : ℕ) :
    ((Fin m → Side × Side) × (Fin k → Side) × (Fin n → Leaf)) ≃
      (∀i : EmissionSlot m k n,EmissionOutcome Side Leaf i) where
…
```
Mentions: OAI.TraceReconstruction.EmissionSlot, OAI.TraceReconstruction.EmissionOutcome
def OAI.TraceReconstruction.PairedMechanisms.slotLaw line 87
theorem OAI.TraceReconstruction.PairedMechanisms.slotLaw_mass line 95
theorem OAI.TraceReconstruction.PairedMechanisms.slotLaw_expect line 112
theorem OAI.TraceReconstruction.PairedMechanisms.reportsGiven_slot_expect line 125
Source documentation
Forgetting only the visible flags recovers the genuine independent side, filler and leaf laws at every orientation, before any fit restriction.
```
theorem reportsGiven_slot_expect (R : Fin k → FiniteLaw Side) (P Q : FiniteLaw Leaf)
    (bits : Fin m → Bool) (θ : Fin n → Bool)
    (F : (∀i : EmissionSlot m k n,EmissionOutcome Side Leaf i) → ℝ) :
    ((M.reportsGiven bits).prod ((FiniteLaw.coordinateProduct R).prod (selectedLeafLaw P Q θ))).expect
      (fun x => F (emissionAssignmentEquiv Side Leaf m k n (fun j => (x.1 j).2,x.2)))=
      (FiniteLaw.dependentProduct (M.slotLaw R P Q bits θ)).expect F := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.EmissionSlot, OAI.TraceReconstruction.EmissionOutcome, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.PairedMechanisms.selectedLeafLaw, OAI.TraceReconstruction.emissionAssignmentEquiv, OAI.TraceReconstruction.FiniteLaw.dependentProduct
def OAI.TraceReconstruction.PairedMechanisms.slotDecode line 144
Source documentation
The common, bit-blind projection simply forgets flags and concatenates in the publicly fixed ID order.
```
def slotDecode (f : Side → List Bool) (g : Leaf → List Bool) :
    (i : EmissionSlot m k n) → EmissionOutcome Side Leaf i → List Bool
  | .inl _,x => f x
  | .inr (.inl _),x => f x
  | .inr (.inr _),x => g x
```
Mentions: OAI.TraceReconstruction.EmissionSlot, OAI.TraceReconstruction.EmissionOutcome
def OAI.TraceReconstruction.PairedMechanisms.slotWord line 150
def OAI.TraceReconstruction.PairedMechanisms.slotCost line 158
theorem OAI.TraceReconstruction.PairedMechanisms.slotCost_sum line 163
theorem OAI.TraceReconstruction.PairedMechanisms.slotLaw_simulation line 167

theorem OAI.TraceReconstruction.PairedMechanisms.reportsGiven_simulation line 192

Source documentation

Exact conditional-on-orientation simulation boundary. The orientation is not part of the common projection, and no fit conditioning enters its law.

theorem reportsGiven_simulation {q E : ℝ} (hq : q∈Set.Icc 0 1)
    {L : ℕ} (e : Fin L ≃ EmissionSlot m k n)
    (R : Fin k → FiniteLaw Side) (P Q : FiniteLaw Leaf)
    (f : Side → List Bool) (g : Leaf → List Bool) (U V : Fin m → List Bool)
    (W : Fin k → List Bool) (atom : Bool → List Bool)
    (hU : ∀j,SimulatesTrace q (M.first j) f (U j))
    (hV : ∀j,SimulatesTrace q (M.second j) f (V j))
    (hW : ∀j,SimulatesTrace q (R j) f (W j))
    (hP : ApproximatesTrace q P g (atom false) E) (hQ : ApproximatesTrace q Q g (atom true) E)
    (bits : Fin m → Bool) (θ : Fin n → Bool) :
    ApproximatesTrace q
      ((M.reportsGiven bits).prod ((FiniteLaw.coordinateProduct R).prod (selectedLeafLaw P Q θ)))
…

Mentions: OAI.TraceReconstruction.EmissionSlot, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.SimulatesTrace, OAI.TraceReconstruction.ApproximatesTrace, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.PairedMechanisms.selectedLeafLaw

theorem OAI.TraceReconstruction.PairedMechanisms.canonical_filled_expect line 229

Source documentation

The actual metadata-first oracle with independent genuine fillers has exactly the orientation-first product experiment, in the displayed order.

theorem canonical_filled_expect (R : Fin k → FiniteLaw Side) (P Q : FiniteLaw Leaf)
    (θ : (Fin m → Bool) → Fin n → Bool)
    (F : Reports Side m × (Fin k → Side) × (Fin n → Leaf) → ℝ) :
    ((M.canonicalOracle P Q θ).prod (FiniteLaw.coordinateProduct R)).expect
      (fun x => F (x.1.1,x.2,x.1.2))=
    (fairOrientations m).expect (fun bits =>
      ((M.reportsGiven bits).prod ((FiniteLaw.coordinateProduct R).prod
        (selectedLeafLaw P Q (θ bits)))).expect F) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.PairedMechanisms.fairOrientations, OAI.TraceReconstruction.PairedMechanisms.selectedLeafLaw

theorem OAI.TraceReconstruction.PairedMechanisms.canonical_filled_simulation line 248

Source documentation

Unconditional common simulation of the actual full canonical oracle. The only layout charge is the unconditional fair-orientation failure mass. No orientation or side metadata is conditioned on successful fitting.

theorem canonical_filled_simulation {q E : ℝ} (hq : q∈Set.Icc 0 1) (hE : 0≤E)
    {L : ℕ} (e : Fin L ≃ EmissionSlot m k n)
    (R : Fin k → FiniteLaw Side) (P Q : FiniteLaw Leaf)
    (f : Side → List Bool) (g : Leaf → List Bool) (U V : Fin m → List Bool)
    (W : Fin k → List Bool) (atom : Bool → List Bool)
    (hU : ∀j,SimulatesTrace q (M.first j) f (U j))
    (hV : ∀j,SimulatesTrace q (M.second j) f (V j))
    (hW : ∀j,SimulatesTrace q (R j) f (W j))
    (hP : ApproximatesTrace q P g (atom false) E) (hQ : ApproximatesTrace q Q g (atom true) E)
    (θ : (Fin m → Bool) → Fin n → Bool) (w : List Bool)
    (good : (Fin m → Bool) → Prop) [DecidablePred good]
    (hword : ∀bits,good bits → coordinateWord
…

theorem OAI.TraceReconstruction.source_motif_central line 309
Source documentation
The one-based source offset still puts the complete motif in the central third under the true fit threshold. The stronger numerical margin is an eventual consequence of L=o(T), not an additional stochastic event.
```
theorem source_motif_central (T t s : ℕ) (bits : Fin t → Bool) (v : ℤ)
    (hT : 24 ≤ T) (he : Even T) (hL : 24*2^s ≤ T)
    (hfit : |8*((∑i,(bitIndex (bits i):ℤ))-(t/2:ℕ)+v)| ≤ (T:ℤ))
    (u : Fin T)
    (hu : motifIndicator s ((u.val:ℤ)-((T/2:ℕ)-1+(t/2:ℕ))+
      (∑i,(bitIndex (bits i):ℤ))+v)≠0) : u∈centralThird T := by
…
```
Mentions: OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.motifIndicator, OAI.TraceReconstruction.centralThird

theorem OAI.TraceReconstruction.sourceTreeFit_central line 330

Source documentation

Fit controls every internal source motif, retaining all orientations in the law. The incoming displacement of the root is supplied separately.

theorem sourceTreeFit_central (T n : ℕ → ℕ) (s b : ℕ)
    (center : ℕ → ℤ) (hc : ∀j≤b,center j=sourceLocalCenter T n j)
    (hT : ∀j≤b,24≤T j) (he : ∀j≤b,Even (T j)) (hL : ∀j≤b,24*2^s≤T j)
    (bits : WindowAssignments T n (sourceScheduledTrials T n) Bool (b+1)) (incoming : ℤ)
    (hroot : |8*((∑i,(bitIndex (bits.1 i):ℤ))-(n b/2:ℕ)+incoming)|≤(T b:ℤ))
    (hfit : SourceTreeFit T n (b+1) bits) :
    SourceCentral T n (sourceScheduledTrials T n) s center (sourceScheduledShift T n)
      (fun j => centralThird (T j)) (b+1) bits incoming := by
…

Mentions: OAI.TraceReconstruction.sourceLocalCenter, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.SourceCentral, OAI.TraceReconstruction.sourceScheduledShift, OAI.TraceReconstruction.centralThird

theorem OAI.TraceReconstruction.source_root_fit line 359
Source documentation
The actual root side count has no parity restriction. Its entire range lies inside the fit displacement interval when J=o(T).
```
theorem source_root_fit (T J : ℕ) (bits : Fin J → Bool) (h : 4*(J+1)≤T) :
    |8*((∑i,(bitIndex (bits i):ℤ))-(J/2:ℕ))|≤(T:ℤ) := by
…
```
Mentions: OAI.TraceReconstruction.bitIndex
theorem OAI.TraceReconstruction.sourceNoncentralMass_le_fit line 372

theorem OAI.TraceReconstruction.sourceTreeWord_eq_center_interior line 399

Source documentation

Only interior trials are paired in even bundles. The top J may be odd.

theorem sourceTreeWord_eq_center_interior (s : ℕ) (P T n h : ℕ → ℕ) (center : ℕ → ℤ)
    (atom : Bool → List Bool) (b : ℕ) (H : SourceLayoutMargins s P T n h (b-1))
    (htop : ∀j<b,0<T j)
    (hc : ∀j, j+1<b → center j=sourceLocalCenter T n j)
    (bits : WindowAssignments T n (sourceScheduledTrials T n) Bool b)
    (incoming : ℤ) (τ : Bool) (hfit : SourceTreeFit T n b bits) :
    sourceTreeWord s P T n h center atom b bits incoming τ=
      sourceCenterWord s P T n center atom b bits incoming τ := by
…

Mentions: OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.sourceLocalCenter, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.sourceTreeWord, OAI.TraceReconstruction.sourceCenterWord

def OAI.TraceReconstruction.sourceFullWord line 481
Source documentation
Full literal unconditioned root partition, including both members of every outer paired side. Its top trial count is the source's J, even or odd.
```
def sourceFullWord (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b : ℕ)
    (bits : WindowAssignments T n (sourceScheduledTrials T n) Bool (b+1)) (τ : Bool) : List Bool :=
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials
theorem OAI.TraceReconstruction.bitIndex_sum_le line 487

theorem OAI.TraceReconstruction.sourceFullWord_eq_block line 497

Source documentation

The source root's floor anchor and paired side counts have their literal unmarked word interpretation, without requiring J to be even.

theorem sourceFullWord_eq_block (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool)
    (b : ℕ) (H : SourceLayoutMargins s P T n h b) (hpos : 0<T b)
    (hroot : P b=n b*(2*h b+1)+T b) (he : Even (T b))
    (hJ : 4*(n b+1)≤T b) (hL : 8*2^s≤T b)
    (bits : WindowAssignments T n (sourceScheduledTrials T n) Bool (b+1))
    (τ : Bool) (hfit : SourceTreeFit T n (b+1) bits) :
    sourceFullWord s P T n h atom b bits τ=sourceBlockWord s P atom (b+1) τ := by
…

Mentions: OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.sourceFullWord, OAI.TraceReconstruction.sourceBlockWord

def OAI.TraceReconstruction.WindowFiller line 559
Source documentation
Pure filler IDs. At bottom leaf windows the two fillers have zero length; they are deterministic empty outputs, not extra information.
```
def WindowFiller (T : ℕ → ℕ) : ℕ → Type
  | 0 => PEmpty
  | b+1 => (Fin (T b) × Bool) ⊕ (Fin (T b) × WindowFiller T b)
```
instance OAI.TraceReconstruction.windowFillerFintype line 563
abbrev OAI.TraceReconstruction.TreeEmission line 569
def OAI.TraceReconstruction.TreeEmission.up line 572
def OAI.TraceReconstruction.treeLocalSlots line 578
def OAI.TraceReconstruction.treeGlobalSlots line 581

def OAI.TraceReconstruction.treeChronology line 589

Source documentation

Public chronological IDs. Each child carries its own local paired sides; the group's global sides and deterministic fillers surround that child. The order is fixed independently of all bits and both hypotheses.

def treeChronology (T n g : ℕ → ℕ)
    (pre post : (b : ℕ) → Fin (g b) → Fin (T b)) :
    (b : ℕ) → List (TreeEmission T n g b)
  | 0 => [.inr (.inr (show WindowLeaf T 0 from (0 : Fin 1)))]
  | b+1 => treeLocalSlots T n g b false ++
      (List.ofFn (fun u : Fin (T b) =>
        treeGlobalSlots T n g b false (pre b) u ++
        [.inr (.inl (.inl (u,false)))] ++
        (treeChronology T n g pre post b).map (TreeEmission.up T n g b u) ++
        treeGlobalSlots T n g b true (post b) u ++
        [.inr (.inl (.inl (u,true)))])).flatten ++
      treeLocalSlots T n g b true

Mentions: OAI.TraceReconstruction.TreeEmission, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.treeLocalSlots, OAI.TraceReconstruction.treeGlobalSlots, OAI.TraceReconstruction.TreeEmission.up

theorem OAI.TraceReconstruction.sum_fiber_list_length line 602
theorem OAI.TraceReconstruction.treeChronology_length line 614
theorem OAI.TraceReconstruction.treeChronology_mem line 634
theorem OAI.TraceReconstruction.treeChronology_nodup line 682
def OAI.TraceReconstruction.treeChronologyEquiv line 696
Source documentation
A genuine complete chronological bijection, not an assumed layout.
```
def treeChronologyEquiv (T n g : ℕ → ℕ)
    (pre post : (b : ℕ) → Fin (g b) → Fin (T b)) (b : ℕ) :
    Fin (treeChronology T n g pre post b).length ≃ TreeEmission T n g b :=
…
```
Mentions: OAI.TraceReconstruction.treeChronology, OAI.TraceReconstruction.TreeEmission
def OAI.TraceReconstruction.pairedSideCount line 710
theorem OAI.TraceReconstruction.pairedSideCount_false line 712
theorem OAI.TraceReconstruction.pairedSideCount_true line 715
theorem OAI.TraceReconstruction.pairedSideCount_sum_pre line 718
theorem OAI.TraceReconstruction.pairedSideCount_sum_total line 723
theorem OAI.TraceReconstruction.pairedSideCount_sum_post line 733
def OAI.TraceReconstruction.sourceGlobalPre line 740
Source documentation
Global trial positions are ID functions, not positions inferred from a realized output or orientation.
```
def sourceGlobalPre (N t : ℕ) (k : Fin ((N/4)*t)) : Fin N :=
…
```
def OAI.TraceReconstruction.sourceGlobalPost line 744
theorem OAI.TraceReconstruction.sum_globalSides line 748
theorem OAI.TraceReconstruction.sourcePreCount_slots line 762
theorem OAI.TraceReconstruction.sourcePostCount_slots line 792

theorem OAI.TraceReconstruction.filter_chunks_flatten line 826

Source documentation

Flattening selected equal-atom chunks sums exactly their genuine lengths.

theorem filter_chunks_flatten {ι : Type*} [Fintype ι] [DecidableEq ι]
    (l : List ι) (p : ι → Bool) (c : ι → ℕ) (w : List Bool) :
    ((l.filter p).map (fun i => pureAtomRun w (c i))).flatten=
      pureAtomRun w ((l.map (fun i => if p i then c i else 0)).sum) := by
…

Mentions: OAI.TraceReconstruction.pureAtomRun

def OAI.TraceReconstruction.sourceScheduledPre line 847
def OAI.TraceReconstruction.sourceScheduledPost line 852

def OAI.TraceReconstruction.sourceTrialWord line 858

Source documentation

Two actual deterministic pure binary side words for each paired trial ID.

def sourceTrialWord (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) :
    (b : ℕ) → WindowTrial T n (sourceScheduledTrials T n) b → Bool → List Bool
  | 0,i,_ => PEmpty.elim i
  | b+1,.inl _,c => pureAtomRun (sourceBlockWord s P atom b false) (h b+bitIndex c)
  | 1,.inr (.inl k),_ => Fin.elim0 k
  | b+2,.inr (.inl _),c => pureAtomRun (sourceBlockWord s P atom b false) (h b+bitIndex c)
  | b+1,.inr (.inr (_,i)),c => sourceTrialWord s P T n h atom b i c

/-- Fixed pure fillers, including the deterministic empty bottom fillers. -/

Mentions: OAI.TraceReconstruction.WindowTrial, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourceBlockWord, OAI.TraceReconstruction.bitIndex

def OAI.TraceReconstruction.sourceFillerWord line 867

Source documentation

Fixed pure fillers, including the deterministic empty bottom fillers.

def sourceFillerWord (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) :
    (b : ℕ) → WindowFiller T b → List Bool
  | 0,i => PEmpty.elim i
  | b+1,.inl (u,p) => match b,u with
    | 0,_ => []
    | b+1,u => pureAtomRun (sourceBlockWord s P atom b false)
        (if p then sourcePostFiller (T (b+1)) (sourceNominalPost P T b) (n b) (h b) u
          else sourcePreFiller (T (b+1)) (sourceNominalPre P T b) (n b) (h b) u)
  | b+1,.inr (_,i) => sourceFillerWord s P T n h atom b i

Mentions: OAI.TraceReconstruction.WindowFiller, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourceBlockWord, OAI.TraceReconstruction.sourcePostFiller, OAI.TraceReconstruction.sourceNominalPost, OAI.TraceReconstruction.sourcePreFiller, OAI.TraceReconstruction.sourceNominalPre

def OAI.TraceReconstruction.sourceSlotWord line 877
def OAI.TraceReconstruction.sourceChronologicalWord line 885
theorem OAI.TraceReconstruction.sourceSlotWord_up line 891
theorem OAI.TraceReconstruction.treeChronology_eval line 899
theorem OAI.TraceReconstruction.sourceLocalSlots_word line 921
theorem OAI.TraceReconstruction.sourceGlobalSlots_word line 933
def OAI.TraceReconstruction.sourceFramedWord line 956
theorem OAI.TraceReconstruction.sourceChronologicalWord_eq_framed line 964
theorem OAI.TraceReconstruction.sourceChronologicalWord_eq_block line 1028
Source documentation
Chronological side/filler/leaf slots produce the SAME full source word on the joint fit event. No orientation is removed or conditioned away.
```
theorem sourceChronologicalWord_eq_block (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool)
    (b : ℕ) (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)
    (bits : WindowAssignments T n (sourceScheduledTrials T n) Bool (b+1)) (τ : Bool)
    (hfit : SourceTreeFit T n (b+1) bits) :
    sourceChronologicalWord s P T n h (sourceLocalCenter T n) atom (b+1) bits 0 τ=
      sourceBlockWord s P atom (b+1) τ := by
…
```
Mentions: OAI.TraceReconstruction.SourceLayoutMargins, OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.sourceChronologicalWord, OAI.TraceReconstruction.sourceLocalCenter, OAI.TraceReconstruction.sourceBlockWord
def OAI.TraceReconstruction.finEnumeration line 1050
abbrev OAI.TraceReconstruction.SourceTrialCount line 1052
abbrev OAI.TraceReconstruction.SourceFillerCount line 1053
abbrev OAI.TraceReconstruction.SourceLeafCount line 1054
def OAI.TraceReconstruction.sourceEmissionEnum line 1056
def OAI.TraceReconstruction.sourceAssignmentCode line 1062
theorem OAI.TraceReconstruction.sourceAssignmentCode_eval line 1072
def OAI.TraceReconstruction.sourceChronologyCode line 1079
def OAI.TraceReconstruction.sourceFlatLeafType line 1085
def OAI.TraceReconstruction.sourceFlatTrialWord line 1089
def OAI.TraceReconstruction.sourceFlatFillerWord line 1093
theorem OAI.TraceReconstruction.sourceSlotWord_code line 1097
theorem OAI.TraceReconstruction.treeChronologyEquiv_word line 1114
theorem OAI.TraceReconstruction.source_slotCode_word line 1126
theorem OAI.TraceReconstruction.source_fair_code_expect line 1146
Source documentation
Reindex the genuine independent orientations, retaining the whole source tree.
```
theorem source_fair_code_expect (T n : ℕ → ℕ) (b : ℕ)
    (F : WindowAssignments T n (sourceScheduledTrials T n) Bool b → ℝ) :
    (PairedMechanisms.fairOrientations (SourceTrialCount T n b)).expect
      (fun bits => F ((sourceAssignmentCode T n Bool b).symm bits)) =
    (windowPosteriorLaw T n (sourceScheduledTrials T n) b
      (noReveals T n (sourceScheduledTrials T n) b)).expect F := by
…
```
Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.PairedMechanisms.fairOrientations, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.sourceAssignmentCode, OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.noReveals
theorem OAI.TraceReconstruction.sourceTreeFit_tail_interior line 1161
Source documentation
The fit event uses only interior even bundles. In particular no parity assumption is made on the top root count J.
```
theorem sourceTreeFit_tail_interior (T n : ℕ → ℕ) (b : ℕ)
    (hn : ∀j,j+1<b → 0<n j) (he : ∀j,j+1<b → Even (n j)) :
    (windowPosteriorLaw T n (sourceScheduledTrials T n) b
      (noReveals T n (sourceScheduledTrials T n) b)).expect
        (fun bits => if SourceTreeFit T n b bits then 0 else 1) ≤ sourceFitTail T n b := by
…
```
Mentions: OAI.TraceReconstruction.windowPosteriorLaw, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.noReveals, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.sourceFitTail
theorem OAI.TraceReconstruction.source_flat_fit_tail line 1241
Source documentation
Honest source joint-fit failure after the actual finite coding.
```
theorem source_flat_fit_tail (T n : ℕ → ℕ) (b : ℕ)
    (hn : ∀j,j+1<b → 0<n j) (he : ∀j,j+1<b → Even (n j)) :
    (PairedMechanisms.fairOrientations (SourceTrialCount T n b)).expect
      (fun bits => if SourceTreeFit T n b ((sourceAssignmentCode T n Bool b).symm bits) then 0 else 1)
      ≤ sourceFitTail T n b := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms.fairOrientations, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceTreeFit, OAI.TraceReconstruction.sourceAssignmentCode, OAI.TraceReconstruction.sourceFitTail
def OAI.TraceReconstruction.sourceOracleDecode line 1251
Source documentation
A fixed public decoder. It does not know the hidden orientations or the input hypothesis, and it drops rather than reveals all pairing flags.
```
def sourceOracleDecode {Side Leaf : Type} (T n : ℕ → ℕ) (b : ℕ)
    (f : Side → List Bool) (g : Leaf → List Bool) :
    ((Reports Side (SourceTrialCount T n b) × (Fin (SourceLeafCount T b) → Leaf)) ×
      (Fin (SourceFillerCount T b) → Side)) → List Bool := fun x =>
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.SourceTrialCount, OAI.TraceReconstruction.SourceLeafCount, OAI.TraceReconstruction.SourceFillerCount

theorem OAI.TraceReconstruction.source_canonical_simulation line 1262

Source documentation

The complete canonical oracle now simulates the LITERAL source block. All IDs, words, leaf types and chronology instantiate the actual construction. The only failed-layout cost is its original unconditional fair-bit mass.

theorem source_canonical_simulation {Side Leaf : Type} [Fintype Side] [Fintype Leaf]
    {q E : ℝ} (hq : q∈Set.Icc 0 1) (hE : 0≤E)
    (s : ℕ) (P T n h : ℕ → ℕ) (atom : Bool → List Bool) (b : ℕ)
    (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