Every above-two report shape supplies correctness and exact guard certificates.
theorem
V7.Stage4AboveTwoFinalTrial.phaseOneNewTrace_exact
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
TraceExact oracle (phaseOneNewTrace p eps M D x0 oracle m)
theorem
V7.Stage4AboveTwoFinalTrial.phaseTwoNewTrace_exact
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
TraceExact oracle (phaseTwoNewTrace p eps M D x0 oracle m)
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_trace_exact
{d : ℕ}
{eps : ℝ}
{oracle : PairOracle d}
{report : TrialReport d}
{p M D : ℝ}
{x0 : Point d}
{m₁ m₂ : ℕ}
(hshape : FullShape p eps M D x0 oracle report m₁ m₂)
:
TraceExact oracle report.trace
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_outcome_exhaustive
{d : ℕ}
{eps : ℝ}
{oracle : PairOracle d}
{report : TrialReport d}
{p M D : ℝ}
{x0 : Point d}
{m₁ m₂ : ℕ}
(hshape : FullShape p eps M D x0 oracle report m₁ m₂)
:
TrialOutcomeExhaustive report
theorem
V7.Stage4AboveTwoFinalTrial.phaseOneChecks_not_fails
{d : ℕ}
(p M eps D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
(hholds :
∀ k < m,
Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1)))
(check : ObservableGuardCheck d)
:
check ∈ phaseOneChecks p eps M D x0 oracle m → ¬GuardFails p M oracle check.failure
theorem
V7.Stage4AboveTwoFinalTrial.phaseTwoChecks_not_fails
{d : ℕ}
(p M eps D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
(hholds :
∀ k < m,
Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1)))
(check : ObservableGuardCheck d)
:
check ∈ phaseTwoChecks p eps M D x0 oracle m → ¬GuardFails p M oracle check.failure
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_guard_data
{d : ℕ}
{eps : ℝ}
{oracle : PairOracle d}
{report : TrialReport d}
{cached : CachedPair d}
{x0 : O3.Vec d}
{p M D : ℝ}
{m₁ m₂ : ℕ}
(hcached : cached.observation = O3.PairOracle.observe oracle x0)
(hshape : FullShape p eps M D x0 oracle report m₁ m₂)
:
GuardDataExact cached oracle report
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_certificate
{d : ℕ}
{eps : ℝ}
{report : TrialReport d}
{cached : CachedPair d}
{p M D : ℝ}
{x0 : Point d}
{m₁ m₂ : ℕ}
(hp : 2 < p)
(heps : 0 < eps)
(hM : 0 < M)
(hD : 0 < D)
(inst : PositiveInstance p d x0)
(hcached : cached.observation = O3.PairOracle.observe inst.oracle x0)
(hshape : FullShape p eps M D x0 inst.oracle report m₁ m₂)
:
TrialCertificate eps p M D inst.L inst.R cached inst.oracle report