A binary answer cutoff for the compiled introspection decider

The cutoff covers full register triples and original answers. Its computation uses binary comparison and three binary shifts; its numeric value is never expanded into a unary counter.

def MIPRE.Introspection.DecisionCompiler.answerBound (Q R : ℕ) : ℕ

Equations

• MIPRE.Introspection.DecisionCompiler.answerBound Q R = 8 * max 1 (max Q R)

noncomputable def MIPRE.Introspection.DecisionCompiler.maxNat : Cost.PolyTimeFun (ℕ × ℕ) ℕ

Equations

• MIPRE.Introspection.DecisionCompiler.maxNat = MIPRE.Cost.PolyTimeFun.leNat.ite MIPRE.Cost.PolyTimeFun.snd MIPRE.Cost.PolyTimeFun.fst

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.maxNat_apply (x : ℕ × ℕ) : maxNat.toFun x = max x.1 x.2

noncomputable def MIPRE.Introspection.DecisionCompiler.doubleNat : Cost.PolyTimeFun ℕ ℕ

Equations

• MIPRE.Introspection.DecisionCompiler.doubleNat = MIPRE.Cost.PolyTimeFun.natBit.comp ((MIPRE.Cost.PolyTimeFun.const false).pair (MIPRE.Cost.PolyTimeFun.id ℕ))

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.doubleNat_apply (n : ℕ) : doubleNat.toFun n = 2 * n

noncomputable def MIPRE.Introspection.DecisionCompiler.cutoff : Cost.PolyTimeFun (ℕ × ℕ) ℕ

Equations

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

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.cutoff_apply (Q R : ℕ) : cutoff.toFun (Q, R) = answerBound Q R

theorem MIPRE.Introspection.DecisionCompiler.answerBound_ansBound {c : ℕ} (hc : 1 ≤ c) : ∃ (K : ℕ), ∀ (lam n : ℕ), 1 ≤ lam → 1 ≤ n → answerBound (SourceCompiler.registerBits c lam n) (SourceCompiler.originalBound lam n) ≤ ansBound K lam n

The concrete binary cutoff fits one fixed introspection answer budget.