Above-two reports have complete consecutive guard ledgers and bounded call counts.
theorem
V7.Stage4AboveTwoFinalTrial.phaseOneTrace_lastD
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
(phaseOneNewTrace p eps M D x0 oracle m).getLastD (phaseOneObs p eps M D x0 oracle 0) = phaseOneObs p eps M D x0 oracle m
theorem
V7.Stage4AboveTwoFinalTrial.phaseTwoTrace_lastD
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
(phaseTwoNewTrace p eps M D x0 oracle m).getLastD (phaseTwoObs p eps M D x0 oracle 0) = phaseTwoObs p eps M D x0 oracle m
theorem
V7.Stage4AboveTwoFinalTrial.phaseOne_chain
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
Stage3BelowTwoS3F.chainChecks (phaseOneObs p eps M D x0 oracle 0) (phaseOneNewTrace p eps M D x0 oracle m) = phaseOneChecks p eps M D x0 oracle m
theorem
V7.Stage4AboveTwoFinalTrial.phaseTwo_chain
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m : ℕ)
:
Stage3BelowTwoS3F.chainChecks (phaseTwoObs p eps M D x0 oracle 0) (phaseTwoNewTrace p eps M D x0 oracle m) = phaseTwoChecks p eps M D x0 oracle m
theorem
V7.Stage4AboveTwoFinalTrial.total_chain
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m₂ : ℕ)
:
Stage3BelowTwoS3F.chainChecks (phaseOneObs p eps M D x0 oracle 0)
(phaseOneNewTrace p eps M D x0 oracle (nF p eps M D) ++ phaseTwoNewTrace p eps M D x0 oracle m₂) = allChecks p eps M D x0 oracle (nF p eps M D) m₂
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_kinds
{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₂)
:
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_ledger
{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₂)
:
ConsecutiveGuardLedger cached report
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_accounting
{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₂)
:
report.consecutiveGuardAccounting
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_calls_le
{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₂)
: