GapCVP proof, part 11, continuation 02

def GapCVP.BinarySourceConvolutionTM.factor400BinarySourceSkipFields : ℕ → List Bool → List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.BinarySourceConvolutionTM.factor400BinarySourceSkipFields 0 = id

noncomputable def GapCVP.BinarySourceConvolutionTM.binarySourceSkipFieldsComputable (count : ℕ) : BitTM (factor400BinarySourceSkipFields count)

GapCVP reduction support.

Equations

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

def GapCVP.BinarySourceConvolutionTM.binarySourceConvolutionCoefficientQuery (coefficient : ℕ) (source : List Bool) : List Bool

Prefix the source with the unary index of the requested convolution coefficient.

Equations

• GapCVP.BinarySourceConvolutionTM.binarySourceConvolutionCoefficientQuery coefficient source = GapCVP.BinaryEncoding.lengthPrefixedWord (List.replicate coefficient true) ++ source

def GapCVP.BinarySourceConvolutionTM.binarySourceConvolutionCoefficientPairWidthOutput : List Bool → List Bool

Read the convolution pair width from the coefficient query's raw source.

Equations

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

noncomputable def GapCVP.BinarySourceConvolutionTM.binarySourceRawConvolutionWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinarySourceConvolutionTM.factor400BinarySourceRawConvolutionComputable : BitTM binarySourceRawConvolutionWord

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySourceConvolutionCorrectness.factor400BinaryFiniteWordBits_drop_head {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) (position : ℕ) (hposition : position < degree) : (List.drop position (BinaryModularReductionTM.finiteWordBits word)).headD false = word ⟨position, hposition⟩

theorem GapCVP.BinarySourceConvolutionCorrectness.factor400BinarySourceConvolution_range_mul_flatMap (outer inner : ℕ) : List.range (outer * inner) = List.flatMap (fun (row : ℕ) => List.map (fun (column : ℕ) => row * inner + column) (List.range inner)) (List.range outer)

@[simp]

theorem GapCVP.BinarySourceConvolutionCorrectness.factor400BinarySourceConvolutionCoefficientPairWidthOutput_query {degree : ℕ} (lower left right : Core.EffectiveBinaryField.Word degree) (coefficient : ℕ) (source : List Bool) : BinarySourceConvolutionTM.binarySourceConvolutionCoefficientPairWidthOutput (BinarySourceConvolutionTM.binarySourceConvolutionCoefficientQuery coefficient (BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldQuery (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits left) (BinaryModularReductionTM.finiteWordBits right) source)) = List.replicate (degree ^ 2) true

theorem GapCVP.BinarySourceConvolutionCorrectness.factor400BinarySourceRawConvolutionWord_valid {degree : ℕ} (lower left right : Core.EffectiveBinaryField.Word degree) (source : List Bool) : BinarySourceConvolutionTM.binarySourceRawConvolutionWord (BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldQuery (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits left) (BinaryModularReductionTM.finiteWordBits right) source) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyWords left right)

def GapCVP.BinarySourceModularReductionFoldTM.binarySourceModularReductionQuery (lower product source : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularReductionFoldTM.binarySourceModularReductionDegreeUnary : 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.BinarySourceModularReductionFoldTM.factor400BinarySourceModularReductionDegreeUnaryComputable : BitTM binarySourceModularReductionDegreeUnary

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.BinarySourceModularReductionFoldTM.factor400BinarySourceModularReductionDegreeUnary_valid {degree : ℕ} (lower : Core.EffectiveBinaryField.Word degree) (product source : List Bool) : binarySourceModularReductionDegreeUnary (binarySourceModularReductionQuery (BinaryModularReductionTM.finiteWordBits lower) product source) = List.replicate degree true

Internal support shared across GapCVP continuation modules.

def GapCVP.BinarySourceModularReductionFoldTM.binarySourceModularReductionInitialState (lower product source : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularReductionFoldTM.binarySourceModularReductionFoldPreparation (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.BinarySourceModularReductionFoldTM.factor400BinarySourceModularReductionFoldPreparationComputable : BitTM binarySourceModularReductionFoldPreparation

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.BinarySourceModularReductionFoldTM.factor400BinarySourceModularReductionFoldPreparation_valid {degree : ℕ} (lower : Core.EffectiveBinaryField.Word degree) (product : Core.EffectiveBinaryField.Word (2 * degree)) (source : List Bool) : binarySourceModularReductionFoldPreparation (binarySourceModularReductionQuery (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits product) source) = OutputBoundedDependentRecordFold.unaryBoundedFoldWord degree (binarySourceModularReductionInitialState (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits product) source)

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceProductReductionQuery (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.BinarySourceFieldMultiplicationTM.factor400BinarySourceProductReductionQueryComputable : BitTM binarySourceProductReductionQuery

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceProductReductionQuery_query (lower left right source : List Bool) : binarySourceProductReductionQuery (factor400BinarySourceFieldQuery lower left right source) = BinarySourceModularReductionFoldTM.binarySourceModularReductionQuery (BinaryModularReductionTM.finiteWordBits (factor400BinarySourcePaddedWord left.length lower)) (BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyWords (factor400BinarySourcePaddedWord left.length left) (factor400BinarySourcePaddedWord left.length right))) (factor400BinarySourceFieldQuery lower left right source)

Internal support shared across GapCVP continuation modules.

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularDegreeState (offset : ℕ) (lower current source : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularOffsetUnary : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularOffsetUnary = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOffsetUnaryComputable : BitTM binarySourceModularOffsetUnary

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOffsetUnaryComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularLowerWord : 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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularLowerWordComputable : BitTM binarySourceModularLowerWord

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularCurrentWord : 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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularCurrentWordComputable : BitTM binarySourceModularCurrentWord

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularOriginalSource : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularOriginalSource = GapCVP.BinarySourceConvolutionTM.factor400BinarySourceSkipFields 3

noncomputable def GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOriginalSourceComputable : BitTM binarySourceModularOriginalSource

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOriginalSourceComputable = GapCVP.BinarySourceConvolutionTM.binarySourceSkipFieldsComputable 3

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOffsetUnary_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularOffsetUnary (binarySourceModularDegreeState offset lower current source) = List.replicate offset true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularLowerWord_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularLowerWord (binarySourceModularDegreeState offset lower current source) = lower

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularCurrentWord_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularCurrentWord (binarySourceModularDegreeState offset lower current source) = current

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularOriginalSource_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularOriginalSource (binarySourceModularDegreeState offset lower current source) = source

Internal support shared across GapCVP continuation modules.

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularLowerDegreeUnary (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.

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularCurrentWidthUnary (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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularCurrentWidthUnaryComputable : BitTM binarySourceModularCurrentWidthUnary

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularDescendingDegreeUnary : 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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularDescendingDegreeUnaryComputable : BitTM binarySourceModularDescendingDegreeUnary

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularShiftStartUnary : 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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularShiftStartUnaryComputable : BitTM binarySourceModularShiftStartUnary

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.BinarySourceModularDegreeStepTM.binarySourceModularLeadingGate : 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.BinarySourceModularDegreeStepTM.factor400BinarySourceModularLeadingGateComputable : BitTM binarySourceModularLeadingGate

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularLowerDegreeUnary_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularLowerDegreeUnary (binarySourceModularDegreeState offset lower current source) = List.replicate lower.length true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.BinarySourceModularDegreeStepTM.factor400BinarySourceModularDescendingDegreeUnary_state (offset : ℕ) (lower current source : List Bool) : binarySourceModularDescendingDegreeUnary (binarySourceModularDegreeState offset lower current source) = List.replicate (current.length - 1 - offset) true

Internal support shared across GapCVP continuation modules.