The unconditional concrete local fusion

For each nonzero vector this module instantiates the generic scheduling recursion with the prepared local blocks. It then converts the bounded deletion at every stage into a block-density certificate for every relevant code. No marker sequence is used.

Specialization of the numerical schedule

@[reducible, inline]

abbrev Wallace.ConcreteFusionRun.blockSize : ℕ → ℕ

The finite-block size schedule used by the concrete integer construction.

Equations

• Wallace.ConcreteFusionRun.blockSize = Wallace.FusionSchedule.blockSize

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

@[reducible, inline]

noncomputable abbrev Wallace.ConcreteFusionRun.independenceBound : ℕ → ℕ

The bounded-independence threshold at each fusion stage.

Equations

• Wallace.ConcreteFusionRun.independenceBound = Wallace.FusionSchedule.stageIndependenceBound

@[reducible, inline]

abbrev Wallace.ConcreteFusionRun.localCarrier (x : TriangularPreprocess.ContinuumFreeGroup) : Set TriangularPreprocess.ContinuumIndex

The countable coordinate closure generated by x.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Wallace.ConcreteFusionRun.LocalGroup (x : TriangularPreprocess.ContinuumFreeGroup) : Type

The free Abelian group supported on the local coordinate closure of x.

Equations

• Wallace.ConcreteFusionRun.LocalGroup x = (↑(Wallace.ConcreteFusionRun.localCarrier x) →₀ ℤ)

@[reducible, inline]

noncomputable abbrev Wallace.ConcreteFusionRun.fresh (x : TriangularPreprocess.ContinuumFreeGroup) : ℕ → Finset (LocalGroup x)

The bounded-independent block presented to each local fusion stage.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Wallace.ConcreteFusionRun.enumeration (x : TriangularPreprocess.ContinuumFreeGroup) : ℕ → LocalGroup x

A fixed enumeration of the countable local group.

Equations

• Wallace.ConcreteFusionRun.enumeration x = Wallace.countableFinsuppEnumeration (Wallace.ConcreteFusionRun.localCarrier x) ⋯

noncomputable def Wallace.ConcreteFusionRun.distinguished (x : TriangularPreprocess.ContinuumFreeGroup) : LocalGroup x

The restriction of x to its local coordinate closure.

Equations

• Wallace.ConcreteFusionRun.distinguished x = Finsupp.subtypeDomain (Wallace.ConcreteFusionRun.localCarrier x) x

theorem Wallace.ConcreteFusionRun.distinguished_ne_zero {x : TriangularPreprocess.ContinuumFreeGroup} (hx : x ≠ 0) : distinguished x ≠ 0

The scheduled run

noncomputable def Wallace.ConcreteFusionRun.scheduledCertificate (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : LocalFusion.ScheduledRunCertificate (fresh ↑x) (distinguished ↑x)

The generic recursion, instantiated with the concrete local blocks.

Equations

• Wallace.ConcreteFusionRun.scheduledCertificate x = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev Wallace.ConcreteFusionRun.run (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : LocalFusion.FusionRun (LocalGroup ↑x)

The certified fusion run attached to a nonzero vector.

Equations

• Wallace.ConcreteFusionRun.run x = (Wallace.ConcreteFusionRun.scheduledCertificate x).run

Deleted positions and their density estimate

noncomputable def Wallace.ConcreteFusionRun.deletedPositions (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) (a : ConcreteLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) (l : ℕ) : Finset ℕ

Positions discarded from the block of a relevant code. Away from that code's refined label this definition is harmless; only labelled stages enter its density certificate.

Equations

• One or more equations did not get rendered due to their size.

theorem Wallace.ConcreteFusionRun.deletedPositions_card_le (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) (a : ConcreteLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) (l : ℕ) (hl : l ∈ ConcreteLocalSetup.refinedLabel blockSize blockSize_pos independenceBound (↑x) a) : (deletedPositions x a l).card ≤ FusionSchedule.protectedBound l

theorem Wallace.ConcreteFusionRun.retainedPositions_mem_ultrafilter (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) (a : ConcreteLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) : (BlockSystem.ofBlockPositions blockSize blockSize_pos).retainedBlocks (ConcreteLocalSetup.refinedLabel blockSize blockSize_pos independenceBound (↑x) a) (deletedPositions x a) ∈ BlockData.ultrafilter blockSize blockSize_pos ↑a

Concrete block certificates and the local output

noncomputable def Wallace.ConcreteFusionRun.codeBlocks (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) (a : ConcreteLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) : LocalFusion.ConcreteCodeBlocks blockSize blockSize_pos independenceBound (↑x) (run x) a

The retained-block certificate associated with one relevant sequence code.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.ConcreteFusionRun.localRunCertificate (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : LocalFusion.LocalRunCertificate blockSize blockSize_pos independenceBound x

A complete local fusion certificate for a fixed nonzero vector.

Equations

• Wallace.ConcreteFusionRun.localRunCertificate x = { run := Wallace.ConcreteFusionRun.run x, self_ne_zero := ⋯, codeBlocks := Wallace.ConcreteFusionRun.codeBlocks x }

theorem Wallace.ConcreteFusionRun.exists_localRunCertificate (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : Nonempty (LocalFusion.LocalRunCertificate blockSize blockSize_pos independenceBound x)

theorem Wallace.ConcreteFusionRun.hasLocalSeparatingCharacters : GlobalAssembly.HasLocalSeparatingCharacters blockSize blockSize_pos independenceBound

The local character required by the transfinite extension exists for every nonzero vector.