The below-two query programs produce exactly the permitted report shapes.

@[instance_reducible]

noncomputable def V7.Stage3BelowTwoS3F.semanticsPropDecidable (q : Prop) : Decidable q

Classical proposition decisions used locally in the below-two program semantics.

Equations

• V7.Stage3BelowTwoS3F.semanticsPropDecidable q = Classical.propDecidable q

theorem V7.Stage3BelowTwoS3F.phaseOneTrace_succ {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : phaseOneNewTrace p eps M D x0 oracle (k + 1) = phaseOneNewTrace p eps M D x0 oracle k ++ [phaseOneObs p eps M D x0 oracle (k + 1)]

theorem V7.Stage3BelowTwoS3F.phaseTwoTrace_succ {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : phaseTwoNewTrace p eps M D x0 oracle (k + 1) = phaseTwoNewTrace p eps M D x0 oracle k ++ [phaseTwoObs p eps M D x0 oracle (k + 1)]

theorem V7.Stage3BelowTwoS3F.phaseOneChecks_succ {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : phaseOneChecks p eps M D x0 oracle (k + 1) = phaseOneChecks p eps M D x0 oracle k ++ [cocoCheck (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))]

theorem V7.Stage3BelowTwoS3F.phaseTwoChecks_succ {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : phaseTwoChecks p eps M D x0 oracle (k + 1) = phaseTwoChecks p eps M D x0 oracle k ++ [cocoCheck (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1))]

theorem V7.Stage3BelowTwoS3F.normalizedGradient_phaseOne {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : normalizedGradient M D (phaseOneObs p eps M D x0 oracle k) = (phaseOneOracle x0 M D oracle).gradient (phaseOneState p eps M D x0 oracle k).x

theorem V7.Stage3BelowTwoS3F.phaseOneState_succ {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : phaseOneState p eps M D x0 oracle (k + 1) = have state := phaseOneState p eps M D x0 oracle k; have sNext := state.s - increment (horizon p eps M D) k • normalizedGradient M D (phaseOneObs p eps M D x0 oracle k); have vNext := belowMirrorMap p sNext; have xNext := (weight (horizon p eps M D) k / weight (horizon p eps M D) (k + 1)) • state.x + (increment (horizon p eps M D) (k + 1) / weight (horizon p eps M D) (k + 1)) • vNext + (increment (horizon p eps M D) k / weight (horizon p eps M D) (k + 1)) • (vNext - state.v); { s := sNext, v := vNext, x := xNext }

@[simp]

theorem V7.Stage3BelowTwoS3F.phaseTwoObs_zero {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) : phaseTwoObs p eps M D x0 oracle 0 = phaseOneObs p eps M D x0 oracle (horizon p eps M D)

theorem V7.Stage3BelowTwoS3F.normalizedGradient_phaseTwo {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : normalizedGradient M D (phaseTwoObs p eps M D x0 oracle k) = (phaseTwoOracle p eps M D x0 oracle).gradient (dualQ p (horizon p eps M D) (phaseTwoOracle p eps M D x0 oracle) k)

theorem V7.Stage3BelowTwoS3F.phaseTwoGradient_zero {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) : (phaseTwoOracle p eps M D x0 oracle).gradient 0 = normalizedGradient M D (phaseOneObs p eps M D x0 oracle (horizon p eps M D))

theorem V7.Stage3BelowTwoS3F.eval_dual_shape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k fuel : ℕ) (G : VectorSeq d) (horizonEq : k + fuel = horizon p eps M D) (hP : ∀ j < horizon p eps M D, cocoPairHolds p M (phaseOneObs p eps M D x0 oracle j) (phaseOneObs p eps M D x0 oracle (j + 1))) (hQ : ∀ j < k, cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle j) (phaseTwoObs p eps M D x0 oracle (j + 1))) (hG : ∀ i ≤ k, G i = (phaseTwoOracle p eps M D x0 oracle).gradient (dualQ p (horizon p eps M D) (phaseTwoOracle p eps M D x0 oracle) i)) (hlarge : eps < lpNorm (conjugateExponent p) (phaseTwoObs p eps M D x0 oracle k).gradient) : have n := horizon p eps M D; have oracle₂ := phaseTwoOracle p eps M D x0 oracle; ∃ (m₁ : ℕ) (m₂ : ℕ), FullShape p eps M D x0 oracle (Program.eval oracle fuel (dualProgram p eps M D n k (phaseTwoCenter p eps M D x0 oracle) (dualQ p n oracle₂ k) (dualR p n oracle₂ k) G (phaseTwoObs p eps M D x0 oracle k) (allChecks p eps M D x0 oracle n k) fuel) (phaseOneNewTrace p eps M D x0 oracle n ++ phaseTwoNewTrace p eps M D x0 oracle k)) m₁ m₂

theorem V7.Stage3BelowTwoS3F.eval_phaseOne_shape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k fuel : ℕ) (horizonEq : k + fuel = horizon p eps M D) (hP : ∀ j < k, cocoPairHolds p M (phaseOneObs p eps M D x0 oracle j) (phaseOneObs p eps M D x0 oracle (j + 1))) (hlarge : eps < lpNorm (conjugateExponent p) (phaseOneObs p eps M D x0 oracle k).gradient) : ∃ (m₁ : ℕ) (m₂ : ℕ), FullShape p eps M D x0 oracle (Program.eval oracle (phaseOneBudget (horizon p eps M D) fuel) (phaseOneProgram p eps M D x0 (horizon p eps M D) k (phaseOneState p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle k) (phaseOneChecks p eps M D x0 oracle k) fuel) (phaseOneNewTrace p eps M D x0 oracle k)) m₁ m₂