GapCVP proof, part 07, continuation 06

def GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentSourceCountWord (count : Polynomial ℕ) (original : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentSourceCountWord count original = List.replicate (Polynomial.eval original.length count) true

noncomputable def GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveFamilyIndependentSourceCountComputable (count : Polynomial ℕ) : BitTM (fiveIndependentSourceCountWord count)

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveFamilyIndependentSourceCountComputable count = GapCVP.CNFBoundedRecordFoldTM.polynomialValueUnaryComputable count

def GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentSourceRankWords (count : ℕ) : List (List Bool)

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentSourceRankWords count = List.map (fun (rank : ℕ) => List.replicate rank true) (List.range count)

noncomputable def GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentAnchoredFamilyBundledStreamWord (bound count : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (candidate : List Bool → List Bool) (original : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveIndependentAnchoredFamilyBundledStreamComputable (bound count : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) {candidate : List Bool → List Bool} (computer : BitTM candidate) : BitTM (fiveIndependentAnchoredFamilyBundledStreamWord bound count machine candidate)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM.fiveFamilyIndependentAnchoredFamilyBundledStreamWord_valid (bound count : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (candidate : List Bool → List Bool) (original : List Bool) (hfit : ∀ (rank : Fin (Polynomial.eval original.length count)), (candidate (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original)).length ≤ (CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original).length) : fiveIndependentAnchoredFamilyBundledStreamWord bound count machine candidate original = List.flatMap (fun (rank : List Bool) => BinaryEncoding.lengthPrefixedWord (candidate (BinaryEncoding.lengthPrefixedWord rank ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original))) (fiveIndependentSourceRankWords (Polynomial.eval original.length count))

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveFamilyActualAnnotatedRecord_fits_originalAnchor (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (clause : CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : (CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord clause).length ≤ (CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original).length