The below-two report shape yields its guard ledger, call accounting, and operational contract.
noncomputable def
V7.Stage3BelowTwoS3F.shapeWitness
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m₁ m₂ : ℕ)
:
The concrete below-two trajectories packaged as a witness for the completed phase lengths.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
V7.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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.Stage3BelowTwoS3F.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₂)
:
theorem
V7.Stage3BelowTwoS3F.fullShape_operational_contract
{d : ℕ}
{eps : ℝ}
{oracle : PairOracle d}
{report : TrialReport d}
{cached : CachedPair d}
{p M D : ℝ}
{x0 : O3.Vec d}
{m₁ m₂ : ℕ}
(hp : 1 < p)
(heps : 0 < eps)
(hM : 0 < M)
(hD : 0 < D)
(hcached : cached.observation = O3.PairOracle.observe oracle x0)
(hshape : FullShape p eps M D x0 oracle report m₁ m₂)
:
BelowTrialOperationalContract p eps M D x0 cached oracle report (shapeWitness p eps M D x0 oracle m₁ m₂)