RepresentationDomainSoundness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

One-sided soundness of the arbitrary-input representation runtime

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_background_subset_outside line 15
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_background_color line 24
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_background_sides_disjoint line 34
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.raw_parentDomain_shared line 46
Source documentation
Only top-domain indices can be shared by the left and right parents.
```
theorem raw_parentDomain_shared (z : Layout n) (g : Guesses n)
    (f : R.Partitions z) (B : Fin n → Fin 2 × Fin 4) :
    RepresentationUniverse.parentDomain (R.rawLeaf z g f B 0) ∩
      RepresentationUniverse.parentDomain (R.rawLeaf z g f B 1) ⊆
        R.orderedMixers z 0 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.RepresentationUniverse.parentDomain
theorem OAI.LowSpaceSubsetSum.representation_capacity_pair_le line 74

theorem OAI.LowSpaceSubsetSum.RepresentationData.trial_sound line 95

Source documentation

Every accepting random history yields an indexed solution, for an arbitrary input and without any survival, resource or sampling assumptions.

theorem trial_sound (h : D.zeroSetup.PrimeHistory) (r : D.zeroSetup.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (q : ℕ) (hq : 0 < q) (B : ℕ)
    (families : Fin 4 → Array (Finset (Fin (2 * RepresentationSetup.blockHalf n 0))))
    (hyes : D.trial h r hn hlog q hq B families = true) : Solvable D.input := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf, OAI.LowSpaceSubsetSum.Solvable