OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorEncodedCheck.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LowSpaceSubsetSum.TopCoordinates line 9
2. def OAI.LowSpaceSubsetSum.TopCoordinates.domain line 17
3. def OAI.LowSpaceSubsetSum.TopCoordinates.encodeMask line 19
4. theorem OAI.LowSpaceSubsetSum.TopCoordinates.encodeMask_mem line 22
5. def OAI.LowSpaceSubsetSum.TopCoordinates.encodeEntry line 25
6. theorem OAI.LowSpaceSubsetSum.TopCoordinates.disjoint_of_encoded line 28
7. theorem OAI.LowSpaceSubsetSum.TopCoordinates.encoded_disjoint line 36
8. def OAI.LowSpaceSubsetSum.TopCoordinates.check line 42
9. theorem OAI.LowSpaceSubsetSum.TopCoordinates.sound line 46
10. theorem OAI.LowSpaceSubsetSum.TopCoordinates.subset_sum_sound line 58

    Source documentation

    The stored key witnesses suffice for original-input one-sided soundness.

    theorem subset_sum_sound (I : Instance n) (F : Finset (Fin n))
        (families : Fin 4 → Array (Finset (Fin g)))
        (xs ys : List (Entry (Fin n))) (hsize : xs.length + ys.length ≤ 2 ^ n)
        (leftDomain rightDomain : Finset (Fin n))
        (hshared : leftDomain ∩ rightDomain ⊆ C.domain)
        (hleft : ∀ x ∈ xs, Represents (flip (fun i => (I.values i : ℤ)) F) leftDomain C.domain x)
        (hright : ∀ y ∈ ys, Represents (flip (fun i => (I.values i : ℤ)) F) rightDomain C.domain y)
        (hyes : (C.check families ((I.target : ℤ) - weight (fun i => (I.values i : ℤ)) F)
          xs ys).accepted = true) : Solvable I := by
    …

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.Represents, OAI.LowSpaceSubsetSum.flip, OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.Solvable