Nisan--Wigderson fixed-advice reconstruction -- proof internals #

theorem Complexity.NWDesign.card_outsideCoordinates_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

(design.outsideCoordinates current).card = seedLength - inputLength

(laterCoordinates current).card = outputLength - (↑current + 1)

theorem Complexity.NWDesign.card_outsideAssignments_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

Fintype.card (↥(design.outsideCoordinates current) → Bool) = 2 ^ (seedLength - inputLength)

Fintype.card (↥(laterCoordinates current) → Bool) = 2 ^ (outputLength - (↑current + 1))

theorem Complexity.NWDesign.reconstructionSeed_apply_coordinates_internal {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

theorem Complexity.NWDesign.reconstructionSeed_apply_outside_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (coordinate : ↥(design.outsideCoordinates current)) :

design.reconstructionSeed current outside challenge ↑coordinate = outside coordinate

theorem Complexity.NWDesign.reconstructionSeed_restrict_internal {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

theorem Complexity.NWDesign.reconstructionBackground_targetBit_internal {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

theorem Complexity.NWDesign.reconstructionQuery_eq_hybridOutput_internal {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)

theorem Complexity.NWDesign.reconstructionTestAtCandidate_eq_internal {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

theorem Complexity.NWDesign.reconstructionPredictor_eq_internal {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 = NextBitPrediction.predictFromTest ((design.generator hardFunction).testAtCandidate test current (design.reconstructionBackground current outside later challenge) candidate) candidate

theorem Complexity.NWDesign.reconstructionPredictor_agrees_iff_internal {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)

theorem Complexity.NWDesign.reconstructionDataBitsAt_eq_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

design.reconstructionDataBitsAt current = design.overlapCostAt current + (seedLength - inputLength) + 1

theorem Complexity.NWDesign.reconstructionDataBitsAt_le_of_hasOverlapBudget_internal {outputLength inputLength seedLength budget : ℕ} {design : NWDesign outputLength inputLength seedLength} (hbudget : design.HasOverlapBudget budget) (current : Fin outputLength) :

design.reconstructionDataBitsAt current ≤ budget + (seedLength - inputLength) + 1

Documentation