Basic.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

The physical Thorp chain on every binary position. A tape enumerates independent fair pair coins; its push-forward is the full permutation distribution.

abbrev OAI.CubeShuffle.Card line 15
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:165 (same declaration text).
def OAI.CubeShuffle.Coins line 19
Source documentation
One coin for each pair, indexed by the unchanged tail of a binary position. The one-card case is the deterministic extension of the physical definition.
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:167 (same declaration text).
```
def Coins : ℕ → Type
  | 0 => Unit
  | d + 1 => Card d → Bool
```
Mentions: OAI.CubeShuffle.Card
instance OAI.CubeShuffle.(instance at line 23) line 23
instance OAI.CubeShuffle.(instance at line 26) line 26
def OAI.CubeShuffle.switchFun line 30
Source documentation
Switch the first-coordinate pairs, without rotating.
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:177 (same declaration text).
```
def switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=
…
```
Mentions: OAI.CubeShuffle.Card
theorem OAI.CubeShuffle.switchFun_involutive line 33
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:180 (same declaration text).
def OAI.CubeShuffle.pairSwitch line 42
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:189 (same declaration text).
def OAI.CubeShuffle.rotate line 49
Source documentation
(x₁,…,x_d) ↦ (x₂,…,x_d,x₁).
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:195 (same declaration text).
```
def rotate (d : ℕ) : Equiv.Perm (Card d) where
…
```
Mentions: OAI.CubeShuffle.Card
def OAI.CubeShuffle.step line 56
Source documentation
One physical shuffle: rotate after independently switching each pair.
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:201 (same declaration text).
```
def step : (d : ℕ) → Coins d → Equiv.Perm (Card d)
  | 0, _ => 1
  | d + 1, ξ => rotate (d + 1) * pairSwitch ξ

/-- The time-t permutation, with the latest physical shuffle multiplying on the left. -/
```
Mentions: OAI.CubeShuffle.Coins, OAI.CubeShuffle.Card, OAI.CubeShuffle.rotate, OAI.CubeShuffle.pairSwitch
def OAI.CubeShuffle.run line 61
Source documentation
The time-t permutation, with the latest physical shuffle multiplying on the left.
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:205 (same declaration text).
```
def run (d : ℕ) : (t : ℕ) → (Fin t → Coins d) → Equiv.Perm (Card d)
  | 0, _ => 1
  | t + 1, ω => step d (ω (Fin.last t)) * run d t (fun i => ω i.castSucc)

/-- The push-forward of the uniform law on all independent fair coin tapes. -/
```
Mentions: OAI.CubeShuffle.Coins, OAI.CubeShuffle.Card, OAI.CubeShuffle.step, OAI.CubeShuffle.law
def OAI.CubeShuffle.law line 66
Source documentation
The push-forward of the uniform law on all independent fair coin tapes.
```
noncomputable def law (d t : ℕ) (g : Equiv.Perm (Card d)) : ℝ :=
…
```
Mentions: OAI.CubeShuffle.Card
def OAI.CubeShuffle.distance line 71
Source documentation
Full-permutation total variation, with the source's factor one half.
```
noncomputable def distance (d t : ℕ) : ℝ :=
…
```
def OAI.CubeShuffle.mixingTime line 77
Source documentation
First physical time with TV at most 1/4. The main conclusion proves this set nonempty for every sufficiently large d.
```
noncomputable def mixingTime (d : ℕ) : ℕ :=
…
```
def OAI.CubeShuffle.supportTimeBound line 81
Source documentation
The exact integer lower bound, using log base two.
```
noncomputable def supportTimeBound (d : ℕ) : ℤ :=
…
```
def OAI.CubeShuffle.OptimalOrder line 87
Source documentation
Every clause of the literal optimal-order endpoint. The single absolute C is in PHYSICAL time; convergence is to zero, not merely below a fixed cutoff.
```
def OptimalOrder : Prop :=
…
```
def OAI.CubeShuffle.finiteLaw line 101
Source documentation
A finite uniform experiment pushed forward by an arbitrary map.
```
noncomputable def finiteLaw {α β : Type*} [Fintype α] (f : α → β) (b : β) : ℝ := by
…
```
lemma OAI.CubeShuffle.sum_card_fibers line 105
lemma OAI.CubeShuffle.finiteLaw_nonneg line 111
lemma OAI.CubeShuffle.finiteLaw_sum line 115
lemma OAI.CubeShuffle.finiteLaw_eq_zero_of_not_mem line 124

lemma OAI.CubeShuffle.event_le_totalVariation line 132

Source documentation

An event discrepancy is bounded by one-half L1, with no missing factor of two.

lemma event_le_totalVariation {β : Type*} [Fintype β] [DecidableEq β]
    (p q : β → ℝ) (hpq : ∑ b, (p b - q b) = 0) (s : Finset β) :
    (∑ b ∈ s, p b) - (∑ b ∈ s, q b) ≤ (1 / 2 : ℝ) * ∑ b, |p b - q b| := by
…

lemma OAI.CubeShuffle.finiteLaw_support_bound line 147

Source documentation

Information-theoretic support obstruction for a finite uniform experiment.

lemma finiteLaw_support_bound {α β : Type*} [Fintype α] [Nonempty α]
    [Fintype β] [Nonempty β] (f : α → β) :
    1 - (Fintype.card α : ℝ) / (Fintype.card β : ℝ) ≤
      (1 / 2 : ℝ) * ∑ b, |finiteLaw f b - 1 / (Fintype.card β : ℝ)| := by
…

Mentions: OAI.CubeShuffle.finiteLaw

lemma OAI.CubeShuffle.card_positions line 171
Also declared: ComparatorChallenges/WeightedSweepMoments.lean:209 (same declaration text).
lemma OAI.CubeShuffle.card_permutations line 174
lemma OAI.CubeShuffle.card_coins_succ line 177
lemma OAI.CubeShuffle.card_tapes_succ line 180
lemma OAI.CubeShuffle.law_eq_finiteLaw line 183
lemma OAI.CubeShuffle.law_nonneg line 189
lemma OAI.CubeShuffle.law_sum line 193
lemma OAI.CubeShuffle.physical_support_bound_succ line 197
lemma OAI.CubeShuffle.step_succ_formula line 206
Source documentation
The coordinate formula in the manuscript, before any sweep conversion.
```
lemma step_succ_formula (d : ℕ) (ξ : Coins (d + 1)) (x : Card (d + 1)) :
    step (d + 1) ξ x = Fin.snoc (Fin.tail x) (Bool.xor (x 0) (ξ (Fin.tail x))) := by
…
```
Mentions: OAI.CubeShuffle.Coins, OAI.CubeShuffle.Card, OAI.CubeShuffle.step
lemma OAI.CubeShuffle.distance_nonneg line 212
lemma OAI.CubeShuffle.physical_support_bound line 217
Source documentation
The exact support clause, uniform over every physical time and deck dimension.
```
lemma physical_support_bound (d t : ℕ) :
    1 - (2 : ℝ) ^ ((t : ℝ) * (2 : ℝ) ^ d / 2) /
      (Nat.factorial (2 ^ d) : ℝ) ≤ distance d t := by
…
```
Mentions: OAI.CubeShuffle.distance
lemma OAI.CubeShuffle.supportTimeBound_le_of_distance_le line 234
Source documentation
Every time that attains the prescribed TV tolerance obeys the integer lower bound.
```
lemma supportTimeBound_le_of_distance_le (d t : ℕ) (ht : distance d t ≤ (1 / 4 : ℝ)) :
    supportTimeBound d ≤ (t : ℤ) := by
…
```
Mentions: OAI.CubeShuffle.distance, OAI.CubeShuffle.supportTimeBound
lemma OAI.CubeShuffle.supportTimeBound_le_mixingTime line 257
Source documentation
Once the defining set is nonempty, its minimum inherits the exact obstruction.
```
lemma supportTimeBound_le_mixingTime {d : ℕ}
    (h : ({t : ℕ | distance d t ≤ (1 / 4 : ℝ)} : Set ℕ).Nonempty) :
    supportTimeBound d ≤ (mixingTime d : ℤ) := by
…
```
Mentions: OAI.CubeShuffle.distance, OAI.CubeShuffle.supportTimeBound, OAI.CubeShuffle.mixingTime
lemma OAI.CubeShuffle.log_factorial_lower line 263
lemma OAI.CubeShuffle.log_three_quarters_lower line 272
lemma OAI.CubeShuffle.linear_le_supportTimeBound line 282
Source documentation
An explicit version of the source's 2d - O(1) support lower bound.
```
lemma linear_le_supportTimeBound (d : ℕ) :
    2 * (d : ℝ) - 4 / Real.log 2 ≤ (supportTimeBound d : ℝ) := by
…
```
Mentions: OAI.CubeShuffle.supportTimeBound
lemma OAI.CubeShuffle.linear_le_time_of_distance_le line 309
lemma OAI.CubeShuffle.entropy_chord line 317
lemma OAI.CubeShuffle.split_entropy_lower line 328
def OAI.CubeShuffle.Butterfly line 364
Source documentation
Two independently routed half-sized butterflies, followed by the final layer of first-coordinate pair switches. Coordinates are named in the reverse of their editing order, as in the manuscript's recursive proof.
```
def Butterfly : ℕ → Type
  | 0 => Unit
  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)
```
Mentions: OAI.CubeShuffle.Card
def OAI.CubeShuffle.childLift line 368
def OAI.CubeShuffle.butterflyPerm line 374
def OAI.CubeShuffle.childMarks line 379
Source documentation
The marked input paths assigned to one of the two recursive children.
```
noncomputable def childMarks {d : ℕ} (s : Finset (Card (d + 1))) (ε : Bool) :
    Finset (Card d) := (s.filter (fun x => x 0 = ε)).image Fin.tail
```
Mentions: OAI.CubeShuffle.Card
lemma OAI.CubeShuffle.card_childMarks line 382
lemma OAI.CubeShuffle.card_childMarks_add line 392
def OAI.CubeShuffle.topMeetings line 401
Source documentation
The switches in the final layer used by two marked paths. A switch is indexed by the common tail at the end of the two child butterflies.
```
noncomputable def topMeetings {d : ℕ} (b : Butterfly (d + 1))
    (s : Finset (Card (d + 1))) : Finset (Card d) :=
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card
lemma OAI.CubeShuffle.card_topMeetings_le line 406

def OAI.CubeShuffle.encounters line 416

Source documentation

Total number of shared switches along the distinct marked routes.

noncomputable def encounters : (d : ℕ) → Butterfly d → Finset (Card d) → ℕ
  | 0, _, _ => 0
  | d + 1, b, s => encounters d (b.2 false) (childMarks s false) +
      encounters d (b.2 true) (childMarks s true) + (topMeetings b s).card

/-- Butterfly encounter estimate (`net:encounters`): no random hypotheses are
needed, and each switch contains at most two paths because each child routes
by a bijection. -/

Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.childMarks, OAI.CubeShuffle.topMeetings

lemma OAI.CubeShuffle.butterfly_encounters line 424
Source documentation
Butterfly encounter estimate (net:encounters): no random hypotheses are needed, and each switch contains at most two paths because each child routes by a bijection.
```
lemma butterfly_encounters (d : ℕ) (b : Butterfly d) (s : Finset (Card d)) :
    (encounters d b s : ℝ) ≤ (s.card : ℝ) * Real.log s.card / (2 * Real.log 2) := by
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.encounters
lemma OAI.CubeShuffle.prod_split_at line 450
lemma OAI.CubeShuffle.prod_split_two line 457

lemma OAI.CubeShuffle.swap_average_product line 473

Source documentation

A fair transposition preserves the upper product bound on every inclusion moment; this is the elementary input used in the factorial-moment route, 11-palindrome.tex:94–97.

lemma swap_average_product {α : Type*} [DecidableEq α] (s : Finset α) (p : α → ℝ)
    (hp : ∀ i, 0 ≤ p i) (a b : α) :
    ((∏ i ∈ s, p i) + ∏ i ∈ s, p (Equiv.swap a b i)) / 2 ≤
      ∏ i ∈ s, (p i + p (Equiv.swap a b i)) / 2 := by
…

def OAI.CubeShuffle.CylinderBound line 511
Source documentation
Abstract inclusion moments m(S) and their coordinate marginal majorant. This definition does not postulate independence.
```
def CylinderBound {α : Type*} (m : Finset α → ℝ) (p : α → ℝ) : Prop :=
…
```
lemma OAI.CubeShuffle.CylinderBound.fair_swap line 514
def OAI.CubeShuffle.finiteMean line 529
Source documentation
Uniform expectation in a finite experiment, kept in the real numbers.
```
noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=
…
```

def OAI.CubeShuffle.inclusionMoment line 533

Source documentation

The inclusion moment of the random marked set F.

noncomputable def inclusionMoment {α Ω : Type*} [Fintype Ω]
    (F : Ω → Finset α) (s : Finset α) : ℝ := by
…

lemma OAI.CubeShuffle.inclusionMoment_nonneg line 538
lemma OAI.CubeShuffle.indicator_subset_prod line 544
lemma OAI.CubeShuffle.inclusionMoment_const line 553
lemma OAI.CubeShuffle.cylinder_const line 560

def OAI.CubeShuffle.fairSetSwap line 569

Source documentation

Add an independent fair coin which chooses whether to transpose a and b.

noncomputable def fairSetSwap {α Ω : Type*} [DecidableEq α]
    (F : Ω → Finset α) (a b : α) : Ω × Bool → Finset α :=
…

lemma OAI.CubeShuffle.subset_swap_image_iff line 573
lemma OAI.CubeShuffle.inclusionMoment_fairSetSwap line 584
lemma OAI.CubeShuffle.cylinder_fairSetSwap line 595
def OAI.CubeShuffle.SwitchSamples line 606
Source documentation
An explicit product of independent fair coins, of a recursively specified length.
```
def SwitchSamples : ℕ → Type
  | 0 => Unit
  | n + 1 => SwitchSamples n × Bool
```
instance OAI.CubeShuffle.(instance at line 610) line 610
instance OAI.CubeShuffle.(instance at line 615) line 615

def OAI.CubeShuffle.switchedSet line 621

Source documentation

Successive independent fair transpositions, listed in reverse time order.

noncomputable def switchedSet {α : Type*} [DecidableEq α] (A : Finset α) :
    (L : List (α × α)) → SwitchSamples L.length → Finset α
  | [], _ => A
  | (a,b) :: L, ω => fairSetSwap (switchedSet A L) a b ω

/-- Actual inclusion moments after any deterministic sequence of independent
fair switches satisfy the upper product-of-marginals bound. -/

Mentions: OAI.CubeShuffle.SwitchSamples, OAI.CubeShuffle.fairSetSwap

lemma OAI.CubeShuffle.switchedSet_cylinder line 628
Source documentation
Actual inclusion moments after any deterministic sequence of independent fair switches satisfy the upper product-of-marginals bound.
```
lemma switchedSet_cylinder {α : Type*} [DecidableEq α] (A : Finset α)
    (L : List (α × α)) :
    CylinderBound (inclusionMoment (switchedSet A L))
      (fun i => inclusionMoment (switchedSet A L) {i}) := by
…
```
Mentions: OAI.CubeShuffle.CylinderBound, OAI.CubeShuffle.inclusionMoment, OAI.CubeShuffle.switchedSet
lemma OAI.CubeShuffle.finiteMean_congr line 636
lemma OAI.CubeShuffle.finiteMean_add line 642
lemma OAI.CubeShuffle.finiteMean_mul_const line 646
lemma OAI.CubeShuffle.finiteMean_sum line 652
lemma OAI.CubeShuffle.finiteMean_mono line 657
lemma OAI.CubeShuffle.finiteMean_equiv line 661
lemma OAI.CubeShuffle.finiteMean_prod_left line 669
lemma OAI.CubeShuffle.finiteMean_pi_eval line 676
lemma OAI.CubeShuffle.finiteMean_eq_indicator line 687
lemma OAI.CubeShuffle.exp_finiteMean_le line 691