Causal local trial actions, observable reports, guard ledgers, and correctness certificates.

structure V7.ObservableGuardCheck (d : ℕ) : Type

An observable guard kind together with the exact pairs used to evaluate it.

• kind : ObservableGuardKind

  The observable inequality to be evaluated.

• xPair : Observation d

  The observation at the guard's first point.

• yPair : Observation d

  The observation at the guard's second point.

def V7.ObservableGuardCheck.failure {d : ℕ} (check : ObservableGuardCheck d) : ObservableGuardFailure d

The point-based failure witness associated with an observation-based guard check.

Equations

• check.failure = { kind := check.kind, x := check.xPair.point, y := check.yPair.point }

inductive V7.TrialOutcome (d : ℕ) : Type

A trial terminates with gradient success, a failed scale guard, or an insufficient radius.

• success {d : ℕ} (terminalPair : Observation d) : TrialOutcome d
• scale {d : ℕ} (failedCheck : ObservableGuardCheck d) : TrialOutcome d
• radius {d : ℕ} (terminalPair : Observation d) : TrialOutcome d

structure V7.TrialReport (d : ℕ) : Type

Observable data only: no M<L or D<R conclusion is stored here.

• trace : List (Observation d)

  The chronological new observations made by the trial.

• checkedGuards : List (ObservableGuardCheck d)

  The chronological observable guards checked by the trial.

• outcome : TrialOutcome d

  The terminal trial outcome and its observable witness.

def V7.TrialReport.calls {d : ℕ} (report : TrialReport d) : ℕ

The number of new oracle observations recorded by the trial.

Equations

• report.calls = report.trace.length

structure V7.CachedPair (d : ℕ) : Type

An observation retained for reuse without another oracle call.

• observation : Observation d

  The previously obtained exact value-gradient observation.

inductive V7.LocalTrialAction (d : ℕ) (State : Type) : Type

A local trial either requests an observation or finishes with guards and an outcome.

• query {d : ℕ} {State : Type} (point : Point d) (next : Observation d → State) : LocalTrialAction d State
• finish {d : ℕ} {State : Type} (guards : List (ObservableGuardCheck d)) (outcome : TrialOutcome d) : LocalTrialAction d State

structure V7.LocalTrial (d : ℕ) : Type 1

A causal local trial: cached data enters the initial state, and all later objective information enters only through query continuations.

• State : Type

  The internal state type of the causal local trial.

• initial : ℝ → ℝ → CachedPair d → self.State

  The initial state determined by the trial estimates and cached observation.

• action : self.State → LocalTrialAction d self.State

  The next observable action determined by the current internal state.

def V7.LocalTrial.runFuel {d : ℕ} (trial : LocalTrial d) (oracle : PairOracle d) : ℕ → trial.State → List (Observation d) → Option (TrialReport d)

The finite-fuel local execution, returning no report if its action budget is exhausted.

Equations

• One or more equations did not get rendered due to their size.
• trial.runFuel oracle 0 x✝¹ x✝ = none

def V7.LocalTrial.Executes {d : ℕ} (trial : LocalTrial d) (M D : ℝ) (cached : CachedPair d) (oracle : PairOracle d) (report : TrialReport d) : Prop

Some finite-fuel execution from the prescribed initial state returns this report.

Equations

• trial.Executes M D cached oracle report = ∃ (fuel : ℕ), trial.runFuel oracle fuel (trial.initial M D cached) [] = some report

def V7.SuccessCorrect {d : ℕ} (eps p M : ℝ) (oracle : PairOracle d) (report : TrialReport d) : Prop

A success report returns an exact queried point meeting the gradient target after accepted guards.

Equations

• One or more equations did not get rendered due to their size.

def V7.ScaleCorrect {d : ℕ} (p M L : ℝ) (oracle : PairOracle d) (report : TrialReport d) : Prop

A scale report identifies the first failed guard and certifies that the smoothness estimate is too small.

Equations

• One or more equations did not get rendered due to their size.

def V7.RadiusCorrect {d : ℕ} (eps p M D R : ℝ) (oracle : PairOracle d) (report : TrialReport d) : Prop

A radius report has accepted guards and certifies that its radius estimate is too small.

Equations

• One or more equations did not get rendered due to their size.

def V7.TrialOutcomeExhaustive {d : ℕ} (report : TrialReport d) : Prop

The report belongs to one of the three possible terminal outcome cases.

Equations

• One or more equations did not get rendered due to their size.

def V7.TrialReport.consecutiveGuardAccounting {d : ℕ} (report : TrialReport d) : Prop

The numbers of consecutive guard checks and calls agree with the terminal outcome.

Equations

• One or more equations did not get rendered due to their size.

def V7.ObservationAvailable {d : ℕ} (cached : CachedPair d) (report : TrialReport d) (obs : Observation d) : Prop

The observation is either cached or present in the trial's new query trace.

Equations

• V7.ObservationAvailable cached report obs = (obs = cached.observation ∨ obs ∈ report.trace)

def V7.ConsecutiveAvailable {d : ℕ} (cached : CachedPair d) (report : TrialReport d) (check : ObservableGuardCheck d) : Prop

The guard's observations are consecutive in the cached observation followed by the trial trace.

Equations

• One or more equations did not get rendered due to their size.

def V7.CheckedGuardsHaveKinds {d : ℕ} (report : TrialReport d) (allowed : List ObservableGuardKind) : Prop

Every recorded guard has a kind in the allowed list.

Equations

• V7.CheckedGuardsHaveKinds report allowed = ∀ check ∈ report.checkedGuards, check.kind ∈ allowed

def V7.GuardRecorded {d : ℕ} (report : TrialReport d) (kind : ObservableGuardKind) (x y : Point d) : Prop

A guard of the specified kind and ordered pair of points occurs in the checked list.

Equations

• V7.GuardRecorded report kind x y = ∃ check ∈ report.checkedGuards, check.kind = kind ∧ check.xPair.point = x ∧ check.yPair.point = y

def V7.ConsecutiveGuardLedger {d : ℕ} (cached : CachedPair d) (report : TrialReport d) : Prop

Each guard uses the corresponding consecutive pair in the cached observation and query trace.

Equations

• One or more equations did not get rendered due to their size.

def V7.GuardDataExact {d : ℕ} (cached : CachedPair d) (oracle : PairOracle d) (report : TrialReport d) : Prop

Every predicate reported by the routine is evaluated on exact pairs that the routine actually possesses: the cached pair or a chronological query.

Equations

• One or more equations did not get rendered due to their size.

def V7.TrialCertificate {d : ℕ} (eps p M D L R : ℝ) (cached : CachedPair d) (oracle : PairOracle d) (report : TrialReport d) : Prop

Correctness proposition kept separate from observable trial data.

Equations

• One or more equations did not get rendered due to their size.