ButterflyCycles.lean`

121 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CubeShuffle.cycleFiber line 15
Source documentation
Ownership by distinguishable cycle slots; none means unselected.
```
def cycleFiber (o : Card d → Option (Fin A)) (i : Fin A) : Finset (Card d) := by
…
```
Mentions: OAI.CubeShuffle.Card
lemma OAI.CubeShuffle.mem_cycleFiber line 19
abbrev OAI.CubeShuffle.Terminal line 24
def OAI.CubeShuffle.slotWeight line 26
def OAI.CubeShuffle.pathWeight line 29
def OAI.CubeShuffle.withinWeight line 34
def OAI.CubeShuffle.rotationMeeting line 42
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 : Card d → Option (Fin A)) (z : Terminal o)
    (u v : Card d) : ℝ :=
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Terminal
lemma OAI.CubeShuffle.card_cycleFiber line 50
lemma OAI.CubeShuffle.terminal_mean line 55
lemma OAI.CubeShuffle.slotWeight_antitone line 69
lemma OAI.CubeShuffle.rotationMeeting_mean line 78
lemma OAI.CubeShuffle.pathWeight_sum line 111
lemma OAI.CubeShuffle.withinWeight_sum_bound line 128
def OAI.CubeShuffle.rotationCharge line 150
lemma OAI.CubeShuffle.rotationCharge_mean_bound line 154

lemma OAI.CubeShuffle.rotation_exp_bound line 174

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 : Card d → Option (Fin A)}
    [∀ i : Fin A, Nonempty {x : Card d // o x = some i}]
    (hm : Monotone (fun i => (cycleFiber o i).card)) (b : Butterfly d) :
    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 o b z)) := by
…

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.cycleFiber, OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.Terminal, OAI.CubeShuffle.rotationCharge

def OAI.CubeShuffle.orbitSet line 199
Source documentation
The full cycle as an orbit, including one-element cycles.
```
noncomputable def orbitSet (p : Equiv.Perm α) (x : α) : Finset α :=
…
```
lemma OAI.CubeShuffle.mem_orbitSet line 202
lemma OAI.CubeShuffle.orbitSet_nonempty line 207
lemma OAI.CubeShuffle.orbitSet_eq line 210
lemma OAI.CubeShuffle.orbitSet_apply line 216
lemma OAI.CubeShuffle.orbitSet_eq_or_disjoint line 220
lemma OAI.CubeShuffle.perm_minimalPeriod_pos line 231
lemma OAI.CubeShuffle.orbitSet_card line 235
def OAI.CubeShuffle.walkSet line 255
Source documentation
Inputs of the first r path queries, in temporal order forgotten.
```
def walkSet (p : Equiv.Perm α) (r : ℕ) (x : α) : Finset α :=
…
```
lemma OAI.CubeShuffle.mem_walkSet line 259
lemma OAI.CubeShuffle.walkSet_zero line 264
lemma OAI.CubeShuffle.walkSet_succ_last line 268
lemma OAI.CubeShuffle.walkSet_succ_first line 273
lemma OAI.CubeShuffle.not_mem_short_walk line 287
lemma OAI.CubeShuffle.walkSet_period line 296
lemma OAI.CubeShuffle.walkSet_card line 310
lemma OAI.CubeShuffle.walkSet_subset_orbit line 319

def OAI.CubeShuffle.cycleTrace line 329

Source documentation

Deterministic semantics of the adaptive cycle validator. The result records all visited inputs and the unique terminal (closing-path input).

def cycleTrace (p : Equiv.Perm α) (S : Finset α) (a : α) :
    ℕ → α → Finset α → Option (Finset α × α)
  | 0, x, V => if x ∈ S ∧ x ∉ V ∧ p x = a then some (insert x V,x) else none
  | r+1, x, V => if x ∈ S ∧ x ∉ V then cycleTrace p S a r (p x) (insert x V) else none

lemma OAI.CubeShuffle.cycleTrace_walk line 334
lemma OAI.CubeShuffle.cycleTrace_orbit line 368
def OAI.CubeShuffle.exposedPaths line 391
Source documentation
Precisely the switch record produced by exposing a set of complete paths.
```
noncomputable def exposedPaths (d : ℕ) (b : Butterfly d) (V : Finset (Card d)) :
    Finset (SwitchIndex d) :=
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex
lemma OAI.CubeShuffle.exposedPaths_empty line 395
lemma OAI.CubeShuffle.exposedPaths_insert line 399
def OAI.CubeShuffle.terminalCharge line 404
lemma OAI.CubeShuffle.QueryTree.followPath_stale_charge line 409

lemma OAI.CubeShuffle.QueryTree.seekCycle_semantics line 423

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 (d : ℕ) (S : Finset (Card d)) (a : Card d) (r : ℕ)
    (x : Card d) (V W : Finset (Card d)) (z : Card d)
    (k : Finset (Card d) → QueryTree (SwitchIndex d)) (ω : SwitchIndex d → Bool)
    (h : cycleTrace (butterflyPerm d (decodeButterfly d ω)) S a r x V = some (W,z)) :
    (seekCycle d S a r x V k).succeeds ω = (k W).succeeds ω ∧
      (seekCycle d S a r x V k).staleCharge (exposedPaths d (decodeButterfly d ω) V) ω =
        (k W).staleCharge (exposedPaths d (decodeButterfly d ω) W) ω +
          terminalCharge d (decodeButterfly d ω) z (W.erase z) := by
…

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.QueryTree, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.cycleTrace, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.QueryTree.seekCycle, OAI.CubeShuffle.QueryTree.succeeds, OAI.CubeShuffle.QueryTree.staleCharge, OAI.CubeShuffle.exposedPaths, OAI.CubeShuffle.terminalCharge

lemma OAI.CubeShuffle.QueryTree.seekCycle_orbit line 453
lemma OAI.CubeShuffle.mem_exposedPaths line 468
lemma OAI.CubeShuffle.terminalCharge_sum line 480
def OAI.CubeShuffle.priorPaths line 503
Source documentation
All slots before time t, including the whole current cycle when t=i+1.
```
noncomputable def priorPaths {d A : ℕ} (o : Card d → Option (Fin A)) (t : ℕ) : Finset (Card d) :=
…
```
Mentions: OAI.CubeShuffle.Card
lemma OAI.CubeShuffle.mem_priorPaths line 506
lemma OAI.CubeShuffle.terminalCharge_prior_sum line 511
lemma OAI.CubeShuffle.rotationMeeting_eq_slot_sum line 528
lemma OAI.CubeShuffle.rotationCharge_eq_terminal_sum line 582
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 {d A : ℕ} (o : Card d → Option (Fin A))
    (b : Butterfly d) (z : Terminal o) :
    rotationCharge o b z = ∑ i : Fin A,
      (terminalCharge d b (z i).val ((priorPaths o (i.val+1)).erase (z i).val) : ℝ) := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Terminal, OAI.CubeShuffle.rotationCharge, OAI.CubeShuffle.terminalCharge, OAI.CubeShuffle.priorPaths
lemma OAI.CubeShuffle.priorPaths_zero line 590
lemma OAI.CubeShuffle.priorPaths_succ line 595
lemma OAI.CubeShuffle.priorPaths_disjoint line 610
lemma OAI.CubeShuffle.QueryTree.seekCycles_owned line 624
Source documentation
Success and exact exposed-switch charge for a realized, disjoint collection of full permutation cycles in ordered distinguishable slots.
```
lemma seekCycles_owned {d A : ℕ} (S : Finset (Card d)) (r : Fin A → ℕ)
    (o : Card d → Option (Fin A)) (z : Terminal o) (ω : SwitchIndex d → Bool)
    (hS : ∀ i, cycleFiber o i ⊆ S)
    (hO : ∀ i, orbitSet (butterflyPerm d (decodeButterfly d ω)) (z i).val = cycleFiber o i)
    (hC : ∀ i, (cycleFiber o i).card = r i+1) :
    let p := butterflyPerm d (decodeButterfly d ω)
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Terminal, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.cycleFiber, OAI.CubeShuffle.orbitSet, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly
def OAI.CubeShuffle.ValidCycleSlots line 676
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 (Card d)) (S : Finset (Card d)) (r : Fin A → ℕ)
    (o : Card d → Option (Fin A)) : Prop :=
…
```
Mentions: OAI.CubeShuffle.Card
abbrev OAI.CubeShuffle.CycleSlots line 682
instance OAI.CubeShuffle.(instance at line 685) line 685
lemma OAI.CubeShuffle.CycleSlots.terminal_nonempty line 688
lemma OAI.CubeShuffle.owner_ext line 694
abbrev OAI.CubeShuffle.RootedSlots line 706
def OAI.CubeShuffle.rootedStart line 709
lemma OAI.CubeShuffle.rootedStart_injective line 715
lemma OAI.CubeShuffle.sum_comp_injective_le line 728

lemma OAI.CubeShuffle.rooted_weight_sum_le line 738

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 (Card d)) (r : Fin A → ℕ) (ω : SwitchIndex d → Bool) :
    (∑ c : RootedSlots (butterflyPerm d (decodeButterfly d ω)) S r,
      ((2:ℝ)^d)^A * Real.exp (-Real.log 2 * rotationCharge c.1.val (decodeButterfly d ω) c.2)) ≤
    ∑ a : Fin A → S,
      if (QueryTree.seekCycles d S (List.ofFn (fun i => ((a i).val,r i))) ∅).succeeds ω then
        ((2:ℝ)^d)^A / (2:ℝ)^(QueryTree.seekCycles d S (List.ofFn (fun i => ((a i).val,r i))) ∅).staleCharge ∅ ω
      else 0 := by
…

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.RootedSlots, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.rotationCharge, OAI.CubeShuffle.QueryTree.seekCycles

def OAI.CubeShuffle.rotationLower line 765
def OAI.CubeShuffle.collectionWeight line 768
lemma OAI.CubeShuffle.collectionWeight_pos line 771
lemma OAI.CubeShuffle.collection_rotation_lower line 775
lemma OAI.CubeShuffle.cycleSlots_weighted_moment line 805
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 (Card d)) (r : Fin A → ℕ) (hr : Monotone r) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
      (Fintype.card (CycleSlots (butterflyPerm d (decodeButterfly d ω)) S r) : ℝ)) *
      collectionWeight d r ≤ (S.card : ℝ)^A := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.CycleSlots, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.collectionWeight
lemma OAI.CubeShuffle.cycleSlots_moment line 838
lemma OAI.CubeShuffle.collectionWeight_eq_sqrt line 845
lemma OAI.CubeShuffle.butterfly_cycleSlots_moment line 872
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 (Card d)) (r : Fin A → ℕ) (hr : Monotone r) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
      (Fintype.card (CycleSlots (butterflyPerm d (decodeButterfly d ω)) S r) : ℝ)) ≤
        ((S.card : ℝ) / Real.sqrt ((2:ℝ)^d))^A *
          ∏ i : Fin A, (1 / Real.sqrt (r i+1)) := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.CycleSlots, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly
abbrev OAI.CubeShuffle.SelectedCycle line 889
Source documentation
The genuine cycles retained completely in S; fixed points are included.
```
abbrev SelectedCycle (p : Equiv.Perm (Card d)) (S : Finset (Card d)) :=
…
```
Mentions: OAI.CubeShuffle.Card
instance OAI.CubeShuffle.(instance at line 892) line 892
lemma OAI.CubeShuffle.SelectedCycle.nonempty line 895
lemma OAI.CubeShuffle.SelectedCycle.orbit_eq line 901
lemma OAI.CubeShuffle.SelectedCycle.eq_of_mem line 907
abbrev OAI.CubeShuffle.SlotAssignment line 912
instance OAI.CubeShuffle.(instance at line 915) line 915
def OAI.CubeShuffle.slotsToAssignment line 918
def OAI.CubeShuffle.assignmentOwner line 932
lemma OAI.CubeShuffle.assignmentOwner_eq_some line 937
lemma OAI.CubeShuffle.assignmentOwner_fiber line 955
def OAI.CubeShuffle.assignmentToSlots line 960
def OAI.CubeShuffle.cycleSlotsEquivAssignments line 976
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 (Card d)) (S : Finset (Card d)) (r : Fin A → ℕ) :
    CycleSlots p S r ≃ SlotAssignment p S r where
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.CycleSlots, OAI.CubeShuffle.SlotAssignment
abbrev OAI.CubeShuffle.LengthClass line 997
def OAI.CubeShuffle.slotClass line 999
abbrev OAI.CubeShuffle.SlotsOfLength line 1002
abbrev OAI.CubeShuffle.CyclesOfLength line 1003
instance OAI.CubeShuffle.(instance at line 1006) line 1006
abbrev OAI.CubeShuffle.GroupedAssignments line 1009
def OAI.CubeShuffle.assignmentToGroups line 1012
def OAI.CubeShuffle.groupsEmbedding line 1017
def OAI.CubeShuffle.groupsToAssignment line 1024
def OAI.CubeShuffle.assignmentEquivGroups line 1029
lemma OAI.CubeShuffle.card_cycleSlots_factorial line 1044
lemma OAI.CubeShuffle.butterfly_factorial_moment line 1055
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 (Card d)) (r : Fin A → ℕ) (hr : Monotone r) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
       (∏ j : LengthClass r,
         (Fintype.card (CyclesOfLength (butterflyPerm d (decodeButterfly d ω)) 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.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.LengthClass, OAI.CubeShuffle.CyclesOfLength, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.SlotsOfLength
def OAI.CubeShuffle.assignmentRelabel line 1069
lemma OAI.CubeShuffle.card_cycleSlots_relabel line 1078
lemma OAI.CubeShuffle.butterfly_cycleSlots_moment_all line 1084
abbrev OAI.CubeShuffle.ShortCycle line 1094
instance OAI.CubeShuffle.(instance at line 1097) line 1097
def OAI.CubeShuffle.shortCycleLength line 1100
lemma OAI.CubeShuffle.shortCycleLength_add_one line 1104
def OAI.CubeShuffle.shortEmbeddingEquiv line 1110
lemma OAI.CubeShuffle.shortCycle_factorial_eq line 1136

lemma OAI.CubeShuffle.factorial_mgf line 1151

Source documentation

A bounded integer variable with Poisson-dominated falling factorial moments has the corresponding exponential generating-function bound.

lemma factorial_mgf {Ω : Type*} [Fintype Ω] (F : Ω → ℕ) (k : ℕ) (Λ q : ℝ)
    (hF : ∀ ω, F ω ≤ k) (hΛ : 0 ≤ Λ) (hq : 1 ≤ q)
    (hm : ∀ a, finiteMean (fun ω => ((F ω).descFactorial a : ℝ)) ≤ Λ^a) :
    finiteMean (fun ω => q^(F ω)) ≤ Real.exp ((q-1)*Λ) := by
…

Mentions: OAI.CubeShuffle.finiteMean

lemma OAI.CubeShuffle.inv_sqrt_step line 1188
lemma OAI.CubeShuffle.sum_inv_sqrt line 1196
lemma OAI.CubeShuffle.butterfly_shortCycle_moment line 1211
def OAI.CubeShuffle.cycleMass line 1230
lemma OAI.CubeShuffle.cycleMass_le line 1233
lemma OAI.CubeShuffle.shortCycle_card_le line 1251
lemma OAI.CubeShuffle.butterfly_shortCycle_mgf line 1260
abbrev OAI.CubeShuffle.LongCycle line 1274
instance OAI.CubeShuffle.(instance at line 1276) line 1276
lemma OAI.CubeShuffle.selectedCycle_card_split line 1279
lemma OAI.CubeShuffle.longCycle_card_bound line 1285
lemma OAI.CubeShuffle.finiteMean_pos line 1301
lemma OAI.CubeShuffle.longCycle_pow_bound line 1307
lemma OAI.CubeShuffle.butterfly_cycle_log_mgf line 1322
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 (Card d)) (J : ℕ) (hJ : 0 < J)
    (q : ℝ) (hq : 1 ≤ q) :
    Real.log (finiteMean (fun ω : SwitchIndex d → Bool =>
      q^(Fintype.card (SelectedCycle (butterflyPerm d (decodeButterfly d ω)) S)))) ≤
      (S.card : ℝ)/J * Real.log q + 2*q*S.card*Real.sqrt J / Real.sqrt ((2:ℝ)^d) := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.SelectedCycle, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly