Averaging NW reconstruction to fixed advice

Uniform NW seeds split bijectively into the challenge block and outside seed coordinates, while a normalized hybrid tail splits into irrelevant earlier bits and the later bits used by reconstruction. Consequently the global next-bit success probability is exactly the joint fixed-advice agreement probability, and averaging fixes one advice choice with no loss in agreement. A finite reverse-averaging bound additionally quantifies the probability that a uniform advice draw retains half of the advantage.

theorem Complexity.NWDesign.predictionSuccessProbability_eq_averageReconstructionAgreement {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) : NextBitPrediction.successProbability ((design.generator hardFunction).targetBit current) ((design.generator hardFunction).testAtCandidate test current) = design.averageReconstructionAgreement hardFunction test current

The canonical next-bit success probability is exactly average agreement of the reconstructed fixed-advice predictors with the hard function.

theorem Complexity.NWDesign.exists_reconstructionAdvice_agreement_ge {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) : ∃ (advice : design.ReconstructionAdvice current), NextBitPrediction.successProbability ((design.generator hardFunction).targetBit current) ((design.generator hardFunction).testAtCandidate test current) ≤ design.reconstructionAgreementProbability hardFunction test current advice

Some fixed outside seed, later tail, and candidate preserve at least the global next-bit success probability over uniform challenges.

theorem Complexity.NWDesign.averageReconstructionAgreement_eq_uniformMean {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) : design.averageReconstructionAgreement hardFunction test current = uniformMean fun (advice : design.ReconstructionAdvice current) => design.reconstructionAgreementProbability hardFunction test current advice

Joint reconstruction agreement is the uniform mean of the fixed-advice agreement probabilities.

theorem Complexity.NWDesign.average_sub_div_le_goodReconstructionAdviceProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (agreementThreshold : ℚ) (hthreshold : agreementThreshold < 1) : (design.averageReconstructionAgreement hardFunction test current - agreementThreshold) / (1 - agreementThreshold) ≤ design.goodReconstructionAdviceProbability hardFunction test current agreementThreshold

Exact reverse-averaging bound for sampling a fixed advice choice above a given agreement threshold.

theorem Complexity.NWDesign.half_advantage_le_goodReconstructionAdviceProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (advantage : ℚ) (hadvantage : 0 ≤ advantage) (haverage : 1 / 2 + advantage ≤ design.averageReconstructionAgreement hardFunction test current) : advantage / 2 ≤ design.goodReconstructionAdviceProbability hardFunction test current (1 / 2 + advantage / 2)

If mean agreement is 1/2 + ε, at least an ε/2 fraction of advice choices have agreement 1/2 + ε/2.

theorem Complexity.NWDesign.exists_fixed_reconstruction_of_randomTest {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength) (advice : design.ReconstructionAdvice current), 1 / 2 + density / ↑outputLength ≤ design.reconstructionAgreementProbability hardFunction (BitGenerator.orientTest test complement) current advice ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

End-to-end finite NW reconstruction: a dense random test and weak-design budget yield one fixed predictor with the hybrid agreement advantage and an exact non-codec payload bound.

theorem Complexity.NWDesign.exists_fixed_reconstruction_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength) (advice : design.ReconstructionAdvice current), 1 / 2 + density / ↑outputLength ≤ design.reconstructionAgreementProbability hardFunction (BitGenerator.orientTest test complement) current advice ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

The same fixed-predictor theorem with generator low complexity discharged by direct descriptions shorter than the randomness threshold.

theorem Complexity.NWDesign.exists_goodAdviceProbability_ge_of_randomTest {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), density / ↑outputLength / 2 ≤ design.goodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Hirahara's randomized-certificate sampling bound: for the selected hybrid coordinate, a uniform advice draw achieves half the agreement advantage with probability at least half that advantage.

theorem Complexity.NWDesign.exists_goodAdviceProbability_ge_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold budget : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hdensity : 0 ≤ density) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) (hbudget : design.HasOverlapBudget budget) : ∃ (complement : Bool) (current : Fin outputLength), density / ↑outputLength / 2 ≤ design.goodReconstructionAdviceProbability hardFunction (BitGenerator.orientTest test complement) current (1 / 2 + density / ↑outputLength / 2) ∧ design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

The randomized advice-sampling bound with low complexity discharged by direct short-seed descriptions.