OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedScalarBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Application-scale bounds for measured scalar samplers

Only the actual prime tests incur the half-exponential factor. Permutation range tests, retained candidate buffers and tuple assembly remain polynomial.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.self_le_pow line 17
  2. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.multiple_power line 20
  3. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.small_tail line 23
  4. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.factor_numeric line 30
  5. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.permutation_numeric line 56
  6. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.prime_modulus_fits line 87

    Source documentation

    The executed modulus itself fits, using strict width slack in the application.

    theorem prime_modulus_fits (I : Instance n) {ell : ℕ} (hell : ell ≤ n) :
    (WordSeedPowerExecution.run ell).1 < 2^wordWidth I := by
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.WordSeedPowerExecution.run, OAI.LowSpaceSubsetSum.wordWidth

  7. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.factorWork_le line 92
  8. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.prime_work_le line 97
  9. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.permutation_bounds line 104
  10. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.permutation_bounded_scale line 110
  11. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.scalar_cells_le line 117
  12. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.factor_bounded_scale line 130
  13. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.prime_bounded_scale line 137
  14. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.compression_bounds line 144
  15. theorem OAI.LowSpaceSubsetSum.WordSeedScalarBounds.compression_bounded_scale line 178