Uniform families of finite Boolean list codes -- definitions

Hirahara's reconstruction needs more than a single semantic code. The code is indexed by message length and inverse accuracy, its truth-table length and decoder list size obey polynomial bounds, and one uniform machine computes each encoder or full decoder across every parameter choice.

This definitions layer keeps those three obligations separate so an explicit algebraic construction can discharge them independently.

structure Complexity.BooleanListCodeFamily : Type

A family of Boolean list codes indexed by message length and inverse accuracy. Codeword coordinates are Boolean strings of a family-specified length.

• coordinateLength : ℕ → ℕ → ℕ

  Number of input bits addressing one codeword coordinate.

• listSize : ℕ → ℕ → ℕ

  Number of indexed candidates returned by the decoder.

• code (messageLength inverseAccuracy : ℕ) : BooleanListCode messageLength (self.listSize messageLength inverseAccuracy) (Fin (self.coordinateLength messageLength inverseAccuracy) → Bool)

  The semantic code at each message length and inverse accuracy.

def Complexity.BooleanListCodeFamily.truthTableBits {coordinateLength : ℕ} (word : (Fin coordinateLength → Bool) → Bool) : List Bool

Canonical little-endian truth-table order on a Boolean cube.

Equations

• Complexity.BooleanListCodeFamily.truthTableBits word = List.ofFn fun (index : Fin (2 ^ coordinateLength)) => word { toFin := index }.getLsb

def Complexity.BooleanListCodeFamily.encoderInput (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : List Bool

Canonically framed input to a uniform encoder machine.

Equations

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

def Complexity.BooleanListCodeFamily.encoderOutput (family : BooleanListCodeFamily) (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : List Bool

Canonical full truth table output of a family encoder.

Equations

• family.encoderOutput messageLength inverseAccuracy message = Complexity.BooleanListCodeFamily.truthTableBits ((family.code messageLength inverseAccuracy).encode message)

def Complexity.BooleanListCodeFamily.decoderInput (family : BooleanListCodeFamily) (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : List Bool

Canonically framed input to a uniform full-list decoder machine.

Equations

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

def Complexity.BooleanListCodeFamily.decoderOutput (family : BooleanListCodeFamily) (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : List Bool

Canonical concatenation of every indexed decoder output.

Equations

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

def Complexity.BooleanListCodeFamily.IsListDecodableAtInverseAccuracy (family : BooleanListCodeFamily) : Prop

Semantic list decoding at radius 1/2 - 1/q, where q is the inverse accuracy parameter. The lower bound 2 ≤ q keeps the radius nonnegative.

Equations

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

structure Complexity.BooleanListCodeFamily.PolynomialParameterBounds (family : BooleanListCodeFamily) : Type

Concrete polynomial parameter bounds for a list-code family. Bounding 2^coordinateLength directly captures the content of coordinateLength = O(log(messageLength / epsilon)) without hiding a choice of multivariate asymptotic convention.

• codewordConstant : ℕ

  Multiplicative constant for full codeword length.

• codewordDegree : ℕ

  Polynomial degree for full codeword length.

• listConstant : ℕ

  Multiplicative constant for decoder list size.

• listDegree : ℕ

  Polynomial degree for decoder list size.

• codewordLength_le (messageLength inverseAccuracy : ℕ) : 2 ^ family.coordinateLength messageLength inverseAccuracy ≤ self.codewordConstant * (messageLength + inverseAccuracy + 1) ^ self.codewordDegree

  The full truth table has polynomial length in message length and inverse accuracy.

• listSize_le (messageLength inverseAccuracy : ℕ) : family.listSize messageLength inverseAccuracy ≤ self.listConstant * (inverseAccuracy + 1) ^ self.listDegree

  The decoder returns polynomially many candidates in inverse accuracy.

structure Complexity.BooleanListCodeFamily.UniformPolynomialTimeRealization (family : BooleanListCodeFamily) : Type 1

Uniform machine realization of a list-code family. A single encoder and a single full-list decoder handle every parameter choice; only their inputs vary. The time bounds are polynomial in the numeric parameters, matching unary parameterization even though the canonical framing stores the numbers in binary.

• encoderTapes : ℕ

  Work-tape count of the uniform encoder.

• decoderTapes : ℕ

  Work-tape count of the uniform full-list decoder.

• encoderMachine : TM self.encoderTapes

  One encoder machine for the entire family.

• decoderMachine : TM self.decoderTapes

  One full-list decoder machine for the entire family.

• encoderTime : ℕ → ℕ → ℕ

  Pointwise encoder clock.

• decoderTime : ℕ → ℕ → ℕ

  Pointwise decoder clock.

• encoder_correct (messageLength inverseAccuracy : ℕ) (message : Fin messageLength → Bool) : self.encoderMachine.ProducesInTime (encoderInput messageLength inverseAccuracy message) (family.encoderOutput messageLength inverseAccuracy message) (self.encoderTime messageLength inverseAccuracy)

  Uniform encoder correctness on every canonical family input.

• decoder_correct (messageLength inverseAccuracy : ℕ) (received : (Fin (family.coordinateLength messageLength inverseAccuracy) → Bool) → Bool) : self.decoderMachine.ProducesInTime (family.decoderInput messageLength inverseAccuracy received) (family.decoderOutput messageLength inverseAccuracy received) (self.decoderTime messageLength inverseAccuracy)

  Uniform full-list decoder correctness on every received word.

• timeConstant : ℕ

  Shared polynomial-time multiplicative constant.

• timeDegree : ℕ

  Shared polynomial-time degree.

• encoderTime_le (messageLength inverseAccuracy : ℕ) : self.encoderTime messageLength inverseAccuracy ≤ self.timeConstant * (messageLength + inverseAccuracy + 1) ^ self.timeDegree

  Encoder time is polynomial in message length and inverse accuracy.

• decoderTime_le (messageLength inverseAccuracy : ℕ) : self.decoderTime messageLength inverseAccuracy ≤ self.timeConstant * (messageLength + inverseAccuracy + 1) ^ self.timeDegree

  Full-list decoder time is polynomial in the same parameters.