Efficient threshold search for logarithmic-gap MINKT -- proof internals

theorem Complexity.GapMINKT.Logarithmic.Efficient.encodedTimeSearchEstimator_mem_FP_internal (decide : List Bool → Bool) (hdecide : (fun (bits : List Bool) => [decide bits]) ∈ FP) : encodedTimeSearchEstimator decide ∈ FP

theorem Complexity.GapMINKT.Logarithmic.Efficient.encodedTimeSearchEstimator_encode_internal (decide : List Bool → Bool) (inst : MINKT.Instance) : encodedTimeSearchEstimator decide inst.encode = List.replicate (timeSearchEstimator decide inst) true

theorem Complexity.GapMINKT.Logarithmic.Efficient.encodedTimeSearchEstimator_length_encode_internal (decide : List Bool → Bool) (inst : MINKT.Instance) : (encodedTimeSearchEstimator decide inst.encode).length = timeSearchEstimator decide inst

theorem Complexity.GapMINKT.Logarithmic.Efficient.executableEstimator_eq_timeSearchEstimator_internal (decide : List Bool → Bool) : executableEstimator decide = timeSearchEstimator decide

theorem Complexity.GapMINKT.Logarithmic.Efficient.fp_and_satisfiesBoundsOn_printerClock_internal {tapes : ℕ} {machine : TM tapes} {parameters : Parameters} (huniversal : machine.IsEfficientlyUniversal) {decide : List Bool → Bool} (hdecide : (fun (bits : List Bool) => [decide bits]) ∈ FP) (haccept : ∀ bits ∈ yesLanguage machine, decide bits = true) (hreject : ∀ bits ∈ noLanguage machine parameters, decide bits = false) : ∃ (coefficient : ℕ) (exponent : ℕ), encodedTimeSearchEstimator decide ∈ FP ∧ (executableEstimator decide).SatisfiesBoundsOn machine parameters fun (inst : MINKT.Instance) => coefficient * (2 * inst.output.length + 3) ^ exponent ≤ inst.time