RepresentationChosenStreams.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The surviving representation in the executable parent streams

theorem OAI.LowSpaceSubsetSum.MaskRestriction.compatible_inter line 15
Source documentation
Restricting a compatible full mask to a leaf preserves its prefix tests.
```
theorem compatible_inter {n : ℕ} (P : MaskRestriction n)
    {M S A : Finset (Fin n)} (hA : A ⊆ M) (h : P.Compatible M S) :
    P.Compatible A (S ∩ A) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRawParent line 30
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenNamedParent line 36
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParentData line 44
Source documentation
The designated analysis task uses one of the actual normalized parent residues. The program itself receives only the primitive data of this record.
```
def chosenParentData (h : R.PrimeHistory) (r : R.Residues h.2) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (j : Fin 2) (P : ℤ) (hP : 0 < P) (C : ℕ) (restriction : MaskRestriction n) :
    RepresentationParentData n where
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RepresentationParentData
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParentData_weights line 63
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRawParent_weight line 70
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRawParent_topMask line 83
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLeaf_compatible line 93

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRawParent_eligible line 111

Source documentation

Both low-filtered children, their high-key match, and exact local validity hold for the same chosen raw parent. No array-membership premise is assumed.

theorem chosenRawParent_eligible (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (j : Fin 2) (P : ℤ) (hP : 0 < P) (C : ℕ) (restriction : MaskRestriction n)
    (hcompat : restriction.Compatible (R.orderedMixers h.1.1.1 0)
      (orientedMask (j != 0)
        (R.chosenMasks (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r 0)
        (R.selectedHalves h.1.1.1 0))) :
    (R.chosenParentData h r hn hlog j P hP C restriction).RawEligible
      (R.chosenRawParent h r hn hlog j) := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.orientedMask

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_rawEntries line 144

Source documentation

The emitted entry is the exact chosen weight/top-mask key.

theorem chosenEntry_rawEntries (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (j : Fin 2) (P : ℤ) (hP : 0 < P) (C : ℕ) (restriction : MaskRestriction n)
    (hcompat : restriction.Compatible (R.orderedMixers h.1.1.1 0)
      (orientedMask (j != 0)
        (R.chosenMasks (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r 0)
        (R.selectedHalves h.1.1.1 0))) :
    RepresentationUniverse.entry (R.signedWeights h.1.1.1) (R.chosenRawParent h r hn hlog j) ∈
      (R.chosenParentData h r hn hlog j P hP C restriction).rawEntries := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.orientedMask, OAI.LowSpaceSubsetSum.RepresentationUniverse.entry

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntries_match line 161

Source documentation

The two concrete entry keys still partition the chosen top half and sum to the signed target after raw tuple generation.

theorem chosenEntries_match (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r) :
    let e := fun j => RepresentationUniverse.entry (R.signedWeights h.1.1.1)
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.RepresentationUniverse.entry

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mixer_disjoint_rawOutside line 193
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_domains_disjoint line 203
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.raw_validEntries_bounded line 222
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParentBucket line 238
Source documentation
The actual distinct-entry bucket containing the designated representation.
```
def chosenParentBucket (h : R.PrimeHistory) (r : R.Residues h.2) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (j : Fin 2) (P : ℤ) : Finset (Entry (Fin n)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParent_rawEntries_subset line 247

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_collected line 269

Source documentation

Capacity is measured on distinct exact entries. Once this actual bucket fits, every compatible chosen witness reaches the bounded array.

theorem chosenEntry_collected (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (j : Fin 2) (P : ℤ) (hP : 0 < P) (C B : ℕ) (restriction : MaskRestriction n)
    (hcompat : restriction.Compatible (R.orderedMixers h.1.1.1 0)
      (orientedMask (j != 0)
        (R.chosenMasks (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r 0)
        (R.selectedHalves h.1.1.1 0)))
    (hcap : (R.chosenParentBucket h r hn hlog j P).card ≤ C) :
    ((R.chosenParentData h r hn hlog j P hP C restriction).collect B).state.user.keys.overflow = false ∧
    RepresentationUniverse.entry (R.signedWeights h.1.1.1) (R.chosenRawParent h r hn hlog j) ∈
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.orientedMask, OAI.collect, OAI.LowSpaceSubsetSum.RepresentationUniverse.entry