Executable NW reconstruction certificate search

The finite search checks exact truth-table agreement, tries both orientations of the supplied statistical test, and returns the first successful global coordinate/advice trial. Its success probability dominates the favorable orientation supplied by the NW hybrid argument.

@[simp]

theorem Complexity.NWDesign.reconstructionCertificatePasses_eq_true_iff {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (certificate : ReconstructionCertificate outputLength seedLength) : design.reconstructionCertificatePasses hardFunction test agreementThreshold certificate = true ↔ design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate

The executable certificate checker accepts exactly the certificates whose induced predictor meets the agreement threshold.

theorem Complexity.NWDesign.checkReconstructionTrial_isSome_iff {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (trial : ReconstructionTrial outputLength seedLength) : (design.checkReconstructionTrial? hardFunction test agreementThreshold trial).isSome = true ↔ ∃ (complement : Bool), design.IsGoodReconstructionCertificate hardFunction test agreementThreshold { complement := complement, trial := trial }

Trying both polarities for one trial succeeds exactly when one orientation meets the agreement threshold.

theorem Complexity.NWDesign.checkReconstructionTrial_sound {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (trial : ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength) (hcheck : design.checkReconstructionTrial? hardFunction test agreementThreshold trial = some certificate) : design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate ∧ certificate.trial = trial

Every certificate returned from one trial is good and contains exactly that sampled trial.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_isSome_iff {outputLength inputLength seedLength trials : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (batch : Fin trials → ReconstructionTrial outputLength seedLength) : (design.findGoodReconstructionCertificate? hardFunction test agreementThreshold batch).isSome = true ↔ ∃ (index : Fin trials) (complement : Bool), design.IsGoodReconstructionCertificate hardFunction test agreementThreshold { complement := complement, trial := batch index }

Batch search succeeds exactly when some sampled trial meets the threshold under one of the two test orientations.

theorem Complexity.NWDesign.findGoodReconstructionCertificate_sound {outputLength inputLength seedLength trials : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (batch : Fin trials → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength) (hfind : design.findGoodReconstructionCertificate? hardFunction test agreementThreshold batch = some certificate) : design.IsGoodReconstructionCertificate hardFunction test agreementThreshold certificate ∧ ∃ (index : Fin trials), certificate.trial = batch index

Every result returned by batch search meets the agreement threshold and comes from one of the supplied samples.

theorem Complexity.NWDesign.repeatedGoodReconstructionTrialProbability_le_checked {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (complement : Bool) (agreementThreshold : ℚ) (trials : ℕ) : design.repeatedGoodReconstructionTrialProbability hardFunction (BitGenerator.orientTest test complement) agreementThreshold trials ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test agreementThreshold trials

Checking both orientations can only improve on repeated sampling for any one fixed orientation.

theorem Complexity.NWDesign.half_le_checkedReconstructionBatch_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) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? hardFunction test (1 / 2 + density / ↑outputLength / 2) batch = some certificate → design.reconstructionDataBitsAt certificate.trial.1 ≤ budget + (seedLength - inputLength) + 1

End-to-end executable finite selection: exact checking of ceil(2m / δ) global samples finds an agreement-1/2 + δ/(2m) certificate with probability at least one half. Every returned certificate retains the weak-design payload bound.

theorem Complexity.NWDesign.half_le_checkedReconstructionBatch_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) : 1 / 2 ≤ design.checkedReconstructionBatchSuccessProbability hardFunction test (1 / 2 + density / ↑outputLength / 2) (reconstructionAdviceTrialCount outputLength density) ∧ ∀ (batch : Fin (reconstructionAdviceTrialCount outputLength density) → ReconstructionTrial outputLength seedLength) (certificate : ReconstructionCertificate outputLength seedLength), design.findGoodReconstructionCertificate? hardFunction test (1 / 2 + density / ↑outputLength / 2) batch = some certificate → design.reconstructionDataBitsAt certificate.trial.1 ≤ budget + (seedLength - inputLength) + 1

The executable finite selection theorem with low generator complexity discharged by direct short-seed descriptions.