Absolute simulation bounds on the original legal answer cut

Ambient boundedness controls input-size degree as well as a time coefficient. On four bit strings of length at most (2^n)^λ, the resulting absolute cost has a quadratic exponent in λ. The polynomial-exponent introspection budget absorbs this cost without enlarging the original game's answer alphabet.

These lemmas concern actual source and universal-simulator runs. They do not yet construct the introspective decider's format checks or other subtests.

theorem MIPRE.Introspection.legal_query_size_le (R : ℕ) (x y a b : Cost.BitStr) (hx : List.length x ≤ R) (hy : List.length y ≤ R) (ha : List.length a ≤ R) (hb : List.length b ≤ R) : Cost.esize (x, y, a, b) + 1 ≤ 16 * R + 8

Exact linear size bound for the four fields of a legal decider query.

theorem MIPRE.Introspection.legal_query_cost_le {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) (hx : List.length x ≤ (2 ^ n) ^ lam) (hy : List.length y ≤ (2 ^ n) ^ lam) (ha : List.length a ≤ (2 ^ n) ^ lam) (hb : List.length b ≤ (2 ^ n) ^ lam) : (2 ^ n) ^ lam * (Cost.esize (x, y, a, b) + 1) ^ lam ≤ ansBound 5 lam n

Legal-input ambient costs fit the repaired budget with exponent five.

theorem MIPRE.Introspection.original_decider_haltsWithin {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) (hx : List.length x ≤ (2 ^ n) ^ lam) (hy : List.length y ≤ (2 ^ n) ^ lam) (ha : List.length a ≤ (2 ^ n) ^ lam) (hb : List.length b ≤ (2 ^ n) ^ lam) : Cost.HaltsWithin V.decider.prog (Cost.encode (2 ^ n, x, y, a, b)) (ansBound 5 lam n)

An actual bounded decider halts within an absolute polynomial-exponent budget on every input from the original answer cut.

theorem MIPRE.Introspection.polynomial_ansBound (P : Polynomial ℕ) (k : ℕ) : ∃ (C : ℕ), ∀ (lam n : ℕ), 1 ≤ lam → 1 ≤ n → Polynomial.eval (ansBound k lam n) P ≤ ansBound C lam n

Any fixed polynomial overhead is absorbed by another polynomial exponent.

theorem MIPRE.Introspection.original_simulation_haltsWithin (U : Cost.UniversalMachine) : ∃ (C : ℕ), ∀ {ℓ lam n : ℕ} (V : Verifier ℓ), V.IsBounded lam → 1 ≤ n → ∀ (x y a b : Cost.BitStr), List.length x ≤ (2 ^ n) ^ lam → List.length y ≤ (2 ^ n) ^ lam → List.length a ≤ (2 ^ n) ^ lam → List.length b ≤ (2 ^ n) ^ lam → Cost.HaltsWithin U.univ ((Cost.encode V.decider.prog).cons (Cost.encode (2 ^ n, x, y, a, b))) (ansBound C lam n)

Uniform absolute time for the actual universal simulation, on the original legal question and answer cut. The exponent depends only on the universal machine.