Repeated sampling of NW reconstruction advice -- proof internals

The exact finite repetition law and its quantitative reciprocal bound are specialized to the advice event produced by NW reconstruction averaging.

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

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

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

theorem Complexity.NWDesign.repeatedGoodReconstructionAdviceProbability_eq_one_sub_pow_internal {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

theorem Complexity.NWDesign.one_sub_pow_le_repeatedGoodReconstructionAdviceProbability_internal {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

theorem Complexity.NWDesign.half_le_repeatedGoodReconstructionAdviceProbability_internal {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

theorem Complexity.NWDesign.exists_repeatedGoodAdviceProbability_ge_of_randomTest_internal {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

theorem Complexity.NWDesign.exists_half_le_repeatedGoodAdviceProbability_of_randomTest_internal {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

theorem Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodAdvice_of_randomTest_internal {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

theorem Complexity.NWDesign.exists_repeatedGoodAdviceProbability_ge_of_seedDescriptions_internal {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

theorem Complexity.NWDesign.exists_half_le_repeatedGoodAdviceProbability_of_seedDescriptions_internal {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

theorem Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodAdvice_of_seedDescriptions_internal {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