Documentation

Complexitylib.Metacomplexity.NisanWigderson.Reconstruction.Program.Encoding.Internal

Bit encoding of explicit NW reconstruction programs -- proof internals #

source
theorem Complexity.NWDesign.card_reconstructionPayloadIndex_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :
Fintype.card (design.ReconstructionPayloadIndex current) = design.reconstructionDataBitsAt current
source
theorem Complexity.NWDesign.length_encodeBooleanPayload_internal {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
program.encodeBooleanPayload.length = design.reconstructionDataBitsAt program.current
source
theorem Complexity.NWDesign.length_encodeBooleanPayload_eq_booleanPayloadSize_internal {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
program.encodeBooleanPayload.length = program.booleanPayloadSize
source
theorem Complexity.NWDesign.ReconstructionProgram.length_encode_internal {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
program.encode.length = 1 + Fin.bitWidth outputLength + design.reconstructionDataBitsAt program.current
source
theorem Complexity.NWDesign.decodeReconstructionBooleanPayload?_encode_internal {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
design.decodeReconstructionBooleanPayload? program.complement program.current program.encodeBooleanPayload = some program
source
theorem Complexity.NWDesign.decodeReconstructionProgram?_encode_internal {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
design.decodeReconstructionProgram? program.encode = some program
source
theorem Complexity.NWDesign.decodeReconstructionBooleanPayload?_eq_none_iff_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (complement : Bool) (current : Fin outputLength) (bits : List Bool) :
design.decodeReconstructionBooleanPayload? complement current bits = none ↔ bits.length ≠ design.reconstructionDataBitsAt current
source
theorem Complexity.NWDesign.findGoodReconstructionCertificate_encodedProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
source
theorem Complexity.NWDesign.findGoodReconstructionCertificate_fullyEncodedProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)
source
theorem Complexity.NWDesign.half_le_encodedReconstructionProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
source
theorem Complexity.NWDesign.half_le_fullyEncodedReconstructionProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)
source
theorem Complexity.NWDesign.half_le_encodedReconstructionProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
source
theorem Complexity.NWDesign.half_le_fullyEncodedReconstructionProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)