Affine transport of algorithms, oracle observations, and exact chronological traces.

noncomputable def V7.Stage5AboveTwoLowerS5F.physicalForward {d : ℕ} (x0 : Point d) (R rT : ℝ) (z : Point d) : Point d

The affine map from normalized coordinates to the requested physical radius and center.

Equations

• V7.Stage5AboveTwoLowerS5F.physicalForward x0 R rT z = x0 + (R / rT) • z

noncomputable def V7.Stage5AboveTwoLowerS5F.physicalBackward {d : ℕ} (x0 : Point d) (R rT : ℝ) (x : Point d) : Point d

The affine map from physical coordinates back to the normalized construction.

Equations

• V7.Stage5AboveTwoLowerS5F.physicalBackward x0 R rT x = (rT / R) • (x - x0)

theorem V7.Stage5AboveTwoLowerS5F.physicalForward_backward {d : ℕ} (x0 : Point d) {R rT : ℝ} (hR : 0 < R) (hrT : 0 < rT) (x : Point d) : physicalForward x0 R rT (physicalBackward x0 R rT x) = x

theorem V7.Stage5AboveTwoLowerS5F.physicalBackward_forward {d : ℕ} (x0 : Point d) {R rT : ℝ} (hR : 0 < R) (hrT : 0 < rT) (z : Point d) : physicalBackward x0 R rT (physicalForward x0 R rT z) = z

noncomputable def V7.Stage5AboveTwoLowerS5F.physicalOracle {d : ℕ} (x0 : Point d) (L R rT : ℝ) (bar : PairOracle d) : PairOracle d

The normalized oracle rescaled to the prescribed physical smoothness and radius.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5F.physicalObservation {d : ℕ} (x0 : Point d) (L R rT : ℝ) (obs : Observation d) : Observation d

An observation transported to physical coordinates with rescaled value and gradient.

Equations

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

theorem V7.Stage5AboveTwoLowerS5F.physicalObservation_observe {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (z : Point d) : physicalObservation x0 L R rT (O3.PairOracle.observe bar z) = O3.PairOracle.observe (physicalOracle x0 L R rT bar) (physicalForward x0 R rT z)

noncomputable def V7.Stage5AboveTwoLowerS5F.normalizedAdversaryAlgorithm {d : ℕ} (x0 : Point d) (L R rT : ℝ) (algorithm : DeterministicExactPairAlgorithm d) : DeterministicExactPairAlgorithm d

The physical algorithm transported to the normalized resisting construction.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5F.physicalTrace {d : ℕ} (x0 : Point d) (L R rT : ℝ) (trace : List (Observation d)) : List (Observation d)

The normalized observation trace transported to physical coordinates.

Equations

• V7.Stage5AboveTwoLowerS5F.physicalTrace x0 L R rT trace = List.map (V7.Stage5AboveTwoLowerS5F.physicalObservation x0 L R rT) trace

theorem V7.Stage5AboveTwoLowerS5F.physicalTrace_take {d : ℕ} (x0 : Point d) (L R rT : ℝ) (trace : List (Observation d)) (t : ℕ) : List.take t (physicalTrace x0 L R rT trace) = physicalTrace x0 L R rT (List.take t trace)

theorem V7.Stage5AboveTwoLowerS5F.physicalTrace_generated {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hR : 0 < R) (hrT : 0 < rT) (algorithm : DeterministicExactPairAlgorithm d) (unitTrace : List (Observation d)) (hgenerated : GeneratedBy (normalizedAdversaryAlgorithm x0 L R rT algorithm) 0 unitTrace) : GeneratedBy algorithm x0 (physicalTrace x0 L R rT unitTrace)

theorem V7.Stage5AboveTwoLowerS5F.physicalTrace_exact {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (trace : List (Observation d)) (hexact : TraceExact bar trace) : TraceExact (physicalOracle x0 L R rT bar) (physicalTrace x0 L R rT trace)

theorem V7.Stage5AboveTwoLowerS5F.physicalTrace_head_point {d : ℕ} (x0 : Point d) {L R rT : ℝ} (trace : List (Observation d)) (hhead : Option.map O3.Observation.point trace.head? = some 0) : Option.map O3.Observation.point (physicalTrace x0 L R rT trace).head? = some x0