Globally sampling NW reconstruction coordinates and advice -- definitions

A fixed-width reconstruction trial chooses a hybrid coordinate together with full seed and output assignments and a candidate bit. Restricting the full assignments produces the coordinate-dependent outside-seed and later-tail advice. This realizes Hirahara's random tuple in one finite uniform sample space without weighting coordinates by their varying advice-space sizes.

@[reducible, inline]

abbrev Complexity.NWDesign.RawReconstructionAdvice (outputLength seedLength : ℕ) : Type

Fixed-width raw advice from which every coordinate's reconstruction advice is obtained by restriction.

Equations

• Complexity.NWDesign.RawReconstructionAdvice outputLength seedLength = ((Fin seedLength → Bool) × (Fin outputLength → Bool) × Bool)

@[reducible, inline]

abbrev Complexity.NWDesign.ReconstructionTrial (outputLength seedLength : ℕ) : Type

One globally sampled reconstruction coordinate and its fixed-width raw advice.

Equations

• Complexity.NWDesign.ReconstructionTrial outputLength seedLength = (Fin outputLength × Complexity.NWDesign.RawReconstructionAdvice outputLength seedLength)

def Complexity.NWDesign.reconstructionAdviceOfRaw {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (raw : RawReconstructionAdvice outputLength seedLength) : design.ReconstructionAdvice current

Restrict fixed-width raw advice to the outside-seed and later-tail coordinates used at current.

Equations

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

def Complexity.NWDesign.reconstructionAdviceOfTrial {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (trial : ReconstructionTrial outputLength seedLength) : design.ReconstructionAdvice trial.1

Coordinate-dependent reconstruction advice extracted from one global trial.

Equations

• design.reconstructionAdviceOfTrial trial = design.reconstructionAdviceOfRaw trial.1 trial.2

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

Agreement probability of the predictor encoded by a global trial.

Equations

• design.reconstructionTrialAgreementProbability hardFunction test trial = design.reconstructionAgreementProbability hardFunction test trial.1 (design.reconstructionAdviceOfTrial trial)

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

Global trials whose reconstructed predictor attains an agreement threshold.

Equations

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

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

One-draw probability that a uniformly sampled coordinate and fixed-width raw advice encode a predictor meeting the agreement threshold.

Equations

• design.goodReconstructionTrialProbability hardFunction test agreementThreshold = Complexity.uniformProbability (design.goodReconstructionTrialEvent hardFunction test agreementThreshold)

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

Probability that at least one of several independent global trials encodes a predictor meeting the agreement threshold.

Equations

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