OAI/Combinatorics/UniformKServer/RawCertificate.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite arithmetic certificates of the unknown-offset construction. The verifier checks every finite word and every hindsight label history; no competitive conclusion is an input. All its checks are primitive recursive.

  1. abbrev OAI.UniformKServer.RawCertificate.Input line 15
  2. abbrev OAI.UniformKServer.RawCertificate.Certificate line 16
  3. def OAI.UniformKServer.RawCertificate.ell line 18
  4. def OAI.UniformKServer.RawCertificate.bits line 19
  5. def OAI.UniformKServer.RawCertificate.cap line 20
  6. def OAI.UniformKServer.RawCertificate.restart line 21
  7. def OAI.UniformKServer.RawCertificate.diam line 22
  8. def OAI.UniformKServer.RawCertificate.sep line 23
  9. def OAI.UniformKServer.RawCertificate.table line 24
  10. def OAI.UniformKServer.RawCertificate.horizon line 26
  11. def OAI.UniformKServer.RawCertificate.rowOK line 28
  12. def OAI.UniformKServer.RawCertificate.rowsOK line 33
  13. def OAI.UniformKServer.RawCertificate.tableOK line 36
  14. def OAI.UniformKServer.RawCertificate.numbersOK line 41
  15. def OAI.UniformKServer.RawCertificate.boundsOK line 47
  16. def OAI.UniformKServer.RawCertificate.verify line 51
  17. theorem OAI.UniformKServer.RawCertificate.primitive_le line 61
  18. theorem OAI.UniformKServer.RawCertificate.primitive_any line 63
  19. theorem OAI.UniformKServer.RawCertificate.primitive_horizon line 68
  20. theorem OAI.UniformKServer.RawCertificate.primitive_rowOK line 70
  21. theorem OAI.UniformKServer.RawCertificate.primitive_rowsOK line 73
  22. theorem OAI.UniformKServer.RawCertificate.primitive_tableOK line 76
  23. theorem OAI.UniformKServer.RawCertificate.primitive_numbersOK line 82
  24. theorem OAI.UniformKServer.RawCertificate.primitive_boundsOK line 86
  25. theorem OAI.UniformKServer.RawCertificate.primitive_verify line 90