Cost of the conjunction of the last state-compatibility checks
ProvedOAI.ThreeMachine.StackCompiler.Costs.scDEFHIJThroughout, a routine R : Uniform f is a program in the compiler's while-language Code, with a charge function, that computes the function family on encoded data. R.time i x is the charge of on the encoding of , a natural number that bounds the number of evaluation steps of the program on that input. For , the predicate Poly s f d means that there is a constant with for all . Here Uniform.scDEFHIJ is the routine evaluating, on an input consisting of a universe, a matrix, a state and a set, the last clauses of Algorithm.State.Compatible: the middle and right parts are disjoint, the middle has three elements, and the relation has no edges from middle to middle, middle to left, right to left, and right to middle. Its running time satisfies Poly of degree in the number of jobs.
Formalization Note The statement is reproduced verbatim from upstream StateCosts.lean (openai/math, Apache-2.0, credit OpenAI). It feeds the bound requestRawBound_poly and the running-time statement of main_theorem.
import Mathlib
import Definitions.Def_OAIThreeMachineSched02
set_option maxHeartbeats 2000000
set_option maxRecDepth 100000
set_option linter.all false
set_option Elab.async false
namespace OAI
universe u1 u2 u3 u4 u5 u6 u7 u8
section
namespace ThreeMachine.StackCompiler.Uniform
variable {I : Type u1} {α : I → Type u2} {β : I → Type u3} [∀ i, Coding (α i)] [∀ i, Coding (β i)]
end ThreeMachine.StackCompiler.Uniform
namespace ThreeMachine.StackCompiler.Uniform
variable {I : Type u7} {α : I → Type u8} [∀ i, Coding (α i)]
end ThreeMachine.StackCompiler.Uniform
end
section
namespace ThreeMachine.StackCompiler
namespace Costs
end Costs
namespace Uniform
end Uniform
namespace Costs
end Costs
end ThreeMachine.StackCompiler
end
section
namespace ThreeMachine.StackCompiler.Uniform
end ThreeMachine.StackCompiler.Uniform
namespace ThreeMachine.StackCompiler.Costs
end ThreeMachine.StackCompiler.Costs
end
section
namespace ThreeMachine.StackCompiler.Costs
end ThreeMachine.StackCompiler.Costs
namespace ThreeMachine.StackCompiler.Uniform
end ThreeMachine.StackCompiler.Uniform
namespace ThreeMachine.StackCompiler.Costs
theorem scDEFHIJ : Poly (fun x : Σ n, Uniform.CompatInput n => x.1)
(fun x => Uniform.scDEFHIJ.time x.1 x.2) 5 := by
sorry
end ThreeMachine.StackCompiler.Costs
end
end OAI