Nisan--Wigderson fixed-advice reconstruction

This module turns the overlap tables into the exact query made by the Yao next-bit predictor. It also removes irrelevant seed and tail coordinates from the fixed advice and proves the resulting Boolean payload bound overlapCostAt + (d - ell) + 1, before codec and parameter overhead. The averaging submodule fixes one advice choice without losing success probability, repeated sampling finds such advice with an explicit geometric guarantee, and global sampling chooses the hybrid coordinate and advice in one fixed-width trial matching the randomized reconstruction algorithm. Certificate search then checks both test orientations by exact finite agreement and returns the first successful sampled trial. Finally, explicit reconstruction programs materialize the predecessor tables so that evaluating a selected predictor no longer accesses the hard function, serialize the complete program and decoder index exactly, compose its agreement guarantee with finite list decoding, and turn the resulting short string into a machine-relative bounded-complexity certificate whenever the fixed decoder has a TM realization, then transfer it to any efficiently universal machine through explicit compiler and clock overheads.

@[simp]

theorem Complexity.NWDesign.card_outsideCoordinates {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : (design.outsideCoordinates current).card = seedLength - inputLength

There are exactly d - ell seed coordinates outside one design block.

@[simp]

theorem Complexity.NWDesign.card_laterCoordinates {outputLength : ℕ} (current : Fin outputLength) : (laterCoordinates current).card = outputLength - (↑current + 1)

There are exactly m - (i + 1) output coordinates after coordinate i.

theorem Complexity.NWDesign.card_outsideAssignments {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : Fintype.card (↥(design.outsideCoordinates current) → Bool) = 2 ^ (seedLength - inputLength)

Exact number of outside-seed assignments.

theorem Complexity.NWDesign.card_laterAssignments {outputLength : ℕ} (current : Fin outputLength) : Fintype.card (↥(laterCoordinates current) → Bool) = 2 ^ (outputLength - (↑current + 1))

Exact number of later-tail assignments.

@[simp]

theorem Complexity.NWDesign.reconstructionSeed_apply_coordinates {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (input : Fin inputLength) : design.reconstructionSeed current outside challenge ((design.coordinates current) input) = challenge input

A reconstructed seed reads the supplied challenge on the current block.

@[simp]

theorem Complexity.NWDesign.reconstructionSeed_restrict {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (seed : Fin seedLength → Bool) : design.reconstructionSeed current (BooleanDependency.restrict (design.outsideCoordinates current) seed) (design.restrictSeed current seed) = seed

Restricting a seed to the outside and current-block coordinates and then reconstructing it recovers the original seed exactly.

@[simp]

theorem Complexity.NWDesign.reconstructionBackground_targetBit {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) : (design.generator hardFunction).targetBit current (design.reconstructionBackground current outside later challenge) = hardFunction challenge

The target bit on a reconstruction background is the hard function applied to the varying challenge.

theorem Complexity.NWDesign.reconstructionQuery_eq_hybridOutput {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (candidate : Bool) : design.reconstructionQuery hardFunction current outside later challenge candidate = (design.generator hardFunction).hybridOutput (↑current) (BitGenerator.assembleCandidate (design.reconstructionBackground current outside later challenge) candidate)

The table-based reconstruction query is exactly the hybrid query built from the corresponding candidate background.

@[simp]

theorem Complexity.NWDesign.reconstructionTestAtCandidate_eq {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (candidate : Bool) : design.reconstructionTestAtCandidate hardFunction test current outside later challenge candidate = (design.generator hardFunction).testAtCandidate test current (design.reconstructionBackground current outside later challenge) candidate

Evaluating the test on the reconstructed query agrees exactly with the canonical next-bit experiment.

theorem Complexity.NWDesign.reconstructionPredictor_agrees_iff {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (candidate : Bool) (challenge : Fin inputLength → Bool) : design.reconstructionPredictor hardFunction test current outside later candidate challenge = hardFunction challenge ↔ NextBitPrediction.predictFromTest ((design.generator hardFunction).testAtCandidate test current (design.reconstructionBackground current outside later challenge) candidate) candidate = (design.generator hardFunction).targetBit current (design.reconstructionBackground current outside later challenge)

Pointwise agreement of the fixed-advice reconstruction predictor with the hard function is exactly the success event in the canonical experiment.

theorem Complexity.NWDesign.reconstructionDataBitsAt_eq {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : design.reconstructionDataBitsAt current = design.overlapCostAt current + (seedLength - inputLength) + 1

Exact reconstruction payload before encoding the test, design parameters, coordinate, and polarity.

theorem Complexity.NWDesign.reconstructionDataBitsAt_le_of_hasOverlapBudget {outputLength inputLength seedLength budget : ℕ} {design : NWDesign outputLength inputLength seedLength} (hbudget : design.HasOverlapBudget budget) (current : Fin outputLength) : design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

A weak-design budget bounds the fixed predictor's non-codec payload by the budget, the outside seed, and one candidate bit.