Uniform providers for normalized refinement operations

The three concrete operations share a single increasing radius bound and a monotone prime threshold. A finite radius horizon therefore fixes the prime before any choices in the refinement run are made.

structure EGZ.NormalizedFaceStep {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (K R : ℕ) : Type

Concrete chart data for a normalized face operation.

• odd : Odd p
• charts (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) ⋯).flag.Node) : IntegerLatticeChart ((FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) ⋯).liftedSupport x)

  Integer lattice charts for the lifted supports of the face-refined decomposition.

• modInjective (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) ⋯).flag.Node) : Function.Injective ⇑((FlagDecomposition.Rechart.chart (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) ⋯) self.charts x).modp p)
• centered (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) ⋯).flag.Node) (q : IntCoord (self.charts x).rank) : q ∈ (self.charts x).coordinateSupport → IsCenteredLift p q
• radius : ℕ

  The radius of the normalized face step, bounded between K and R.

• radius_ge : K ≤ self.radius
• radius_le : self.radius ≤ R
• bounded : (FlagDecomposition.FaceRefinement.normalized Φ anchor Γ ⋯ self.charts ⋯ ⋯).IsKBounded fun (x : (FlagDecomposition.FaceRefinement.normalized Φ anchor Γ ⋯ self.charts ⋯ ⋯).flag.Node) => self.radius

@[reducible, inline]

noncomputable abbrev EGZ.NormalizedFaceStep.decomposition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : FlagDecomposition p d f

The normalized decomposition supplied by a face step.

Equations

• D.decomposition = EGZ.FlagDecomposition.FaceRefinement.normalized Φ anchor Γ ⋯ D.charts ⋯ ⋯

structure EGZ.NormalizedGapStep {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (K R : ℕ) (α : ℝ) : Type

Concrete deletion and chart data for normalized gap cleanup.

• weights : Φ.PrunedWeights

  The pruned weights used to correct the gap condition.

• odd : Odd p
• charts (x : (self.weights.cleaned ⋯).flag.Node) : IntegerLatticeChart ((self.weights.cleaned ⋯).liftedSupport x)

  Integer lattice charts for the supports remaining after cleaning the pruned weights.

• modInjective (x : (self.weights.cleaned ⋯).flag.Node) : Function.Injective ⇑((FlagDecomposition.Rechart.chart (self.weights.cleaned ⋯) self.charts x).modp p)
• centered (x : (self.weights.cleaned ⋯).flag.Node) (q : IntCoord (self.charts x).rank) : q ∈ (self.charts x).coordinateSupport → IsCenteredLift p q
• radius : ℕ

  The radius of the normalized gap step, bounded between K and R.

• radius_ge : K ≤ self.radius
• radius_le : self.radius ≤ R
• atoms (x : Φ.flag.Node) (v : FpCoord p d) : self.weights.weight x v = 0 ∨ self.weights.weight x v = Φ.localWeight x v
• bounded : (self.weights.normalized ⋯ self.charts ⋯ ⋯).IsKBounded fun (x : (self.weights.normalized ⋯ self.charts ⋯ ⋯).flag.Node) => self.radius
• mass_loss : ↑Φ.retainedMass - ↑(self.weights.normalized ⋯ self.charts ⋯ ⋯).retainedMass ≤ α * ↑Φ.retainedMass
• gap_bound (x : (self.weights.normalized ⋯ self.charts ⋯ ⋯).flag.Node) : α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑self.radius + 1) ^ d) ≤ ↑((self.weights.normalized ⋯ self.charts ⋯ ⋯).gap x)

@[reducible, inline]

noncomputable abbrev EGZ.NormalizedGapStep.decomposition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K R : ℕ} {α : ℝ} (D : NormalizedGapStep Φ K R α) : FlagDecomposition p d f

The normalized decomposition supplied by a gap step.

Equations

• D.decomposition = D.weights.normalized ⋯ D.charts ⋯ ⋯

structure EGZ.NormalizedCompleteStep {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (g : ℕ → ℕ) (K R : ℕ) (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) : Type

Concrete selected directions, active nodes, and charts for a normalized complete-element operation.

• odd : Odd p
• widths : ℕ → ℕ

  The width bound chosen for each dimension during complete preparation.

• preparation : Φ.CompletePreparation anchor self.widths δ

  The data preparing the anchor for the completeness refinement.

• charts (x : (self.preparation.diagram ⋯ hδ hsmall).Node) : IntegerLatticeChart ((self.preparation.diagram ⋯ hδ hsmall).support x)

  Integer lattice charts for the supports in the prepared completion diagram.

• modInjective (x : (self.preparation.diagram ⋯ hδ hsmall).Node) : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (self.charts x).map).modp p)
• centered (x : (self.preparation.diagram ⋯ hδ hsmall).Node) (q : IntCoord (self.charts x).rank) : q ∈ (self.charts x).coordinateSupport → IsCenteredLift p q
• radius : ℕ

  The radius of the normalized completion step, bounded between K and R.

• radius_ge : K ≤ self.radius
• radius_le : self.radius ≤ R
• widths_monotone : Monotone self.widths
• widths_zero : self.widths 0 = K
• desired_width : g self.radius ≤ self.widths (self.preparation.count + 1)
• bounded : (self.preparation.normalized ⋯ hδ hsmall self.charts ⋯ ⋯).IsKBounded fun (x : (self.preparation.normalized ⋯ hδ hsmall self.charts ⋯ ⋯).flag.Node) => self.radius

@[reducible, inline]

noncomputable abbrev EGZ.NormalizedCompleteStep.decomposition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : FlagDecomposition p d f

The normalized decomposition supplied by a completion step.

Equations

• D.decomposition = D.preparation.normalized ⋯ hδ hsmall D.charts ⋯ ⋯

theorem EGZ.NormalizedFaceStep.isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : D.decomposition.IsMinimal

theorem EGZ.NormalizedFaceStep.isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : D.decomposition.IsReduced

theorem EGZ.NormalizedFaceStep.retainedMass {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : D.decomposition.retainedMass = Φ.retainedMass

theorem EGZ.NormalizedFaceStep.card_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : Fintype.card D.decomposition.flag.Node ≤ 2 * Fintype.card Φ.flag.Node

noncomputable def EGZ.NormalizedFaceStep.subdivisionMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) : Φ.SubdivisionMap D.decomposition

The subdivision map carried by the normalized face step.

Equations

• D.subdivisionMap = EGZ.FlagDecomposition.FaceRefinement.normalizedSubdivisionMap Φ anchor Γ ⋯ D.charts ⋯ ⋯

@[reducible, inline]

noncomputable abbrev EGZ.NormalizedFaceStep.targetNode {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : D.decomposition.flag.Node

The retained target node of the normalized face step.

Equations

• D.targetNode hΓ hred = EGZ.FlagDecomposition.FaceRefinement.normalizedTargetNode Φ anchor Γ ⋯ D.charts ⋯ ⋯ hΓ hred

noncomputable def EGZ.NormalizedFaceStep.targetFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (D.decomposition.flag.polytope (D.targetNode hΓ hred)).Face

The target face of the normalized face step in its new coordinates.

Equations

• D.targetFace hΓ hred = EGZ.FlagDecomposition.FaceRefinement.normalizedTargetFace Φ anchor Γ ⋯ D.charts ⋯ ⋯ hΓ hred

theorem EGZ.NormalizedFaceStep.target_isRealized {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : D.decomposition.IsRealizedFace (D.targetNode hΓ hred) (D.targetFace hΓ hred)

theorem EGZ.NormalizedFaceStep.target_projection {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : D.subdivisionMap.node (D.targetNode hΓ hred) = anchor

theorem EGZ.NormalizedFaceStep.targetFace_carrier {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {Γ : (Φ.flag.polytope anchor).Face} {K R : ℕ} (D : NormalizedFaceStep Φ anchor Γ K R) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (D.targetFace hΓ hred).carrier = (D.decomposition.flag.polytope (D.targetNode hΓ hred)).carrier ∩ ⇑(D.subdivisionMap.fibre (D.targetNode hΓ hred)) ⁻¹' Γ.carrier

theorem EGZ.NormalizedGapStep.isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K R : ℕ} {α : ℝ} (D : NormalizedGapStep Φ K R α) : D.decomposition.IsMinimal

theorem EGZ.NormalizedGapStep.isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K R : ℕ} {α : ℝ} (D : NormalizedGapStep Φ K R α) : D.decomposition.IsReduced

theorem EGZ.NormalizedGapStep.card_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K R : ℕ} {α : ℝ} (D : NormalizedGapStep Φ K R α) : Fintype.card D.decomposition.flag.Node ≤ Fintype.card Φ.flag.Node

noncomputable def EGZ.NormalizedGapStep.subdivisionMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K R : ℕ} {α : ℝ} (D : NormalizedGapStep Φ K R α) : Φ.SubdivisionMap D.decomposition

The subdivision map carried by the normalized gap step.

Equations

• D.subdivisionMap = D.weights.normalizedSubdivisionMap ⋯ D.charts ⋯ ⋯

theorem EGZ.NormalizedCompleteStep.isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : D.decomposition.IsMinimal

theorem EGZ.NormalizedCompleteStep.isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : D.decomposition.IsReduced

theorem EGZ.NormalizedCompleteStep.mass_loss {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : ↑Φ.retainedMass - ↑D.decomposition.retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor))

theorem EGZ.NormalizedCompleteStep.card_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : Fintype.card D.decomposition.flag.Node ≤ 2 * Fintype.card Φ.flag.Node

noncomputable def EGZ.NormalizedCompleteStep.subdivisionMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : Φ.SubdivisionMap D.decomposition

The subdivision map carried by the normalized completion step.

Equations

• D.subdivisionMap = D.preparation.normalizedSubdivisionMap ⋯ hδ hsmall D.charts ⋯ ⋯

@[reducible, inline]

noncomputable abbrev EGZ.NormalizedCompleteStep.targetNode {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : D.decomposition.flag.Node

The distinguished complete node of the normalized completion step.

Equations

• D.targetNode = D.preparation.normalizedCompleteNode ⋯ hδ hsmall D.charts ⋯ ⋯

theorem EGZ.NormalizedCompleteStep.target_isComplete {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : D.decomposition.IsCompleteElement D.targetNode (g D.radius) δ

theorem EGZ.NormalizedCompleteStep.target_cumulativeWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) : D.decomposition.cumulativeWeight D.targetNode = restrictWeight (Φ.cumulativeWeight anchor) D.preparation.selectedSet

theorem EGZ.NormalizedCompleteStep.node_ne_upperAnchor {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {g : ℕ → ℕ} {K R : ℕ} {δ : ℝ} {hδ : 0 ≤ δ} {hsmall : 3 ^ (d + 1) * δ < 1} (D : NormalizedCompleteStep Φ anchor g K R δ hδ hsmall) (x : D.decomposition.flag.Node) : ↑x ≠ D.preparation.upperAnchor ⋯ hδ hsmall

structure EGZ.NormalizedOperationParameters (d : ℕ) (g : ℕ → ℕ) : Type

Uniform numerical parameters together with providers of all three concrete normalized operations.

• radiusGrowth : ℕ → ℕ

  A uniform bound on the radius after one normalized operation.

• radiusGrowth_growing : IsGrowing self.radiusGrowth
• primeThreshold : ℕ → ℕ

  The prime threshold ensuring normalized operations exist at the specified radius.

• primeThreshold_monotone : Monotone self.primeThreshold
• primeThreshold_ge_two (K : ℕ) : 2 ≤ self.primeThreshold K
• face (K p : ℕ) [NeZero p] [Fact (Nat.Prime p)] : self.primeThreshold K < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face), Γ ≠ ⊤ → Φ.IsReducedElement anchor → (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → Nonempty (NormalizedFaceStep Φ anchor Γ K (self.radiusGrowth K))
• gap (K p : ℕ) [NeZero p] [Fact (Nat.Prime p)] : self.primeThreshold K < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f), (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → ∀ (α : ℝ), 0 ≤ α → α < 1 → Nonempty (NormalizedGapStep Φ K (self.radiusGrowth K) α)
• complete (K p : ℕ) [NeZero p] [Fact (Nat.Prime p)] : self.primeThreshold K < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1), (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → Nonempty (NormalizedCompleteStep Φ anchor g K (self.radiusGrowth K) δ hδ hsmall)

def EGZ.thresholdEnvelope (q : ℕ → ℕ) (K : ℕ) : ℕ

Monotone majorant of a numerical threshold, taking a finite maximum over all smaller radii.

Equations

• EGZ.thresholdEnvelope q K = (Finset.range (K + 1)).sup q

theorem EGZ.le_thresholdEnvelope (q : ℕ → ℕ) (K : ℕ) : q K ≤ thresholdEnvelope q K

theorem EGZ.thresholdEnvelope_monotone (q : ℕ → ℕ) : Monotone (thresholdEnvelope q)

theorem EGZ.exists_normalizedOperationParameters (d : ℕ) (g : ℕ → ℕ) (hg : Monotone g) : Nonempty (NormalizedOperationParameters d g)

noncomputable def EGZ.normalizedOperationParameters (d : ℕ) (g : ℕ → ℕ) (hg : Monotone g) : NormalizedOperationParameters d g

Choose uniform radius and prime bounds together with providers of the normalized operations.

Equations

• EGZ.normalizedOperationParameters d g hg = Classical.choice ⋯

theorem EGZ.NormalizedOperationParameters.radiusGrowth_ge {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (K : ℕ) : K ≤ P.radiusGrowth K

def EGZ.NormalizedOperationParameters.radiusHorizon {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (K N : ℕ) : ℕ

The radius bound obtained after N successive applications of the growth function.

Equations

• P.radiusHorizon K N = P.radiusGrowth^[N] K

def EGZ.NormalizedOperationParameters.primeHorizon {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (K N : ℕ) : ℕ

The prime threshold at the radius bound after N normalized operations.

Equations

• P.primeHorizon K N = P.primeThreshold (P.radiusHorizon K N)

theorem EGZ.NormalizedOperationParameters.radius_sequence_le {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (r : ℕ → ℕ) {K : ℕ} (hstart : r 0 ≤ K) (hstep : ∀ (i : ℕ), r (i + 1) ≤ P.radiusGrowth (r i)) (i : ℕ) : r i ≤ P.radiusHorizon K i

theorem EGZ.NormalizedOperationParameters.radiusHorizon_monotone {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (K : ℕ) : Monotone (P.radiusHorizon K)

theorem EGZ.NormalizedOperationParameters.primeThreshold_lt_of_le_horizon {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {K N b p : ℕ} (hp : P.primeHorizon K N < p) (hb : b ≤ P.radiusHorizon K N) : P.primeThreshold b < p

One prime chosen for the finite horizon works at every smaller radius, including radii produced by arbitrary prior refinement choices.

theorem EGZ.NormalizedOperationParameters.primeThreshold_lt_of_radius_sequence {d : ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (r : ℕ → ℕ) {K N p : ℕ} (hp : P.primeHorizon K N < p) (hstart : r 0 ≤ K) (hstep : ∀ (i : ℕ), r (i + 1) ≤ P.radiusGrowth (r i)) {i : ℕ} (hi : i ≤ N) : P.primeThreshold (r i) < p