GapCVP proof, part 08

theorem GapCVP.ofClassicalDecide08 {proposition : Prop} (proof : decide proposition = true) : proposition

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentActualSourceClauseCountPolynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Polynomial ℕ

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentSquareGridTime (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CL.Time (CLCellRowBounds.rowWidth bound machine original)

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentSquareGridPosition (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CL.Position (CLCellRowBounds.rowWidth bound machine original)

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentSquareGridSlots (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Time (CLCellRowBounds.rowWidth bound machine original) × CL.Position (CLCellRowBounds.rowWidth bound machine original))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentForbiddenGridWindow (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CL.Window (CLCellRowBounds.rowWidth bound machine original)

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentForbiddenGridWindows (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Window (CLCellRowBounds.rowWidth bound machine original))

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentAtLeastRankWorker_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFlatRowMajorAtLeastClauseRecordWord (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm + 1) (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.atLeastOneClause (fiveFamilyIndependentSquareGridTime bound machine original rank) (fiveIndependentSquareGridPosition bound machine original rank))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentAtMostRankWorker_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (pair : CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm) × CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentAtMostFixedPairWorker (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm + 1) (↑pair.1) (↑pair.2) (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (if pair.1 < pair.2 then CL.atMostOneClause (fiveFamilyIndependentSquareGridTime bound machine original rank) (fiveIndependentSquareGridPosition bound machine original rank) pair.1 pair.2 else CL.atLeastOneClause (fiveFamilyIndependentSquareGridTime bound machine original rank) (fiveIndependentSquareGridPosition bound machine original rank))

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentInitialGridPosition (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CL.Position (CLCellRowBounds.rowWidth bound machine original)

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentInitialGridPosition bound machine original rank = ⟨↑rank, ⋯⟩

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentInitialRankWorker_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : Fin (Polynomial.eval original.length (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CNFFiveFamilyPackedInitialCellDecoderTM.fiveFlatWholePackedInitialClauseRecordWord bound machine (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.initialClause (CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSpecification bound machine original).input (fiveIndependentInitialGridPosition bound machine original rank))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentForbiddenRankWorker_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (symbols : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) (rank : Fin (Polynomial.eval original.length (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine * CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine))) : CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM.fiveIndependentForbiddenFixedTupleWorker bound machine symbols (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord bound machine original) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (if CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSymbolAllowed machine symbols = false then CL.transitionClause (fiveIndependentForbiddenGridWindow bound machine original rank) symbols else CL.atLeastOneClause (↑(fiveIndependentForbiddenGridWindow bound machine original rank)).1 (↑(fiveIndependentForbiddenGridWindow bound machine original rank)).2)

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentPhysicalAtLeastSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentPhysicalAtMostSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentInitialGridPositions (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Position (CLCellRowBounds.rowWidth bound machine original))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentPhysicalInitialSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentPhysicalForbiddenSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveIndependentPhysicalSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine original) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity.fiveFamilyIndependentPhysicalSourceClauses_toFinset (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : (fiveIndependentPhysicalSourceClauses bound machine original).toFinset = CL.tableauFormula (CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSpecification bound machine original)

Internal support shared across GapCVP continuation modules.