Cost of one entry of a transitive-closure step
ProvedOAI.ThreeMachine.StackCompiler.Costs.nextMatrixCellThroughout, 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 . The routine Uniform.nextMatrixCell computes one entry of nextMatrix M R, the Boolean matrix step used to compute reachability, at a given pair of indices. Its running time satisfies Poly of degree in the number of jobs.
Formalization Note The statement is reproduced verbatim from upstream OutputCosts.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
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
end
section
namespace ThreeMachine.StackCompiler
end ThreeMachine.StackCompiler
end
section
namespace ThreeMachine.StackCompiler
namespace Poly
variable {J : Type} {s n : J → ℕ} {d e : ℕ}
end Poly
namespace Costs
end Costs
end ThreeMachine.StackCompiler
end
section
namespace ThreeMachine.StackCompiler.Costs
theorem nextMatrixCell : Poly
(fun x : Σ n, (Fin n × Fin n) × (Universe n × (Matrix n × Matrix n)) => x.1)
(fun x => Uniform.nextMatrixCell.time x.1 x.2) 10 := by
sorry
end ThreeMachine.StackCompiler.Costs
end
end OAI