Executable NW reconstruction certificate search -- proof internals #
theorem
Complexity.NWDesign.reconstructionCertificatePasses_eq_true_iff_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(certificate : ReconstructionCertificate outputLength seedLength)
:
design.reconstructionCertificatePasses hardFunction test agreementThreshold certificate = true ↔ design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate
theorem
Complexity.NWDesign.checkReconstructionTrial_isSome_iff_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(trial : ReconstructionTrial outputLength seedLength)
:
(design.checkReconstructionTrial? hardFunction test agreementThreshold trial).isSome = true ↔ ∃ (complement : Bool),
design.IsGoodReconstructionCertificate hardFunction test agreementThreshold
{ complement := complement, trial := trial }
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_isSome_iff_internal
{outputLength inputLength seedLength trials : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
:
(design.findGoodReconstructionCertificate? hardFunction test agreementThreshold batch).isSome = true ↔ ∃ (index : Fin trials) (complement : Bool),
design.IsGoodReconstructionCertificate hardFunction test agreementThreshold
{ complement := complement, trial := batch index }
theorem
Complexity.NWDesign.checkReconstructionTrial_sound_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(trial : ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hcheck : design.checkReconstructionTrial? hardFunction test agreementThreshold trial = some certificate)
:
design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate ∧ certificate.trial = trial
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_sound_internal
{outputLength inputLength seedLength trials : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(agreementThreshold : ℚ)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? hardFunction test agreementThreshold batch = some certificate)
:
design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate ∧ ∃ (index : Fin trials), certificate.trial = batch index
theorem
Complexity.NWDesign.repeatedGoodReconstructionTrialProbability_le_checked_internal
{outputLength inputLength seedLength : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(hardFunction : (Fin inputLength → Bool) → Bool)
(test : Finset (Fin outputLength → Bool))
(complement : Bool)
(agreementThreshold : ℚ)
(trials : ℕ)
:
design.repeatedGoodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement)
agreementThreshold trials ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test agreementThreshold trials
theorem
Complexity.NWDesign.half_le_checkedReconstructionBatch_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 →
design.reconstructionDataBitsAt certificate.trial.1 ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_checkedReconstructionBatch_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 →
design.reconstructionDataBitsAt certificate.trial.1 ≤ budget + (seedLength - inputLength) + 1