A local character-fusion core

This file packages the analytic part of the countable fusion separately from the finite stage constructor. A FusionRun records exactly the output of successive applications of bounded deletion and exists_character_fusion_stage: characters, protected finite sets, and retained new sets. From these proved finite-stage certificates we construct the pointwise limit character and derive:

• extension/detection of the distinguished element;
• estimates on every retained block;
• local ultrafilter admissibility.

The second half of the file carries out the scheduling induction for the concrete Wallace data.

The bounded-deletion input to one stage

theorem Wallace.LocalFusion.exists_character_after_deletion {G : Type} [AddCommGroup G] [DecidableEq G] (l : ℕ) (A X : Finset G) (hA : A.card ≤ FusionSchedule.protectedBound l) (hXcard : X.card ≤ FusionSchedule.blockSize l) (hX : FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) X) (old : G →+ UnitAddCircle) : ∃ (Y : Finset G) (next : G →+ UnitAddCircle), Y ⊆ X ∧ (X \ Y).card ≤ A.card ∧ (∀ a ∈ A, ‖next a - old a‖ < FusionSchedule.stageError l) ∧ ∀ y ∈ Y, ‖next y‖ < FusionSchedule.stageError l

A scheduled bounded-deletion and finite-fusion stage.

Certified countable runs and their pointwise limits

structure Wallace.LocalFusion.FusionRun (G : Type u) [AddCommGroup G] : Type u

Data produced by the local fusion induction. Every field is a checkable mathematical certificate: there is no assertion that an arbitrary run exists. The finite scheduling induction and the uniform Kronecker theorem populate these fields directly.

• character : ℕ → G →+ UnitAddCircle

  The character after stage l.

• guardSet : ℕ → Finset G

  The finite set protected while passing from stage l to l+1.

• retained : ℕ → Finset G

  New points retained after bounded deletion at stage l.

• eventually_protected (g : G) : ∀ᶠ (l : ℕ) in Filter.atTop, g ∈ self.guardSet l

  Every element is protected at all sufficiently late stages.

• protected_step (l : ℕ) (g : G) : g ∈ self.guardSet l → dist ((self.character l) g) ((self.character (l + 1)) g) ≤ FusionSchedule.stageError l

  Consecutive characters are close on protected points.

• retained_at_stage (l : ℕ) (g : G) : g ∈ self.retained l → ‖(self.character (l + 1)) g‖ ≤ FusionSchedule.stageError l

  A retained point is nearly annihilated when it is introduced.

• retained_protected (l : ℕ) (g : G) : g ∈ self.retained l → ∀ (k : ℕ), l + 1 ≤ k → g ∈ self.guardSet k

  Once introduced, retained points are protected forever.

theorem Wallace.LocalFusion.FusionRun.tail_step_le {G : Type u} [AddCommGroup G] (R : FusionRun G) (g : G) : ∃ (L : ℕ), ∀ (n : ℕ), dist ((R.character (L + n)) g) ((R.character (L + n + 1)) g) ≤ FusionSchedule.stageError (L + n)

A pointwise tail of a certified fusion has the geometric step estimate.

theorem Wallace.LocalFusion.FusionRun.cauchySeq {G : Type u} [AddCommGroup G] (R : FusionRun G) (g : G) : CauchySeq fun (l : ℕ) => (R.character l) g

Every coordinate of a certified fusion is Cauchy.

noncomputable def Wallace.LocalFusion.FusionRun.limitCharacter {G : Type u} [AddCommGroup G] (R : FusionRun G) : G →+ UnitAddCircle

The local character obtained as the pointwise limit of a certified run.

Equations

• R.limitCharacter = Wallace.pointwiseLimitCharacter R.character ⋯

theorem Wallace.LocalFusion.FusionRun.tendsto_limitCharacter {G : Type u} [AddCommGroup G] (R : FusionRun G) (g : G) : Filter.Tendsto (fun (l : ℕ) => (R.character l) g) Filter.atTop (nhds (R.limitCharacter g))

theorem Wallace.LocalFusion.FusionRun.norm_limitCharacter_le_of_mem_retained {G : Type u} [AddCommGroup G] (R : FusionRun G) (l : ℕ) {g : G} (hg : g ∈ R.retained l) : ‖R.limitCharacter g‖ ≤ 2 * FusionSchedule.stageError l

The final value of a retained point is bounded by twice the stage error: one stage error when the point is introduced, plus the subsequent geometric tail.

Initial detection

theorem Wallace.LocalFusion.FusionRun.dist_limitCharacter_le_initial {G : Type u} [AddCommGroup G] (R : FusionRun G) (x : G) (hprotect : ∀ (l : ℕ), x ∈ R.guardSet l) : dist ((R.character 0) x) (R.limitCharacter x) ≤ ∑' (l : ℕ), FusionSchedule.stageError l

If a distinguished point is protected at every stage and has prescribed initial value, its limit remains close to that value.

theorem Wallace.LocalFusion.FusionRun.limitCharacter_ne_zero_of_initial_half {G : Type u} [AddCommGroup G] (R : FusionRun G) {x : G} (hhalf : (R.character 0) x = ↑(1 / 2)) (hprotect : ∀ (l : ℕ), x ∈ R.guardSet l) : R.limitCharacter x ≠ 0

Starting at the half-period and protecting x throughout makes the limiting character nonzero.

Retained blocks imply local ultrafilter admissibility

structure Wallace.LocalFusion.FusionRun.CodeBlocks {G : Type u} [AddCommGroup G] (R : FusionRun G) : Type u

Abstract block data associated with one relevant code in the local closure.

• p : Ultrafilter ℕ

  The ultrafilter used for this code.

• block : ℕ → Finset ℕ

  The finite block at each stage label.

• labels : Set ℕ

  The stages assigned to this code.

• deletions : ℕ → Finset ℕ

  The positions deleted from each block.

• difference : ℕ → G

  The local group difference represented by each position.

• retained_mem : ⋃ l ∈ self.labels, ↑(self.block l \ self.deletions l) ∈ self.p
• retained_in_stage (l n : ℕ) : l ∈ self.labels → n ∈ self.block l \ self.deletions l → self.difference n ∈ R.retained l

theorem Wallace.LocalFusion.FusionRun.norm_limit_difference_le_on_retained {G : Type u} [AddCommGroup G] (R : FusionRun G) (B : R.CodeBlocks) {n : ℕ} (hn : n ∈ ⋃ l ∈ B.labels, ↑(B.block l \ B.deletions l)) : ∃ l ∈ B.labels, n ∈ B.block l \ B.deletions l ∧ ‖R.limitCharacter (B.difference n)‖ ≤ 2 * FusionSchedule.stageError l

On every retained index, the norm of the limiting character is controlled by twice the stage error of the unique block containing that index.

theorem Wallace.LocalFusion.FusionRun.tendsto_limit_difference_zero_of_blockPositions {G : Type u} [AddCommGroup G] (R : FusionRun G) (B : R.CodeBlocks) (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (hp : ↑B.p ≤ Filter.cofinite) (hblock : ∀ (l : ℕ), B.block l = TriangularPreprocess.blockPositions N hN l) : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (B.difference n)) (↑B.p) (nhds 0)

Concrete block-position version of tendsto_limit_difference_zero. Here freeness of the ultrafilter and the partition theorem for blockPositions supply the required divergence of block labels automatically.

theorem Wallace.LocalFusion.FusionRun.tendsto_limit_prepared {G : Type u} [AddCommGroup G] (R : FusionRun G) (B : R.CodeBlocks) (prepared : ℕ → G) (basis : G) (hdifference : ∀ (n : ℕ), B.difference n = prepared n - basis) (hzero : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (B.difference n)) (↑B.p) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (prepared n)) (↑B.p) (nhds (R.limitCharacter basis))

Additivity turns convergence of the differences into the required local admissibility equation.

structure Wallace.LocalFusion.FusionRun.PreparedCodeBlocks {G : Type u} [AddCommGroup G] (R : FusionRun G) (p : Ultrafilter ℕ) (block : ℕ → Finset ℕ) (difference : ℕ → G) : Type u

A block certificate whose abstract fields are identified with a particular prepared sequence, ultrafilter, and block partition.

• blocks : R.CodeBlocks

  The underlying retained-block data.

• p_eq : self.blocks.p = p
• block_eq (l : ℕ) : self.blocks.block l = block l
• difference_eq (n : ℕ) : self.blocks.difference n = difference n

theorem Wallace.LocalFusion.FusionRun.PreparedCodeBlocks.tendsto_prepared {G : Type u} [AddCommGroup G] {R : FusionRun G} {p : Ultrafilter ℕ} {block : ℕ → Finset ℕ} {difference prepared : ℕ → G} {basis : G} (C : R.PreparedCodeBlocks p block difference) (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (hp : ↑p ≤ Filter.cofinite) (hblock : ∀ (l : ℕ), block l = TriangularPreprocess.blockPositions N hN l) (hdifference : ∀ (n : ℕ), difference n = prepared n - basis) : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (prepared n)) (↑p) (nhds (R.limitCharacter basis))

A prepared block certificate supplies the corresponding ultrafilter limit.

A generic concrete scheduling recursion

structure Wallace.LocalFusion.FusionState (G : Type) [AddCommGroup G] (l : ℕ) : Type

The finite state before stage l: its character and the union of every set retained at earlier stages. The cardinality invariant is the exact invariant used by protectedBound.

• character : G →+ UnitAddCircle

  The character constructed before stage l.

• pastRetained : Finset G

  The union of all finite sets retained before stage l.

• pastRetained_card_le : self.pastRetained.card ≤ FusionSchedule.accumulatedSize l

def Wallace.LocalFusion.stageGuard {G : Type} [AddCommGroup G] [DecidableEq G] (enumeration : ℕ → G) (x : G) (l : ℕ) (S : FusionState G l) : Finset G

The stage guard contains the distinguished point, an initial segment of a surjective enumeration, and every point retained before the stage.

Equations

• Wallace.LocalFusion.stageGuard enumeration x l S = S.pastRetained ∪ {x} ∪ Finset.image enumeration (Finset.range (l + 1))

theorem Wallace.LocalFusion.stageGuard_card_le {G : Type} [AddCommGroup G] [DecidableEq G] (enumeration : ℕ → G) (x : G) (l : ℕ) (S : FusionState G l) : (stageGuard enumeration x l S).card ≤ FusionSchedule.protectedBound l

structure Wallace.LocalFusion.FusionStep {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (l : ℕ) (S : FusionState G l) : Type

All data selected at one fusion stage.

• retained : Finset G

  The subset of the fresh block retained at this stage.

• next : G →+ UnitAddCircle

  The character produced by this stage.

• retained_subset : self.retained ⊆ fresh l
• deleted_card_le : (fresh l \ self.retained).card ≤ (stageGuard enumeration x l S).card
• protected_closeness (g : G) : g ∈ stageGuard enumeration x l S → dist (S.character g) (self.next g) ≤ FusionSchedule.stageError l
• retained_small (g : G) : g ∈ self.retained → ‖self.next g‖ ≤ FusionSchedule.stageError l

theorem Wallace.LocalFusion.fusionStep_nonempty {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (l : ℕ) (S : FusionState G l) : Nonempty (FusionStep fresh enumeration x l S)

The finite deletion/fusion theorem supplies the next state at every stage.

noncomputable def Wallace.LocalFusion.chosenFusionStep {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (l : ℕ) (S : FusionState G l) : FusionStep fresh enumeration x l S

A stage choice, fixed once and reused by both the state recursion and its certificate.

Equations

• Wallace.LocalFusion.chosenFusionStep fresh enumeration x hfresh_card hfresh_independent l S = Classical.choice ⋯

noncomputable def Wallace.LocalFusion.nextFusionState {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (l : ℕ) (S : FusionState G l) : FusionState G (l + 1)

Update the state using the single chosen stage certificate.

Equations

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

def Wallace.LocalFusion.fusionStates {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (initial : G →+ UnitAddCircle) (l : ℕ) : FusionState G l

The dependent natural-number recursion starting from initial.

Equations

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

@[simp]

theorem Wallace.LocalFusion.fusionStates_zero {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (initial : G →+ UnitAddCircle) : (fusionStates fresh enumeration x hfresh_card hfresh_independent initial 0).character = initial

theorem Wallace.LocalFusion.fusionStates_pastRetained_subset_succ {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (initial : G →+ UnitAddCircle) (l : ℕ) : (Wallace.LocalFusion.states✝ fresh enumeration x hfresh_card hfresh_independent initial l).pastRetained ⊆ (Wallace.LocalFusion.states✝ fresh enumeration x hfresh_card hfresh_independent initial (l + 1)).pastRetained

theorem Wallace.LocalFusion.fusionStates_pastRetained_mono {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (initial : G →+ UnitAddCircle) : Monotone fun (l : ℕ) => (Wallace.LocalFusion.states✝ fresh enumeration x hfresh_card hfresh_independent initial l).pastRetained

noncomputable def Wallace.LocalFusion.scheduledRun {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (initial : G →+ UnitAddCircle) (henumeration : Function.Surjective enumeration) : FusionRun G

The fully scheduled run associated with a chosen initial character.

Equations

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

structure Wallace.LocalFusion.ScheduledRunCertificate {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (x : G) : Type

Public certificate exported by the scheduling recursion.

• run : FusionRun G

  The certified infinite fusion run.

• initial_half : (self.run.character 0) x = ↑(1 / 2)
• distinguished_protected (l : ℕ) : x ∈ self.run.guardSet l
• retained_subset (l : ℕ) : self.run.retained l ⊆ fresh l
• deleted_card_le (l : ℕ) : (fresh l \ self.run.retained l).card ≤ (self.run.guardSet l).card
• guard_card_le (l : ℕ) : (self.run.guardSet l).card ≤ FusionSchedule.protectedBound l

theorem Wallace.LocalFusion.exists_scheduledRunCertificate_of_initial_half {G : Type} [AddCommGroup G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (initial : G →+ UnitAddCircle) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (hinitial : initial x = ↑(1 / 2)) (henumeration : Function.Surjective enumeration) : Nonempty (ScheduledRunCertificate fresh x)

Starting with the exact half-turn character and applying the dependent recursion produces a complete certified run; no run is assumed as input.

theorem Wallace.LocalFusion.exists_scheduledRunCertificate {G : Type} [AddCommGroup G] [IsAddTorsionFree G] [DecidableEq G] (fresh : ℕ → Finset G) (enumeration : ℕ → G) (x : G) (hx : x ≠ 0) (hfresh_card : ∀ (l : ℕ), (fresh l).card ≤ FusionSchedule.blockSize l) (hfresh_independent : ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (FusionSchedule.stageIndependenceBound l) (fresh l)) (henumeration : Function.Surjective enumeration) : Nonempty (ScheduledRunCertificate fresh x)

Fully existential form of the generic scheduling recursion.

Interface from concrete runs to the global assembly

@[reducible, inline]

abbrev Wallace.LocalFusion.ConcreteCodeBlocks (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (R : FusionRun (↑(ConcreteClosure.closure N hN M x) →₀ ℤ)) (a : ConcreteLocalSetup.RelevantCode N hN M x) : Type

Integer specialization of the shared prepared-block certificate.

Equations

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

theorem Wallace.LocalFusion.ConcreteCodeBlocks.tendsto_prepared {N : ℕ → ℕ} {hN : ∀ (l : ℕ), 0 < N l} {M : ℕ → ℕ} {x : TriangularPreprocess.ContinuumFreeGroup} {R : FusionRun (↑(ConcreteClosure.closure N hN M x) →₀ ℤ)} {a : ConcreteLocalSetup.RelevantCode N hN M x} (C : ConcreteCodeBlocks N hN M x R a) : Filter.Tendsto (fun (n : ℕ) => R.limitCharacter (Finsupp.subtypeDomain (ConcreteClosure.closure N hN M x) (ConcreteData.prepared N hN M (↑a) n))) (↑(BlockData.ultrafilter N hN ↑a)) (nhds (R.limitCharacter (Finsupp.single ⟨TriangularPreprocess.codeIndex ↑a, ⋯⟩ 1)))

A concrete retained-block certificate gives precisely the local admissibility equation for its relevant code.

structure Wallace.LocalFusion.LocalRunCertificate (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : Type

Complete local output for one distinguished nonzero vector. This is a deliberately small interface: a concrete scheduling recursion supplies the run and one block certificate for each relevant code; all limiting arguments are discharged above.

• run : FusionRun (↑(ConcreteClosure.closure N hN M ↑x) →₀ ℤ)

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

• self_ne_zero : self.run.limitCharacter (Finsupp.subtypeDomain (ConcreteClosure.closure N hN M ↑x) ↑x) ≠ 0
• codeBlocks (a : ConcreteLocalSetup.RelevantCode N hN M ↑x) : ConcreteCodeBlocks N hN M (↑x) self.run a

  A retained-block certificate for every locally relevant code.

theorem Wallace.LocalFusion.LocalRunCertificate.locallyAdmissible {N : ℕ → ℕ} {hN : ∀ (l : ℕ), 0 < N l} {M : ℕ → ℕ} {x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }} (C : LocalRunCertificate N hN M x) : TransfiniteExtension.LocallyAdmissible (ConcreteData.transfiniteData N hN M) (ConcreteClosure.closure N hN M ↑x) C.run.limitCharacter

The concrete run certificate satisfies the exact local interface consumed by the transfinite-extension and global-assembly modules.

theorem Wallace.LocalFusion.hasLocalSeparatingCharacters_of_certificates (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : ∀ (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }), Nonempty (LocalRunCertificate N hN M x)) : GlobalAssembly.HasLocalSeparatingCharacters N hN M

It is enough to construct a certified concrete fusion run for every nonzero vector.