GapCVP proof, part 11

structure GapCVP.BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer : Type 1

GapCVP reduction support.

• output : List Bool → List Bool

  GapCVP reduction support.

• computer : BitTM self.output

  GapCVP reduction support.

def GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangePrefixedOutput (worker : SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangePrefixedOutput worker input = GapCVP.BinaryEncoding.lengthPrefixedWord (worker.output input)

noncomputable def GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangePrefixedComputable (worker : SourcePhysicalLagrangeWordComputer) : BitTM (sourcePhysicalLagrangePrefixedOutput worker)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangeMultiplyWord (lower left right : SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangeMultiplyComputable (multiplyComputer : BitTM BinarySourceFieldMultiplicationTM.binarySourceMultiplyModWord) (lower left right : SourcePhysicalLagrangeWordComputer) : BitTM (sourcePhysicalLagrangeMultiplyWord lower left right)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalLagrangeCoefficientTM.sourcePhysicalLagrangeMultiplyWord_valid {degree : ℕ} (lowerWord leftWord rightWord : Core.EffectiveBinaryField.Word degree) (lower left right : SourcePhysicalLagrangeWordComputer) (row column : ℕ) (source : List Bool) (hlower : lower.output (BinaryExplicitAffineRows.affineCellQuery row column source) = BinaryModularReductionTM.finiteWordBits lowerWord) (hleft : left.output (BinaryExplicitAffineRows.affineCellQuery row column source) = BinaryModularReductionTM.finiteWordBits leftWord) (hright : right.output (BinaryExplicitAffineRows.affineCellQuery row column source) = BinaryModularReductionTM.finiteWordBits rightWord) : sourcePhysicalLagrangeMultiplyWord lower left right (BinaryExplicitAffineRows.affineCellQuery row column source) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyMod lowerWord leftWord rightWord)

def GapCVP.BinaryFieldInverseTM.binarySourceFieldInverseQuery (lower operand source : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseTM.binarySourceFieldInverseQuery lower operand source = GapCVP.BinaryEncoding.lengthPrefixedWord lower ++ GapCVP.BinaryEncoding.lengthPrefixedWord operand ++ source

def GapCVP.BinaryFieldInverseTM.binarySourceFieldInverseSource (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseTM.binarySourceFieldInverseSource input = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix (GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix input)

noncomputable def GapCVP.BinaryFieldInverseTM.factor400BinarySourceFieldInverseSourceComputable : BitTM binarySourceFieldInverseSource

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryFieldInverseTM.factor400BinarySourceFieldInverseSource_query (lower operand source : List Bool) : binarySourceFieldInverseSource (binarySourceFieldInverseQuery lower operand source) = source

def GapCVP.BinaryFieldInverseTM.binarySourceFieldPowerCandidate (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryFieldInverseTM.factor400BinarySourceFieldPowerCandidateComputable (multiplyComputer : BitTM BinarySourceFieldMultiplicationTM.binarySourceMultiplyModWord) : BitTM binarySourceFieldPowerCandidate

GapCVP reduction support.

Equations

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

def GapCVP.BinaryFieldInverseTM.sourceFieldPowerStep {degree : ℕ} (lower operand current : Core.EffectiveBinaryField.Word degree) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseTM.sourceFieldPowerStep lower operand current = GapCVP.Core.EffectiveBinaryField.multiplyMod lower current operand

def GapCVP.BinaryFieldInverseTM.sourceFieldPowerIterate {degree : ℕ} (lower operand : Core.EffectiveBinaryField.Word degree) (steps : ℕ) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseTM.sourceFieldPowerIterate lower operand steps = (GapCVP.BinaryFieldInverseTM.sourceFieldPowerStep lower operand)^[steps] operand

theorem GapCVP.BinaryFieldInverseTM.factor400BinarySourceFieldPowerRotation_iterate {degree : ℕ} (lower current operand : Core.EffectiveBinaryField.Word degree) (source : List Bool) (steps : ℕ) : have anchor := binarySourceFieldInverseQuery (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits operand) source; (SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRecordRotationOutput binarySourceFieldPowerCandidate)^[steps] (BinaryEncoding.lengthPrefixedWord anchor ++ BinaryEncoding.lengthPrefixedWord (BinaryModularReductionTM.finiteWordBits current)) = BinaryEncoding.lengthPrefixedWord anchor ++ BinaryEncoding.lengthPrefixedWord (BinaryModularReductionTM.finiteWordBits ((sourceFieldPowerStep lower operand)^[steps] current))