RepresentationKeys.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-cost representation keys on bounded stored masks

The lists below are the stored mask representation. Their intrinsic length bound applies to every value of the type, independently of successful sampling or membership in an enumerated universe. Finite sets occur only in the semantic map. All signed membership tests are executed on stored lists.

structure OAI.LowSpaceSubsetSum.IndexedMask line 16
def OAI.LowSpaceSubsetSum.IndexedMask.semantic line 24
def OAI.LowSpaceSubsetSum.IndexedMask.ofFinset line 28
Source documentation
A canonical representation for the semantic correspondence. Enumeration can instead retain its already generated sublist, with no sorting step.
```
def ofFinset (S : Finset (Fin n)) : IndexedMask n :=
…
```
Mentions: OAI.LowSpaceSubsetSum.IndexedMask
theorem OAI.LowSpaceSubsetSum.IndexedMask.ofFinset_semantic line 31
structure OAI.LowSpaceSubsetSum.LeafRecord line 36
def OAI.LowSpaceSubsetSum.LeafRecord.semantic line 45
def OAI.LowSpaceSubsetSum.LeafRecord.ofOccurrence line 48
theorem OAI.LowSpaceSubsetSum.LeafRecord.ofOccurrence_semantic line 51
def OAI.LowSpaceSubsetSum.RepresentationKeys.signedAt line 61
Source documentation
Indexed input lookup, one explicit sign membership test, and negation.
```
def signedAt (I : Instance n) (F : IndexedMask n) (i : Fin n) : ℤ × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.signedAt_value line 65
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.signedAt_work line 70
def OAI.LowSpaceSubsetSum.RepresentationKeys.sumIndices line 79
Source documentation
All input indices are visited; both membership and signed-input lookup are charged even at indices outside the selected mask.
```
def sumIndices (I : Instance n) (F M : IndexedMask n) : List (Fin n) → ℤ × ℕ
  | [] => (0, 1)
  | i :: xs =>
    let selected := CountedWeights.member i M.indices
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.CountedWeights.member
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sumIndices_value line 88
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sumIndices_work line 99
def OAI.LowSpaceSubsetSum.RepresentationKeys.weight line 110
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.weight_value line 113
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.weight_work line 119
def OAI.LowSpaceSubsetSum.RepresentationKeys.leafWeight line 123
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.leafWeight_value line 129
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.leafWeight_work line 134
def OAI.LowSpaceSubsetSum.RepresentationKeys.pairSemantic line 142
def OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey line 146
Source documentation
Both complete leaf weights and every modular operation are charged.
```
def pairKey (I : Instance n) (F : IndexedMask n) (P : ℤ) (mode : FilteredStream.Mode)
    (x : LeafRecord n × LeafRecord n) : ℤ × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.LeafRecord
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey_value line 154
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey_work line 163
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey_scale line 173
Source documentation
Uniform bound for every representable key, with no record-membership or successful-trial hypothesis.
```
theorem pairKey_scale (I : Instance n) (F : IndexedMask n) (P : ℤ)
    (mode : FilteredStream.Mode) (x : LeafRecord n × LeafRecord n)
    (hn : 10000 ≤ n) :
    (pairKey I F P mode x).2 ≤ inputScale I ^ 3 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey, OAI.LowSpaceSubsetSum.inputScale
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.parent_pairKey_value line 186
Source documentation
The parent key is recovered by the semantic mask map. The sign representation is fixed once before any reader is created.
```
theorem parent_pairKey_value (D : RepresentationParentData n) (F : IndexedMask n)
    (hF : F.semantic = D.signs) (j : Fin 2) (x : LeafRecord n × LeafRecord n) :
    (pairKey D.input F D.modulus (D.pair j).mode x).1 = D.key j (pairSemantic x) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey, OAI.LowSpaceSubsetSum.RepresentationKeys.pairSemantic
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.stored_reader line 192
def OAI.LowSpaceSubsetSum.RepresentationKeys.read line 199
Source documentation
All internal tournament keys use the concrete list-mask evaluator.
```
def read (I : Instance n) (F : IndexedMask n) (P : ℤ) (mode : FilteredStream.Mode)
    (right : Array (LeafRecord n)) {d : ℕ}
    (s : MergedReader.State (fun x => (pairKey I F P mode x).1)
      (FilteredStream.view right) d) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.MergedReader.State, OAI.LowSpaceSubsetSum.RepresentationKeys.pairKey, OAI.LowSpaceSubsetSum.FilteredStream.view
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.read_value line 206
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.read_work line 216
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.read_polynomial line 229
theorem OAI.LowSpaceSubsetSum.RepresentationKeys.read_scale line 250