Explicit NW reconstruction programs -- proof internals #
theorem
Complexity.NWDesign.materializeReconstructionProgram_query_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(complement : Bool)
(current : Fin outputLength)
(advice : design.ReconstructionAdvice current)
(challenge : Fin inputLength → Bool)
:
(design.materializeReconstructionProgram hardFunction complement current advice).query challenge = design.reconstructionQuery hardFunction current advice.1 advice.2.1 challenge advice.2.2
theorem
Complexity.NWDesign.materializeReconstructionProgram_predictor_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(complement : Bool)
(current : Fin outputLength)
(advice : design.ReconstructionAdvice current)
:
(design.materializeReconstructionProgram hardFunction complement current advice).predictor test = design.reconstructionPredictor hardFunction (BitGenerator.orientTest test complement) current advice.1 advice.2.1
advice.2.2
theorem
Complexity.NWDesign.materializeReconstructionProgram_agreementProbability_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(complement : Bool)
(current : Fin outputLength)
(advice : design.ReconstructionAdvice current)
:
(design.materializeReconstructionProgram hardFunction complement current advice).agreementProbability hardFunction
test = design.reconstructionAgreementProbability hardFunction (BitGenerator.orientTest test complement) current advice
theorem
Complexity.NWDesign.reconstructionCertificate_toProgram_agreementProbability_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(certificate : ReconstructionCertificate outputLength seedLength)
:
(certificate.toProgram design hardFunction).agreementProbability hardFunction test = design.reconstructionTrialAgreementProbability hardFunction (BitGenerator.orientTest test certificate.complement)
certificate.trial
theorem
Complexity.NWDesign.ReconstructionProgram.booleanPayloadSize_eq_internal
{outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.ReconstructionProgram)
:
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_program_sound_internal
{outputLength inputLength seedLength trials budget : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(hbudget : design.HasOverlapBudget budget)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? hardFunction test agreementThreshold batch = some certificate)
:
agreementThreshold ≤ (certificate.toProgram design hardFunction).agreementProbability hardFunction test ∧ (certificate.toProgram design hardFunction).booleanPayloadSize ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_materializedReconstructionProgram_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)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? hardFunction test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
1 / 2 + density / ↑outputLength / 2 ≤ (certificate.toProgram design hardFunction).agreementProbability hardFunction test ∧ (certificate.toProgram design hardFunction).booleanPayloadSize ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_materializedReconstructionProgram_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)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? hardFunction test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
1 / 2 + density / ↑outputLength / 2 ≤ (certificate.toProgram design hardFunction).agreementProbability hardFunction test ∧ (certificate.toProgram design hardFunction).booleanPayloadSize ≤ budget + (seedLength - inputLength) + 1