Uniform families of finite Boolean list codes -- proof internals

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

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

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

theorem Complexity.BooleanListCodeFamily.exists_indexBits_of_half_add_inverseAccuracy_internal (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

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

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

theorem Complexity.BooleanListCodeFamily.length_decoderOutput_le_internal {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

theorem Complexity.BooleanListCodeFamily.UniformPolynomialTimeRealization.encoder_spec_internal {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

theorem Complexity.BooleanListCodeFamily.UniformPolynomialTimeRealization.decoder_spec_internal {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