Uniform list-code families in NW reconstruction -- definitions

def Complexity.NWDesign.reconstructionInverseAccuracy (outputLength inverseDensity : ℕ) : ℕ

Inverse list-decoding accuracy corresponding to NW output length m and test density 1 / inverseDensity: q = 2 * m * inverseDensity.

Equations

• Complexity.NWDesign.reconstructionInverseAccuracy outputLength inverseDensity = 2 * outputLength * inverseDensity

def Complexity.NWDesign.inverseDensityDescriptionBound (family : BooleanListCodeFamily) (bounds : family.PolynomialParameterBounds) (messageLength outputLength inverseDensity seedLength budget : ℕ) : ℕ

Complete bit-length bound delivered by inverse-density reconstruction with a polynomially bounded list-code family.

Equations

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

structure Complexity.NWDesign.UniformEncodedMessageDecoderRealization (family : BooleanListCodeFamily) : Type 1

A single decoder machine for every instance of one Boolean list-code family. The NW design and statistical test are supplied through an explicit ambient encoding, while the indexed reconstruction program remains the self-delimiting second component of the machine input.

This is an oracle-free uniformity interface. In particular, the length of the ambient encoding is charged explicitly rather than hidden in the universal compiler constant.

• ambientEncoding {messageLength inverseAccuracy outputLength seedLength : ℕ} : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength → Finset (Fin outputLength → Bool) → List Bool

  Explicit binary representation of the design and statistical test used by one decoder invocation.

• tapes : ℕ

  Number of work tapes used by the one uniform decoder machine.

• machine : TM self.tapes

  Machine interpreting every framed ambient/program pair.

• time : ℕ → ℕ

  Decoder clock as a function of total framed input length.

• time_mono : Monotone self.time

  Larger framed inputs receive no smaller clock.

• correct {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (test : Finset (Fin outputLength → Bool)) (description : List Bool) (message : Fin messageLength → Bool) : design.decodeIndexedMessage? (family.code messageLength inverseAccuracy) test description = some message → self.machine.ProducesInTime (pair (self.ambientEncoding design test) description) (List.ofFn message) (self.time (pair (self.ambientEncoding design test) description).length)

  Correctness simultaneously for every parameter choice and ambient instance.

def Complexity.NWDesign.UniformEncodedMessageDecoderRealization.framedDescriptionBound {family : BooleanListCodeFamily} (realization : UniformEncodedMessageDecoderRealization family) {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (test : Finset (Fin outputLength → Bool)) (descriptionBound : ℕ) : ℕ

Total description bound after self-delimiting framing of the ambient encoding with an indexed reconstruction description of length at most descriptionBound.

Equations

• realization.framedDescriptionBound design test descriptionBound = 2 * (realization.ambientEncoding design test).length + 2 + descriptionBound

def Complexity.NWDesign.UniformEncodedMessageDecoderRealization.inverseDensityFramedDescriptionBound {family : BooleanListCodeFamily} (realization : UniformEncodedMessageDecoderRealization family) (bounds : family.PolynomialParameterBounds) {messageLength outputLength inverseDensity seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength) (test : Finset (Fin outputLength → Bool)) (budget : ℕ) : ℕ

Total framed description bound for the canonical inverse-density NW reconstruction parameters.

Equations

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

structure Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization (family : BooleanListCodeFamily) : Type 1

A single oracle decoder machine for every instance of one Boolean list-code family. All numeric parameters and the NW design are supplied by the canonical self-describing instance codec; the statistical test remains separate oracle access and contributes no program bits.

• tapes : ℕ

  Number of ordinary work tapes in addition to the query tape.

• machine : OracleTM self.tapes

  One oracle decoder machine for the whole family.

• time : ℕ → ℕ

  Decoder clock as a function of total framed program length.

• time_mono : Monotone self.time

  Larger framed programs receive no smaller clock.

• correct {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (test : Finset (Fin outputLength → Bool)) (description : List Bool) (message : Fin messageLength → Bool) : design.decodeIndexedMessage? (family.code messageLength inverseAccuracy) test description = some message → self.machine.ProducesInTime (finiteTestOracle test) (pair (decoderInstance messageLength inverseAccuracy design).encode description) (List.ofFn message) (self.time (pair (decoderInstance messageLength inverseAccuracy design).encode description).length)

  Correctness for every family parameter, canonically encoded design, and finite test oracle.

def Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.framedDescriptionBound {family : BooleanListCodeFamily} {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (descriptionBound : ℕ) : ℕ

Total program bound after framing a design encoding with an indexed reconstruction description of length at most descriptionBound.

Equations

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

def Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.inverseDensityFramedDescriptionBound {family : BooleanListCodeFamily} (bounds : family.PolynomialParameterBounds) {messageLength outputLength inverseDensity seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength) (budget : ℕ) : ℕ

Total framed program bound at the canonical inverse-density parameters.

Equations

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