Finite affine transcripts are indistinguishable from a sufficiently distant hard-family instance.

theorem V7.Stage6StrictDeterministic.hard_affine_observation_eq {eps H : ℝ} (x0 x : StrictPoint) (hx : x 0 - x0 0 < H) : O3.PairOracle.observe (hardOracle eps x0 H) x = O3.PairOracle.observe (strictAffineOracle eps x0) x

On the whole pre-transition half-line, both exact oracle fields coincide.

theorem V7.Stage6StrictDeterministic.hard_runConsistent_of_affine {method : StrictLocalMethod} {eps H : ℝ} {trace : StrictTranscript} (haffine : StrictRunConsistent method (strictAffineOracle eps method.x0) trace) (hleft : ∀ obs ∈ trace, obs.point 0 - method.x0 0 < H) : StrictRunConsistent method (hardOracle eps method.x0 H) trace

Exact transcript coupling: exactness is transported observation by observation, while the causal prefix/query equations are literally unchanged.

theorem V7.Stage6StrictDeterministic.all_queries_fail_of_left {eps H : ℝ} (heps : 0 < eps) (x0 : StrictPoint) {trace : StrictTranscript} {N : ℕ} (hlen : List.length trace = N) (hleft : ∀ obs ∈ trace, obs.point 0 - x0 0 < H) : StrictAllFirstNQueriesFail eps (hardOracle eps x0 H) trace N

theorem V7.Stage6StrictDeterministic.finite_output_fails_of_left {method : StrictLocalMethod} {eps H : ℝ} (heps : 0 < eps) (heq : method.eps = eps) (trace : StrictTranscript) (N : ℕ) (hleft : method.output N trace 0 - method.x0 0 < H) : StrictFiniteOutputFails method (hardOracle eps method.x0 H) trace N