OAI/Probability/CubeShuffle/RoutingNetwork.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CubeShuffle.RoutingNetwork line 13

   Source documentation

   A finite fair routing network certified by its actual test algorithms and path/meeting geometry. The fields are local routing facts, not probability or mixing assumptions. Below they are constructed for parallel butterflies.

   structure RoutingNetwork (α ι : Type*) [Fintype α] [DecidableEq α]
       [Fintype ι] [DecidableEq ι] (d : ℕ) where
   …

2. lemma OAI.CubeShuffle.RoutingNetwork.card_switches_using line 40
3. lemma OAI.CubeShuffle.RoutingNetwork.switch_incidence_sum line 49
4. lemma OAI.CubeShuffle.RoutingNetwork.weighted_switch_min_bound line 78

   Source documentation

   The weighted threshold estimate in the rotation argument. It applies to any weights and so in particular to 1/j on selected length-j cycles.

   lemma weighted_switch_min_bound (b : ι → Bool) (w : α → ℝ) :
       ∑ i : ι, min (w (R.users b i).1) (w (R.users b i).2) ≤
         (d : ℝ) / 2 * ∑ x : α, w x := by
   …

5. def OAI.CubeShuffle.RoutingNetwork.cycleFiber line 95

   Source documentation

   Ownership by distinguishable cycle slots; none means unselected.

   def cycleFiber (o : α → Option (Fin A)) (i : Fin A) : Finset (α) := by
   …

6. lemma OAI.CubeShuffle.RoutingNetwork.mem_cycleFiber line 100
7. abbrev OAI.CubeShuffle.RoutingNetwork.Terminal line 105
8. def OAI.CubeShuffle.RoutingNetwork.slotWeight line 107
9. def OAI.CubeShuffle.RoutingNetwork.pathWeight line 110
10. def OAI.CubeShuffle.RoutingNetwork.withinWeight line 115
11. def OAI.CubeShuffle.RoutingNetwork.rotationMeeting line 123

    Source documentation

    Charge at a meeting after independently rotating the selected cycles. A later slot is the only possible closer, except within a single cycle where either user can be its terminal.

    noncomputable def rotationMeeting (o : α → Option (Fin A)) (z : Terminal o)
        (u v : α) : ℝ :=
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.Terminal

12. lemma OAI.CubeShuffle.RoutingNetwork.card_cycleFiber line 132
13. lemma OAI.CubeShuffle.RoutingNetwork.terminal_mean line 137
14. lemma OAI.CubeShuffle.RoutingNetwork.slotWeight_antitone line 152
15. lemma OAI.CubeShuffle.RoutingNetwork.rotationMeeting_mean line 161
16. lemma OAI.CubeShuffle.RoutingNetwork.pathWeight_sum line 195
17. lemma OAI.CubeShuffle.RoutingNetwork.withinWeight_sum_bound line 212
18. def OAI.CubeShuffle.RoutingNetwork.rotationCharge line 234
19. lemma OAI.CubeShuffle.RoutingNetwork.rotationCharge_mean_bound line 238
20. lemma OAI.CubeShuffle.RoutingNetwork.rotation_exp_bound line 258

    Source documentation

    The Jensen rotation bound, still expressed in exponentials so that all normalizing constants and the factor one half are explicit.

    lemma rotation_exp_bound {o : α → Option (Fin A)}
        [∀ i : Fin A, Nonempty {x : α // o x = some i}]
        (hm : Monotone (fun i => (cycleFiber o i).card)) (b : ι → Bool) :
        Real.exp (-Real.log 2 * ((A:ℝ)*d/2 +
          ∑ i : Fin A, Real.log (cycleFiber o i).card / (2 * Real.log 2))) ≤
          finiteMean (fun z : Terminal o => Real.exp (-Real.log 2 * rotationCharge R o b z)) := by
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.cycleFiber, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.Terminal, OAI.CubeShuffle.RoutingNetwork.rotationCharge

21. def OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle line 281

    Source documentation

    Inspect one proposed length-(r+1) cycle. Every queried input must be in S and must not have appeared in an earlier slot or earlier in this cycle.

    noncomputable def seekCycle (R : RoutingNetwork α ι d) (S : Finset (α)) (a : α) :
        ℕ → α → Finset (α) → (Finset (α) → QueryTree (ι)) →
          QueryTree (ι)
      | 0, x, V, k => if x ∈ S ∧ x ∉ V then R.close x a (k (insert x V)) else reject
      | r + 1, x, V, k => if x ∈ S ∧ x ∉ V then R.follow x
          (fun y => seekCycle R S a r y (insert x V) k) else reject

    Mentions: OAI.CubeShuffle.RoutingNetwork, OAI.CubeShuffle.QueryTree

22. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle_raw_charge line 288
23. def OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycles line 310

    Source documentation

    Distinguishable cycle slots, with each requested length encoded as r+1. Later factorial-moment counting divides by precisely these rotation counts.

    noncomputable def seekCycles (R : RoutingNetwork α ι d) (S : Finset (α)) :
        List (α × ℕ) → Finset (α) → QueryTree (ι)
      | [], _ => accept
      | (a,r) :: L, V => seekCycle R S a r a V (fun V => seekCycles R S L V)

    Mentions: OAI.CubeShuffle.RoutingNetwork, OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle

24. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycles_raw_charge line 315
25. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.cycles_weighted_success line 332

    Source documentation

    The actual fixed-start weighted exploration inequality in FAC.3. The stale charge counts exposed closing-path switches exactly, not a postulated conditional-independence bound. Failure includes repeats, short cycles and visiting outside the marked subset, and can occur at ANY earlier query.

    lemma cycles_weighted_success (S : Finset (α)) (L : List (α × ℕ)) :
        finiteMean (fun ω : ι → Bool =>
          if (seekCycles R S L ∅).succeeds ω then
            ((2:ℝ)^d)^L.length / (2:ℝ)^(seekCycles R S L ∅).staleCharge ∅ ω else 0) ≤ 1 := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycles

26. def OAI.CubeShuffle.RoutingNetwork.exposedPaths line 356
27. lemma OAI.CubeShuffle.RoutingNetwork.exposedPaths_empty line 360
28. lemma OAI.CubeShuffle.RoutingNetwork.exposedPaths_insert line 364
29. def OAI.CubeShuffle.RoutingNetwork.terminalCharge line 369
30. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle_semantics line 376

    Source documentation

    The cycle-query certificate has exactly its deterministic cycle-trace semantics, including the complete exposure record and terminal encounter charge.

    lemma seekCycle_semantics (S : Finset (α)) (a : α) (r : ℕ)
        (x : α) (V W : Finset (α)) (z : α)
        (k : Finset (α) → QueryTree (ι)) (ω : ι → Bool)
        (h : cycleTrace (R.perm ω) S a r x V = some (W,z)) :
        (seekCycle R S a r x V k).succeeds ω = (k W).succeeds ω ∧
          (seekCycle R S a r x V k).staleCharge (exposedPaths R (ω) V) ω =
            (k W).staleCharge (exposedPaths R (ω) W) ω +
              terminalCharge R (ω) z (W.erase z) := by
    …

    Mentions: OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.cycleTrace, OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle, OAI.CubeShuffle.RoutingNetwork.exposedPaths, OAI.CubeShuffle.RoutingNetwork.terminalCharge

31. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycle_orbit line 405
32. lemma OAI.CubeShuffle.RoutingNetwork.mem_exposedPaths line 419
33. lemma OAI.CubeShuffle.RoutingNetwork.terminalCharge_sum line 431
34. def OAI.CubeShuffle.RoutingNetwork.priorPaths line 454

    Source documentation

    All slots before time t, including the whole current cycle when t=i+1.

    noncomputable def priorPaths {A : ℕ} (o : α → Option (Fin A)) (t : ℕ) : Finset (α) :=
    …

35. lemma OAI.CubeShuffle.RoutingNetwork.mem_priorPaths line 458
36. lemma OAI.CubeShuffle.RoutingNetwork.terminalCharge_prior_sum line 463
37. lemma OAI.CubeShuffle.RoutingNetwork.rotationMeeting_eq_slot_sum line 480
38. lemma OAI.CubeShuffle.RoutingNetwork.rotationCharge_eq_terminal_sum line 534

    Source documentation

    The geometric rotation charge equals the actual sum of exposed terminal route meetings, with exactly the earlier slots and own cycle made available.

    lemma rotationCharge_eq_terminal_sum {A : ℕ} (o : α → Option (Fin A))
        (b : ι → Bool) (z : Terminal o) :
        rotationCharge R o b z = ∑ i : Fin A,
          (terminalCharge R b (z i).val ((priorPaths o (i.val+1)).erase (z i).val) : ℝ) := by
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.Terminal, OAI.CubeShuffle.RoutingNetwork.rotationCharge, OAI.CubeShuffle.RoutingNetwork.terminalCharge, OAI.CubeShuffle.RoutingNetwork.priorPaths

39. lemma OAI.CubeShuffle.RoutingNetwork.priorPaths_zero line 543
40. lemma OAI.CubeShuffle.RoutingNetwork.priorPaths_succ line 548
41. lemma OAI.CubeShuffle.RoutingNetwork.priorPaths_disjoint line 564
42. lemma OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycles_owned line 579

    Source documentation

    Success and exact exposed-switch charge for a realized, disjoint collection of full permutation cycles in ordered distinguishable slots.

    lemma seekCycles_owned {A : ℕ} (S : Finset (α)) (r : Fin A → ℕ)
        (o : α → Option (Fin A)) (z : Terminal o) (ω : ι → Bool)
        (hS : ∀ i, cycleFiber o i ⊆ S)
        (hO : ∀ i, orbitSet (R.perm ω) (z i).val = cycleFiber o i)
        (hC : ∀ i, (cycleFiber o i).card = r i+1) :
        let p := R.perm ω
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.Terminal, OAI.CubeShuffle.RoutingNetwork.cycleFiber, OAI.CubeShuffle.orbitSet

43. def OAI.CubeShuffle.RoutingNetwork.ValidCycleSlots line 629

    Source documentation

    A permutation-cycle collection in distinguishable slots, including all length-one cycles. No selection has been weakened to a collection of paths.

    def ValidCycleSlots (p : Equiv.Perm (α)) (S : Finset (α)) (r : Fin A → ℕ)
        (o : α → Option (Fin A)) : Prop :=
    …

44. abbrev OAI.CubeShuffle.RoutingNetwork.CycleSlots line 635
45. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 638) line 638
46. lemma OAI.CubeShuffle.RoutingNetwork.CycleSlots.terminal_nonempty line 641
47. lemma OAI.CubeShuffle.RoutingNetwork.owner_ext line 648
48. abbrev OAI.CubeShuffle.RoutingNetwork.RootedSlots line 660
49. def OAI.CubeShuffle.RoutingNetwork.rootedStart line 663
50. lemma OAI.CubeShuffle.RoutingNetwork.rootedStart_injective line 669
51. lemma OAI.CubeShuffle.RoutingNetwork.rooted_weight_sum_le line 684

    Source documentation

    Sum over every rooted realized collection is controlled by the sum over all starts. This injectivity step retains cycle disjointness and all rotations.

    lemma rooted_weight_sum_le (S : Finset (α)) (r : Fin A → ℕ) (ω : ι → Bool) :
        (∑ c : RootedSlots (R.perm ω) S r,
          ((2:ℝ)^d)^A * Real.exp (-Real.log 2 * rotationCharge R c.1.val (ω) c.2)) ≤
        ∑ a : Fin A → S,
          if (QueryTree.seekCycles R S (List.ofFn (fun i => ((a i).val,r i))) ∅).succeeds ω then
            ((2:ℝ)^d)^A / (2:ℝ)^(QueryTree.seekCycles R S (List.ofFn (fun i => ((a i).val,r i))) ∅).staleCharge ∅ ω
          else 0 := by
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.RootedSlots, OAI.CubeShuffle.RoutingNetwork.rotationCharge, OAI.CubeShuffle.RoutingNetwork.QueryTree.seekCycles

52. lemma OAI.CubeShuffle.RoutingNetwork.collection_rotation_lower line 711
53. lemma OAI.CubeShuffle.RoutingNetwork.cycleSlots_weighted_moment line 741

    Source documentation

    The weighted collection inequality obtained by summing the actual adaptive query certificate over starts. The subsequent simplification yields FAC.3.

    lemma cycleSlots_weighted_moment (S : Finset (α)) (r : Fin A → ℕ) (hr : Monotone r) :
        finiteMean (fun ω : ι → Bool =>
          (Fintype.card (CycleSlots (R.perm ω) S r) : ℝ)) *
          collectionWeight d r ≤ (S.card : ℝ)^A := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.CycleSlots, OAI.CubeShuffle.collectionWeight

54. lemma OAI.CubeShuffle.RoutingNetwork.cycleSlots_moment line 774
55. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_cycleSlots_moment line 783

    Source documentation

    The exact fixed-distinguished-slot form of FAC.3, with physical butterfly size n=2^d and every slot a whole permutation cycle of the stated length.

    lemma butterfly_cycleSlots_moment (S : Finset (α)) (r : Fin A → ℕ) (hr : Monotone r) :
        finiteMean (fun ω : ι → Bool =>
          (Fintype.card (CycleSlots (R.perm ω) S r) : ℝ)) ≤
            ((S.card : ℝ) / Real.sqrt ((2:ℝ)^d))^A *
              ∏ i : Fin A, (1 / Real.sqrt (r i+1)) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.CycleSlots

56. abbrev OAI.CubeShuffle.RoutingNetwork.SelectedCycle line 800

    Source documentation

    The genuine cycles retained completely in S; fixed points are included.

    abbrev SelectedCycle (p : Equiv.Perm (α)) (S : Finset (α)) :=
    …

57. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 803) line 803
58. lemma OAI.CubeShuffle.RoutingNetwork.SelectedCycle.nonempty line 806
59. lemma OAI.CubeShuffle.RoutingNetwork.SelectedCycle.orbit_eq line 812
60. lemma OAI.CubeShuffle.RoutingNetwork.SelectedCycle.eq_of_mem line 818
61. abbrev OAI.CubeShuffle.RoutingNetwork.SlotAssignment line 823
62. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 826) line 826
63. def OAI.CubeShuffle.RoutingNetwork.slotsToAssignment line 829
64. def OAI.CubeShuffle.RoutingNetwork.assignmentOwner line 843
65. lemma OAI.CubeShuffle.RoutingNetwork.assignmentOwner_eq_some line 848
66. lemma OAI.CubeShuffle.RoutingNetwork.assignmentOwner_fiber line 866
67. def OAI.CubeShuffle.RoutingNetwork.assignmentToSlots line 871
68. def OAI.CubeShuffle.RoutingNetwork.cycleSlotsEquivAssignments line 887

    Source documentation

    Ownership and labelled distinct full cycles are equivalent, not merely bounded by one another. This identifies the factorial-moment combinatorics.

    noncomputable def cycleSlotsEquivAssignments (p : Equiv.Perm (α)) (S : Finset (α)) (r : Fin A → ℕ) :
        CycleSlots p S r ≃ SlotAssignment p S r where
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.CycleSlots, OAI.CubeShuffle.RoutingNetwork.SlotAssignment

69. abbrev OAI.CubeShuffle.RoutingNetwork.LengthClass line 908
70. def OAI.CubeShuffle.RoutingNetwork.slotClass line 910
71. abbrev OAI.CubeShuffle.RoutingNetwork.SlotsOfLength line 913
72. abbrev OAI.CubeShuffle.RoutingNetwork.CyclesOfLength line 914
73. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 917) line 917
74. abbrev OAI.CubeShuffle.RoutingNetwork.GroupedAssignments line 920
75. def OAI.CubeShuffle.RoutingNetwork.assignmentToGroups line 923
76. def OAI.CubeShuffle.RoutingNetwork.groupsEmbedding line 928
77. def OAI.CubeShuffle.RoutingNetwork.groupsToAssignment line 935
78. def OAI.CubeShuffle.RoutingNetwork.assignmentEquivGroups line 940
79. lemma OAI.CubeShuffle.RoutingNetwork.card_cycleSlots_factorial line 955
80. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_factorial_moment line 966

    Source documentation

    Factorial moments for independently fair butterflies, including every fixed point. The product is over the distinct positive lengths in the given sorted slot list.

    lemma butterfly_factorial_moment (S : Finset (α)) (r : Fin A → ℕ) (hr : Monotone r) :
        finiteMean (fun ω : ι → Bool =>
           (∏ j : LengthClass r,
             (Fintype.card (CyclesOfLength (R.perm ω) S j.val)).descFactorial
               (Fintype.card (SlotsOfLength r j)) : ℕ)) ≤
          ((S.card : ℝ) / Real.sqrt ((2:ℝ)^d))^A *
            ∏ i : Fin A, (1 / Real.sqrt (r i+1)) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.LengthClass, OAI.CubeShuffle.RoutingNetwork.CyclesOfLength, OAI.CubeShuffle.RoutingNetwork.SlotsOfLength

81. def OAI.CubeShuffle.RoutingNetwork.assignmentRelabel line 980
82. lemma OAI.CubeShuffle.RoutingNetwork.card_cycleSlots_relabel line 989
83. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_cycleSlots_moment_all line 995
84. abbrev OAI.CubeShuffle.RoutingNetwork.ShortCycle line 1005
85. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 1008) line 1008
86. def OAI.CubeShuffle.RoutingNetwork.shortCycleLength line 1011
87. lemma OAI.CubeShuffle.RoutingNetwork.shortCycleLength_add_one line 1015
88. def OAI.CubeShuffle.RoutingNetwork.shortEmbeddingEquiv line 1021
89. lemma OAI.CubeShuffle.RoutingNetwork.shortCycle_factorial_eq line 1047
90. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_shortCycle_moment line 1063
91. def OAI.CubeShuffle.RoutingNetwork.cycleMass line 1082
92. lemma OAI.CubeShuffle.RoutingNetwork.cycleMass_le line 1085
93. lemma OAI.CubeShuffle.RoutingNetwork.shortCycle_card_le line 1103
94. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_shortCycle_mgf line 1112
95. abbrev OAI.CubeShuffle.RoutingNetwork.LongCycle line 1126
96. instance OAI.CubeShuffle.RoutingNetwork.(instance at line 1128) line 1128
97. lemma OAI.CubeShuffle.RoutingNetwork.selectedCycle_card_split line 1131
98. lemma OAI.CubeShuffle.RoutingNetwork.longCycle_card_bound line 1137
99. lemma OAI.CubeShuffle.RoutingNetwork.longCycle_pow_bound line 1153
100. lemma OAI.CubeShuffle.RoutingNetwork.butterfly_cycle_log_mgf line 1168

     Source documentation

     FAC.4 for a full fair butterfly, with actual whole permutation cycles retained inside the marked set. No asymptotic or numerical oracle enters.

     lemma butterfly_cycle_log_mgf (S : Finset (α)) (J : ℕ) (hJ : 0 < J)
         (q : ℝ) (hq : 1 ≤ q) :
         Real.log (finiteMean (fun ω : ι → Bool =>
           q^(Fintype.card (SelectedCycle (R.perm ω) S)))) ≤
           (S.card : ℝ)/J * Real.log q + 2*q*S.card*Real.sqrt J / Real.sqrt ((2:ℝ)^d) := by
     …

     Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.SelectedCycle