The unconditional local fusion for the rational direct sum

For each nonzero rational vector this module instantiates the generic fusion recursion with the prepared local blocks, proves the density bound for deleted positions, and packages the resulting separating, locally admissible character.

@[reducible, inline]

abbrev Wallace.RationalFusionRun.blockSize : ℕ → ℕ

The finite-block size schedule used by the rational construction.

Equations

• Wallace.RationalFusionRun.blockSize = Wallace.FusionSchedule.blockSize

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

@[reducible, inline]

noncomputable abbrev Wallace.RationalFusionRun.independenceBound : ℕ → ℕ

The bounded-independence threshold at each fusion stage.

Equations

• Wallace.RationalFusionRun.independenceBound = Wallace.FusionSchedule.stageIndependenceBound

@[reducible, inline]

abbrev Wallace.RationalFusionRun.localCarrier (x : RationalTriangularPreprocess.ContinuumRationalGroup) : Set RationalTriangularPreprocess.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.RationalFusionRun.LocalGroup (x : RationalTriangularPreprocess.ContinuumRationalGroup) : Type

The rational direct sum supported on the local coordinate closure of x.

Equations

• Wallace.RationalFusionRun.LocalGroup x = (↑(Wallace.RationalFusionRun.localCarrier x) →₀ ℚ)

@[reducible, inline]

noncomputable abbrev Wallace.RationalFusionRun.fresh (x : RationalTriangularPreprocess.ContinuumRationalGroup) : ℕ → 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.RationalFusionRun.localEnumeration (x : RationalTriangularPreprocess.ContinuumRationalGroup) : ℕ → LocalGroup x

A fixed surjection used to make every local point eventually protected.

Equations

• Wallace.RationalFusionRun.localEnumeration x = Wallace.countableFinsuppEnumeration (Wallace.RationalFusionRun.localCarrier x) ⋯

noncomputable def Wallace.RationalFusionRun.distinguished (x : RationalTriangularPreprocess.ContinuumRationalGroup) : LocalGroup x

The restriction of x to its local coordinate closure.

Equations

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

theorem Wallace.RationalFusionRun.distinguished_ne_zero {x : RationalTriangularPreprocess.ContinuumRationalGroup} (hx : x ≠ 0) : distinguished x ≠ 0

noncomputable def Wallace.RationalFusionRun.scheduledCertificate (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : LocalFusion.ScheduledRunCertificate (fresh ↑x) (distinguished ↑x)

The generic scheduling recursion instantiated on the rational local group.

Equations

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

@[reducible, inline]

noncomputable abbrev Wallace.RationalFusionRun.run (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : LocalFusion.FusionRun (LocalGroup ↑x)

The certified fusion run attached to a nonzero rational vector.

Equations

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

noncomputable def Wallace.RationalFusionRun.deletedPositions (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) (l : ℕ) : Finset ℕ

Positions discarded from the block assigned to a relevant code.

Equations

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

theorem Wallace.RationalFusionRun.deletedPositions_card_le (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) (l : ℕ) (hl : l ∈ RationalLocalSetup.refinedLabel blockSize blockSize_pos independenceBound (↑x) a) : (deletedPositions x a l).card ≤ FusionSchedule.protectedBound l

theorem Wallace.RationalFusionRun.retainedPositions_mem_ultrafilter (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) : (BlockSystem.ofBlockPositions blockSize blockSize_pos).retainedBlocks (RationalLocalSetup.refinedLabel blockSize blockSize_pos independenceBound (↑x) a) (deletedPositions x a) ∈ BlockData.ultrafilter blockSize blockSize_pos ↑a

Rational block and run certificates

@[reducible, inline]

abbrev Wallace.RationalFusionRun.RationalCodeBlocks (x : RationalTriangularPreprocess.ContinuumRationalGroup) (R : LocalFusion.FusionRun (LocalGroup x)) (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound x) : Type

Rational specialization of the shared prepared-block certificate.

Equations

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

theorem Wallace.RationalFusionRun.RationalCodeBlocks.tendsto_prepared {x : RationalTriangularPreprocess.ContinuumRationalGroup} {R : LocalFusion.FusionRun (LocalGroup x)} {a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound x} (C : RationalCodeBlocks x R a) : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (Finsupp.subtypeDomain (localCarrier x) (RationalData.prepared blockSize blockSize_pos independenceBound (↑a) n))) (↑(BlockData.ultrafilter blockSize blockSize_pos ↑a)) (nhds (R.limitCharacter (Finsupp.single ⟨RationalTriangularPreprocess.codeIndex ↑a, ⋯⟩ 1)))

structure Wallace.RationalFusionRun.LocalRunCertificate (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : Type

Complete local fusion output for one nonzero rational vector.

• run : LocalFusion.FusionRun (LocalGroup ↑x)

  The fusion run on the countable local group generated by x.

• self_ne_zero : self.run.limitCharacter (Finsupp.subtypeDomain (localCarrier ↑x) ↑x) ≠ 0
• codeBlocks (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) : RationalCodeBlocks (↑x) self.run a

  A retained-block certificate for every locally relevant code.

theorem Wallace.RationalFusionRun.LocalRunCertificate.locallyAdmissible {x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }} (C : LocalRunCertificate x) : RationalTransfiniteExtension.LocallyAdmissible (RationalData.transfiniteData blockSize blockSize_pos independenceBound) (localCarrier ↑x) C.run.limitCharacter

noncomputable def Wallace.RationalFusionRun.codeBlocks (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) (a : RationalLocalSetup.RelevantCode blockSize blockSize_pos independenceBound ↑x) : RationalCodeBlocks (↑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.RationalFusionRun.localRunCertificate (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : LocalRunCertificate x

Complete local separating and admissibility certificate.

Equations

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