Repeated sampling of NW reconstruction advice

The probability of finding at least one good reconstruction advice choice in k independent trials is exactly 1 - (1 - p)^k, where p is the one-draw success probability. In particular, k * p ≥ 1 gives success probability at least one half. Combined with the NW averaging bound p ≥ δ / (2m), this is a finite, explicit form of Hirahara's O(m / δ) randomized advice search.

theorem Complexity.NWDesign.ratio_le_reconstructionAdviceTrialCount (outputLength : ℕ) (density : ℚ) : 2 * ↑outputLength / density ≤ ↑(reconstructionAdviceTrialCount outputLength density)

The canonical trial count is at least the exact ratio 2m / δ.

theorem Complexity.NWDesign.reconstructionAdviceTrialCount_lt_ratio_add_one (outputLength : ℕ) (density : ℚ) (hdensity : 0 < density) : ↑(reconstructionAdviceTrialCount outputLength density) < 2 * ↑outputLength / density + 1

For positive density, the canonical trial count is strictly below 2m / δ + 1, making its O(m / δ) cost explicit.

theorem Complexity.NWDesign.one_le_reconstructionAdviceTrialCount_mul_halfAdvantage (outputLength : ℕ) (density : ℚ) (houtputLength : 0 < outputLength) (hdensity : 0 < density) : 1 ≤ ↑(reconstructionAdviceTrialCount outputLength density) * (density / ↑outputLength / 2)

The canonical ceiling trial count meets the repetition threshold exactly needed for half-success advice search.

theorem Complexity.NWDesign.repeatedGoodReconstructionAdviceProbability_eq_one_sub_pow {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) (trials : ℕ) : design.repeatedGoodReconstructionAdviceProbability hardFunction test current agreementThreshold trials = 1 - (1 - design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold) ^ trials

Exact independent-repetition law for sampling good reconstruction advice.

theorem Complexity.NWDesign.one_sub_pow_le_repeatedGoodReconstructionAdviceProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) (trials : ℕ) (singleDrawLower : ℚ) (hlower : singleDrawLower ≤ design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold) : 1 - (1 - singleDrawLower) ^ trials ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction test current agreementThreshold trials

Any certified one-draw success lower bound lifts to the exact independent repetition lower bound.

theorem Complexity.NWDesign.half_le_repeatedGoodReconstructionAdviceProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) (trials : ℕ) (singleDrawLower : ℚ) (hlower : singleDrawLower ≤ design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold) (htrials : 1 ≤ ↑trials * singleDrawLower) : 1 / 2 ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction test current agreementThreshold trials

If trials times a one-draw success lower bound is at least one, repeated advice sampling finds a good predictor with probability at least one half.

theorem Complexity.NWDesign.exists_repeatedGoodAdviceProbability_ge_of_randomTest {outputLength inputLength seedLength tapes time threshold budget trials : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 - (1 - density / ↑outputLength / 2) ^ trials ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) trials ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

End-to-end repeated advice search from a dense random test, with the exact geometric success lower bound and the fixed predictor payload bound.

theorem Complexity.NWDesign.exists_half_le_repeatedGoodAdviceProbability_of_randomTest {outputLength inputLength seedLength tapes time threshold budget trials : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (htrials : 1 ≤ ↑trials * (density / ↑outputLength / 2)) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 / 2 ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) trials ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Hirahara's O(m / δ) advice-search step in explicit finite form: when trials * (δ / (2m)) ≥ 1, repeated sampling finds a predictor with agreement 1/2 + δ / (2m) with probability at least one half.

theorem Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodAdvice_of_randomTest {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 < density) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 / 2 ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

The canonical ceil(2m / δ) advice count finds a reconstruction predictor of agreement 1/2 + δ/(2m) with probability at least one half.

theorem Complexity.NWDesign.exists_repeatedGoodAdviceProbability_ge_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold budget trials : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 - (1 - density / ↑outputLength / 2) ^ trials ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) trials ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Exact repeated advice-search bound when generator complexity is discharged by direct short-seed descriptions.

theorem Complexity.NWDesign.exists_half_le_repeatedGoodAdviceProbability_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold budget trials : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (htrials : 1 ≤ ↑trials * (density / ↑outputLength / 2)) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 / 2 ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) trials ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Half-success repeated advice search with low complexity discharged by direct short-seed descriptions.

theorem Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodAdvice_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 < density) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), 1 / 2 ≤ design.repeatedGoodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Canonical-count half-success advice search with low complexity discharged by direct short-seed descriptions.