List decoding explicit NW reconstruction programs -- definitions

An explicit reconstruction program approximating an encoded message can be fed directly to the code's list decoder. Besides the finite candidate set, this module defines the complete bitstring decoder, bounded decoded certificates, and the machine-realization interface used to obtain a machine-relative time-bounded Kolmogorov bound.

structure Complexity.NWDesign.IndexedReconstructionProgram {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (listSize : ℕ) : Type

An explicit NW reconstruction program together with one indexed output of a list decoder.

• reconstruction : design.ReconstructionProgram

  The oracle-free Boolean predictor materialized from reconstruction advice.

• decoderIndex : Fin listSize

  Which one of the list decoder's indexed outputs to select.

def Complexity.NWDesign.IndexedReconstructionProgram.decodedMessage {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)) : Fin messageLength → Bool

Source message selected by an indexed reconstruction program.

Equations

• program.decodedMessage code test = code.decode (program.reconstruction.predictor test) program.decoderIndex

def Complexity.NWDesign.IndexedReconstructionProgram.encodeBooleanPayload {listSize outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.IndexedReconstructionProgram listSize) : List Bool

Flat Boolean data stored by an indexed reconstruction program. The polarity and hybrid coordinate remain external codec metadata.

Equations

• program.encodeBooleanPayload = program.reconstruction.encodeBooleanPayload ++ Complexity.BooleanListCode.encodeDecoderIndex program.decoderIndex

def Complexity.NWDesign.IndexedReconstructionProgram.encode {listSize outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.IndexedReconstructionProgram listSize) : List Bool

Complete encoding of an indexed reconstruction program: polarity, hybrid coordinate, reconstruction data, and list-decoder index. Only ambient parameters remain external.

Equations

• program.encode = program.reconstruction.complement :: program.reconstruction.current.toBits ++ program.encodeBooleanPayload

def Complexity.NWDesign.decodeIndexedReconstructionBooleanPayload? {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (listSize : ℕ) (complement : Bool) (current : Fin outputLength) (bits : List Bool) : Option (design.IndexedReconstructionProgram listSize)

Decode the Boolean payload of an indexed reconstruction program using an externally supplied polarity and hybrid coordinate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NWDesign.decodeIndexedReconstructionProgram? {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (listSize : ℕ) (bits : List Bool) : Option (design.IndexedReconstructionProgram listSize)

Decode a complete indexed reconstruction program relative to its ambient design and list-size parameters.

Equations

• One or more equations did not get rendered due to their size.
• design.decodeIndexedReconstructionProgram? listSize [] = none

def Complexity.NWDesign.decodeIndexedMessage? {messageLength listSize outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (code : BooleanListCode messageLength listSize (Fin inputLength → Bool)) (test : Finset (Fin outputLength → Bool)) (bits : List Bool) : Option (Fin messageLength → Bool)

Decode a complete indexed-program bit string and run its semantic source message decoder. The ambient design, list code, and statistical test are fixed parameters rather than hidden program fields.

Equations

• design.decodeIndexedMessage? code test bits = match design.decodeIndexedReconstructionProgram? listSize bits with | some program => some (program.decodedMessage code test) | none => none

def Complexity.NWDesign.HasEncodedMessageCertificateWithin {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 : ℕ) : Prop

A literal bitstring description, bounded in length, that the fixed indexed reconstruction decoder maps to a source message.

Equations

• design.HasEncodedMessageCertificateWithin code test message bound = ∃ (description : List Bool), design.decodeIndexedMessage? code test description = some message ∧ description.length ≤ bound

structure Complexity.NWDesign.EncodedMessageDecoderRealization {messageLength listSize outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (code : BooleanListCode messageLength listSize (Fin inputLength → Bool)) (test : Finset (Fin outputLength → Bool)) : Type 1

A deterministic machine realizing the fixed indexed-message decoder. The clock depends on description length and is monotone so a length bound yields a single common time budget.

• tapes : ℕ

  Number of work tapes used by the decoder machine.

• machine : TM self.tapes

  Machine interpreting complete indexed reconstruction descriptions.

• time : ℕ → ℕ

  Decoder time as a function of description length.

• time_mono : Monotone self.time

  Larger descriptions receive no smaller clock.

• correct (description : List Bool) (message : Fin messageLength → Bool) : design.decodeIndexedMessage? code test description = some message → self.machine.ProducesInTime description (List.ofFn message) (self.time description.length)

  Every semantically decoded message is produced by the machine within the advertised clock.

structure Complexity.NWDesign.OracleEncodedMessageDecoderRealization {messageLength listSize outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (code : BooleanListCode messageLength listSize (Fin inputLength → Bool)) : Type 1

One oracle machine realizing the indexed-message decoder for every finite statistical test. The design and list code remain fixed machine parameters, but the test is supplied through its canonical Boolean oracle and therefore does not occupy program bits.

• tapes : ℕ

  Number of ordinary work tapes used in addition to the query tape.

• machine : OracleTM self.tapes

  Oracle machine interpreting complete indexed reconstruction programs.

• time : ℕ → ℕ

  Decoder time as a function of program length.

• time_mono : Monotone self.time

  Larger descriptions receive no smaller clock.

• correct (test : Finset (Fin outputLength → Bool)) (description : List Bool) (message : Fin messageLength → Bool) : design.decodeIndexedMessage? code test description = some message → self.machine.ProducesInTime (finiteTestOracle test) description (List.ofFn message) (self.time description.length)

  Correctness for every finite test supplied through finiteTestOracle.

def Complexity.NWDesign.ReconstructionProgram.listDecoderCandidates {messageLength listSize outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) (code : BooleanListCode messageLength listSize (Fin inputLength → Bool)) (test : Finset (Fin outputLength → Bool)) : Finset (Fin messageLength → Bool)

Candidate source messages obtained by list decoding the Boolean predictor stored in an explicit reconstruction program.

Equations

• program.listDecoderCandidates code test = code.candidates (program.predictor test)