OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSchedule.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The input-only loop through the lifted parent residue classes

  1. structure OAI.LowSpaceSubsetSum.RepresentationScheduleData line 11

    Source documentation

    Primitive data retained before the residue loop. There is no designated solution or selected successful residue in the runtime state.

    structure RepresentationScheduleData (n g : ℕ) where
…
  2. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.target line 30
  3. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.modulus line 33
  4. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.modulus_positive line 35
  5. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.leftResidue line 39
  6. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.parentData line 41
  7. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.bucket line 55
  8. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.scanBuckets line 63

    Source documentation

    A counter loop, with no array of all residues. Each completed iteration releases its parent workspace before the next iteration.

    def scanBuckets (B : ℕ) (families : Fin 4 → Array (Finset (Fin g))) : ℕ → ℕ → Bool
  | _, 0 => false
  | z, remaining + 1 =>
    if (D.bucket z).run B families then true else scanBuckets B families (z + 1) remaining

    Mentions: OAI.LowSpaceSubsetSum.RepresentationScheduleData.run

  9. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.run line 68
  10. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.scanBuckets_sound line 71
  11. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.scanBuckets_complete line 84
  12. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.run_complete line 100
  13. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.run_sound line 105