Bit encoding of explicit NW reconstruction programs

The stored predecessor tables, outside seed, later tail, and candidate are serialized as one canonical flat bit string. A complete program encoding prefixes its polarity and a ceiling-logarithmic hybrid coordinate, leaving only the ambient design parameters external to the decoder.

theorem Complexity.NWDesign.card_reconstructionPayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : Fintype.card (design.ReconstructionPayloadIndex current) = design.reconstructionDataBitsAt current

The total payload-index type has exactly the previously derived number of Boolean reconstruction entries.

@[simp]

theorem Complexity.NWDesign.length_encodeBooleanPayload {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : program.encodeBooleanPayload.length = design.reconstructionDataBitsAt program.current

The canonical flat payload has exactly the reconstruction entry count.

theorem Complexity.NWDesign.length_encodeBooleanPayload_eq_booleanPayloadSize {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : program.encodeBooleanPayload.length = program.booleanPayloadSize

Flat payload length agrees exactly with the explicit program's semantic Boolean payload size.

@[simp]

theorem Complexity.NWDesign.ReconstructionProgram.length_encode {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : program.encode.length = 1 + Fin.bitWidth outputLength + design.reconstructionDataBitsAt program.current

A complete reconstruction-program encoding pays one polarity bit and a ceiling-logarithmic hybrid coordinate beyond its Boolean payload.

@[simp]

theorem Complexity.NWDesign.decodeReconstructionBooleanPayload?_encode {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : design.decodeReconstructionBooleanPayload? program.complement program.current program.encodeBooleanPayload = some program

Exact round trip for the reconstruction Boolean payload when its polarity and coordinate metadata are supplied.

@[simp]

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

Complete reconstruction-program encoding round-trips from the ambient design alone.

@[simp]

theorem Complexity.NWDesign.decodeReconstructionBooleanPayload?_eq_none_iff {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

Payload decoding fails exactly on strings whose length differs from the exact reconstruction entry count.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_encodedProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1

A selected certificate materializes to a predictor meeting the agreement threshold whose actual flat payload obeys the weak-design length bound.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_fullyEncodedProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)

The same checked certificate bound for the complete program encoding, including polarity and hybrid-coordinate metadata.

theorem Complexity.NWDesign.half_le_encodedReconstructionProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1

End-to-end encoded reconstruction: canonical checked sampling succeeds with probability at least one half and every selected stored predictor has agreement 1/2 + δ/(2m) and the claimed actual payload length.

theorem Complexity.NWDesign.half_le_fullyEncodedReconstructionProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)

End-to-end reconstruction with the polarity and hybrid coordinate included in every selected program's actual encoding.

theorem Complexity.NWDesign.half_le_encodedReconstructionProgram_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).encodeBooleanPayload.length ≤ budget + (seedLength - inputLength) + 1

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

theorem Complexity.NWDesign.half_le_fullyEncodedReconstructionProgram_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).encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - inputLength) + 1)

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