Actual finite refinement runs

A prime is fixed for a prescribed finite radius horizon before the run is built. Unfinished states advance by concrete normalized operations; finished states and stages beyond the horizon keep their state. No infinite sequence of progress certificates is assumed.

structure EGZ.FlagDecomposition.Iteration.NextProgress {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (s : State p d f) (ε δ : ℝ) (g H : ℕ → ℕ) : Type 1

One actual progress step, together with the uniform radius estimate.

• target : State p d f

  State produced by the next certified refinement step.

• progress : Progress s self.target ε δ g

  Certificate of progress from the current state to the target.

• radius_le : self.target.radius ≤ H s.radius

theorem EGZ.FlagDecomposition.Iteration.exists_nextProgress {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) {i : ℕ} (s : BoundedState P ε i) (hprime : P.primeThreshold s.radius < p) (hnot : ¬s.Finished ε (stageScale d ε i) g) : Nonempty (NextProgress s.toState ε (stageScale d ε i) g P.radiusGrowth)

noncomputable def EGZ.FlagDecomposition.Iteration.nextProgress {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) {i : ℕ} (s : BoundedState P ε i) (hprime : P.primeThreshold s.radius < p) (hnot : ¬s.Finished ε (stageScale d ε i) g) : NextProgress s.toState ε (stageScale d ε i) g P.radiusGrowth

Choose a certified next refinement step within the prescribed radius bound.

Equations

• EGZ.FlagDecomposition.Iteration.nextProgress P hd hε hεhalf hg s hprime hnot = Classical.choice ⋯

structure EGZ.FlagDecomposition.Iteration.BoundedTransition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) (N : ℕ) : Type 1

A transition either makes certified progress or keeps the old state. Before the horizon it must progress whenever the state is unfinished.

• target : BoundedState P ε (i + 1)

  Bounded state at the next iteration index.

• radius_le : self.target.radius ≤ P.radiusGrowth s.radius
• progress_or_eq : Nonempty (Progress s.toState self.target.toState ε (stageScale d ε i) g) ∨ self.target.toState = s.toState
• forced_progress : i < N → ¬s.Finished ε (stageScale d ε i) g → Nonempty (Progress s.toState self.target.toState ε (stageScale d ε i) g)
• after_horizon : N ≤ i → self.target.toState = s.toState

noncomputable def EGZ.FlagDecomposition.Iteration.boundedTransition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (N : ℕ) (hprime : P.primeHorizon 1 N < p) {i : ℕ} (s : BoundedState P ε i) : BoundedTransition P s N

Advance the bounded iteration, retaining a finished state when appropriate.

Equations

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

noncomputable def EGZ.FlagDecomposition.Iteration.boundedRun {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : BoundedState P ε i

The actual recursively chosen bounded run, kept constant after the prescribed horizon.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.Iteration.boundedRun.state {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : State p d f

Underlying unbounded state at a given index of the bounded run.

Equations

• EGZ.FlagDecomposition.Iteration.boundedRun.state P hd hε hεhalf hg hf N hprime i = (EGZ.FlagDecomposition.Iteration.boundedRun P hd hε hεhalf hg hf N hprime i).toState

@[simp]

theorem EGZ.FlagDecomposition.Iteration.boundedRun.initial_retainedMass {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) : (state P hd hε hεhalf hg hf N hprime 0).decomposition.retainedMass = natMass f

theorem EGZ.FlagDecomposition.Iteration.boundedRun.card_bound {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : Fintype.card (state P hd hε hεhalf hg hf N hprime i).decomposition.flag.Node ≤ 2 ^ i

theorem EGZ.FlagDecomposition.Iteration.boundedRun.radius_bound {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : (state P hd hε hεhalf hg hf N hprime i).radius ≤ P.radiusHorizon 1 i

theorem EGZ.FlagDecomposition.Iteration.boundedRun.radius_le_horizon {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) (hi : i ≤ N) : (state P hd hε hεhalf hg hf N hprime i).radius ≤ P.radiusHorizon 1 N

theorem EGZ.FlagDecomposition.Iteration.boundedRun.radius_step {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : (state P hd hε hεhalf hg hf N hprime (i + 1)).radius ≤ P.radiusGrowth (state P hd hε hεhalf hg hf N hprime i).radius

theorem EGZ.FlagDecomposition.Iteration.boundedRun.progress_or_eq {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : Nonempty (Progress (state P hd hε hεhalf hg hf N hprime i) (state P hd hε hεhalf hg hf N hprime (i + 1)) ε (stageScale d ε i) g) ∨ state P hd hε hεhalf hg hf N hprime (i + 1) = state P hd hε hεhalf hg hf N hprime i

theorem EGZ.FlagDecomposition.Iteration.boundedRun.progress {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) (hi : i < N) (hnot : ¬(state P hd hε hεhalf hg hf N hprime i).Finished ε (stageScale d ε i) g) : Nonempty (Progress (state P hd hε hεhalf hg hf N hprime i) (state P hd hε hεhalf hg hf N hprime (i + 1)) ε (stageScale d ε i) g)

theorem EGZ.FlagDecomposition.Iteration.boundedRun.state_succ_eq_of_ge {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) (hi : N ≤ i) : state P hd hε hεhalf hg hf N hprime (i + 1) = state P hd hε hεhalf hg hf N hprime i

theorem EGZ.FlagDecomposition.Iteration.boundedRun.state_eq_horizon {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) (hi : N ≤ i) : state P hd hε hεhalf hg hf N hprime i = state P hd hε hεhalf hg hf N hprime N

theorem EGZ.FlagDecomposition.Iteration.boundedRun.radius_mono_step {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : (state P hd hε hεhalf hg hf N hprime i).radius ≤ (state P hd hε hεhalf hg hf N hprime (i + 1)).radius

theorem EGZ.FlagDecomposition.Iteration.boundedRun.radius_monotone {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) : Monotone fun (i : ℕ) => (state P hd hε hεhalf hg hf N hprime i).radius

theorem EGZ.FlagDecomposition.Iteration.boundedRun.mass_mono_step {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : (state P hd hε hεhalf hg hf N hprime (i + 1)).decomposition.retainedMass ≤ (state P hd hε hεhalf hg hf N hprime i).decomposition.retainedMass

theorem EGZ.FlagDecomposition.Iteration.boundedRun.mass_antitone {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) : Antitone fun (i : ℕ) => (state P hd hε hεhalf hg hf N hprime i).decomposition.retainedMass

theorem EGZ.FlagDecomposition.Iteration.boundedRun.card_step {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : Fintype.card (state P hd hε hεhalf hg hf N hprime (i + 1)).decomposition.flag.Node ≤ 2 * Fintype.card (state P hd hε hεhalf hg hf N hprime i).decomposition.flag.Node

theorem EGZ.FlagDecomposition.Iteration.boundedRun.mass_step {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : ↑(state P hd hε hεhalf hg hf N hprime i).decomposition.retainedMass - ↑(state P hd hε hεhalf hg hf N hprime (i + 1)).decomposition.retainedMass ≤ DecompositionParameters.lossBudget d ε (DecompositionParameters.initialScale d ε) (i + 1) * ↑(natMass f)

theorem EGZ.FlagDecomposition.Iteration.boundedRun.retainedMass_bounds {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (i : ℕ) : ↑(natMass f) / 2 ≤ ↑(state P hd hε hεhalf hg hf N hprime i).decomposition.retainedMass ∧ (1 - ε) * ↑(natMass f) ≤ ↑(state P hd hε hεhalf hg hf N hprime i).decomposition.retainedMass

theorem EGZ.FlagDecomposition.Iteration.boundedRun.mass_loss_tail {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (s n : ℕ) : ↑(state P hd hε hεhalf hg hf N hprime s).decomposition.retainedMass - ↑(state P hd hε hεhalf hg hf N hprime (n + s)).decomposition.retainedMass ≤ ε ^ 2 / 8 * 2⁻¹ ^ s * ↑(natMass f)

The geometric tail bound holds for every interval of the extended finite run, including intervals crossing its constant tail.

theorem EGZ.FlagDecomposition.Iteration.boundedRun.mass_loss_tail_relative {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) (s n : ℕ) : ↑(state P hd hε hεhalf hg hf N hprime s).decomposition.retainedMass - ↑(state P hd hε hεhalf hg hf N hprime (n + s)).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(state P hd hε hεhalf hg hf N hprime s).decomposition.retainedMass

theorem EGZ.FlagDecomposition.Iteration.boundedRun.finished_or_progress {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (N : ℕ) (hprime : P.primeHorizon 1 N < p) : (∃ i ≤ N, (state P hd hε hεhalf hg hf N hprime i).Finished ε (stageScale d ε i) g) ∨ Nonempty ((i : ℕ) → i < N → Progress (state P hd hε hεhalf hg hf N hprime i) (state P hd hε hεhalf hg hf N hprime (i + 1)) ε (stageScale d ε i) g)

The actual finite run either reaches a finished bounded state by its horizon, or provides a family of progress certificates at every earlier stage. Its state sequence is defined and constant beyond the horizon.