OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Representation runtime data without a supplied solution

The zero-target wrapper supplies layout and domain facts. Its solution and target do not enter the runtime's input, signs or signed target.

  1. structure OAI.LowSpaceSubsetSum.RepresentationData line 15
  2. def OAI.LowSpaceSubsetSum.RepresentationData.zeroSetup line 25
  3. def OAI.LowSpaceSubsetSum.RepresentationData.scheduleData line 35

    Source documentation

    All fields are determined by the input and the random draw history. In particular, the second layout coordinate is the actual sign mask.

    def scheduleData (h : D.zeroSetup.PrimeHistory) (r : D.zeroSetup.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (q : ℕ) (hq : 0 < q) : RepresentationScheduleData n (2 * RepresentationSetup.blockHalf n 0) where
…

    Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.RepresentationScheduleData, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf

  4. def OAI.LowSpaceSubsetSum.RepresentationData.trial line 54
  5. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeData line 67
  6. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeHistory line 71

    Source documentation

    Convert the successful-analysis coordinates to the actual random signs. The finite partition and prime choices do not depend on the fixed solution.

    def runtimeHistory (h : R.PrimeHistory) : R.runtimeData.zeroSetup.PrimeHistory :=
…
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_schedule_eq line 74
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_trial_eq line 82