Globally sampling NW reconstruction coordinates and advice -- proof internals #
theorem
Complexity.NWDesign.goodRawAdviceProbability_eq_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(current : Fin outputLength)
(agreementThreshold : ℚ)
:
uniformProbability
{raw : RawReconstructionAdvice outputLength seedLength |
agreementThreshold ≤ design.reconstructionAgreementProbability hardFunction test current
(design.reconstructionAdviceOfRaw current raw)} = design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold
theorem
Complexity.NWDesign.goodReconstructionTrialProbability_eq_average_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(houtputLength : 0 < outputLength)
:
design.goodReconstructionTrialProbability hardFunction test agreementThreshold = (∑ current : Fin outputLength,
design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold) / ↑outputLength
theorem
Complexity.NWDesign.exists_orientation_sum_averageReconstructionAgreement_ge_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(advantage : ℚ)
(hadvantage : advantage ≤ (design.generator hardFunction).distinguishingAdvantage test)
:
∃ (complement : Bool),
↑outputLength / 2 + advantage ≤ ∑ current : Fin outputLength,
design.averageReconstructionAgreement hardFunction (BitGenerator.orientTest test complement) current
theorem
Complexity.NWDesign.exists_orientation_goodReconstructionTrialProbability_ge_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(density : ℚ)
(houtputLength : 0 < outputLength)
(hdensity : 0 ≤ density)
(hdensityLeOne : density ≤ 1)
(hadvantage : density ≤ (design.generator hardFunction).distinguishingAdvantage test)
:
∃ (complement : Bool),
density / ↑outputLength / 2 ≤ design.goodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement)
(1 / 2 + density / ↑outputLength / 2)
theorem
Complexity.NWDesign.repeatedGoodReconstructionTrialProbability_eq_one_sub_pow_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(trials : ℕ)
(houtputLength : 0 < outputLength)
:
design.repeatedGoodReconstructionTrialProbability hardFunction test agreementThreshold trials = 1 - (1 - design.goodReconstructionTrialProbability hardFunction test agreementThreshold) ^ trials
theorem
Complexity.NWDesign.exists_goodReconstructionTrialProbability_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),
density / ↑outputLength / 2 ≤ design.goodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement)
(1 / 2 + density / ↑outputLength / 2) ∧ ∀ (trial : ReconstructionTrial outputLength seedLength),
design.reconstructionDataBitsAt trial.1 ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodTrial_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),
1 / 2 ≤ design.repeatedGoodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement)
(1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (trial : ReconstructionTrial outputLength seedLength),
design.reconstructionDataBitsAt trial.1 ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.exists_half_le_canonicalRepeatedGoodTrial_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),
1 / 2 ≤ design.repeatedGoodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement)
(1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (trial : ReconstructionTrial outputLength seedLength),
design.reconstructionDataBitsAt trial.1 ≤ budget + (seedLength - inputLength) + 1