GapCVP proof, part 07

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFlatRowMajorAtMostClauseRecordWord (grid : Polynomial ℕ) (first second : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFamilyFlatRowMajorAtMostClauseRecordComputable (grid : Polynomial ℕ) (first second : ℕ) : BitTM (fiveFlatRowMajorAtMostClauseRecordWord grid first second)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFamilyFlatRowMajorAtMostClauseRecordWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (time : CL.Time (CLCellRowBounds.rowWidth bound machine original)) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) (first second : CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) (hpair : first < second) : fiveFlatRowMajorAtMostClauseRecordWord (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) (↑first) (↑second) (BinaryEncoding.lengthPrefixedWord (List.replicate (CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatSourceRowMajorIndex time position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.atMostOneClause time position first second)

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFlatSourceVariableSingletonRecordWord (sign : Bool) (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFamilyFlatSourceVariableSingletonRecordComputable (sign : Bool) : BitTM (fiveFlatSourceVariableSingletonRecordWord sign)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM.fiveFamilyFlatSourceVariableSingletonRecordWord_valid {T S : ℕ} (atom : CL.Variable T S) (sign : Bool) : fiveFlatSourceVariableSingletonRecordWord sign (List.replicate (Encodable.encode atom) true) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord {(atom, sign)}

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceFourFamilyMarkerRotationTM.fourFamilyOriginalMarkerRotationOutput (marker : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyMarkerRotationTM.sourceFourFamilyOriginalMarkerRotationComputable {marker : List Bool → List Bool} (computer : BitTM marker) : BitTM (fourFamilyOriginalMarkerRotationOutput marker)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyMarkerRotationTM.sourceFourFamilyOriginalMarkerRotationOutput_eq (marker : List Bool → List Bool) (input : List Bool) : fourFamilyOriginalMarkerRotationOutput marker input = SourceFormulaStructuralDecoder.firstFieldSuffix (input ++ marker (SourceFormulaStructuralDecoder.firstFieldContents input))

def GapCVP.SourceFourFamilyMarkerRotationTM.fourFamilyOriginalMarkerStream (marker : List Bool → List Bool) (queries : List (List Bool)) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFourFamilyMarkerRotationTM.fourFamilyOriginalMarkerStream marker queries = List.flatMap marker queries

theorem GapCVP.SourceFourFamilyMarkerRotationTM.sourceFourFamilyFirstFieldSuffix_length_le (input : List Bool) : (SourceFormulaStructuralDecoder.firstFieldSuffix input).length ≤ input.length

noncomputable def GapCVP.SourceFourFamilyMarkerRotationTM.fourFamilyOriginalMarkerFoldComputable {marker : List Bool → List Bool} (computer : BitTM marker) (hmarker : ∀ (input : List Bool), (marker input).length ≤ 1) : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput (fourFamilyOriginalMarkerRotationOutput marker))

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyMarkerRotationTM.boundedRecordFoldOutput_sourceFourFamilyOriginalMarkerQueries (marker : List Bool → List Bool) (queries : List (List Bool)) (suffix : List Bool) : OutputBoundedDependentRecordFold.boundedRecordFoldOutput (fourFamilyOriginalMarkerRotationOutput marker) (OutputBoundedDependentRecordFold.unaryBoundedFoldWord queries.length (SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixOriginalSourceQueryStream queries ++ suffix)) = suffix ++ fourFamilyOriginalMarkerStream marker queries

def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotWord : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotWord = GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (fun (x : List Bool) => [false]) [true]

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotComputable : BitTM sourceFourFamilyBooleanNotWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotWord_bit (bit : Bool) : sourceFourFamilyBooleanNotWord [bit] = [!bit]

def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanAndPairWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanAndPairComputable : BitTM sourceFourFamilyBooleanAndPairWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanAndPairWord_bits (first second : Bool) : sourceFourFamilyBooleanAndPairWord [first, second] = [first && second]

def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanAndOutput (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyBooleanAndComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (sourceFourFamilyBooleanAndOutput first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyBooleanAndOutput_bits (first second : List Bool → List Bool) (input : List Bool) (firstBit secondBit : Bool) (hfirst : first input = [firstBit]) (hsecond : second input = [secondBit]) : sourceFourFamilyBooleanAndOutput first second input = [firstBit && secondBit]

def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotOutput (marker : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotOutput marker = GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotWord ∘ marker

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyBooleanNotOutputComputable {marker : List Bool → List Bool} (computer : BitTM marker) : BitTM (sourceFourFamilyBooleanNotOutput marker)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyBooleanNotOutput_bit (marker : List Bool → List Bool) (input : List Bool) (bit : Bool) (hmarker : marker input = [bit]) : sourceFourFamilyBooleanNotOutput marker input = [!bit]

def GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyDelimitedUnaryComparisonInput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyDelimitedUnaryComparisonInputComputable : BitTM fourFamilyDelimitedUnaryComparisonInput

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyDelimitedUnaryComparisonInput_valid (first second : ℕ) (suffix : List Bool) : fourFamilyDelimitedUnaryComparisonInput (BinaryEncoding.lengthPrefixedWord (List.replicate first true) ++ BinaryEncoding.lengthPrefixedWord (List.replicate second true) ++ suffix) = BinaryEncoding.lengthPrefixedWord (Computability.encodeNat first) ++ BinaryEncoding.lengthPrefixedWord (Computability.encodeNat second)

def GapCVP.SourceFourFamilyBooleanPredicateTM.fourFamilyNaturalOrderingBitsOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyNaturalOrderingBitsComputable : BitTM fourFamilyNaturalOrderingBitsOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnarySumOutput (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnarySumOutput first second input = first input ++ second input

noncomputable def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnarySumComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (fourFamilyComputedUnarySumOutput first second)

GapCVP reduction support.

Equations

• GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnarySumComputable hfirst hsecond = GapCVP.CNFFlatPhysicalBinaryAppendTM.pointwiseAppendComputable hfirst hsecond

theorem GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnarySumOutput_valid (first second : List Bool → List Bool) (input : List Bool) (left right : ℕ) (hfirst : first input = List.replicate left true) (hsecond : second input = List.replicate right true) : fourFamilyComputedUnarySumOutput first second input = List.replicate (left + right) true

def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryProductOutput (left right : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryProductComputable {left right : List Bool → List Bool} (hleft : BitTM left) (hright : BitTM right) : BitTM (fourFamilyComputedUnaryProductOutput left right)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryProductOutput_valid (left right : List Bool → List Bool) (input : List Bool) (first second : ℕ) (hfirst : left input = List.replicate first true) (hsecond : right input = List.replicate second true) : fourFamilyComputedUnaryProductOutput left right input = List.replicate (first * second) true

def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryLessBitOutput (left right : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryLessBitComputable {left right : List Bool → List Bool} (hleft : BitTM left) (hright : BitTM right) : BitTM (fourFamilyComputedUnaryLessBitOutput left right)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryLessBitOutput_valid (left right : List Bool → List Bool) (input : List Bool) (first second : ℕ) (hfirst : left input = List.replicate first true) (hsecond : right input = List.replicate second true) : fourFamilyComputedUnaryLessBitOutput left right input = [decide (first < second)]

theorem GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyComputedUnaryLessBitOutput_length (left right : List Bool → List Bool) (input : List Bool) : (fourFamilyComputedUnaryLessBitOutput left right input).length = 1

def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.sourceFourFamilyBooleanOrOutput (first second : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.sourceFourFamilyBooleanOrComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (sourceFourFamilyBooleanOrOutput first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM.fourFamilyBooleanOrOutput_bits (first second : List Bool → List Bool) (input : List Bool) (firstBit secondBit : Bool) (hfirst : first input = [firstBit]) (hsecond : second input = [secondBit]) : sourceFourFamilyBooleanOrOutput first second input = [firstBit || secondBit]

def GapCVP.SourceFourFamilyDiagonalMembershipPredicateTM.fourFamilyComputedUnaryEqBitOutput (first second : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFourFamilyDiagonalMembershipPredicateTM.fourFamilyComputedUnaryEqBitComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (fourFamilyComputedUnaryEqBitOutput first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFourFamilyDiagonalMembershipPredicateTM.fourFamilyComputedUnaryEqBitOutput_valid (first second : List Bool → List Bool) (input : List Bool) (left right : ℕ) (hleft : first input = List.replicate left true) (hright : second input = List.replicate right true) : fourFamilyComputedUnaryEqBitOutput first second input = [decide (left = right)]

def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fivePackedActualOffsetObservation (bound grid : Polynomial ℕ) (original : List Bool) (position block offset : ℕ) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyPackedActualOffsetObservation_length (bound grid : Polynomial ℕ) (original : List Bool) (position block offset : ℕ) : (fivePackedActualOffsetObservation bound grid original position block offset).length = 6

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fivePackedInitialWholeFeatureWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyPackedInitialWholeFeatureComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (fivePackedInitialWholeFeatureWord bound machine)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyPackedInitialWholeFeatureWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) : fivePackedInitialWholeFeatureWord bound machine (BinaryEncoding.lengthPrefixedWord (List.replicate (↑position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.flatMap (fivePackedActualOffsetObservation bound (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) original (↑position) (CLLocalWindows.blockSize machine.tm)) (List.range (CLLocalWindows.blockSize machine.tm)) ++ List.flatMap (fivePackedActualOffsetObservation bound (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) original 0 (CLLocalWindows.blockSize machine.tm)) (List.range (CLLocalWindows.blockSize machine.tm))

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyPackedInitialDecodedCell {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (features : List Bool) : CLCompleteVerifierSimulation.CompletePhaseCell machine.tm

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyPackedInitialDecodedCell_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) : fiveFamilyPackedInitialDecodedCell machine (fivePackedInitialWholeFeatureWord bound machine (BinaryEncoding.lengthPrefixedWord (List.replicate (↑position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix)) = CLCompleteVerifierSimulation.initialPhaseCell bound machine original position

Internal support shared across GapCVP continuation modules.