Uniform families of finite Boolean list codes

This layer states the semantic, parameter-size, and uniform machine obligations of the efficiently list-decodable code used in Hirahara's reconstruction. It also turns inverse-accuracy agreement into an actual fixed-width decoder index.

@[simp]

theorem Complexity.BooleanListCodeFamily.length_truthTableBits {coordinateLength : ℕ} (word : (Fin coordinateLength → Bool) → Bool) : (truthTableBits word).length = 2 ^ coordinateLength

A Boolean-cube truth table has exactly 2^coordinateLength bits.

@[simp]

theorem Complexity.BooleanListCodeFamily.length_encoderOutput (family : BooleanListCodeFamily) (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : (family.encoderOutput messageLength inverseAccuracy message).length = 2 ^ family.coordinateLength messageLength inverseAccuracy

A family encoder emits the complete truth table of its codeword.

@[simp]

theorem Complexity.BooleanListCodeFamily.length_decoderOutput (family : BooleanListCodeFamily) (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : (family.decoderOutput messageLength inverseAccuracy received).length = family.listSize messageLength inverseAccuracy * messageLength

The full decoder output concatenates exactly listSize messages of the original message length.

theorem Complexity.BooleanListCodeFamily.exists_indexBits_of_half_add_inverseAccuracy (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) {messageLength inverseAccuracy : ℕ} (haccuracy : 2 ≤ inverseAccuracy) (message : Fin messageLength → Bool) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) (hagreement : 1 / 2 + 1 / ↑inverseAccuracy ≤ BooleanListCode.agreementProbability ((family.code messageLength inverseAccuracy).encode message) received) : ∃ (bits : List Bool), bits.length = BooleanListCode.decoderIndexBitWidth (family.listSize messageLength inverseAccuracy) ∧ (family.code messageLength inverseAccuracy).decodeAtIndexBits? received bits = some message

Inverse-accuracy list decoding turns 1/2 + 1/q agreement into a real fixed-width string selecting the original message.

theorem Complexity.BooleanListCodeFamily.decoderIndexBitWidth_le_polynomialBound {family : BooleanListCodeFamily} (bounds : family.PolynomialParameterBounds) (messageLength inverseAccuracy : ℕ) : BooleanListCode.decoderIndexBitWidth (family.listSize messageLength inverseAccuracy) ≤ Nat.clog 2 (bounds.listConstant * (inverseAccuracy + 1) ^ bounds.listDegree)

Polynomial list size gives a concrete ceiling-logarithmic upper bound on the selecting decoder-index width.

theorem Complexity.BooleanListCodeFamily.length_encoderOutput_le {family : BooleanListCodeFamily} (bounds : family.PolynomialParameterBounds) (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : (family.encoderOutput messageLength inverseAccuracy message).length ≤ bounds.codewordConstant * (messageLength + inverseAccuracy + 1) ^ bounds.codewordDegree

Polynomial parameter bounds control the actual encoder output string.

theorem Complexity.BooleanListCodeFamily.length_decoderOutput_le {family : BooleanListCodeFamily} (bounds : family.PolynomialParameterBounds) (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : (family.decoderOutput messageLength inverseAccuracy received).length ≤ bounds.listConstant * (inverseAccuracy + 1) ^ bounds.listDegree * messageLength

Polynomial list-size bounds control the actual concatenated decoder output.

theorem Complexity.BooleanListCodeFamily.UniformPolynomialTimeRealization.encoder_spec {family : BooleanListCodeFamily} (realization : family.UniformPolynomialTimeRealization) (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : realization.encoderMachine.ProducesInTime (encoderInput messageLength inverseAccuracy message) (family.encoderOutput messageLength inverseAccuracy message) (realization.encoderTime messageLength inverseAccuracy) ∧ realization.encoderTime messageLength inverseAccuracy ≤ realization.timeConstant * (messageLength + inverseAccuracy + 1) ^ realization.timeDegree

The uniform encoder machine produces the exact family codeword within its advertised common polynomial bound.

theorem Complexity.BooleanListCodeFamily.UniformPolynomialTimeRealization.decoder_spec {family : BooleanListCodeFamily} (realization : family.UniformPolynomialTimeRealization) (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : realization.decoderMachine.ProducesInTime (family.decoderInput messageLength inverseAccuracy received) (family.decoderOutput messageLength inverseAccuracy received) (realization.decoderTime messageLength inverseAccuracy) ∧ realization.decoderTime messageLength inverseAccuracy ≤ realization.timeConstant * (messageLength + inverseAccuracy + 1) ^ realization.timeDegree

The single uniform decoder machine emits the exact concatenated candidate list within the same kind of polynomial bound.