States and progress certificates for the decomposition iteration

States are minimal and reduced, with a positive constant coordinate radius. An event records an unsatisfied conclusion. Its color orders completeness and face events by the represented level, with gap cleanup last.

theorem EGZ.FlagDecomposition.isRealizedFace_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : Φ.IsRealizedFace x ⊤

def EGZ.FlagDecomposition.faceAtNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (Γ : (Φ.flag.polytope x).Face) (h : y = x) : (Φ.flag.polytope y).Face

A node equality transports its face without choosing coordinates.

Equations

• Φ.faceAtNode Γ h = ⋯ ▸ Γ

@[simp]

theorem EGZ.FlagDecomposition.faceAtNode_rfl {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x : Φ.flag.Node} (Γ : (Φ.flag.polytope x).Face) : Φ.faceAtNode Γ ⋯ = Γ

structure EGZ.FlagDecomposition.Iteration.State (p d : ℕ) [NeZero p] (f : FpCoord p d → ℕ) : Type 1

A minimal flag decomposition equipped with a positive radius for the iteration.

• decomposition : FlagDecomposition p d f

  The flag decomposition at the current stage.

• radius : ℕ

  The positive radius controlling the current decomposition.

• radius_pos : 1 ≤ self.radius
• minimal : self.decomposition.IsMinimal
• reduced : self.decomposition.IsReduced
• bounded : self.decomposition.IsKBounded fun (x : self.decomposition.flag.Node) => self.radius

def EGZ.FlagDecomposition.Iteration.State.GapCondition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (s : State p d f) (δ : ℝ) : Prop

Every node gap exceeds the prescribed scale relative to the total input mass.

Equations

• s.GapCondition δ = ∀ (x : s.decomposition.flag.Node), δ ^ 3 * (↑s.radius)⁻¹ ^ d * ↑(EGZ.natMass f) ≤ ↑(s.decomposition.gap x)

def EGZ.FlagDecomposition.Iteration.State.Finished {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (s : State p d f) (ε δ : ℝ) (g : ℕ → ℕ) : Prop

The state satisfies the gap bound and the required completeness condition.

Equations

• s.Finished ε δ g = (s.GapCondition δ ∧ s.decomposition.IsComplete (fun (x : s.decomposition.flag.Node) => g s.radius) ε δ)

inductive EGZ.FlagDecomposition.Iteration.State.Event {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (s : State p d f) : Type

The three possible reasons for refining a state: a gap, a face, or an incomplete node.

• gap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {s : State p d f} : s.Event
• face {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {s : State p d f} (x : s.decomposition.flag.Node) (Γ : (s.decomposition.flag.polytope x).Face) : s.Event
• complete {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {s : State p d f} (x : s.decomposition.flag.Node) : s.Event

def EGZ.FlagDecomposition.Iteration.State.Event.Valid {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {s : State p d f} (ε δ : ℝ) (g : ℕ → ℕ) : s.Event → Prop

The chosen event witnesses a failure of the corresponding termination condition.

Equations

• One or more equations did not get rendered due to their size.
• EGZ.FlagDecomposition.Iteration.State.Event.Valid ε δ g EGZ.FlagDecomposition.Iteration.State.Event.gap = ¬s.GapCondition δ
• EGZ.FlagDecomposition.Iteration.State.Event.Valid ε δ g (EGZ.FlagDecomposition.Iteration.State.Event.face x_1 Γ) = (s.decomposition.IsLargeFace ε x_1 Γ ∧ ¬s.decomposition.IsRealizedFace x_1 Γ)

noncomputable def EGZ.FlagDecomposition.Iteration.State.Event.cutoff {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} : s.Event → ℕ

The largest level required to remain stable during this event.

Equations

• EGZ.FlagDecomposition.Iteration.State.Event.gap.cutoff = (d + 1) ^ 2
• (EGZ.FlagDecomposition.Iteration.State.Event.face x_1 Γ).cutoff = s.decomposition.level x_1
• (EGZ.FlagDecomposition.Iteration.State.Event.complete x_1).cutoff = s.decomposition.level x_1

noncomputable def EGZ.FlagDecomposition.Iteration.State.Event.color {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} : s.Event → ℕ

Encode the event type and its level as a natural number for the stopping argument.

Equations

• EGZ.FlagDecomposition.Iteration.State.Event.gap.color = 2 * (d + 1) ^ 2
• (EGZ.FlagDecomposition.Iteration.State.Event.face x_1 Γ).color = 2 * s.decomposition.level x_1 + 1
• (EGZ.FlagDecomposition.Iteration.State.Event.complete x_1).color = 2 * s.decomposition.level x_1

theorem EGZ.FlagDecomposition.Iteration.State.Event.color_lt {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} (E : s.Event) : E.color < 2 * (d + 1) ^ 2 + 1

theorem EGZ.FlagDecomposition.Iteration.State.Event.cutoff_ge_of_color_ge {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} (E : s.Event) {L : ℕ} (h : 2 * L ≤ E.color) : L ≤ E.cutoff

theorem EGZ.FlagDecomposition.Iteration.State.Event.cutoff_le_square {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} (E : s.Event) : E.cutoff ≤ (d + 1) ^ 2

theorem EGZ.FlagDecomposition.Iteration.State.exists_valid_event {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (s : State p d f) (ε δ : ℝ) (g : ℕ → ℕ) (h : ¬s.Finished ε δ g) : ∃ (E : s.Event), Event.Valid ε δ g E

def EGZ.FlagDecomposition.Iteration.Resolves {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s t : State p d f} (S : s.decomposition.SubdivisionMap t.decomposition) (δ : ℝ) : s.Event → Prop

A face event has a surviving node at the same level where its selected face has become realized. Completeness events kill the selected low-level lineage. Gap events establish the gap condition at the current scale.

Equations

• One or more equations did not get rendered due to their size.
• EGZ.FlagDecomposition.Iteration.Resolves S δ EGZ.FlagDecomposition.Iteration.State.Event.gap = t.GapCondition δ

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

Everything used by the termination argument is certified by a concrete normalized operation. Stable mass transport is required only below the event's cutoff.

• event : s.Event

  The event triggering the transition between the two states.

• valid : State.Event.Valid ε δ g self.event
• subdivision : s.decomposition.SubdivisionMap t.decomposition

  The subdivision map relating the new decomposition to the preceding one.

• level_parent (y : t.decomposition.flag.Node) : s.decomposition.level (self.subdivision.node y) ≤ t.decomposition.level y
• stable (y : t.decomposition.flag.Node) : t.decomposition.level y ≤ self.event.cutoff → s.decomposition.StableNodeMap t.decomposition (self.subdivision.node y) y

  Stable node maps for all new nodes at or below the event cutoff.

• stable_real (y : t.decomposition.flag.Node) (h : t.decomposition.level y ≤ self.event.cutoff) : (self.stable y h).coord.real = self.subdivision.fibre y
• parent_injective : Set.InjOn ⇑self.subdivision.node {y : t.decomposition.flag.Node | t.decomposition.level y ≤ self.event.cutoff}
• resolves : Resolves self.subdivision δ self.event
• radius_le : s.radius ≤ t.radius
• card_le : Fintype.card t.decomposition.flag.Node ≤ 2 * Fintype.card s.decomposition.flag.Node
• mass_le : t.decomposition.retainedMass ≤ s.decomposition.retainedMass
• mass_loss_le : ↑s.decomposition.retainedMass - ↑t.decomposition.retainedMass ≤ (ε * δ ^ 2 + 3 ^ (d + 1) * δ) * ↑s.decomposition.retainedMass