Uniform list-code families in NW reconstruction

This layer specializes checked NW reconstruction to a code family at inverse accuracy q, under the exact relation 1/q = density/(2*outputLength) used in Hirahara's argument. Polynomial list size then gives a concrete logarithmic bound on the encoded decoder choice. For density 1/inverseDensity, the final theorem chooses q = 2*outputLength*inverseDensity and discharges that relation. The final endpoints compose this exact specialization with any efficiently universal machine while retaining the compiler constant and polynomial clock. A family-uniform realization chooses those constants before all ambient instances and charges the explicit design/test encoding in the description. An oracle-relative endpoint instead supplies the finite test through canonical membership queries and retains the original reconstruction-description bound. Its efficiently universal specialization exposes one transfer law valid for all finite test oracles before applying the half-success reconstruction result. A fully uniform oracle specialization chooses the compiler constants before all numeric parameters and designs, charging the exact canonical fixed-width design encoding.

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.uniformTimeBoundedKolmogorovComplexity_le {family : BooleanListCodeFamily} {messageLength inverseAccuracy outputLength seedLength : ℕ} {design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength} {test : Finset (Fin outputLength → Bool)} {message : Fin messageLength → Bool} {bound : ℕ} (realization : UniformEncodedMessageDecoderRealization family) (hcertificate : design.HasEncodedMessageCertificateWithin (family.code messageLength inverseAccuracy) test message bound) : realization.machine.timeBoundedKolmogorovComplexity (List.ofFn message) (realization.time (realization.framedDescriptionBound design test bound)) ≤ ↑(realization.framedDescriptionBound design test bound)

A bounded indexed reconstruction description remains a bounded program for one decoder machine shared by every instance of a list-code family. The exact self-delimiting cost of the ambient design/test encoding is included in the description bound.

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.uniformOracleTimeBoundedKolmogorovComplexity_le {family : BooleanListCodeFamily} {messageLength inverseAccuracy outputLength seedLength : ℕ} {design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength} {test : Finset (Fin outputLength → Bool)} {message : Fin messageLength → Bool} {bound : ℕ} (realization : UniformOracleEncodedMessageDecoderRealization family) (hcertificate : design.HasEncodedMessageCertificateWithin (family.code messageLength inverseAccuracy) test message bound) : realization.machine.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message) (realization.time (UniformOracleEncodedMessageDecoderRealization.framedDescriptionBound design bound)) ≤ ↑(UniformOracleEncodedMessageDecoderRealization.framedDescriptionBound design bound)

A bounded indexed reconstruction certificate remains a bounded oracle-relative program for one decoder machine shared across the whole code family. The design encoding is charged explicitly; the finite test remains oracle access.

theorem Complexity.NWDesign.UniformEncodedMessageDecoderRealization.efficientlyUniversal_transfer {family : BooleanListCodeFamily} {universalTapes : ℕ} (realization : UniformEncodedMessageDecoderRealization family) (universal : TM universalTapes) (huniversal : universal.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (test : Finset (Fin outputLength → Bool)) (message : Fin messageLength → Bool) (bound : ℕ), design.HasEncodedMessageCertificateWithin (family.code messageLength inverseAccuracy) test message bound → universal.timeBoundedKolmogorovComplexity (List.ofFn message) (coefficient * (realization.framedDescriptionBound design test bound + realization.time (realization.framedDescriptionBound design test bound) + 1) ^ exponent) ≤ ↑(realization.framedDescriptionBound design test bound + constant)

A single uniform family decoder gives one set of universal compiler constants valid simultaneously for all lengths, accuracies, designs, tests, messages, and certificate bounds. Ambient information is explicit in the framed description length and therefore cannot leak into those constants.

@[simp]

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.framedDescriptionBound_eq {family : BooleanListCodeFamily} {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (descriptionBound : ℕ) : framedDescriptionBound design descriptionBound = 4 * (messageLength.size + inverseAccuracy.size + outputLength.size + (family.coordinateLength messageLength inverseAccuracy).size + seedLength.size) + 22 + 2 * (outputLength * family.coordinateLength messageLength inverseAccuracy * Fin.bitWidth seedLength) + descriptionBound

Canonical design framing has an exact parameter-only bit cost.

@[simp]

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.inverseDensityFramedDescriptionBound_eq {family : BooleanListCodeFamily} (bounds : family.PolynomialParameterBounds) {messageLength outputLength inverseDensity seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength) (budget : ℕ) : inverseDensityFramedDescriptionBound bounds design budget = 4 * (messageLength.size + (reconstructionInverseAccuracy outputLength inverseDensity).size + outputLength.size + (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).size + seedLength.size) + 22 + 2 * (outputLength * family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity) * Fin.bitWidth seedLength) + inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget

At inverse-density parameters, canonical design framing makes the complete description bound an explicit arithmetic expression.

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.efficientlyUniversal_transfer {family : BooleanListCodeFamily} {universalTapes : ℕ} (realization : UniformOracleEncodedMessageDecoderRealization family) (universal : OracleTM universalTapes) (huniversal : universal.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ {messageLength inverseAccuracy outputLength seedLength : ℕ} (design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength) (test : Finset (Fin outputLength → Bool)) (message : Fin messageLength → Bool) (bound : ℕ), design.HasEncodedMessageCertificateWithin (family.code messageLength inverseAccuracy) test message bound → universal.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message) (coefficient * (framedDescriptionBound design bound + realization.time (framedDescriptionBound design bound) + 1) ^ exponent) ≤ ↑(framedDescriptionBound design bound + constant)

One oracle-universal compiler constant and polynomial clock transfer every certificate across all lengths, accuracies, designs, tests, and messages for a uniform family decoder. Design framing is explicit and the test remains an oracle.

theorem Complexity.NWDesign.two_le_reconstructionInverseAccuracy {outputLength inverseDensity : ℕ} (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) : 2 ≤ reconstructionInverseAccuracy outputLength inverseDensity

Positive output length and inverse density make the canonical inverse accuracy at least two.

theorem Complexity.NWDesign.reconstructionInverseAccuracy_margin_eq {outputLength inverseDensity : ℕ} (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) : 1 / ↑(reconstructionInverseAccuracy outputLength inverseDensity) = 1 / ↑inverseDensity / ↑outputLength / 2

The canonical inverse accuracy has exactly the NW reconstruction margin for a test of density 1 / inverseDensity.

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_codeFamily {messageLength inverseAccuracy outputLength seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (haccuracy : 2 ≤ inverseAccuracy) {design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hmargin : 1 / ↑inverseAccuracy = density / ↑outputLength / 2) (houtputLength : 0 < outputLength) (hdensity : 0 < density) (hlow : (design.generator ((family.code messageLength inverseAccuracy).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength inverseAccuracy).encode message) test (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength inverseAccuracy).encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate → ∃ (indexed : design.IndexedReconstructionProgram (family.listSize messageLength inverseAccuracy)), indexed.reconstruction = certificate.toProgram design ((family.code messageLength inverseAccuracy).encode message) ∧ indexed.decodedMessage (family.code messageLength inverseAccuracy) test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - family.coordinateLength messageLength inverseAccuracy) + 1) + BooleanListCode.decoderIndexBitWidth (family.listSize messageLength inverseAccuracy)

Fully encoded NW reconstruction instantiated by a semantic inverse-accuracy list-code family.

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_polynomialCodeFamily {messageLength inverseAccuracy outputLength seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (haccuracy : 2 ≤ inverseAccuracy) {design : NWDesign outputLength (family.coordinateLength messageLength inverseAccuracy) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hmargin : 1 / ↑inverseAccuracy = density / ↑outputLength / 2) (houtputLength : 0 < outputLength) (hdensity : 0 < density) (hlow : (design.generator ((family.code messageLength inverseAccuracy).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength inverseAccuracy).encode message) test (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength inverseAccuracy).encode message) test (1 / 2 + density / ↑outputLength / 2) batch = some certificate → ∃ (indexed : design.IndexedReconstructionProgram (family.listSize messageLength inverseAccuracy)), indexed.reconstruction = certificate.toProgram design ((family.code messageLength inverseAccuracy).encode message) ∧ indexed.decodedMessage (family.code messageLength inverseAccuracy) test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - family.coordinateLength messageLength inverseAccuracy) + 1) + Nat.clog 2 (bounds.listConstant * (inverseAccuracy + 1) ^ bounds.listDegree)

Hirahara-style specialization with the list-index cost bounded by the family's polynomial list-size guarantee.

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → ∃ (indexed : design.IndexedReconstructionProgram (family.listSize messageLength (reconstructionInverseAccuracy outputLength inverseDensity))), indexed.reconstruction = certificate.toProgram design ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) ∧ indexed.decodedMessage (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) test = message ∧ indexed.encode.length ≤ 1 + Fin.bitWidth outputLength + (budget + (seedLength - family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) + 1) + Nat.clog 2 (bounds.listConstant * (reconstructionInverseAccuracy outputLength inverseDensity + 1) ^ bounds.listDegree)

Paper-shaped family reconstruction at density 1 / inverseDensity. The inverse accuracy is fixed canonically to 2 * outputLength * inverseDensity, so no arithmetic compatibility premise remains.

theorem Complexity.NWDesign.half_le_encodedMessageCertificate_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → design.HasEncodedMessageCertificateWithin (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) test message (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget)

Bitstring-certificate form of the inverse-density reconstruction theorem: with probability at least one half, every returned checked certificate yields an actual short string decoded to the original source message.

theorem Complexity.NWDesign.half_le_timeBoundedKolmogorovComplexity_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (realization : design.EncodedMessageDecoderRealization (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) test) (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → realization.machine.timeBoundedKolmogorovComplexity (List.ofFn message) (realization.time (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget)) ≤ ↑(inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget)

Time-bounded Kolmogorov form of inverse-density reconstruction. For any machine realization of the fixed indexed-message decoder, canonical sampling succeeds with probability at least one half and every returned certificate proves the advertised machine-relative Kt upper bound.

theorem Complexity.NWDesign.half_le_oracleTimeBoundedKolmogorovComplexity_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (realization : design.OracleEncodedMessageDecoderRealization (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity))) (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → realization.machine.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message) (realization.time (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget)) ≤ ↑(inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget)

Oracle-relative form of inverse-density reconstruction. One decoder machine handles every finite statistical test through its canonical membership oracle. Canonical certificate search succeeds with probability at least one half, and each returned certificate gives the source message the exact existing description bound with no test-truth-table bits added to the program.

theorem Complexity.NWDesign.half_le_efficientlyUniversalOracleKolmogorovComplexity_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget universalTapes : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (realization : design.OracleEncodedMessageDecoderRealization (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity))) (universal : OracleTM universalTapes) (huniversal : universal.IsEfficientlyUniversal) (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), (∀ (otherTest : Finset (Fin outputLength → Bool)) (otherMessage : Fin messageLength → Bool) (bound : ℕ), design.HasEncodedMessageCertificateWithin (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) otherTest otherMessage bound → universal.timeBoundedKolmogorovComplexity (finiteTestOracle otherTest) (List.ofFn otherMessage) (coefficient * (bound + realization.time bound + 1) ^ exponent) ≤ ↑(bound + constant)) ∧ 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → universal.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message) (coefficient * (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget + realization.time (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget) + 1) ^ exponent) ≤ ↑(inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget + constant)

End-to-end inverse-density reconstruction for an arbitrary efficiently universal oracle machine. The returned compiler constant and polynomial clock first satisfy a transfer law for every finite test oracle. Checked certificate search for the current test then succeeds with probability at least one half, and every returned certificate gives the source message the explicit reconstruction-description bound plus that constant.

theorem Complexity.NWDesign.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity {messageLength outputLength inverseDensity seedLength tapes time threshold budget universalTapes : ℕ} (family : BooleanListCodeFamily) (hfamily : family.IsListDecodableAtInverseAccuracy) (bounds : family.PolynomialParameterBounds) (houtputLength : 0 < outputLength) (hinverseDensity : 0 < inverseDensity) {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (realization : design.EncodedMessageDecoderRealization (family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) test) (universal : TM universalTapes) (huniversal : universal.IsEfficientlyUniversal) (hlow : (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test (1 / ↑inverseDensity)) (hbudget : design.HasOverlapBudget budget) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → universal.timeBoundedKolmogorovComplexity (List.ofFn message) (coefficient * (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget + realization.time (inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget) + 1) ^ exponent) ≤ ↑(inverseDensityDescriptionBound family bounds messageLength outputLength inverseDensity seedLength budget + constant)

End-to-end inverse-density reconstruction for an arbitrary efficiently universal machine. Canonical sampling succeeds with probability at least one half; every returned certificate gives the source message a description of the explicit reconstruction length plus the universal compiler constant, under the compiler's polynomial clock. The decoder realization remains fixed in the ambient design/code/test parameters.

theorem Complexity.NWDesign.UniformEncodedMessageDecoderRealization.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity {family : BooleanListCodeFamily} {universalTapes : ℕ} (realization : UniformEncodedMessageDecoderRealization family) (universal : TM universalTapes) (huniversal : universal.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ (bounds : family.PolynomialParameterBounds) {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)}, family.IsListDecodableAtInverseAccuracy → 0 < outputLength → 0 < inverseDensity → (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold → BitGenerator.IsTimeBoundedRandomTest test machine time threshold → BitGenerator.IsDenseTest test (1 / ↑inverseDensity) → design.HasOverlapBudget budget → 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → universal.timeBoundedKolmogorovComplexity (List.ofFn message) (coefficient * (realization.inverseDensityFramedDescriptionBound bounds design test budget + realization.time (realization.inverseDensityFramedDescriptionBound bounds design test budget) + 1) ^ exponent) ≤ ↑(realization.inverseDensityFramedDescriptionBound bounds design test budget + constant)

Uniform inverse-density NW reconstruction on an arbitrary efficiently universal machine. One compiler constant and one polynomial clock work simultaneously for every numeric parameter, NW design, statistical test, and source message. The ambient design/test representation is not hidden: its self-delimiting framing is charged by inverseDensityFramedDescriptionBound.

This is a fully uniform oracle-free transfer theorem. Replacing the explicit ambient string by random-access oracle access requires a separate oracle machine model and is not asserted here.

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity {family : BooleanListCodeFamily} {universalTapes : ℕ} (realization : UniformOracleEncodedMessageDecoderRealization family) (universal : OracleTM universalTapes) (huniversal : universal.IsEfficientlyUniversal) : ∃ (constant : ℕ) (coefficient : ℕ) (exponent : ℕ), ∀ (bounds : family.PolynomialParameterBounds) {messageLength outputLength inverseDensity seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength (family.coordinateLength messageLength (reconstructionInverseAccuracy outputLength inverseDensity)) seedLength} {message : Fin messageLength → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)}, family.IsListDecodableAtInverseAccuracy → 0 < outputLength → 0 < inverseDensity → (design.generator ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message)).HasLowTimeBoundedComplexity machine time threshold → BitGenerator.IsTimeBoundedRandomTest test machine time threshold → BitGenerator.IsDenseTest test (1 / ↑inverseDensity) → design.HasOverlapBudget budget → 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength (1 / ↑inverseDensity)) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? ((family.code messageLength (reconstructionInverseAccuracy outputLength inverseDensity)).encode message) test (1 / 2 + 1 / ↑inverseDensity / ↑outputLength / 2) batch = some certificate → universal.timeBoundedKolmogorovComplexity (finiteTestOracle test) (List.ofFn message) (coefficient * (inverseDensityFramedDescriptionBound bounds design budget + realization.time (inverseDensityFramedDescriptionBound bounds design budget) + 1) ^ exponent) ≤ ↑(inverseDensityFramedDescriptionBound bounds design budget + constant)

Fully family-uniform oracle-relative inverse-density reconstruction. One decoder machine and one oracle-universal compiler serve every length, accuracy, design encoding, finite test oracle, and source message. The test costs no program bits; the explicitly framed design encoding is charged exactly.