The realized controller path has the prescribed geometric sequence of scales and radii.

def V7.Stage2.pathScale (Ma : ℝ) (s : ℕ) : ℝ

The dyadic smoothness estimate at scale index s.

Equations

• V7.Stage2.pathScale Ma s = 2 ^ s * Ma

noncomputable def V7.Stage2.pathRadius (G Ma : ℝ) (s j : ℕ) : ℝ

The dyadic radius at scale index s and radius index j.

Equations

• V7.Stage2.pathRadius G Ma s j = 2 ^ j * G / V7.Stage2.pathScale Ma s

noncomputable def V7.Stage2.pathVisit (G Ma : ℝ) (s j : ℕ) : ControllerVisit

The controller visit associated with the two geometric indices.

Equations

• V7.Stage2.pathVisit G Ma s j = { M := V7.Stage2.pathScale Ma s, D := V7.Stage2.pathRadius G Ma s j }

noncomputable def V7.Stage2.pathGrid (G Ma : ℝ) (S : ℕ) (lastRadius : ℕ → ℕ) : List ControllerVisit

The chronological path through each scale's realized initial segment of radii.

Equations

• V7.Stage2.pathGrid G Ma S lastRadius = List.flatMap (fun (s : ℕ) => List.map (fun (j : ℕ) => V7.Stage2.pathVisit G Ma s j) (List.range (lastRadius s + 1))) (List.range (S + 1))

theorem V7.Stage2.controllerPath_has_grid {d : ℕ} {G Ma Da : ℝ} (hMa : 0 < Ma) (hDa : Da = G / Ma) {visits : List ControllerVisit} {reports : List (TrialReport d)} (hpath : ControllerPath G Ma Da visits reports) : ∃ (S : ℕ) (lastRadius : ℕ → ℕ), visits = pathGrid G Ma S lastRadius