RepresentationParentComplete.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Complete bounded parent arrays and preservation of exact entry keys

def OAI.LowSpaceSubsetSum.RepresentationParentData.rawEntries line 14
Source documentation
Mathematical list of valid entries emitted by this task. The executable collector keeps only the bounded deduplicated array.
```
def rawEntries : List (Entry (Fin n)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry
def OAI.LowSpaceSubsetSum.RepresentationParentData.RawEligible line 18
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.key_match_iff line 23
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.rawEligible_parent_mod line 42
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.rawEligible_of_filters line 48
Source documentation
The two low child filters and one full parent filter place a designated raw tuple in the actual streams. Prefix tests are on its individual leaves.
```
theorem rawEligible_of_filters (x : Parent (n := n))
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData.Parent
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.rawEntries_mem line 68
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.rawEntries_parent_mod line 78
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.collect_eq_records line 83
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.entries_raw line 95

theorem OAI.LowSpaceSubsetSum.RepresentationParentData.collect_fits line 105

Source documentation

Equal keys can arise from many repeated raw representations. The bound is on the containing distinct-entry universe, not the number of reports.

theorem collect_fits (B : ℕ) (U : Finset (Entry (Fin n)))
    (hcap : U.card ≤ D.capacity) (hU : ∀ e ∈ D.rawEntries, e ∈ U) :
    (D.collect B).state.user.keys.overflow = false ∧ ∀ q,
      (∃ e ∈ (D.entries B).toList, WeightEncoding.entryKey D.input e = q) ↔
        ∃ e ∈ D.rawEntries, WeightEncoding.entryKey D.input e = q := by
…

Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.WeightEncoding.entryKey

theorem OAI.LowSpaceSubsetSum.RepresentationParentData.entries_mem_iff line 126
Source documentation
Fixed-width keys lose no exact weight/mask entry on the actual bounded weight universe. Deduplication can change the witness but not the entry.
```
theorem entries_mem_iff (B : ℕ) (U : Finset (Entry (Fin n)))
    (hcap : U.card ≤ D.capacity) (hU : ∀ e ∈ D.rawEntries, e ∈ U)
    (hbounded : ∀ e ∈ U, WeightEncoding.BoundedWeight D.input e.value)
    (e : Entry (Fin n)) : e ∈ (D.entries B).toList ↔ e ∈ D.rawEntries := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.WeightEncoding.BoundedWeight
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.entries_mem_iff_of_complete line 141
Source documentation
A completed task retains every emitted exact entry, whether or not an ambient capacity bound was supplied in advance.
```
theorem entries_mem_iff_of_complete (B : ℕ)
    (hc : (D.collect B).state.user.keys.overflow = false)
    (hbounded : ∀ e ∈ D.rawEntries, WeightEncoding.BoundedWeight D.input e.value)
    (e : Entry (Fin n)) : e ∈ (D.entries B).toList ↔ e ∈ D.rawEntries := by
…
```
Mentions: OAI.LowSpaceSubsetSum.WeightEncoding.BoundedWeight, OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.rawEntries_represents line 162