Initialization and anchor search splice into the causal controller execution.
def
V7.Stage8Main.runtimeDataFromAnchor
{d : ℕ}
(input : MethodInput d)
(hp : 1 < input.p)
(heps : 0 < input.eps)
(hM0 : 0 < input.M0)
(cached : CachedPair d)
(G : ℝ)
(hGdef : G = lpNorm (conjugateExponent input.p) cached.observation.gradient)
(hG : 0 < G)
(anchorResult : O3.AnchorResult d)
:
The runtime data assembled from valid primitive inputs and an accepted anchor search.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
V7.Stage8Main.currentMethod_early_run
{d : ℕ}
(oracle : PairOracle d)
(input : MethodInput d)
(hp : 1 < input.p)
(heps : 0 < input.eps)
(hM0 : 0 < input.M0)
(hsmall : lpNorm (conjugateExponent input.p) (oracle.gradient input.x0) ≤ input.eps)
:
theorem
V7.Stage8Main.currentMethod_anchor_splice
{d : ℕ}
(oracle : PairOracle d)
(input : MethodInput d)
(hp : 1 < input.p)
(heps : 0 < input.eps)
(hM0 : 0 < input.M0)
(cached : CachedPair d)
(G : ℝ)
(hGdef : G = lpNorm (conjugateExponent input.p) cached.observation.gradient)
(hG : 0 < G)
{anchorFuel epoch : ℕ}
{anchorHistory : List (Observation d)}
{anchorResult : O3.AnchorResult d}
{publicPrefix : List (Observation d)}
{tailFuel : ℕ}
{result : O3.RunResult d}
:
O3.runAnchor oracle (O3.anchorPrefixConfig input.toO3 cached.observation.value cached.observation.gradient G) anchorFuel
epoch anchorHistory = some anchorResult →
(currentMethod d).runFuel oracle tailFuel
(CurrentMethodState.controllerReady (runtimeDataFromAnchor input hp heps hM0 cached G hGdef hG anchorResult)
initialRuntimeControllerState)
(publicPrefix ++ anchorResult.observations) = some result →
∃ (methodFuel : ℕ),
(currentMethod d).runFuel oracle methodFuel
(CurrentMethodState.anchoring input hp heps hM0 cached G hGdef hG epoch anchorHistory)
(publicPrefix ++ anchorHistory) = some result
theorem
V7.Stage8Main.currentMethod_full_splice
{d : ℕ}
(oracle : PairOracle d)
(input : MethodInput d)
(hp : 1 < input.p)
(heps : 0 < input.eps)
(hM0 : 0 < input.M0)
(hlarge : input.eps < lpNorm (conjugateExponent input.p) (oracle.gradient input.x0))
{anchorFuel : ℕ}
{anchorResult : O3.AnchorResult d}
{tailFuel : ℕ}
{result : O3.RunResult d}
(hrun :
O3.runAnchor oracle
(O3.anchorPrefixConfig input.toO3 (oracle.value input.x0) (oracle.gradient input.x0)
(lpNorm (conjugateExponent input.p) (oracle.gradient input.x0)))
anchorFuel 0 [] = some anchorResult)
(htail :
(currentMethod d).runFuel oracle tailFuel
(CurrentMethodState.controllerReady
(runtimeDataFromAnchor input hp heps hM0 { observation := O3.PairOracle.observe oracle input.x0 }
(lpNorm (conjugateExponent input.p) (oracle.gradient input.x0)) ⋯ ⋯ anchorResult)
initialRuntimeControllerState)
([O3.PairOracle.observe oracle input.x0] ++ anchorResult.observations) = some result)
: