OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedFamilyBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Family generation stays inside the application budgets

The family count is exponential only in one top block. Range tests and permutation materialization keep polynomial work per sampled mask.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.self_le_power line 19
  2. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.coefficient_power line 22
  3. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.maskBudget_add_le line 25
  4. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.family_envelope line 49
  5. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.prepared_envelope line 59
  6. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.familiesPrepared_bounded_scale line 88
  7. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.familiesPrepared_application line 97
  8. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.canonical_family_half line 111
  9. theorem OAI.LowSpaceSubsetSum.WordSeedFamilyBounds.canonical_family_codes line 116