Model.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Indexed Subset Sum and the random sign transformation

The input is indexed: equal numerical values at different indices remain different choices. The empty subset is included. These definitions and lemmas implement the sign transformation in §3 of A Low-Space Algorithm for Worst-Case Subset Sum (equation alg:sign-flip). No distributional assumption on the input weights is made.

structure OAI.LowSpaceSubsetSum.Instance line 23
Source documentation
A positive-integer input, with a nonnegative target.
```
structure Instance (n : ℕ) where
…
```

def OAI.LowSpaceSubsetSum.weight line 29

Source documentation

Exact integer weight of an indexed subset.

def weight {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a : ι → ℤ) (S : Finset ι) : ℤ :=
…

def OAI.LowSpaceSubsetSum.Solvable line 34
Source documentation
The decision predicate includes the empty subset.
```
def Solvable {n : ℕ} (I : Instance n) : Prop :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance
theorem OAI.LowSpaceSubsetSum.weight_empty line 37
theorem OAI.LowSpaceSubsetSum.zero_target_solvable line 41

def OAI.LowSpaceSubsetSum.flip line 46

Source documentation

Negate precisely the indices in F.

def flip {ι : Type*} [DecidableEq ι] (a : ι → ℤ) (F : Finset ι) (i : ι) : ℤ :=
…

theorem OAI.LowSpaceSubsetSum.weight_flip line 50
Source documentation
The signed weight is a translated original weight after toggling indices.
```
theorem weight_flip {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a : ι → ℤ) (F S : Finset ι) :
    weight (flip a F) S = weight a (S ∆ F) - weight a F := by
…
```
Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.flip
theorem OAI.LowSpaceSubsetSum.signed_solution_iff line 61
Source documentation
Toggling the sign set translates solutions in both directions.
```
theorem signed_solution_iff {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a : ι → ℤ) (t : ℤ) (F S : Finset ι) :
    weight (flip a F) S = t - weight a F ↔ weight a (S ∆ F) = t := by
…
```
Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.flip
theorem OAI.LowSpaceSubsetSum.signed_solvable_iff line 67

theorem OAI.LowSpaceSubsetSum.weight_union line 78

Source documentation

Disjoint joins preserve exact weights.

theorem weight_union {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a : ι → ℤ) {S T : Finset ι} (h : Disjoint S T) :
    weight a (S ∪ T) = weight a S + weight a T := by
…

Mentions: OAI.LowSpaceSubsetSum.weight

theorem OAI.LowSpaceSubsetSum.match_sound line 90

Source documentation

An exact disjoint signed match certifies an original indexed solution.

theorem match_sound {n : ℕ} (I : Instance n) (F L R : Finset (Fin n))
    (hd : Disjoint L R)
    (hm : weight (flip (fun i => (I.values i : ℤ)) F) L +
      weight (flip (fun i => (I.values i : ℤ)) F) R =
      (I.target : ℤ) - weight (fun i => (I.values i : ℤ)) F) :
    Solvable I := by
…

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

structure OAI.LowSpaceSubsetSum.Entry line 102
Source documentation
A dictionary key retains the exact weight and the entire top-block mask.
```
structure Entry (ι : Type*) where
…
```
def OAI.LowSpaceSubsetSum.Represents line 107
Source documentation
A retained entry has a subset witness within its parent's allowed domain.
```
def Represents {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a : ι → ℤ) (domain top : Finset ι) (e : Entry ι) : Prop :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry

theorem OAI.LowSpaceSubsetSum.disjoint_of_top_masks line 112

Source documentation

If the parents share only top indices, their masks decide compatibility.

theorem disjoint_of_top_masks {ι : Type*} [DecidableEq ι]
    {leftDomain rightDomain top L R : Finset ι}
    (hshared : leftDomain ∩ rightDomain ⊆ top)
    (hL : L ⊆ leftDomain) (hR : R ⊆ rightDomain)
    (hmasks : Disjoint (L ∩ top) (R ∩ top)) : Disjoint L R := by
…

theorem OAI.LowSpaceSubsetSum.entry_match_sound line 125

Source documentation

Soundness depends only on the stored key, so duplicate witnesses can be discarded without changing the existence of a compatible exact match.

theorem entry_match_sound {n : ℕ} (I : Instance n) (F : Finset (Fin n))
    {leftDomain rightDomain top : Finset (Fin n)}
    (hshared : leftDomain ∩ rightDomain ⊆ top) {l r : Entry (Fin n)}
    (hl : Represents (flip (fun i => (I.values i : ℤ)) F) leftDomain top l)
    (hr : Represents (flip (fun i => (I.values i : ℤ)) F) rightDomain top r)
    (hd : Disjoint l.mask r.mask)
    (hw : l.value + r.value = I.target - weight (fun i => (I.values i : ℤ)) F) :
    Solvable I := by
…

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