Averaging NW reconstruction to fixed advice -- proof internals #
theorem
Complexity.NWDesign.predictionSuccessProbability_eq_averageReconstructionAgreement_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
:
NextBitPrediction.successProbability ((design.generator hardFunction).targetBit current)
((design.generator hardFunction).testAtCandidate test current) = design.averageReconstructionAgreement hardFunction test current
theorem
Complexity.NWDesign.exists_reconstructionAdvice_agreement_ge_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
:
∃ (advice : design.ReconstructionAdvice current),
NextBitPrediction.successProbability ((design.generator hardFunction).targetBit current)
((design.generator hardFunction).testAtCandidate test current) ≤ design.reconstructionAgreementProbability hardFunction test current advice
theorem
Complexity.NWDesign.averageReconstructionAgreement_eq_uniformMean_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
:
design.averageReconstructionAgreement hardFunction test current = uniformMean fun (advice : design.ReconstructionAdvice current) =>
design.reconstructionAgreementProbability hardFunction test current advice
theorem
Complexity.NWDesign.average_sub_div_le_goodReconstructionAdviceProbability_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
(agreementThreshold : ℚ)
(hthreshold : agreementThreshold < 1)
:
(design.averageReconstructionAgreement hardFunction test current - agreementThreshold) / (1 - agreementThreshold) ≤ design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold
theorem
Complexity.NWDesign.half_advantage_le_goodReconstructionAdviceProbability_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
(advantage : ℚ)
(hadvantage : 0 ≤ advantage)
(haverage : 1 / 2 + advantage ≤ design.averageReconstructionAgreement hardFunction test current)
:
advantage / 2 ≤ design.goodReconstructionAdviceProbability hardFunction test current (1 / 2 + advantage / 2)
theorem
Complexity.NWDesign.exists_fixed_reconstruction_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)
(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) (advice : design.ReconstructionAdvice current),
1 / 2 + density / ↑outputLength ≤ design.reconstructionAgreementProbability hardFunction (BitGenerator.orientTest test complement) current advice ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.exists_fixed_reconstruction_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)
(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) (advice : design.ReconstructionAdvice current),
1 / 2 + density / ↑outputLength ≤ design.reconstructionAgreementProbability hardFunction (BitGenerator.orientTest test complement) current advice ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.exists_goodAdviceProbability_ge_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),
density / ↑outputLength / 2 ≤ design.goodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current
(1 / 2 + density / ↑outputLength / 2) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.exists_goodAdviceProbability_ge_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),
density / ↑outputLength / 2 ≤ design.goodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current
(1 / 2 + density / ↑outputLength / 2) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1