ParentPrefixSearch.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual depth-first right-parent prefix recomputation

def OAI.LowSpaceSubsetSum.MaskRestriction.force line 15
def OAI.LowSpaceSubsetSum.MaskRestriction.follow line 19
theorem OAI.LowSpaceSubsetSum.MaskRestriction.force_compatible line 22
def OAI.LowSpaceSubsetSum.RepresentationParentData.searchRight line 49
Source documentation
Each task regenerates its restricted leaves and streams. An overflowing full prefix is dropped; a completed array is passed to the actual checker. The first YES returns immediately.
```
def searchRight (B : ℕ) (check : Array (Entry (Fin n)) → Bool) :
    List (Fin n) → MaskRestriction n → Bool
  | order, P =>
    let task := { D with maskRestriction := P }
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.MaskRestriction
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.searchRight_sound line 62
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.searchRight_complete line 82
Source documentation
A fitting task at the end of a designated mask path suffices. Earlier completion reaches the checker; earlier YES also returns immediately.
```
theorem searchRight_complete (B : ℕ) (check : Array (Entry (Fin n)) → Bool)
    (domain S : Finset (Fin n))
    (hfind : ∀ P, P.Compatible domain S →
      ({ D with maskRestriction := P }.collect B).state.user.keys.overflow = false →
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.RepresentationParentData.collect

theorem OAI.LowSpaceSubsetSum.RepresentationParentData.searchRight_subset_sum_sound line 112

Source documentation

No prefix task can introduce a false YES. This applies to every family outcome and every overflow pattern, rather than just the surviving bucket.

theorem searchRight_subset_sum_sound {g : ℕ} (B : ℕ) (C : TopCoordinates n g)
    (families : Fin 4 → Array (Finset (Fin g))) (left : Array (Entry (Fin n)))
    (order : List (Fin n)) (P : MaskRestriction n) (leftDomain : Finset (Fin n))
    (htop : RepresentationUniverse.topDomain D.leaves = C.domain)
    (htl : Disjoint (RepresentationUniverse.topDomain D.leaves)
      (RepresentationUniverse.mixerDomain D.leaves))
    (htb : Disjoint (RepresentationUniverse.topDomain D.leaves)
      (RepresentationUniverse.backgroundDomain D.leaves))
    (hlb : Disjoint (RepresentationUniverse.mixerDomain D.leaves)
      (RepresentationUniverse.backgroundDomain D.leaves))
    (hshared : leftDomain ∩ RepresentationUniverse.parentDomain D.leaves ⊆ C.domain)
    (hleft : ∀ e ∈ left.toList, Represents D.weights leftDomain C.domain e)
…

Mentions: OAI.LowSpaceSubsetSum.TopCoordinates, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.parentDomain, OAI.LowSpaceSubsetSum.Represents