A concrete schedule for the Wallace fusion

This file fixes, once and for all, the numerical parameters used by the character-fusion construction. At stage l, accumulatedSize l is the total size allotted to all earlier blocks, protectedBound l bounds the finite set whose character values must be protected, and blockSize l is the size of the new block. The identity

blockSize l = (l + 2) * protectedBound l

makes the discarded proportion tend to zero. The errors form a geometric series of total mass 1 / 32, leaving a large margin around an initial character value of 1 / 2.

def Wallace.FusionSchedule.accumulatedSize : ℕ → ℕ

Total number of positions allotted to blocks strictly before stage l.

Equations

• Wallace.FusionSchedule.accumulatedSize 0 = 0
• Wallace.FusionSchedule.accumulatedSize l.succ = Wallace.FusionSchedule.accumulatedSize l + (l + 2) * (Wallace.FusionSchedule.accumulatedSize l + 2 * l + 2)

def Wallace.FusionSchedule.protectedBound (l : ℕ) : ℕ

Cardinality bound for the protected set at stage l.

Equations

• Wallace.FusionSchedule.protectedBound l = Wallace.FusionSchedule.accumulatedSize l + 2 * l + 2

def Wallace.FusionSchedule.blockSize (l : ℕ) : ℕ

Size of the fresh finite block at stage l.

Equations

• Wallace.FusionSchedule.blockSize l = (l + 2) * Wallace.FusionSchedule.protectedBound l

@[simp]

theorem Wallace.FusionSchedule.accumulatedSize_succ (l : ℕ) : accumulatedSize (l + 1) = accumulatedSize l + blockSize l

theorem Wallace.FusionSchedule.protectedBound_pos (l : ℕ) : 0 < protectedBound l

theorem Wallace.FusionSchedule.accumulatedSize_add_le_protectedBound (l : ℕ) : accumulatedSize l + l + 2 ≤ protectedBound l

theorem Wallace.FusionSchedule.protectedBound_ne_zero (l : ℕ) : protectedBound l ≠ 0

theorem Wallace.FusionSchedule.blockSize_pos (l : ℕ) : 0 < blockSize l

theorem Wallace.FusionSchedule.protectedBound_div_blockSize (l : ℕ) : ↑(protectedBound l) / ↑(blockSize l) = 1 / (↑l + 2)

The exact discarded-proportion identity behind the density-one argument.

theorem Wallace.FusionSchedule.tendsto_protectedBound_div_blockSize : Filter.Tendsto (fun (l : ℕ) => ↑(protectedBound l) / ↑(blockSize l)) Filter.atTop (nhds 0)

The proportion of a block which bounded deletion may discard tends to zero.

noncomputable def Wallace.FusionSchedule.stageError (l : ℕ) : ℝ

Stage error. In elementary notation this is 2^(-(l+6)).

Equations

• Wallace.FusionSchedule.stageError l = 1 / 32 / 2 / 2 ^ l

theorem Wallace.FusionSchedule.stageError_pos (l : ℕ) : 0 < stageError l

theorem Wallace.FusionSchedule.stageError_add (L n : ℕ) : stageError (L + n) = stageError L / 2 ^ n

Exact geometric-tail identity, convenient for the completeness estimate.

theorem Wallace.FusionSchedule.hasSum_stageError_add (L : ℕ) : HasSum (fun (n : ℕ) => stageError (L + n)) (2 * stageError L)

The tail beginning at stage L has total mass exactly 2 * stageError L.

theorem Wallace.FusionSchedule.summable_stageError_add (L : ℕ) : Summable fun (n : ℕ) => stageError (L + n)

theorem Wallace.FusionSchedule.tsum_stageError_add (L : ℕ) : ∑' (n : ℕ), stageError (L + n) = 2 * stageError L

theorem Wallace.FusionSchedule.summable_stageError : Summable stageError

theorem Wallace.FusionSchedule.tendsto_stageError : Filter.Tendsto stageError Filter.atTop (nhds 0)

theorem Wallace.FusionSchedule.tsum_stageError : ∑' (l : ℕ), stageError l = 1 / 32

The total perturbation budget of the entire fusion is 1/32.

noncomputable def Wallace.FusionSchedule.independenceBound (l Q : ℕ) : ℕ

Independence threshold used before the bounded-deletion step.

Equations

• Wallace.FusionSchedule.independenceBound l Q = Wallace.FiniteCombinatorics.deletionIndependenceBound (Wallace.FusionSchedule.protectedBound l) Q

Uniform Kronecker and deletion bounds

def Wallace.FusionSchedule.tupleLengthBound (l : ℕ) : ℕ

Maximum tuple length which can occur at stage l.

Equations

• Wallace.FusionSchedule.tupleLengthBound l = Wallace.FusionSchedule.protectedBound l + Wallace.FusionSchedule.blockSize l

noncomputable def Wallace.FusionSchedule.rawKroneckerBound (l m : ℕ) : ℕ

One uniform Kronecker bound for a fixed tuple length. All groups in the Wallace construction live in universe zero, so fixing that universe here makes the numerical schedule literally a single sequence of natural numbers.

Equations

• Wallace.FusionSchedule.rawKroneckerBound l m = Classical.choose ⋯

theorem Wallace.FusionSchedule.rawKroneckerBound_spec (l m : ℕ) : IsUniformKroneckerBound m (stageError l) (rawKroneckerBound l m)

noncomputable def Wallace.FusionSchedule.kroneckerBound (l : ℕ) : ℕ

A single relation-height bound which works for every positive tuple length possible at stage l. This is the paper's maximum over 1 ≤ m ≤ R_l + N_l; the maximum with 1 is used by the finite disjointness argument. The empty-tuple case is handled separately below and does not enter the numerical schedule.

Equations

• Wallace.FusionSchedule.kroneckerBound l = max 1 ((Finset.Icc 1 (Wallace.FusionSchedule.tupleLengthBound l)).sup (Wallace.FusionSchedule.rawKroneckerBound l))

theorem Wallace.FusionSchedule.one_le_kroneckerBound (l : ℕ) : 1 ≤ kroneckerBound l

theorem Wallace.FusionSchedule.rawKroneckerBound_le (l m : ℕ) (hm0 : 0 < m) (hm : m ≤ tupleLengthBound l) : rawKroneckerBound l m ≤ kroneckerBound l

theorem Wallace.FusionSchedule.kroneckerBound_spec_zero (l : ℕ) : IsUniformKroneckerBound 0 (stageError l) (kroneckerBound l)

The uniform Kronecker assertion is vacuous for an empty tuple, so no value q(0, ε_l) is needed in the paper's maximum.

theorem Wallace.FusionSchedule.kroneckerBound_spec (l m : ℕ) (hm : m ≤ tupleLengthBound l) : IsUniformKroneckerBound m (stageError l) (kroneckerBound l)

The scheduled height bound is valid for every tuple that can occur at this stage.

noncomputable def Wallace.FusionSchedule.stageIndependenceBound (l : ℕ) : ℕ

The independence threshold M_l used in the preprocessing of stage l.

Equations

• Wallace.FusionSchedule.stageIndependenceBound l = Wallace.FusionSchedule.independenceBound l (Wallace.FusionSchedule.kroneckerBound l)

theorem Wallace.FusionSchedule.card_union_le_tupleLengthBound {G : Type u_1} [DecidableEq G] {l : ℕ} {A Y : Finset G} (hA : A.card ≤ protectedBound l) (hY : Y.card ≤ blockSize l) : (A ∪ Y).card ≤ tupleLengthBound l

theorem Wallace.FusionSchedule.exists_stage_deletion {G : Type u_1} [AddCommGroup G] [DecidableEq G] {l : ℕ} (A X : Finset G) (hA : A.card ≤ protectedBound l) (hX : FiniteCombinatorics.BoundedIndependent (stageIndependenceBound l) X) : ∃ Y ⊆ X, (X \ Y).card ≤ A.card ∧ FiniteCombinatorics.MixedRelationFree (kroneckerBound l) A Y

The bounded-deletion lemma specialized to the numerical schedule.