The early-failure and complete shapes of source Euclidean reports.

@[instance_reducible]

noncomputable def V7.Stage1E03.shapesPropDecidable (q : Prop) : Decidable q

Classical proposition decisions used locally in the report-shape proofs.

Equations

• V7.Stage1E03.shapesPropDecidable q = Classical.propDecidable q

noncomputable def V7.Stage1E03.phaseATraceFrom {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : List (Observation d)

The alternating query and accelerated-point observations of an estimate-phase segment.

Equations

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

noncomputable def V7.Stage1E03.phaseAGuardsFrom {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : List (ObservableGuardCheck d)

The upper-model guards corresponding to an estimate-phase segment.

Equations

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

@[simp]

theorem V7.Stage1E03.phaseATraceFrom_zero {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k : ℕ) : phaseATraceFrom inst M k 0 = []

@[simp]

theorem V7.Stage1E03.phaseAGuardsFrom_zero {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k : ℕ) : phaseAGuardsFrom inst M k 0 = []

theorem V7.Stage1E03.phaseATraceFrom_succ {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : phaseATraceFrom inst M k (fuel + 1) = [O3.PairOracle.observe inst.oracle (estimateQuery M x0 k (sourceEstimateState inst.oracle M x0 k)), O3.PairOracle.observe inst.oracle (sourceEstimateState inst.oracle M x0 (k + 1)).accelerated] ++ phaseATraceFrom inst M (k + 1) fuel

theorem V7.Stage1E03.phaseAGuardsFrom_succ {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : phaseAGuardsFrom inst M k (fuel + 1) = [upperCheck (O3.PairOracle.observe inst.oracle (estimateQuery M x0 k (sourceEstimateState inst.oracle M x0 k))) (O3.PairOracle.observe inst.oracle (sourceEstimateState inst.oracle M x0 (k + 1)).accelerated)] ++ phaseAGuardsFrom inst M (k + 1) fuel

@[simp]

theorem V7.Stage1E03.phaseATraceFrom_length {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : (phaseATraceFrom inst M k fuel).length = 2 * fuel

@[simp]

theorem V7.Stage1E03.phaseAGuardsFrom_length {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (k fuel : ℕ) : (phaseAGuardsFrom inst M k fuel).length = fuel

def V7.Stage1E03.FailureLedger {d : ℕ} (p M : ℝ) (report : TrialReport d) (failed : ObservableGuardCheck d) : Prop

The report records precisely the first failed guard after a prefix of accepted guards.

Equations

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

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

Every observation used in a checked guard occurs in the report's trace.

Equations

• V7.Stage1E03.GuardPairsInTrace report = ∀ check ∈ report.checkedGuards, check.xPair ∈ report.trace ∧ check.yPair ∈ report.trace

theorem V7.Stage1E03.prepend_failureLedger {d : ℕ} (p M : ℝ) (history : List (Observation d)) (guards : List (ObservableGuardCheck d)) (tail : TrialReport d) (failed : ObservableGuardCheck d) (hguards : ∀ check ∈ guards, CheckHolds p M check) (htail : FailureLedger p M tail failed) : FailureLedger p M (prependReport history guards tail) failed

theorem V7.Stage1E03.sourcePhaseAReport_shape {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n fuel k : ℕ) : k + fuel = n → have report := sourcePhaseAReport inst eps M n k fuel; (∃ r < fuel, ∃ (failed : ObservableGuardCheck d), FailureLedger 2 M report failed ∧ GuardPairsInTrace report ∧ report.trace <+: phaseATraceFrom inst M k fuel ∧ report.checkedGuards <+: phaseAGuardsFrom inst M k fuel ∧ report.trace.length = 2 * (r + 1) ∧ report.checkedGuards.length = r + 1 ∧ failed.kind = ObservableGuardKind.upperModel) ∨ (∀ check ∈ phaseAGuardsFrom inst M k fuel, CheckHolds 2 M check) ∧ report = prependReport (phaseATraceFrom inst M k fuel) (phaseAGuardsFrom inst M k fuel) (sourcePhaseBReport inst eps M n (sourceEstimateState inst.oracle M x0 n).accelerated)

theorem V7.Stage1E03.sourcePhaseBReport_shape {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) : have cfg := O3.stage9ExecutionConfig n inst.oracle M U; have newTrace := List.map (fun (j : ℕ) => O3.PairOracle.observe inst.oracle (O3.ogmgState cfg (j + 1)).current) (List.range n); have checks := allInterpolationChecks n fun (i : ℕ) => O3.PairOracle.observe inst.oracle (O3.ogmgState cfg i).current; have terminal := terminalCheck (O3.PairOracle.observe inst.oracle (O3.ogmgState cfg n).current) (O3.PairOracle.observe inst.oracle (O3.ogmgV cfg n)); have report := sourcePhaseBReport inst eps M n U; (∃ (failed : ObservableGuardCheck d), FailureLedger 2 M report failed ∧ (failed.kind = ObservableGuardKind.interpolation ∧ report.trace = newTrace ∧ report.checkedGuards <+: checks ∨ failed.kind = ObservableGuardKind.terminalDescent ∧ report.trace = newTrace ++ [O3.PairOracle.observe inst.oracle (O3.ogmgV cfg n)] ∧ report.checkedGuards = checks ++ [terminal])) ∨ (∃ (on : Observation d), report.outcome = TrialOutcome.success on ∧ on = O3.PairOracle.observe inst.oracle (O3.ogmgState cfg n).current ∧ report.trace = newTrace ++ [O3.PairOracle.observe inst.oracle (O3.ogmgV cfg n)] ∧ report.checkedGuards = checks ++ [terminal] ∧ (∀ check ∈ report.checkedGuards, CheckHolds 2 M check) ∧ lpNorm 2 on.gradient ≤ eps) ∨ ∃ (on : Observation d), report.outcome = TrialOutcome.radius on ∧ on = O3.PairOracle.observe inst.oracle (O3.ogmgState cfg n).current ∧ report.trace = newTrace ++ [O3.PairOracle.observe inst.oracle (O3.ogmgV cfg n)] ∧ report.checkedGuards = checks ++ [terminal] ∧ (∀ check ∈ report.checkedGuards, CheckHolds 2 M check) ∧ eps < lpNorm 2 on.gradient