Canonical encodings of Nisan--Wigderson designs -- proof internals

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

theorem Complexity.NWDesign.decodeCoordinate?_encode_internal {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)

theorem Complexity.NWDesign.decodedCoordinates_encode_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hvalid : ∀ (output : Fin outputLength) (input : Fin inputLength), (decodeCoordinate? outputLength inputLength seedLength design.encode output input).isSome = true) (output : Fin outputLength) (input : Fin inputLength) : decodedCoordinates outputLength inputLength seedLength design.encode hvalid output input = (design.coordinates output) input

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

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

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

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

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

theorem Complexity.NWDesign.DecoderInstance.length_encode_internal (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

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

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

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