List decoding explicit NW reconstruction programs -- proof internals #
theorem
Complexity.NWDesign.IndexedReconstructionProgram.length_encodeBooleanPayload_internal
{listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.IndexedReconstructionProgram listSize)
:
program.encodeBooleanPayload.length = design.reconstructionDataBitsAt program.reconstruction.current + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.IndexedReconstructionProgram.length_encode_internal
{listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.IndexedReconstructionProgram listSize)
:
program.encode.length = 1 + Fin.bitWidth outputLength + design.reconstructionDataBitsAt program.reconstruction.current + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.decodeIndexedReconstructionBooleanPayload?_encode_internal
{listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.IndexedReconstructionProgram listSize)
:
design.decodeIndexedReconstructionBooleanPayload? listSize program.reconstruction.complement
program.reconstruction.current program.encodeBooleanPayload = some program
theorem
Complexity.NWDesign.decodeIndexedReconstructionProgram?_encode_internal
{listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.IndexedReconstructionProgram listSize)
:
theorem
Complexity.NWDesign.decodeIndexedMessage?_encode_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.IndexedReconstructionProgram listSize)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.NWDesign.HasEncodedMessageCertificateWithin.timeBoundedKolmogorovComplexity_le_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{test : Finset (Fin outputLength → Bool)}
{message : Fin messageLength → Bool}
{bound : ℕ}
(realization : design.EncodedMessageDecoderRealization code test)
(hcertificate : design.HasEncodedMessageCertificateWithin code test message bound)
:
realization.machine.timeBoundedKolmogorovComplexity (List.ofFn message) (realization.time bound) ≤ ↑bound
theorem
Complexity.NWDesign.HasEncodedMessageCertificateWithin.oracleTimeBoundedKolmogorovComplexity_le_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{test : Finset (Fin outputLength → Bool)}
{message : Fin messageLength → Bool}
{bound : ℕ}
(realization : design.OracleEncodedMessageDecoderRealization code)
(hcertificate : design.HasEncodedMessageCertificateWithin code test message bound)
:
realization.machine.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message)
(realization.time bound) ≤ ↑bound
theorem
Complexity.NWDesign.OracleEncodedMessageDecoderRealization.efficientlyUniversal_transfer_internal
{messageLength listSize outputLength inputLength seedLength universalTapes : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
(realization : design.OracleEncodedMessageDecoderRealization code)
(universal : OracleTM universalTapes)
(huniversal : universal.IsEfficientlyUniversal)
:
∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ),
∀ (test : Finset (Fin outputLength → Bool)) (message : Fin messageLength → Bool) (bound : ℕ),
design.HasEncodedMessageCertificateWithin code test message bound →
universal.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message)
(coefficient * (bound + realization.time bound + 1) ^ exponent) ≤ ↑(bound + constant)
theorem
Complexity.NWDesign.EncodedMessageDecoderRealization.efficientlyUniversal_transfer_internal
{messageLength listSize outputLength inputLength seedLength universalTapes : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{test : Finset (Fin outputLength → Bool)}
(realization : design.EncodedMessageDecoderRealization code test)
(universal : TM universalTapes)
(huniversal : universal.IsEfficientlyUniversal)
:
∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ),
∀ (message : Fin messageLength → Bool) (bound : ℕ),
design.HasEncodedMessageCertificateWithin code test message bound →
universal.timeBoundedKolmogorovComplexity (List.ofFn message)
(coefficient * (bound + realization.time bound + 1) ^ exponent) ≤ ↑(bound + constant)
theorem
Complexity.NWDesign.ReconstructionProgram.agreementProbability_eq_listCode_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.ReconstructionProgram)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
:
program.agreementProbability (code.encode message) test = BooleanListCode.agreementProbability (code.encode message) (program.predictor test)
theorem
Complexity.NWDesign.ReconstructionProgram.mem_listDecoderCandidates_and_card_le_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.ReconstructionProgram)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hagreement : 1 / 2 + margin ≤ program.agreementProbability (code.encode message) test)
:
message ∈ program.listDecoderCandidates code test ∧ (program.listDecoderCandidates code test).card ≤ listSize
theorem
Complexity.NWDesign.ReconstructionProgram.exists_indexedProgram_of_half_add_margin_internal
{messageLength listSize outputLength inputLength seedLength : ℕ}
{design : NWDesign outputLength inputLength seedLength}
(program : design.ReconstructionProgram)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hagreement : 1 / 2 + margin ≤ program.agreementProbability (code.encode message) test)
:
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = program ∧ indexed.decodedMessage code test = message ∧ indexed.encodeBooleanPayload.length = program.encodeBooleanPayload.length + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_indexedProgram_sound_internal
{messageLength listSize outputLength inputLength seedLength trials budget : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hbudget : design.HasOverlapBudget budget)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + margin) batch = some certificate)
:
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1 + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_fullyEncodedIndexedProgram_sound_internal
{messageLength listSize outputLength inputLength seedLength trials budget : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hbudget : design.HasOverlapBudget budget)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + margin) batch = some certificate)
:
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1) + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_encodedMessage_sound_internal
{messageLength listSize outputLength inputLength seedLength trials budget : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hbudget : design.HasOverlapBudget budget)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + margin) batch = some certificate)
:
theorem
Complexity.NWDesign.findGoodReconstructionCertificate_listDecoding_sound_internal
{messageLength listSize outputLength inputLength seedLength trials budget : ℕ}
(design : NWDesign outputLength inputLength seedLength)
(code : BooleanListCode messageLength listSize (Fin inputLength → Bool))
(message : Fin messageLength → Bool)
(test : Finset (Fin outputLength → Bool))
(margin : ℚ)
(hcode : code.IsListDecodableAt (1 / 2 - margin))
(hbudget : design.HasOverlapBudget budget)
(batch : Fin trials → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength)
(hfind : design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + margin) batch = some certificate)
:
message ∈ (certificate.toProgram design (code.encode message)).listDecoderCandidates code test ∧ ((certificate.toProgram design (code.encode message)).listDecoderCandidates code test).card ≤ listSize ∧ (certificate.toProgram design (code.encode message)).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_listDecodedReconstructionProgram_of_randomTest_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hlow : (design.generator (code.encode message)).HasLowTimeBoundedComplexity machine time threshold)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
message ∈ (certificate.toProgram design (code.encode message)).listDecoderCandidates code test ∧ ((certificate.toProgram design (code.encode message)).listDecoderCandidates code test).card ≤ listSize ∧ (certificate.toProgram design (code.encode message)).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_indexedReconstructionProgram_of_randomTest_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hlow : (design.generator (code.encode message)).HasLowTimeBoundedComplexity machine time threshold)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1 + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_randomTest_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hlow : (design.generator (code.encode message)).HasLowTimeBoundedComplexity machine time threshold)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1) + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.half_le_listDecodedReconstructionProgram_of_seedDescriptions_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hseedLength : seedLength < threshold)
(hproduces :
∀ (seed : Fin seedLength → Bool),
machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator (code.encode message) seed)) time)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
message ∈ (certificate.toProgram design (code.encode message)).listDecoderCandidates code test ∧ ((certificate.toProgram design (code.encode message)).listDecoderCandidates code test).card ≤ listSize ∧ (certificate.toProgram design (code.encode message)).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1
theorem
Complexity.NWDesign.half_le_indexedReconstructionProgram_of_seedDescriptions_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hseedLength : seedLength < threshold)
(hproduces :
∀ (seed : Fin seedLength → Bool),
machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator (code.encode message) seed)) time)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1 + BooleanListCode.decoderIndexBitWidth listSize
theorem
Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_seedDescriptions_internal
{messageLength listSize outputLength inputLength seedLength tapes time threshold budget : ℕ}
{design : NWDesign outputLength inputLength seedLength}
{code : BooleanListCode messageLength listSize (Fin inputLength → Bool)}
{message : Fin messageLength → Bool}
{machine : TM tapes}
{test : Finset (Fin outputLength → Bool)}
{density : ℚ}
(houtputLength : 0 < outputLength)
(hdensity : 0 < density)
(hcode : code.IsListDecodableAt (1 / 2 - density / ↑outputLength / 2))
(hseedLength : seedLength < threshold)
(hproduces :
∀ (seed : Fin seedLength → Bool),
machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator (code.encode message) seed)) time)
(hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold)
(hdense : BitGenerator.IsDenseTest test density)
(hbudget : design.HasOverlapBudget budget)
:
1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability (code.encode message) test (1 / 2 + density / ↑outputLength / 2)
(reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength)
(certificate : ReconstructionCertificate outputLength seedLength),
design.findGoodReconstructionCertificate? (code.encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate →
∃ (indexed : design.IndexedReconstructionProgram listSize),
indexed.reconstruction = certificate.toProgram design (code.encode message) ∧ indexed.decodedMessage code test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1) + BooleanListCode.decoderIndexBitWidth listSize