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

@[instance_reducible]

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

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

Equations

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

theorem V7.Stage4AboveTwoFinalTrial.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.Stage4AboveTwoFinalTrial.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.Stage4AboveTwoFinalTrial.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 ++ [Stage3BelowTwoS3F.cocoCheck (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))]

theorem V7.Stage4AboveTwoFinalTrial.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 ++ [Stage3BelowTwoS3F.cocoCheck (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1))]

theorem V7.Stage4AboveTwoFinalTrial.normalizedGradient_phaseOne {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : Stage3BelowTwoS3F.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.Stage4AboveTwoFinalTrial.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 p (etaF p) (nF p eps M D) k • Stage3BelowTwoS3F.normalizedGradient M D (phaseOneObs p eps M D x0 oracle k); have vNext := aboveMirrorMap p sNext; have xNext := (weight p (etaF p) (nF p eps M D) k / weight p (etaF p) (nF p eps M D) (k + 1)) • state.x + (increment p (etaF p) (nF p eps M D) (k + 1) / weight p (etaF p) (nF p eps M D) (k + 1)) • vNext + (increment p (etaF p) (nF p eps M D) k / weight p (etaF p) (nF p eps M D) (k + 1)) • (vNext - state.v); { s := sNext, v := vNext, x := xNext }

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.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 (nF p eps M D)

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

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

theorem V7.Stage4AboveTwoFinalTrial.eval_dual_shape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k fuel : ℕ) (G : VectorSeq d) (horizonEq : k + fuel = nD p eps M D) (hP : ∀ j < nF p eps M D, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle j) (phaseOneObs p eps M D x0 oracle (j + 1))) (hQ : ∀ j < k, Stage3BelowTwoS3F.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 (etaD p eps M D) (nD 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) : ∃ (m₁ : ℕ) (m₂ : ℕ), FullShape p eps M D x0 oracle (CausalProgram.Program.eval oracle fuel (dualProgram p eps M D (etaD p eps M D) (nD p eps M D) k (phaseTwoCenter p eps M D x0 oracle) (dualQ p (etaD p eps M D) (nD p eps M D) (phaseTwoOracle p eps M D x0 oracle) k) (dualR p (etaD p eps M D) (nD p eps M D) (phaseTwoOracle p eps M D x0 oracle) k) G (phaseTwoObs p eps M D x0 oracle k) (allChecks p eps M D x0 oracle (nF p eps M D) k) fuel) (phaseOneNewTrace p eps M D x0 oracle (nF p eps M D) ++ phaseTwoNewTrace p eps M D x0 oracle k)) m₁ m₂

theorem V7.Stage4AboveTwoFinalTrial.eval_phaseOne_shape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k fuel : ℕ) (horizonEq : k + fuel = nF p eps M D) (hP : ∀ j < k, Stage3BelowTwoS3F.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 (CausalProgram.Program.eval oracle (phaseOneBudget (nD p eps M D) fuel) (phaseOneProgram p eps M D (etaF p) (etaD p eps M D) x0 (nF p eps M D) (nD 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₂