Cost of reading a precedence entry in either frame
ProvedOAI.ThreeMachine.StackCompiler.Costs.matrixGetFrameThroughout, 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 . For a Boolean frame, the routine Uniform.matrixGetFrame frame decides matrixRel M a b, or matrixRel M b a when frame is true. Its running time satisfies Poly of degree in , on input a matrix on jobs and a pair of indices.
Formalization Note The statement is reproduced verbatim from upstream RankCosts.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
section
namespace ThreeMachine.StackCompiler.Costs
variable {J : Type u1} (n : J → ℕ) (x : ∀ j, Uniform.RankCellInput (n j))
end ThreeMachine.StackCompiler.Costs
end
section
namespace ThreeMachine.StackCompiler.Costs
variable {J : Type u2} (n : J → ℕ)
end ThreeMachine.StackCompiler.Costs
end
section
namespace ThreeMachine.StackCompiler.Uniform
end ThreeMachine.StackCompiler.Uniform
namespace ThreeMachine.StackCompiler.Costs
variable {J : Type} (n : J → ℕ)
end ThreeMachine.StackCompiler.Costs
end
section
namespace ThreeMachine.StackCompiler.Uniform
end ThreeMachine.StackCompiler.Uniform
namespace ThreeMachine.StackCompiler.Costs
open ThreeMachine.Structure
theorem matrixGetFrame (frame : Bool) :
Poly (fun x : Σ n, Matrix n × (Fin n × Fin n) => x.1)
(fun x => (Uniform.matrixGetFrame frame).time x.1 x.2) 3 := by
sorry
end ThreeMachine.StackCompiler.Costs
end
end OAI