List decoding explicit NW reconstruction programs

This layer composes checked, encoded NW reconstruction with a finite Boolean list code. Beyond producing a bounded candidate set containing the source message, it stores a selecting decoder index in ceiling-logarithmic space and materializes a program that decodes exactly to the source message. Its complete codec includes polarity, hybrid coordinate, reconstruction data, and list index, leaving only ambient parameters external. The family specialization matches inverse accuracy to reconstruction advantage and converts polynomial list size into a concrete logarithmic description bound, including the canonical choice for inverse-polynomially represented test density. The final decoder layer turns the complete encoding into a literal bitstring certificate and, for any realizing TM, a machine-relative time-bounded Kolmogorov bound. Any arbitrary machine satisfying the generic efficient-universality interface inherits that bound with additive description and polynomial clock overhead. An additional family-uniform decoder interface uses one machine for every ambient instance and exposes the exact self-delimiting cost of encoding the design and test, without conflating explicit input with oracle access. Separately, an oracle decoder realization keeps the design and code fixed but handles every finite test through its canonical membership oracle, yielding a machine-relative oracle C^{t,A} certificate with no test bits in the program. Every oracle machine satisfying the oracle-uniform efficient-universality interface inherits those bounds with constants chosen before the test oracle. A family-uniform oracle decoder goes further: one machine handles every code parameter and design, charging an explicit design encoding while retaining the test as oracle access.

@[simp]

theorem Complexity.NWDesign.IndexedReconstructionProgram.length_encodeBooleanPayload {listSize outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.IndexedReconstructionProgram listSize) : program.encodeBooleanPayload.length = design.reconstructionDataBitsAt program.reconstruction.current + BooleanListCode.decoderIndexBitWidth listSize

The flat Boolean payload of an indexed reconstruction program consists of the reconstruction data followed by exactly clog₂(listSize) index bits.

@[simp]

theorem Complexity.NWDesign.IndexedReconstructionProgram.length_encode {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

Complete indexed-program encoding accounts exactly for polarity, hybrid coordinate, reconstruction data, and list-decoder index.

theorem Complexity.NWDesign.decodeIndexedReconstructionBooleanPayload?_encode {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

The concatenated reconstruction-data and list-index encoding round-trips when polarity and hybrid coordinate are supplied as codec metadata.

@[simp]

theorem Complexity.NWDesign.decodeIndexedReconstructionProgram?_encode {listSize outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.IndexedReconstructionProgram listSize) : design.decodeIndexedReconstructionProgram? listSize program.encode = some program

Complete indexed reconstruction encoding round-trips from its ambient design and list-size parameters alone.

@[simp]

theorem Complexity.NWDesign.decodeIndexedMessage?_encode {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)) : design.decodeIndexedMessage? code test program.encode = some (program.decodedMessage code test)

Decoding and semantically evaluating a complete indexed-program bit string recovers the program's selected source message.

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.timeBoundedKolmogorovComplexity_le {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

Any bounded bitstring certificate for a realized indexed-message decoder gives the corresponding time-bounded Kolmogorov upper bound relative to that arbitrary decoder machine.

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.oracleTimeBoundedKolmogorovComplexity_le {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

A bounded indexed reconstruction certificate gives an oracle-relative time-bounded Kolmogorov upper bound when one decoder machine handles every finite test through its canonical membership oracle. The test truth table occupies no program bits.

theorem Complexity.NWDesign.OracleEncodedMessageDecoderRealization.efficientlyUniversal_transfer {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)

Every efficiently universal oracle machine inherits the decoded description bound using one compiler constant and polynomial clock shared by all finite test oracles.

theorem Complexity.NWDesign.EncodedMessageDecoderRealization.efficientlyUniversal_transfer {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)

Every efficiently universal machine inherits the decoded-description bound with the universal compiler's additive constant and an explicit polynomially larger clock. This is independent of any particular universal-machine implementation.

theorem Complexity.NWDesign.ReconstructionProgram.agreementProbability_eq_listCode {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)

Explicit-program agreement with an encoded message is exactly the generic Boolean list-code agreement statistic.

theorem Complexity.NWDesign.ReconstructionProgram.mem_listDecoderCandidates_and_card_le {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

Sufficient stored-predictor agreement puts the original source message in the decoder candidate set, whose cardinality is at most listSize.

theorem Complexity.NWDesign.ReconstructionProgram.exists_indexedProgram_of_half_add_margin {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

Sufficient agreement materializes an indexed reconstruction program that decodes exactly to the original source message. Its extra Boolean payload is exactly one ceiling-logarithmic list index.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_indexedProgram_sound {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

A checked certificate yields an indexed reconstruction program that recovers the source message and whose actual Boolean payload includes the ceiling-logarithmic decoder index.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_fullyEncodedIndexedProgram_sound {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

A checked certificate yields a complete, round-tripping indexed program that recovers the source message. Its bound accounts for polarity, hybrid coordinate, reconstruction data, and decoder-list index.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_encodedMessage_sound {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) : ∃ (description : List Bool), design.decodeIndexedMessage? code test description = some message ∧ description.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1) + BooleanListCode.decoderIndexBitWidth listSize

A checked reconstruction certificate yields an actual short bit string that the fixed semantic decoder maps to the original source message.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_listDecoding_sound {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

Any checked certificate at agreement 1/2 + margin produces a bounded flat payload and a decoder list of size at most listSize containing the original source message.

theorem Complexity.NWDesign.half_le_listDecodedReconstructionProgram_of_randomTest {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

Finite semantic core of Hirahara's list-decoded NW reconstruction: with probability at least one half, canonical checked sampling returns a bounded payload whose predictor decodes to a bounded list containing the source message.

theorem Complexity.NWDesign.half_le_indexedReconstructionProgram_of_randomTest {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

With probability at least one half, canonical checked sampling returns a certificate that extends to an indexed program decoding exactly to the source message. The actual Boolean payload pays only clog₂(listSize) bits beyond the reconstruction payload.

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_randomTest {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

With probability at least one half, canonical checked sampling yields a complete indexed encoding that round-trips and decodes exactly to the source message, with every program-specific bit explicitly charged.

theorem Complexity.NWDesign.half_le_listDecodedReconstructionProgram_of_seedDescriptions {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

The list-decoded reconstruction theorem with generator complexity discharged by direct short-seed descriptions.

theorem Complexity.NWDesign.half_le_indexedReconstructionProgram_of_seedDescriptions {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

The exact indexed-program reconstruction theorem with generator complexity discharged by direct short-seed descriptions.

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_seedDescriptions {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

The fully encoded indexed reconstruction theorem with generator complexity discharged by direct short-seed descriptions.