RepresentationPrimeTrial.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The extra-prime experiment retains actual fitting solution buckets

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.allocated_successful_with_resources line 14

Source documentation

Preserve the residue-success witness while subtracting resource failure.

theorem allocated_successful_with_resources (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) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

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

abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.ExtraTrialHistory line 49
def OAI.LowSpaceSubsetSum.RepresentationSetup.extraTrialLaw line 53
Source documentation
The prime is drawn after the earlier layout, families, nested primes, and low residues; its law depends only on the prescribed layout parameter.
```
def extraTrialLaw (hn : 100 ≤ n) : FiniteLaw R.ExtraTrialHistory :=
…
```
Mentions: OAI.LowSpaceSubsetSum.FiniteLaw
def OAI.LowSpaceSubsetSum.RepresentationSetup.PrimeBucketFits line 57

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraTrial_success_probability line 70

Source documentation

The ideal experiment now includes the actual extra-prime sampler and both dictionary-capacity events. All success factors are derived.

theorem extraTrial_success_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) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

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