RepresentationRuntimeAcceptance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual-target acceptance under the input-only bounded sampling law

def OAI.LowSpaceSubsetSum.RepresentationData.sampledTrial line 18
Source documentation
The zero-target wrapper supplies only sampling spaces. The execution uses D.input, including its original target.
```
def sampledTrial (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (B : ℕ) (h : D.zeroSetup.BucketTrialHistory (by omega)) : Bool :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_sampledTrial_eq line 30
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_sampledTrial_accepts line 39

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bounded_runtime_acceptance_probability line 49

Source documentation

The executable sampled trial uses the original target, under the actual input-only bounded sampler. The fixed solution appears only in this proof.

theorem bounded_runtime_acceptance_probability (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize))
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) (B : ℕ) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.representation_log_budget