Explicit NW reconstruction programs

Checked finite certificates can be materialized into reconstruction programs that store every predecessor table used by their predictor. Program evaluation therefore has no hard-function oracle; the hard function is used only while materializing and subsequently scoring the stored predictor. The encoding submodule flattens every stored Boolean field into a canonical bit string with an exact decoder and length theorem, then prefixes the polarity and hybrid coordinate to obtain a complete program-specific encoding. The list-decoding submodule turns agreement with an encoded source message into a fully encoded indexed program that decodes exactly to that message, paying only a ceiling-logarithmic list-index cost beyond reconstruction. Its family layer instantiates the result at inverse accuracy q and exposes the exact semantic, polynomial-parameter, and uniform-machine obligations on the code family. A complete bitstring decoder and its realization interface expose the resulting machine-relative time-bounded Kolmogorov certificate, together with its generic transfer to any efficiently universal machine.

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

Materializing predecessor tables preserves the original reconstruction query pointwise.

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

The explicit program's oracle-free evaluator computes exactly the fixed-advice reconstruction predictor from which it was materialized.

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

Materializing a reconstruction predictor preserves its exact agreement probability with the hard function.

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

Materializing a checked certificate preserves its global-trial agreement statistic exactly.

theorem Complexity.NWDesign.ReconstructionProgram.booleanPayloadSize_eq {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : program.booleanPayloadSize = design.reconstructionDataBitsAt program.current

The Boolean fields in an explicit program have exactly the previously derived non-codec reconstruction payload size.

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

A selected certificate materializes to an oracle-free predictor meeting the checked agreement threshold and the weak-design Boolean payload bound.

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

End-to-end explicit reconstruction: with probability at least one half, canonical checked sampling finds a stored, oracle-free predictor of agreement 1/2 + δ/(2m) and weak-design-bounded Boolean payload.

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

The explicit reconstruction theorem with low generator complexity discharged by direct short-seed descriptions.