Every below-two report shape supplies the required correctness and guard certificates.
theorem
V7.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.phaseOneChecks_not_fails
{d : ℕ}
(p M eps D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
(hholds : ∀ k < m, 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.Stage3BelowTwoS3F.phaseTwoChecks_not_fails
{d : ℕ}
(p M eps D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
(hholds : ∀ k < m, 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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.fullShape_certificate
{d : ℕ}
{eps : ℝ}
{report : TrialReport d}
{cached : CachedPair d}
{p M D : ℝ}
{x0 : Point d}
{m₁ m₂ : ℕ}
(hp : 1 < p)
(hp2 : p < 2)
(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