OAI/Probability/TraceReconstruction/Shapes.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

Shapes

Global schedules, edge labels, forced/extra coordinate splitting, finite shape codes, and occupied-label counts.

  1. def OAI.TraceReconstruction.centralThird line 24

    Source documentation

    Source central third, in the zero-based child label convention. The shift of the source one-based indices is recorded in center parameters.

    def centralThird (N : ℕ) : Finset (Fin N) :=
…
  2. def OAI.TraceReconstruction.globalTrialIndex line 29

    Source documentation

    One actual global-pair orientation, ordered by its pre-region block and its local identifier there.

    def globalTrialIndex (N t : ℕ) (v : Fin (N/4)) (a : Fin t) : Fin ((N/4)*t) :=
…
  3. def OAI.TraceReconstruction.scheduledGlobalShift line 35

    Source documentation

    Literal net global displacement immediately before a child window: a pre block at v+1 remains active through its matched post region N-v. The paired displacement has even t trials in each affected region.

    def scheduledGlobalShift (N t : ℕ) (bits : Fin ((N/4)*t) → Bool) (u : Fin N) : ℤ :=
…
  4. theorem OAI.TraceReconstruction.centralThird_active line 39
  5. theorem OAI.TraceReconstruction.globalTrialIndex_bijective line 47
  6. theorem OAI.TraceReconstruction.globalTrial_sum line 73
  7. theorem OAI.TraceReconstruction.scheduledGlobalShift_plateau line 79
  8. def OAI.TraceReconstruction.sourceGlobalTrials line 100

    Source documentation

    The actual complete-tree global schedule has the exact plateau identity needed by the already proved correlated anchor energy theorem.

    def sourceGlobalTrials (T t : ℕ → ℕ) (b : ℕ) : ℕ := (T b/4)*t b
  9. def OAI.TraceReconstruction.sourceGlobalShift line 102
  10. theorem OAI.TraceReconstruction.sourceGlobalShift_hasPlateau line 106
  11. def OAI.TraceReconstruction.OccupiedParityTree.Edge line 120

    Source documentation

    One actual child-label coordinate of an arbitrary ordered occupied shape. Unlike a complete r-ary padding, this contains no unused edges.

    def Edge : {b : ℕ} → OccupiedParityTree b → Type
  | _, .leaf => PEmpty
  | _, .node n children _ => Fin n ⊕ ((i : Fin n) × Edge (children i))

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  12. instance OAI.TraceReconstruction.OccupiedParityTree.edgeFintype line 124
  13. def OAI.TraceReconstruction.OccupiedParityTree.Edge.height line 130
  14. def OAI.TraceReconstruction.OccupiedParityTree.Labels line 138

    Source documentation

    All literal label assignments to this particular ordered shape.

    def Labels (T : ℕ → ℕ) {b : ℕ} (t : OccupiedParityTree b) :=
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  15. instance OAI.TraceReconstruction.OccupiedParityTree.labelsFintype line 141
  16. def OAI.TraceReconstruction.OccupiedParityTree.Labels.child line 144
  17. def OAI.TraceReconstruction.OccupiedParityTree.Forced.labels line 150

    Source documentation

    Projection to the actual labels of a fixed forced subtree. The shape selection is independent of these labels and of all random orientations.

    def Forced.labels (T : ℕ → ℕ) : {b : ℕ} → {t : OccupiedParityTree b} →
    t.Forced → t.Labels T → BinaryWindowLabels T b
  | _, _, .leaf, _ => PUnit.unit
  | _, _, .node a c _ _ _ left right, x =>
      (x (Sum.inl a),x (Sum.inl c),left.labels T (x.child T a),right.labels T (x.child T c))

/-- Edge addresses in a complete binary tree, independent of all actual
numeric labels. False and true are its two children. -/

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels, OAI.TraceReconstruction.OccupiedParityTree.Edge

  18. def OAI.TraceReconstruction.OccupiedParityTree.BinaryEdge line 158

    Source documentation

    Edge addresses in a complete binary tree, independent of all actual numeric labels. False and true are its two children.

    def BinaryEdge : ℕ → Type
  | 0 => PEmpty
  | b+1 => Bool ⊕ (Bool × BinaryEdge b)
  19. instance OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeFintype line 162
  20. def OAI.TraceReconstruction.OccupiedParityTree.BinaryEdge.height line 168
  21. def OAI.TraceReconstruction.OccupiedParityTree.Forced.edge line 174

    Source documentation

    The forced binary tree is embedded in the actual occupied edge set.

    def Forced.edge : {b : ℕ} → {t : OccupiedParityTree b} → t.Forced → BinaryEdge b → t.Edge
  | _, _, .leaf, e => e.elim
  | _, _, .node a _ _ _ _ _ _, Sum.inl false => Sum.inl a
  | _, _, .node _ c _ _ _ _ _, Sum.inl true => Sum.inl c
  | _, _, .node a _ _ _ _ left _, Sum.inr (false,e) => Sum.inr ⟨a,left.edge e⟩
  | _, _, .node _ c _ _ _ _ right, Sum.inr (true,e) => Sum.inr ⟨c,right.edge e⟩

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.OccupiedParityTree.BinaryEdge

  22. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.edge_injective line 181
  23. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.edge_height line 215
  24. def OAI.TraceReconstruction.OccupiedParityTree.edgeCount line 225

    Source documentation

    The finite number of edge coordinates at a given child height.

    def edgeCount {b : ℕ} (t : OccupiedParityTree b) (h : ℕ) : ℕ :=
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  25. theorem OAI.TraceReconstruction.OccupiedParityTree.edgeCount_leaf line 228
  26. theorem OAI.TraceReconstruction.OccupiedParityTree.edgeCount_node line 232
  27. theorem OAI.TraceReconstruction.OccupiedParityTree.Edge.height_lt line 243
  28. theorem OAI.TraceReconstruction.OccupiedParityTree.edgeCount_outside line 251
  29. theorem OAI.TraceReconstruction.OccupiedParityTree.edgeCount_level line 259
  30. def OAI.TraceReconstruction.OccupiedParityTree.BinaryEdgeLabels line 276
  31. instance OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeLabelsFintype line 278
  32. def OAI.TraceReconstruction.OccupiedParityTree.binaryLabelsEquiv line 282

    Source documentation

    Exact coordinates of the recursively defined forced label tuple.

    def binaryLabelsEquiv (T : ℕ → ℕ) : (b : ℕ) → BinaryEdgeLabels T b ≃ BinaryWindowLabels T b
  | 0 =>
    { toFun := fun _ => PUnit.unit
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree.BinaryEdgeLabels, OAI.TraceReconstruction.BinaryWindowLabels

  33. def OAI.TraceReconstruction.OccupiedParityTree.Forced.restrict line 311

    Source documentation

    Restriction to the real forced coordinates, with only equality transport of the child-height index.

    def Forced.restrict (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (x : t.Labels T) : BinaryEdgeLabels T b := fun e =>
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.OccupiedParityTree.BinaryEdgeLabels

  34. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.restrict_labels line 315
  35. def OAI.TraceReconstruction.OccupiedParityTree.Forced.ExtraEdge line 332
  36. instance OAI.TraceReconstruction.OccupiedParityTree.forcedExtraEdgeFintype line 335
  37. def OAI.TraceReconstruction.OccupiedParityTree.Forced.ExtraLabels line 338
  38. instance OAI.TraceReconstruction.OccupiedParityTree.forcedExtraLabelsFintype line 341
  39. def OAI.TraceReconstruction.OccupiedParityTree.Forced.labelsEquiv line 347

    Source documentation

    Exact bijective partition of all actual edge coordinates into the forced binary coordinates and the genuine extra coordinates.

    noncomputable def Forced.labelsEquiv (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced) :
    t.Labels T ≃ BinaryWindowLabels T b × F.ExtraLabels T := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels

  40. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.labelsEquiv_fst line 359
  41. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.labelsEquiv_snd line 363
  42. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.sum_labels line 367

    Source documentation

    Literal finite Fubini over forced labels and all remaining labels.

    theorem Forced.sum_labels (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (f : BinaryWindowLabels T b → F.ExtraLabels T → ℝ) :
    (∑x : t.Labels T,f (F.labels T x) (fun e => x e.val)) =
      ∑p : BinaryWindowLabels T b, ∑z : F.ExtraLabels T,f p z := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels

  43. def OAI.TraceReconstruction.OccupiedParityTree.Forced.ExtraLeafEdge line 374
  44. def OAI.TraceReconstruction.OccupiedParityTree.Forced.ExtraInteriorEdge line 377
  45. instance OAI.TraceReconstruction.OccupiedParityTree.extraLeafEdgeFintype line 380
  46. instance OAI.TraceReconstruction.OccupiedParityTree.extraInteriorEdgeFintype line 383
  47. def OAI.TraceReconstruction.OccupiedParityTree.Forced.InteriorLabels line 386
  48. instance OAI.TraceReconstruction.OccupiedParityTree.extraInteriorLabelsFintype line 389
  49. def OAI.TraceReconstruction.OccupiedParityTree.Forced.extraLabelsEquiv line 395

    Source documentation

    Extra bottom labels are separated from all nonleaf labels without introducing any T₁ factor.

    noncomputable def Forced.extraLabelsEquiv (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b}
    (F : t.Forced) : F.ExtraLabels T ≃ (F.ExtraLeafEdge → Fin (T 0)) × F.InteriorLabels T :=
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  50. def OAI.TraceReconstruction.OccupiedParityTree.Edge.parentPath line 410

    Source documentation

    The parent address of an edge in the full deterministic numerical index tree. In particular it does not contain the edge's own child label.

    def Edge.parentPath (T : ℕ → ℕ) : {b : ℕ} → {t : OccupiedParityTree b} →
    t.Labels T → t.Edge → List ℕ
  | _, .leaf, _, e => e.elim
  | _, .node _n _children _roles, x, e => match e with
    | Sum.inl _ => []
    | Sum.inr z => (x (Sum.inl z.1)).val :: Edge.parentPath T (x.child T z.1) z.2

/-- Every ancestor label of an extra selected leaf is an interior label. -/

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  51. theorem OAI.TraceReconstruction.OccupiedParityTree.Edge.parentPath_congr line 418

    Source documentation

    Every ancestor label of an extra selected leaf is an interior label.

    theorem Edge.parentPath_congr (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b}
    (x y : t.Labels T) (h : ∀e : t.Edge, e.height≠0 → (x e).val=(y e).val)
    (e : t.Edge) : e.parentPath T x=e.parentPath T y := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  52. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.labels_value_eq line 434
  53. def OAI.TraceReconstruction.OccupiedParityTree.Forced.fullLabelsEquiv line 442

    Source documentation

    The combined exact split into forced, extra-leaf and extra-interior labels.

    noncomputable def Forced.fullLabelsEquiv (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b}
    (F : t.Forced) : t.Labels T ≃
      BinaryWindowLabels T b × (F.ExtraLeafEdge → Fin (T 0)) × F.InteriorLabels T :=
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels

  54. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.fullLabelsEquiv_fst line 447
  55. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.fullLabelsEquiv_leaf_value line 451
  56. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.fullLabelsEquiv_interior_value line 455
  57. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.parentPath_extraLeaf_invariant line 461

    Source documentation

    Changing only extra leaf labels changes no ancestor address, even when all the complete-tree mechanisms share their source global bits.

    theorem Forced.parentPath_extraLeaf_invariant (T : ℕ → ℕ) {b : ℕ} {t : OccupiedParityTree b}
    (F : t.Forced) (p : BinaryWindowLabels T b) (h k : F.ExtraLeafEdge → Fin (T 0))
    (z : F.InteriorLabels T) (e : t.Edge) :
    e.parentPath T ((F.fullLabelsEquiv T).symm (p,h,z)) =
      e.parentPath T ((F.fullLabelsEquiv T).symm (p,k,z)) := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.BinaryWindowLabels

  58. def OAI.TraceReconstruction.OccupiedParityTree.FiniteRoleShape line 493

    Source documentation

    A finite ordered-role shape code with at most r children at every vertex. There are no numerical child labels in this type.

    def FiniteRoleShape (r : ℕ) : ℕ → Type
  | 0 => PUnit
  | b+1 => (n : Fin (r+1)) × (Fin n.val → FiniteRoleShape r b) × (Fin n.val → Fin 3)
  59. instance OAI.TraceReconstruction.OccupiedParityTree.finiteRoleShapeFintype line 497
  60. def OAI.TraceReconstruction.OccupiedParityTree.FiniteRoleShape.toTree line 504
  61. theorem OAI.TraceReconstruction.OccupiedParityTree.occupied_arity_le_leaves line 508
  62. theorem OAI.TraceReconstruction.OccupiedParityTree.child_le_leaves line 515
  63. theorem OAI.TraceReconstruction.OccupiedParityTree.exists_finiteRoleShape line 522

    Source documentation

    Every occupied shape with r selected leaves really has a finite code whose domain depends only on r and the depth, not on any window size.

    theorem exists_finiteRoleShape {b : ℕ} (t : OccupiedParityTree b) (r : ℕ)
    (ht : t.occupied) (hr : t.leafCount≤r) :
    ∃x : FiniteRoleShape r b,x.toTree r b=t := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.OccupiedParityTree.FiniteRoleShape

  64. def OAI.TraceReconstruction.OccupiedParityTree.shapeRoleConstant line 539

    Source documentation

    The manuscript's finite shape/role constant, now a literal natural number independent of the actual child-label sizes and all channel data.

    def shapeRoleConstant (r b : ℕ) : ℕ := Fintype.card (FiniteRoleShape r b)

    Mentions: OAI.TraceReconstruction.OccupiedParityTree.FiniteRoleShape

  65. theorem OAI.TraceReconstruction.OccupiedParityTree.finite_bounded_occupied_shapes line 541
  66. def OAI.TraceReconstruction.indexedExtraAverage line 561

    Source documentation

    Extra-leaf index set version of the whole-bit-law sum.

    def indexedExtraAverage {Ω E : Type*} [Fintype Ω] [Fintype E] (P : FiniteLaw Ω)
    (s N : ℕ) (f : Ω → ℝ) (X : Ω → E → ℤ) (h : E → Fin N) : ℝ :=
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  67. theorem OAI.TraceReconstruction.indexedExtraAverage_nonneg line 565
  68. theorem OAI.TraceReconstruction.indexedExtraAverage_sum line 573
  69. theorem OAI.TraceReconstruction.indexedExtraAverage_energy line 597
  70. def OAI.TraceReconstruction.OccupiedParityTree.Labels.node line 618

    Source documentation

    Node-wise assembly of genuine edge labels.

    def OccupiedParityTree.Labels.node (T : ℕ → ℕ) {b k : ℕ}
    {children : Fin k → OccupiedParityTree b} {roles : Fin k → Fin 3}
    (h : Fin k → Fin (T b)) (z : (i : Fin k) → (children i).Labels T) :
    (OccupiedParityTree.node k children roles).Labels T :=
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.OccupiedParityTree.Labels

  71. def OAI.TraceReconstruction.occupiedTermLabels line 627

    Source documentation

    The real numeric labels of the selected occupied configuration.

    def occupiedTermLabels (T : ℕ → ℕ) : (b : ℕ) →
    (S : Finset (WindowLeaf T (b+1))) → (a : OccupiedWindowChoice T b S) →
      (occupiedWindowTerm T b S a).Labels T
  | 0, S, _ => Labels.node T (fun i => (S.equivFin.symm i).val.1) (fun _ e => e.elim)
  | b+1, S, a => Labels.node T (fun i => ((selectedChildren S).equivFin.symm i).val)
      (fun i => occupiedTermLabels T b
        (selectedChildLeaves S ((selectedChildren S).equivFin.symm i).val) (a.1 i))

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

  72. theorem OAI.TraceReconstruction.occupiedTermLabels_forced line 635
  73. def OAI.TraceReconstruction.OccupiedParityTree.labelledLeaves line 667

    Source documentation

    Reading the set of leaf addresses from a shape and numeric edge labels. Repeated or unordered coordinates are allowed; the true encoding is a particular subset of this unrestricted label domain.

    def labelledLeaves (T : ℕ → ℕ) : {b : ℕ} → (t : OccupiedParityTree b) →
    t.Labels T → Finset (WindowLeaf T b)
  | 0, .leaf, _ => {(⟨0,by decide⟩ : Fin 1)}
  | b+1, .node n children roles, x => Finset.univ.biUnion fun i : Fin n =>
      ((children i).labelledLeaves T (x.child T i)).image (fun v => (x (Sum.inl i),v))
end OccupiedParityTree

    Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.WindowLeaf

  74. theorem OAI.TraceReconstruction.mem_selectedChildLeaves line 674
  75. theorem OAI.TraceReconstruction.occupiedTermLabels_leaves line 684
  76. theorem OAI.TraceReconstruction.occupiedWindowTerm_injective line 744

    Source documentation

    The shape remembers all the role choices once the actual selected set is fixed.

    theorem occupiedWindowTerm_injective (T : ℕ → ℕ) (b : ℕ)
    (S : Finset (WindowLeaf T (b+1))) : Function.Injective (occupiedWindowTerm T b S) := by
…

    Mentions: OAI.TraceReconstruction.WindowLeaf, OAI.TraceReconstruction.occupiedWindowTerm

  77. def OAI.TraceReconstruction.occupiedTermEncoding line 759

    Source documentation

    Unrestricted shape/label space really covers the coefficient index without multiplicity.

    def occupiedTermEncoding (T : ℕ → ℕ) (b : ℕ)
    (w : (S : Finset (WindowLeaf T (b+1))) × OccupiedWindowChoice T b S) :
    (t : OccupiedParityTree (b+1)) × t.Labels T :=
…

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

  78. theorem OAI.TraceReconstruction.occupiedTermEncoding_injective line 764
  79. def OAI.TraceReconstruction.OccupiedParityTree.Forced.edgeEquiv line 791
  80. def OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeCount line 798
  81. theorem OAI.TraceReconstruction.OccupiedParityTree.BinaryEdge.height_lt line 800
  82. theorem OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeCount_outside line 808
  83. theorem OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeCount_succ line 815
  84. theorem OAI.TraceReconstruction.OccupiedParityTree.binaryEdgeCount_eq line 823
  85. def OAI.TraceReconstruction.OccupiedParityTree.Forced.extraCount line 836
  86. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.count_partition line 839
  87. theorem OAI.TraceReconstruction.OccupiedParityTree.levelCount_bottom line 851
  88. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.card_extraLeafEdge line 858

    Source documentation

    The extra bottom coordinates are precisely r-2^b, including the empty height-zero case.

    theorem Forced.card_extraLeafEdge {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced) :
    Fintype.card F.ExtraLeafEdge=t.leafCount-2^b := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  89. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.extraCount_le line 877

    Source documentation

    Exact source nonforced vertex bound, now for genuine extra edge-label coordinates rather than an abstract level-count surrogate.

    theorem Forced.extraCount_le {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (ht : t.occupied) (h : ℕ) : F.extraCount h≤t.leafCount-2^b := by
…

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  90. def OAI.TraceReconstruction.OccupiedParityTree.Forced.interiorHeight line 889

    Source documentation

    Extra nonleaf numeric labels grouped by their actual child height.

    def Forced.interiorHeight {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (e : F.ExtraInteriorEdge) : Fin b := ⟨e.val.val.height,e.val.val.height_lt⟩

    Mentions: OAI.TraceReconstruction.OccupiedParityTree

  91. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.interiorFiber_le line 892
  92. theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.card_interiorLabels_le line 905