Uniform list-code families in NW reconstruction -- proof internals

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.uniformTimeBoundedKolmogorovComplexity_le_internal {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)

theorem Complexity.NWDesign.HasEncodedMessageCertificateWithin.uniformOracleTimeBoundedKolmogorovComplexity_le_internal {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)

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.framedDescriptionBound_eq_internal {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

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.inverseDensityFramedDescriptionBound_eq_internal {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

theorem Complexity.NWDesign.UniformEncodedMessageDecoderRealization.efficientlyUniversal_transfer_internal {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)

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.efficientlyUniversal_transfer_internal {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)

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

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

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_codeFamily_internal {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)

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_polynomialCodeFamily_internal {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)

theorem Complexity.NWDesign.half_le_fullyEncodedIndexedReconstructionProgram_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.half_le_encodedMessageCertificate_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.half_le_timeBoundedKolmogorovComplexity_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.half_le_oracleTimeBoundedKolmogorovComplexity_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.half_le_efficientlyUniversalOracleKolmogorovComplexity_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.UniformEncodedMessageDecoderRealization.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity_internal {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)

theorem Complexity.NWDesign.UniformOracleEncodedMessageDecoderRealization.half_le_efficientlyUniversalKolmogorovComplexity_of_inverseDensity_internal {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)