Exact pair-oracle observations and guarded trial reports

This module contains data only: exact oracle observations, finite traces, observable scalar guard checks, and the three possible trial outcomes. In particular, a TrialReport does not contain a proof of a target gradient bound, a radius classification, or successful controller termination. Those properties live in the separate proposition TrialValid and must be proved by the regime-specific trial modules.

@[reducible, inline]

abbrev O3.OracleTrace (d : ℕ) : Type

A finite, chronological list of counted pair-oracle observations.

Equations

• O3.OracleTrace d = List (O3.Observation d)

def O3.oracleCallCount {d : ℕ} (trace : OracleTrace d) : ℕ

Each observation in the trace is one counted pair-oracle call.

Equations

• O3.oracleCallCount trace = List.length trace

def O3.TraceExact {d : ℕ} (oracle : PairOracle d) (trace : OracleTrace d) : Prop

Every recorded observation is the exact answer returned at its point.

Equations

• O3.TraceExact oracle trace = ∀ o ∈ trace, o = oracle.observe o.point

def O3.WasQueried {d : ℕ} (trace : OracleTrace d) (x : Vec d) : Prop

A point was actually queried in the given trace.

Equations

• O3.WasQueried trace x = ∃ o ∈ trace, o.point = x

theorem O3.traceExact_nil {d : ℕ} (oracle : PairOracle d) : TraceExact oracle []

theorem O3.traceExact_append {d : ℕ} {oracle : PairOracle d} {s t : OracleTrace d} (hs : TraceExact oracle s) (ht : TraceExact oracle t) : TraceExact oracle (s ++ t)

theorem O3.oracleCallCount_append {d : ℕ} (s t : OracleTrace d) : oracleCallCount (s ++ t) = oracleCallCount s + oracleCallCount t

inductive O3.GuardKind : Type

The three oracle-checkable guard classes in the frozen TeX source.

• upperModel : GuardKind
• gradientLipschitz : GuardKind
• interpolation : GuardKind

@[instance_reducible]

instance O3.instDecidableEqGuardKind : DecidableEq GuardKind

Equations

• O3.instDecidableEqGuardKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure O3.GuardCheck : Type

An observable guard is stored through its scalar margin. The convention is that the checked inequality passes exactly when 0 ≤ margin.

• kind : GuardKind

  The analytic condition tested by this observable guard.

• margin : ℝ

  The signed slack of the tested inequality, with nonnegative values denoting success.

def O3.GuardCheck.Holds (check : GuardCheck) : Prop

The guard's inequality holds exactly when its signed margin is nonnegative.

Equations

• check.Holds = (0 ≤ check.margin)

noncomputable def O3.upperModelGuard (fx fy linear stepSq M : ℝ) : GuardCheck

Margin for f(y) ≤ f(x) + linear + (M/2) * stepSq.

Equations

• O3.upperModelGuard fx fy linear stepSq M = { kind := O3.GuardKind.upperModel, margin := fx + linear + M / 2 * stepSq - fy }

def O3.gradientGuard (gradDiff stepNorm M : ℝ) : GuardCheck

Margin for gradDiff ≤ M * stepNorm.

Equations

• O3.gradientGuard gradDiff stepNorm M = { kind := O3.GuardKind.gradientLipschitz, margin := M * stepNorm - gradDiff }

noncomputable def O3.interpolationGuard (fi fj pairing gradDiffSq M : ℝ) : GuardCheck

Margin for the ordered Euclidean finite-data interpolation guard f_i-f_j-pairing-(2M)^{-1} gradDiffSq ≥ 0.

Equations

• O3.interpolationGuard fi fj pairing gradDiffSq M = { kind := O3.GuardKind.interpolation, margin := fi - fj - pairing - gradDiffSq / (2 * M) }

theorem O3.upperModelGuard_holds_iff (fx fy linear stepSq M : ℝ) : (upperModelGuard fx fy linear stepSq M).Holds ↔ fy ≤ fx + linear + M / 2 * stepSq

theorem O3.gradientGuard_holds_iff (gradDiff stepNorm M : ℝ) : (gradientGuard gradDiff stepNorm M).Holds ↔ gradDiff ≤ M * stepNorm

theorem O3.interpolationGuard_holds_iff (fi fj pairing gradDiffSq M : ℝ) : (interpolationGuard fi fj pairing gradDiffSq M).Holds ↔ 0 ≤ fi - fj - pairing - gradDiffSq / (2 * M)

def O3.allGuardsPass (guards : List GuardCheck) : Prop

Every guard recorded in the list has a nonnegative margin.

Equations

• O3.allGuardsPass guards = ∀ check ∈ guards, check.Holds

def O3.HasFailedGuard (guards : List GuardCheck) (kind : GuardKind) : Prop

The list contains a failed guard of the specified kind.

Equations

• O3.HasFailedGuard guards kind = ∃ check ∈ guards, check.kind = kind ∧ ¬check.Holds

inductive O3.TrialOutcome (d : ℕ) : Type

Data-level outcome of a deterministic guarded local trial.

• success {d : ℕ} (point : Vec d) : TrialOutcome d
• scale {d : ℕ} (failedKind : GuardKind) : TrialOutcome d
• radius {d : ℕ} (finalPoint : Vec d) : TrialOutcome d

structure O3.TrialReport (d : ℕ) : Type

Finite data emitted by a local trial. calls is deliberately not a free field: it is the length of the exact observation trace.

• observations : OracleTrace d

  The chronological oracle responses obtained during the local trial.

• guards : List GuardCheck

  The observable inequality checks performed by the local trial.

• outcome : TrialOutcome d

  The trial's success or rejection outcome.

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

The number of counted pair-oracle calls in the trial report.

Equations

• report.calls = O3.oracleCallCount report.observations

def O3.TrialReport.OutcomeRecorded {d : ℕ} (report : TrialReport d) : Prop

Purely data-level consistency of the recorded outcome.

Equations

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

def O3.TrialValid {d : ℕ} (oracle : PairOracle d) (gradientSize : Vec d → ℝ) (eps L R M D : ℝ) (report : TrialReport d) : Prop

Semantic obligations proved by a regime-specific local trial. This is a proposition, not a certificate field. The scale and radius conclusions are exactly the directional implications used by the frozen outer-controller lemma.

Equations

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

theorem O3.TrialValid.traceExact {d : ℕ} {oracle : PairOracle d} {gradientSize : Vec d → ℝ} {eps L R M D : ℝ} {report : TrialReport d} (h : TrialValid oracle gradientSize eps L R M D report) : TraceExact oracle report.observations

theorem O3.TrialValid.outcomeRecorded {d : ℕ} {oracle : PairOracle d} {gradientSize : Vec d → ℝ} {eps L R M D : ℝ} {report : TrialReport d} (h : TrialValid oracle gradientSize eps L R M D report) : report.OutcomeRecorded