Layout.lean`

76 declarations, 0 contain sorry, 0 declared as axioms

Layout

Multiwindow and paired layouts, coordinate simulations, and literal source types and trees.

def OAI.TraceReconstruction.framedConcat line 24
Source documentation
Literal unmarked concatenation of fixed windows with separately reported pure pre/post regions. Counts are in atoms, not surviving trace symbols.
```
def framedConcat {α : Type*} (e : α) {k : ℕ}
    (pre post : Fin k → ℕ) (W : Fin k → List α) : List α :=
…
```
theorem OAI.TraceReconstruction.framedConcat_succ line 29

theorem OAI.TraceReconstruction.framedConcat_eq_of_gaps line 38

Source documentation

Only the first, last, and intervening pure lengths are observable in an unmarked word. In particular boundaries may jitter across nominal units.

theorem framedConcat_eq_of_gaps {α : Type*} (e : α) (k : ℕ)
    (pre post pre' post' : Fin (k+1) → ℕ) (W : Fin (k+1) → List α)
    (u u' : ℕ) (hfirst : u+pre 0=u'+pre' 0)
    (hgap : ∀i : Fin k, post i.castSucc+pre i.succ=post' i.castSucc+pre' i.succ)
    (hlast : post (Fin.last k)=post' (Fin.last k)) :
    List.replicate u e ++ framedConcat e pre post W =
      List.replicate u' e ++ framedConcat e pre' post' W := by
…

Mentions: OAI.TraceReconstruction.framedConcat

def OAI.TraceReconstruction.framePrefix line 71
Source documentation
Number of atoms strictly before the indicated padded unit.
```
def framePrefix {k : ℕ} (pre post : Fin k → ℕ) (len : Fin k → ℕ) (i : ℕ) : ℕ :=
…
```
theorem OAI.TraceReconstruction.framePrefix_zero line 74
theorem OAI.TraceReconstruction.framePrefix_step line 77

theorem OAI.TraceReconstruction.framedConcat_eq_of_starts line 94

Source documentation

Equal actual starting positions and equal total counts are enough: there is no requirement that a part coincide with its nominal unit.

theorem framedConcat_eq_of_starts {α : Type*} (e : α) (k : ℕ)
    (pre post pre' post' : Fin (k+1) → ℕ) (W : Fin (k+1) → List α)
    (hstart : ∀i : Fin (k+1),
      framePrefix pre post (fun j => (W j).length) i.val+pre i=
      framePrefix pre' post' (fun j => (W j).length) i.val+pre' i)
    (htotal : framePrefix pre post (fun j => (W j).length) (k+1)=
      framePrefix pre' post' (fun j => (W j).length) (k+1)) :
    framedConcat e pre post W=framedConcat e pre' post' W := by
…

Mentions: OAI.TraceReconstruction.framePrefix, OAI.TraceReconstruction.framedConcat

theorem OAI.TraceReconstruction.framePrefix_constant line 125
theorem OAI.TraceReconstruction.flatten_framedConcat line 136

theorem OAI.TraceReconstruction.template_group_windows line 151

Source documentation

The deterministic multiwindow identity used by the nested simulator. Every motif is covered by its own window. Predetermined pure-region lengths may move the boundaries of nominal units; only their exact cumulative counts are required. Windows and chunks all remain literal unmarked binary words.

theorem template_group_windows (k P T a L : ℕ) (sign : Fin L → Bool)
    (w : Bool → List Bool) (τ : Fin (k+1) → Bool)
    (t pre post : Fin (k+1) → ℕ)
    (hleft : ∀u,t u ≤ a) (hfit : ∀u,a+L ≤ t u+T)
    (hunit : ∀u,t u+T ≤ P)
    (hstart : ∀u,framePrefix pre post (fun _ => T) u.val+pre u=u.val*P+t u)
    (htotal : framePrefix pre post (fun _ => T) (k+1)=(k+1)*P) :
    (List.ofFn (fun u => complementaryWords P a L sign w (τ u))).flatten=
      (List.ofFn (fun u => pureAtomRun (w false) (pre u) ++
        complementaryWords T (a-t u) L sign w (τ u) ++
        pureAtomRun (w false) (post u))).flatten := by
…

Mentions: OAI.TraceReconstruction.framePrefix, OAI.TraceReconstruction.complementaryWords, OAI.TraceReconstruction.pureAtomRun

def OAI.TraceReconstruction.pairedPreCount line 195
Source documentation
Counts of literal side chunks, with one deterministic pure filler in each region. A bundle can contain any even number of paired chunks.
```
def pairedPreCount {N : ℕ} (left : K → Fin N) (filler : Fin N → ℕ)
    (first : K → ℕ) (u : Fin N) : ℕ :=
…
```
def OAI.TraceReconstruction.pairedPostCount line 199
theorem OAI.TraceReconstruction.pairedPreCount_cast line 203
theorem OAI.TraceReconstruction.pairedPostCount_cast line 221
theorem OAI.TraceReconstruction.fin_prefix_delta line 243
Source documentation
Prefix sum of a delta at a prescribed label, with no loss from replacing its real finite support by an interval.
```
theorem fin_prefix_delta {N : ℕ} (a : Fin N) (i : ℕ) (x : ℤ) :
    (∑u : Fin N, if u.val < i then (if a=u then x else 0) else 0)=
      if a.val < i then x else 0 := by
…
```

theorem OAI.TraceReconstruction.pair_activity_identity line 256

Source documentation

Exact paired-interval contribution to the position of a window.

theorem pair_activity_identity {N : ℕ} (l r u : Fin N) (hlr : l.val ≤ r.val) (x : ℤ) :
    (if l.val < u.val then x else 0)-(if r.val < u.val then x else 0)+
      (if l=u then x else 0) =
      if l.val ≤ u.val ∧ u.val ≤ r.val then x else 0 := by
…

theorem OAI.TraceReconstruction.pairedLayout_start line 271

Source documentation

Cumulative pure chunk counts have exactly the source's localBits-plus-active- globalBits jitter. This identity uses the actual chronological pre/post schedule.

theorem pairedLayout_start {N : ℕ} (left right : K → Fin N)
    (horder : ∀v,(left v).val ≤ (right v).val)
    (fpre fpost : Fin N → ℕ) (reserve first : K → ℕ)
    (hfirst : ∀v,first v ≤ 2*reserve v) (A B T : ℕ)
    (hpre : ∀u,fpre u+(∑v,if left v=u then reserve v else 0)=A)
    (hpost : ∀u,fpost u+(∑v,if right v=u then reserve v else 0)=B)
    (u : Fin N) :
    ((framePrefix (pairedPreCount left fpre first)
      (pairedPostCount right fpost reserve first) (fun _ => T) u.val+
      pairedPreCount left fpre first u : ℕ):ℤ)=
      u.val*(A+T+B)+A+
        ∑v, if (left v).val ≤ u.val ∧ u.val ≤ (right v).val then
…

Mentions: OAI.TraceReconstruction.framePrefix, OAI.TraceReconstruction.pairedPreCount, OAI.TraceReconstruction.pairedPostCount

theorem OAI.TraceReconstruction.pairedLayout_total line 333
abbrev OAI.TraceReconstruction.SourceBundle line 357
Source documentation
One localBits bundle at each child, and one globalBits bundle at each vertex in the first quarter, paired with the reflected last-quarter post region.
```
abbrev SourceBundle (N : ℕ) := Fin N ⊕ Fin (N/4)
```
def OAI.TraceReconstruction.sourceBundleLeft line 359
def OAI.TraceReconstruction.sourceBundleRight line 363
theorem OAI.TraceReconstruction.sourceBundle_order line 367
theorem OAI.TraceReconstruction.sum_injective_delta_le line 373
theorem OAI.TraceReconstruction.sourceBundle_reserve_pre line 383
theorem OAI.TraceReconstruction.sourceBundle_reserve_post line 394
def OAI.TraceReconstruction.sourceBundleCount line 412
theorem OAI.TraceReconstruction.sourceBundleCount_le line 417
theorem OAI.TraceReconstruction.sourceBundle_activity line 431
Source documentation
The actual scheduled bits give precisely the arithmetic source displacement Y=H+V, including its common-globalBits plateau and outer-quarter behavior.
```
theorem sourceBundle_activity (N t h : ℕ)
    (localBits : Fin N → Fin t → Bool) (globalBits : Fin ((N/4)*t) → Bool) (u : Fin N) :
    (∑v : SourceBundle N, if (sourceBundleLeft N v).val ≤ u.val ∧
        u.val ≤ (sourceBundleRight N v).val then
      (sourceBundleCount N t h localBits globalBits v:ℤ)-(t*h+t/2:ℕ) else 0)=
      ((∑a : Fin t,(bitIndex (localBits u a):ℤ))-(t/2:ℕ))+
        scheduledGlobalShift N t globalBits u := by
…
```
Mentions: OAI.TraceReconstruction.SourceBundle, OAI.TraceReconstruction.sourceBundleLeft, OAI.TraceReconstruction.sourceBundleRight, OAI.TraceReconstruction.sourceBundleCount, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.scheduledGlobalShift
def OAI.TraceReconstruction.sourceLayoutReserve line 477
Source documentation
One-bundle reserved nominal count is integral because the number of paired trials is even. The actual filler reserves both local and global bundles when both are present in a region.
```
def sourceLayoutReserve (t h : ℕ) : ℕ := t*h+t/2
```
def OAI.TraceReconstruction.sourcePreFiller line 479
def OAI.TraceReconstruction.sourcePostFiller line 482
def OAI.TraceReconstruction.sourcePreCount line 485
def OAI.TraceReconstruction.sourcePostCount line 490
def OAI.TraceReconstruction.sourceDisplacement line 495
def OAI.TraceReconstruction.sourceWindowStart line 499
theorem OAI.TraceReconstruction.sourcePreFiller_nominal line 503
theorem OAI.TraceReconstruction.sourcePostFiller_nominal line 509
theorem OAI.TraceReconstruction.sourceLayout_exact_start line 515
theorem OAI.TraceReconstruction.sourceLayout_exact_total line 530

theorem OAI.TraceReconstruction.sourceLayout_literal_partition line 544

Source documentation

The literal surrogate side chunks, after concatenation, are a correct partition of the actual parent word whenever the windows fit. This is an equality of unmarked binary strings, not an assumed channel identity.

theorem sourceLayout_literal_partition (k A T B t h a L : ℕ) (ht : Even t)
    (hA : 2*sourceLayoutReserve t h ≤ A) (hB : 2*sourceLayoutReserve t h ≤ B)
    (loc : Fin (k+1) → Fin t → Bool) (glob : Fin (((k+1)/4)*t) → Bool)
    (sign : Fin L → Bool) (w : Bool → List Bool) (τ : Fin (k+1) → Bool)
    (hzero : ∀u,0 ≤ (A:ℤ)+sourceDisplacement (k+1) t loc glob u)
    (hleft : ∀u,sourceWindowStart (k+1) A t loc glob u ≤ a)
    (hfit : ∀u,a+L ≤ sourceWindowStart (k+1) A t loc glob u+T)
    (hunit : ∀u,sourceWindowStart (k+1) A t loc glob u+T ≤ A+T+B) :
    (List.ofFn (fun u => complementaryWords (A+T+B) a L sign w (τ u))).flatten=
      (List.ofFn (fun u => pureAtomRun (w false) (sourcePreCount (k+1) A t h loc glob u) ++
        complementaryWords T (a-sourceWindowStart (k+1) A t loc glob u) L sign w (τ u) ++
        pureAtomRun (w false) (sourcePostCount (k+1) B t h loc glob u))).flatten := by
…

Mentions: OAI.TraceReconstruction.sourceLayoutReserve, OAI.TraceReconstruction.sourceDisplacement, OAI.TraceReconstruction.sourceWindowStart, OAI.TraceReconstruction.complementaryWords, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.sourcePreCount, OAI.TraceReconstruction.sourcePostCount

theorem OAI.TraceReconstruction.coordinateProduct_approximates line 576

Source documentation

Independent emissions at all literal slots accumulate their actual approximation errors. The decoders may depend on the fixed slot ID.

theorem coordinateProduct_approximates {α : Type*} [Fintype α]
    {n : ℕ} {q : ℝ} (hq : q∈Set.Icc 0 1) (P : Fin n → FiniteLaw α)
    (f : Fin n → α → 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.coordinateProduct 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.coordinateProduct, OAI.TraceReconstruction.coordinateWord

def OAI.TraceReconstruction.FiniteLaw.indexedProduct line 606
Source documentation
Independent emissions indexed by the actual token IDs of the layout.
```
def indexedProduct (P : ι → FiniteLaw α) : FiniteLaw (ι → α) where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.FiniteLaw.indexedProduct_expect_equiv line 615
Source documentation
Reorder independent emissions by the literal chronological slot order. The order is a bijection, so no output is duplicated or silently discarded.
```
theorem indexedProduct_expect_equiv (P : ι → FiniteLaw α) (e : κ ≃ ι)
    (F : (ι → α) → ℝ) :
    (indexedProduct P).expect F=(indexedProduct (fun j => P (e j))).expect
      (fun x => F (fun i => x (e.symm i))) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.indexedProduct, OAI.TraceReconstruction.FiniteLaw.expect
theorem OAI.TraceReconstruction.FiniteLaw.indexedProduct_map line 633

theorem OAI.TraceReconstruction.indexedProduct_approximates line 661

Source documentation

An arbitrarily indexed actual layout has the same unconditional trace guarantee after its fixed, public chronological ordering is applied.

theorem indexedProduct_approximates {ι α : Type*} [Fintype ι] [Fintype α]
    {n : ℕ} {q : ℝ} (hq : q∈Set.Icc 0 1) (e : Fin n ≃ ι)
    (P : ι → FiniteLaw α) (f : ι → α → List Bool) (w : ι → List Bool) (E : ι → ℝ)
    (h : ∀i,ApproximatesTrace q (P i) (f i) (w i) (E i)) :
    ApproximatesTrace q (FiniteLaw.indexedProduct 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.indexedProduct, OAI.TraceReconstruction.coordinateWord

def OAI.TraceReconstruction.boolTypeSign line 689
Source documentation
The Boolean representation of the source Prouhet signs; true denotes a negative type. No sign convention is changed in passing to literal words.
```
def boolTypeSign (b : Bool) : ℝ := if b then -1 else 1
```
def OAI.TraceReconstruction.prouhetBool line 691
theorem OAI.TraceReconstruction.boolTypeSign_injective line 694
theorem OAI.TraceReconstruction.boolTypeSign_template line 698
theorem OAI.TraceReconstruction.sourceWindowStart_cast_of_fit line 715

theorem OAI.TraceReconstruction.sourceWindowStart_fit line 726

Source documentation

A zero-based centered version of the floor-fit calculation.

theorem sourceWindowStart_fit (N P T t L : ℕ)
    (loc : Fin N → Fin t → Bool) (glob : Fin ((N/4)*t) → Bool)
    (hP : 2*T ≤ P) (hT : 16 ≤ T) (heven : Even T) (hL : 8*L ≤ T)
    (u : Fin N) (hY : |8*sourceDisplacement N t loc glob u| ≤ (T:ℤ)) :
    sourceWindowStart N ((P-T)/2) t loc glob u+T ≤ P ∧
    sourceWindowStart N ((P-T)/2) t loc glob u ≤ P/2 ∧
    P/2+L ≤ sourceWindowStart N ((P-T)/2) t loc glob u+T :=
…

Mentions: OAI.TraceReconstruction.sourceDisplacement, OAI.TraceReconstruction.sourceWindowStart

theorem OAI.TraceReconstruction.sourceWindowStart_anchor line 737

Source documentation

The zero-based centered translated anchor, including both half-trial corrections.

theorem sourceWindowStart_anchor (N P T t L : ℕ)
    (loc : Fin N → Fin t → Bool) (glob : Fin ((N/4)*t) → Bool)
    (hP : 2*T ≤ P) (hT : 16 ≤ T) (heven : Even T) (hL : 8*L ≤ T)
    (u : Fin N) (hY : |8*sourceDisplacement N t loc glob u| ≤ (T:ℤ)) :
    ((P/2-sourceWindowStart N ((P-T)/2) t loc glob u:ℕ):ℤ)=
      (T/2:ℕ)+(t/2:ℕ)-(∑a : Fin t,(bitIndex (loc u a):ℤ))-
        scheduledGlobalShift N t glob u := by
…

Mentions: OAI.TraceReconstruction.sourceDisplacement, OAI.TraceReconstruction.sourceWindowStart, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.scheduledGlobalShift

theorem OAI.TraceReconstruction.sourceWindowStart_oneBased_fit line 755

Source documentation

The manuscript numbers motif slots from one. Thus its actual zero-based onset is P/2-1, not P/2. The strict margins include this endpoint correction.

theorem sourceWindowStart_oneBased_fit (N P T t L : ℕ)
    (loc : Fin N → Fin t → Bool) (glob : Fin ((N/4)*t) → Bool)
    (hP : 2*T ≤ P) (hT : 16 ≤ T) (heven : Even T) (hL : 8*L ≤ T)
    (u : Fin N) (hY : |8*sourceDisplacement N t loc glob u| ≤ (T:ℤ)) :
    sourceWindowStart N ((P-T)/2) t loc glob u+T ≤ P ∧
    sourceWindowStart N ((P-T)/2) t loc glob u ≤ P/2-1 ∧
    P/2-1+L ≤ sourceWindowStart N ((P-T)/2) t loc glob u+T := by
…

Mentions: OAI.TraceReconstruction.sourceDisplacement, OAI.TraceReconstruction.sourceWindowStart

theorem OAI.TraceReconstruction.sourceWindowStart_oneBased_anchor line 769

Source documentation

The exact source anchor in zero-based coordinates. The minus one is forced by the one-based motif-label convention.

theorem sourceWindowStart_oneBased_anchor (N P T t L : ℕ)
    (loc : Fin N → Fin t → Bool) (glob : Fin ((N/4)*t) → Bool)
    (hP : 2*T ≤ P) (hT : 16 ≤ T) (heven : Even T) (hL : 8*L ≤ T)
    (u : Fin N) (hY : |8*sourceDisplacement N t loc glob u| ≤ (T:ℤ)) :
    ((P/2-1-sourceWindowStart N ((P-T)/2) t loc glob u:ℕ):ℤ)=
      (T/2:ℕ)-1+(t/2:ℕ)-(∑a : Fin t,(bitIndex (loc u a):ℤ))-
        scheduledGlobalShift N t glob u := by
…

Mentions: OAI.TraceReconstruction.sourceDisplacement, OAI.TraceReconstruction.sourceWindowStart, OAI.TraceReconstruction.bitIndex, OAI.TraceReconstruction.scheduledGlobalShift

def OAI.TraceReconstruction.sourceBlockWord line 782
Source documentation
The actual recursively substituted source block words. Indices in P are shifted down by one, but physical binary strings are unchanged.
```
def sourceBlockWord (s : ℕ) (P : ℕ → ℕ) (atom : Bool → List Bool) : ℕ → Bool → List Bool
  | 0 => atom
  | j+1 => complementaryWords (P j) (P j/2-1) (2^s) (prouhetBool s)
      (sourceBlockWord s P atom j)
```
Mentions: OAI.TraceReconstruction.complementaryWords, OAI.TraceReconstruction.prouhetBool
def OAI.TraceReconstruction.sourceBlockLength line 787
theorem OAI.TraceReconstruction.sourceBlockWord_length line 791
theorem OAI.TraceReconstruction.sourceBlockWord_injective line 798
def OAI.TraceReconstruction.integerTemplateType line 820
Source documentation
Total Boolean type, also on failed layouts; no conditioning is hidden in the definition.
```
def integerTemplateType (N s : ℕ) (X : ℤ) (τ : Bool) (u : Fin N) : Bool :=
…
```
theorem OAI.TraceReconstruction.boolTypeSign_integerTemplate line 823
theorem OAI.TraceReconstruction.integerTemplateType_nat line 829
def OAI.TraceReconstruction.sourceScheduledTrials line 837
Source documentation
Global trials at a parent use its children's local-trial count. This fixes the index shift between source level labels and zero-based arrays.
```
def sourceScheduledTrials (T n : ℕ → ℕ) : ℕ → ℕ
  | 0 => 0
  | b+1 => (T (b+1)/4)*n b
```
def OAI.TraceReconstruction.sourceScheduledShift line 841
def OAI.TraceReconstruction.sourceLocalCenter line 846
def OAI.TraceReconstruction.sourceNodeAnchor line 849

def OAI.TraceReconstruction.sourceTreeLeafBool line 854

Source documentation

All actual leaf Booleans on the complete deterministic window tree.

def sourceTreeLeafBool (T n : ℕ → ℕ) (s : ℕ) (center : ℕ → ℤ) :
    (b : ℕ) → WindowAssignments T n (sourceScheduledTrials T n) Bool b → ℤ → Bool → WindowLeaf T b → Bool
  | 0, _, _, τ, _ => τ
  | b+1, bits, incoming, τ, v =>
      sourceTreeLeafBool T n s center b (bits.2.2 v.1)
        (sourceScheduledShift T n b bits.2.1 v.1)
        (integerTemplateType (T b) s (sourceNodeAnchor T n center b bits incoming) τ v.1) v.2

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.sourceScheduledShift, OAI.TraceReconstruction.integerTemplateType, OAI.TraceReconstruction.sourceNodeAnchor

theorem OAI.TraceReconstruction.sourceTreeLeafBool_sign line 862
def OAI.TraceReconstruction.sourceNominalPre line 875
def OAI.TraceReconstruction.sourceNominalPost line 876
theorem OAI.TraceReconstruction.sourceNominal_total line 878

def OAI.TraceReconstruction.sourceCenterWord line 884

Source documentation

The actual center before recursively cutting its pure side regions.

def sourceCenterWord (s : ℕ) (P T n : ℕ → ℕ) (center : ℕ → ℤ) (atom : Bool → List Bool) :
    (b : ℕ) → WindowAssignments T n (sourceScheduledTrials T n) Bool b → ℤ → Bool → List Bool
  | 0, _, _, τ => atom τ
  | b+1, bits, incoming, τ => atomString (T b) (sourceBlockWord s P atom b)
      (integerTemplateType (T b) s (sourceNodeAnchor T n center b bits incoming) τ)

/-- The unconditional literal surrogate partition: local and common-global
 pairs contribute their real selected pure lengths, on every bit assignment. -/

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.atomString, OAI.TraceReconstruction.sourceBlockWord, OAI.TraceReconstruction.integerTemplateType, OAI.TraceReconstruction.sourceNodeAnchor

def OAI.TraceReconstruction.sourceTreeWord line 892

Source documentation

The unconditional literal surrogate partition: local and common-global pairs contribute their real selected pure lengths, on every bit assignment.

def sourceTreeWord (s : ℕ) (P T n h : ℕ → ℕ) (center : ℕ → ℤ) (atom : Bool → List Bool) :
    (b : ℕ) → WindowAssignments T n (sourceScheduledTrials T n) Bool b → ℤ → Bool → List Bool
  | 0, _, _, τ => atom τ
  | 1, bits, incoming, τ => sourceCenterWord s P T n center atom 1 bits incoming τ
  | b+2, bits, incoming, τ =>
      let loc := fun u => (bits.2.2 u).1
…

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceCenterWord

def OAI.TraceReconstruction.SourceTreeFit line 910

Source documentation

The actual fit event uses a joint test of all displacements. It does not assert independence and will only be charged probabilistically afterwards.

def SourceTreeFit (T n : ℕ → ℕ) :
    (b : ℕ) → WindowAssignments T n (sourceScheduledTrials T n) Bool b → Prop
  | 0, _ => True
  | 1, _ => True
  | b+2, bits =>
      (∀u, |8*sourceDisplacement (T (b+1)) (n b) (fun v => (bits.2.2 v).1) bits.2.1 u| ≤ (T b:ℤ)) ∧
      ∀u, SourceTreeFit T n (b+1) (bits.2.2 u)

/-- Numerical layout conditions from the source. These contain no word or
 statistical conclusions, only the genuine integer margins. -/

Mentions: OAI.TraceReconstruction.WindowAssignments, OAI.TraceReconstruction.sourceScheduledTrials, OAI.TraceReconstruction.sourceDisplacement

structure OAI.TraceReconstruction.SourceLayoutMargins line 920
Source documentation
Numerical layout conditions from the source. These contain no word or statistical conclusions, only the genuine integer margins.
```
structure SourceLayoutMargins (s : ℕ) (P T n h : ℕ → ℕ) (b : ℕ) : Prop where
…
```
theorem OAI.TraceReconstruction.SourceLayoutMargins.restrict line 930
theorem OAI.TraceReconstruction.sourceTreeWord_eq_center line 944
Source documentation
Every recursively cut surrogate center is literally the actual center on the joint fit event. The source type assignment is retained at all leaves.
```
theorem sourceTreeWord_eq_center (s : ℕ) (P T n h : ℕ → ℕ) (center : ℕ → ℤ)
    (atom : Bool → List Bool) (b : ℕ) (H : SourceLayoutMargins s P T n h b)
    (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