OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationMasks.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Actual solution subsets behind the surviving representation

An arbitrary deterministic background assignment is allowed: its precise integer allocation affects resource costs, but not the survival identities. Filtering the outside indices by that assignment makes the pieces disjoint without imposing another probabilistic assumption.

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.mixerUnion line 23
  2. def OAI.LowSpaceSubsetSum.RepresentationSetup.outside line 26
  3. abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment line 29

    Source documentation

    The program's prescribed background allocation gives one such function.

    abbrev BackgroundAssignment (n : ℕ) := Layout n → Guesses n → Fin n → Fin 4

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses

  4. def OAI.LowSpaceSubsetSum.RepresentationSetup.background line 31
  5. def OAI.LowSpaceSubsetSum.RepresentationSetup.leftBackground line 35
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.orderedMixers_disjoint line 38
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.background_subset_outside line 44
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.background_disjoint_mixer line 48
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.background_disjoint line 60
  10. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.leftBackground_disjoint_mixer line 67
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.background_subset_solution line 73
  12. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.leftBackground_subset_solution line 77
  13. def OAI.LowSpaceSubsetSum.RepresentationSetup.firstTop line 84

    Source documentation

    Child one uses top blocks one and two. Child two uses the remaining top blocks, each once, exactly as in the manuscript's leaf layout.

    def firstTop (z : Layout n) (f : R.Partitions z) (D : Finset (Fin n)) : Finset (Fin n) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout

  14. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstTop_subset line 87
  15. def OAI.LowSpaceSubsetSum.RepresentationSetup.actualOffsets line 90
  16. def OAI.LowSpaceSubsetSum.RepresentationSetup.leftParent line 100
  17. def OAI.LowSpaceSubsetSum.RepresentationSetup.rightParent line 105
  18. def OAI.LowSpaceSubsetSum.RepresentationSetup.firstLeftChild line 108
  19. def OAI.LowSpaceSubsetSum.RepresentationSetup.secondLeftChild line 114
  20. def OAI.LowSpaceSubsetSum.RepresentationSetup.firstRightChild line 117
  21. def OAI.LowSpaceSubsetSum.RepresentationSetup.secondRightChild line 124
  22. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.leftParent_subset_solution line 127
  23. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstLeftChild_subset_parent line 135
  24. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.selectedHalves_disjoint line 146
  25. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.disjoint_three_unions line 150
  26. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstRightChild_disjoint_left line 163
  27. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstRightChild_subset_parent line 186
  28. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.leftParent_weight line 200
  29. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rightParent_weight line 221
  30. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstLeftChild_weight line 229
  31. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstRightChild_weight line 253
  32. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.parents_partition line 279
  33. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.children_partition line 285
  34. def OAI.LowSpaceSubsetSum.RepresentationSetup.ActualFilters line 296
  35. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actualFilters_of_hits line 308
  36. def OAI.LowSpaceSubsetSum.RepresentationSetup.ActualRepresentation line 323
  37. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.successful_actualRepresentation line 338
  38. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actualRepresentation_probability line 350

    Source documentation

    The actual parent subsets represent the fixed signed solution, meet the prescribed smaller/complementary mask counts, and pass all six filters.

    theorem actualRepresentation_probability (B : BackgroundAssignment n)
    (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize)) :
    1 / (inputScale R.input : ℝ) ^ 100 ≤
      R.trialLaw.probability (R.ActualRepresentation B) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment, OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale

  39. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actualRepresentation_with_resources line 363

    Source documentation

    Subtract the unconditional resource failure only after fixing the representation event; no division by its rare probability is made.

    theorem actualRepresentation_with_resources (B : BackgroundAssignment n)
    (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize))
    (E : R.TrialHistory → Prop) {δ : ℝ}
    (hfail : R.trialLaw.probability (fun h => ¬ E h) ≤ δ) :
    1 / (inputScale R.input : ℝ) ^ 100 - δ ≤
      R.trialLaw.probability (fun h => R.ActualRepresentation B h ∧ E h) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment, OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale

  40. theorem OAI.LowSpaceSubsetSum.eventually_actual_representation line 380