OAI/Combinatorics/UniformKServer/HeavyFiniteLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact finite uniform-radius law for the literal heavy process. The slot pool is fixed before the horizon; only the independent tape is truncated at the finite horizon under analysis.

  1. def OAI.UniformKServer.HeavyProcess.radiusStream line 21
  2. theorem OAI.UniformKServer.HeavyProcess.radiusStream_bounds line 25
  3. def OAI.UniformKServer.HeavyProcess.endpoint line 32
  4. theorem OAI.UniformKServer.HeavyProcess.endpoint_centers line 36
  5. def OAI.UniformKServer.HeavyProcess.birthFin line 41
  6. theorem OAI.UniformKServer.HeavyProcess.endpoint_radius line 44
  7. theorem OAI.UniformKServer.HeavyProcess.endpoint_separation line 55
  8. theorem OAI.UniformKServer.HeavyProcess.heavy_close_key line 73