Executable NW reconstruction certificate search -- definitions

A reconstruction certificate records a polarity for the statistical test and one globally sampled coordinate/advice trial. Its quality is checked by exact finite truth-table agreement. A batch search tries both polarities for every sampled trial and returns the first certificate meeting the requested threshold.

structure Complexity.NWDesign.ReconstructionCertificate (outputLength seedLength : ℕ) : Type

Finite reconstruction data selected by the randomized search: a polarity bit and one globally sampled coordinate/advice trial.

• complement : Bool

  Whether to complement the supplied statistical test.

• trial : ReconstructionTrial outputLength seedLength

  The coordinate and fixed-width raw reconstruction advice.

def Complexity.NWDesign.IsGoodReconstructionCertificate {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (certificate : ReconstructionCertificate outputLength seedLength) : Prop

A reconstruction certificate is good when its induced predictor has at least the requested exact truth-table agreement.

Equations

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

def Complexity.NWDesign.reconstructionCertificatePasses {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (certificate : ReconstructionCertificate outputLength seedLength) : Bool

Executable exact-agreement checker for a finite reconstruction certificate.

Equations

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

def Complexity.NWDesign.checkReconstructionTrial? {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (trial : ReconstructionTrial outputLength seedLength) : Option (ReconstructionCertificate outputLength seedLength)

Try both test polarities for one sampled reconstruction trial.

Equations

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

def Complexity.NWDesign.findGoodReconstructionCertificate? {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) : Option (ReconstructionCertificate outputLength seedLength)

Search a finite batch of global reconstruction trials, trying both test polarities at every coordinate/advice sample.

Equations

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

def Complexity.NWDesign.checkedReconstructionBatchEvent {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (trials : ℕ) : Finset (Fin trials → ReconstructionTrial outputLength seedLength)

Batches on which exact checking finds a reconstruction certificate.

Equations

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

def Complexity.NWDesign.checkedReconstructionBatchSuccessProbability {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (agreementThreshold : ℚ) (trials : ℕ) : ℚ

Probability that exact checking of a uniform batch finds a reconstruction certificate in either test orientation.

Equations

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