OAI/Combinatorics/UniformKServer/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.uniform_squared_logarithmic_main line 25

   Source documentation

   The literal finite-control wrapper is a single horizon-free online machine. The very large verified constructor is paid only through a finite, instance- dependent initial delay; each request still takes the fixed linear bit budget.

   Distinct definitions of this name: ComparatorChallenges/UniformKServer.lean:200 (same statement text; different proof or body). Qualify references as OAI.UniformKServer.uniform_squared_logarithmic_main@path.

   theorem uniform_squared_logarithmic_main : UniformAlgorithmClaim := by
   …

   Mentions: OAI.UniformKServer.UniformAlgorithmClaim