Canonical codec for Nisan--Wigderson designs

The complete ordered coordinate table is encoded injectively using exactly outputLength * inputLength * clog_2(seedLength) bits. The executable decoder rejects malformed lengths, out-of-range coordinates, and noninjective blocks, round-trips every valid design, and accepts only that design's canonical encoding. A nested self-delimiting wrapper also records all numeric parameters needed by one uniform list-decoder invocation.

@[simp]

theorem Complexity.NWDesign.length_encode {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) : design.encode.length = outputLength * inputLength * Fin.bitWidth seedLength

Canonical NW-design encoding has the exact rectangular coordinate-table length.

theorem Complexity.NWDesign.encode_injective {outputLength inputLength seedLength : ℕ} : Function.Injective encode

Canonical NW-design encoding is injective.

@[simp]

theorem Complexity.NWDesign.decodeCoordinate?_encode {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (input : Fin inputLength) : decodeCoordinate? outputLength inputLength seedLength design.encode output input = some ((design.coordinates output) input)

Decoding one coordinate from an encoded design recovers it exactly.

@[simp]

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

The canonical NW-design decoder round-trips every valid design.

theorem Complexity.NWDesign.decode?_eq_none_of_length_ne (outputLength inputLength seedLength : ℕ) (bits : List Bool) (hlength : bits.length ≠ outputLength * inputLength * Fin.bitWidth seedLength) : decode? outputLength inputLength seedLength bits = none

The decoder rejects every string whose total length is malformed, including when the design has no output or input coordinates.

theorem Complexity.NWDesign.decode?_eq_some_iff {outputLength inputLength seedLength : ℕ} (bits : List Bool) (design : NWDesign outputLength inputLength seedLength) : decode? outputLength inputLength seedLength bits = some design ↔ bits = design.encode

Decoding yields a given design exactly on its canonical encoding.

@[simp]

theorem Complexity.NWDesign.DecoderInstance.length_encode (data : DecoderInstance) : data.encode.length = 2 * (data.messageLength.size + data.inverseAccuracy.size + data.outputLength.size + data.inputLength.size + data.seedLength.size) + 10 + data.outputLength * data.inputLength * Fin.bitWidth data.seedLength

A self-describing decoder instance has the exact cost of five framed minimal binary parameters followed by the raw coordinate table.

@[simp]

theorem Complexity.NWDesign.DecoderInstance.decode?_encode (data : DecoderInstance) : decode? data.encode = some data

The self-describing instance decoder round-trips every valid instance.

theorem Complexity.NWDesign.DecoderInstance.decode?_eq_some_iff (bits : List Bool) (data : DecoderInstance) : decode? bits = some data ↔ bits = data.encode

Parsing yields a given self-describing instance exactly on its canonical encoding.

theorem Complexity.NWDesign.DecoderInstance.encode_injective : Function.Injective encode

Self-describing decoder-instance encoding is injective.