GapCVP proof, part 10, continuation 02

def GapCVP.SourceMixedRadixMaskSelectedRankTaggedLowerLeftSourceTM.sourceQaryMaskRankTaggedLowerLeftEqualitySelection (first second : List Bool → List Bool) (input : List Bool) : List Bool

Prepend the equality marker for two computed words to the original input.

Equations

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

noncomputable def GapCVP.SourceMixedRadixMaskSelectedRankTaggedLowerLeftSourceTM.sourceQaryMaskRankTaggedLowerLeftEqualitySelectionComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (sourceQaryMaskRankTaggedLowerLeftEqualitySelection first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableScanStructuralFieldAccounting (input : List Bool) : 2 * (SourceFormulaStructuralDecoder.firstFieldContents input).length + (SourceFormulaStructuralDecoder.firstFieldSuffix input).length ≤ input.length

def GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList (formula : ThreeCNF) : List Literal

GapCVP reduction support.

Equations

• GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList formula = List.flatMap (fun (clause : GapCVP.ThreeClause) => [clause 0, clause 1, clause 2]) formula

theorem GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList_variables (formula : ThreeCNF) : List.map Prod.fst (sourceNormalizedVariableLiteralList formula) = SourceMachineCert.formulaVariables formula

def GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableRankQuery (variableIndex : ℕ) (formula : ThreeCNF) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableRankOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableRankComputable : BitTM sourceNormalizedVariableRankOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceNormalizedVariableRankScanTM.sourceNormalizedVariableRankOutput_valid (variableIndex : ℕ) (formula : ThreeCNF) : sourceNormalizedVariableRankOutput (sourceNormalizedVariableRankQuery variableIndex formula) = List.replicate (SourceMachineCert.variableRank formula variableIndex) true

def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceCounter : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceCounter = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceCounterComputable : BitTM compactFirstOccurrenceCounter

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceCounterComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceScanStep (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceScanFoldComputable : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput compactFirstOccurrenceScanStep)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceScanSeed (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceScanSeedComputable : BitTM compactFirstOccurrenceScanSeed

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactSourceOccurringVariableCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactSourceOccurringVariableCountUnaryComputable : BitTM compactSourceOccurringVariableCountUnary

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactRankPrefixIdentity.firstOccurrencePrefixCount (names : List ℕ) (bound : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactRankPrefixIdentity.firstOccurrencePrefixCount names bound = (List.filter (GapCVP.BinaryCompactRankPrefixIdentity.firstOccurrenceAt✝ names) (List.range bound)).length

theorem GapCVP.BinaryCompactRankPrefixIdentity.compactVariableRank_eq_firstOccurrencePrefixCount (formula : ThreeCNF) (name : ℕ) : BinarySourceVariableCompaction.compactVariableRank formula name = firstOccurrencePrefixCount (SourceMachineCert.formulaVariables formula) (SourceMachineCert.variableRank formula name)

def GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceValidState (formula : ThreeCNF) (counter ordinal : ℕ) (pending : List Literal) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceValidState_counter (formula : ThreeCNF) (counter ordinal : ℕ) (pending : List Literal) : compactFirstOccurrenceCounter (compactFirstOccurrenceValidState formula counter ordinal pending) = List.replicate counter true

theorem GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceScanSeed_valid (formula : ThreeCNF) : compactFirstOccurrenceScanSeed (BinaryEncoding.encodeThreeCNF formula) = compactFirstOccurrenceValidState formula 0 0 (SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList formula)

theorem GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactFirstOccurrenceValidState_iterate (formula : ThreeCNF) (index : ℕ) (hindex : index ≤ (SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList formula).length) : compactFirstOccurrenceScanStep^[index] (compactFirstOccurrenceValidState formula 0 0 (SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList formula)) = compactFirstOccurrenceValidState formula (BinaryCompactRankPrefixIdentity.firstOccurrencePrefixCount (SourceMachineCert.formulaVariables formula) index) index (List.drop index (SourceNormalizedVariableRankScanTM.sourceNormalizedVariableLiteralList formula))

theorem GapCVP.BinaryCompactSourceFirstOccurrenceTM.compactSourceOccurringVariableCountUnary_valid (formula : ThreeCNF) : compactSourceOccurringVariableCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (BinarySourceVariableCompaction.occurringVariableCount formula) true

def GapCVP.BinaryExplicitAffineRows.affineCellQuery (row column : ℕ) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRow : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRow = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRowComputable : BitTM sourceExplicitAffineCellRow

GapCVP reduction support.

Equations

• GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRowComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellColumn : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellColumn = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellColumnComputable : BitTM sourceExplicitAffineCellColumn

GapCVP reduction support.

Equations

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

def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSource : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSource = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSourceComputable : BitTM sourceExplicitAffineCellOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRow_query (row column : ℕ) (source : List Bool) : sourceExplicitAffineCellRow (affineCellQuery row column source) = List.replicate row true

@[simp]

theorem GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellColumn_query (row column : ℕ) (source : List Bool) : sourceExplicitAffineCellColumn (affineCellQuery row column source) = List.replicate column true

@[simp]

theorem GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSource_query (row column : ℕ) (source : List Bool) : sourceExplicitAffineCellOriginalSource (affineCellQuery row column source) = source

def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineXorBits (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineXorBits first second input = GapCVP.GaussianXorWorker.binaryGaussianXorHeadWord (first input ++ second input)

noncomputable def GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineXorBitsComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (sourceExplicitAffineXorBits first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineXorBits_valid (first second : List Bool → List Bool) (input : List Bool) (firstBit secondBit : Bool) (hfirst : first input = [firstBit]) (hsecond : second input = [secondBit]) : sourceExplicitAffineXorBits first second input = [firstBit ^^ secondBit]

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordRuntimeCompositionComputer {first second : List Bool → List Bool} (firstComputer : BitTM first) (secondComputer : BitTM second) : BitTM (second ∘ first)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordNaturalWriterComputer : BitTM fun (input : List Bool) => Computability.encodeNat input.length

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordNaturalWriterComputer = GapCVP.CLStructuralNaturalBinaryWriter.structuralNaturalBinaryWriterComputable

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordDropHeadComputer : BitTM List.tail

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordDropHeadComputer = GapCVP.SourceFormulaStructuralDecoder.dropHeadComputable

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordCellOriginalSourceComputer : BitTM BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSource

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordCellOriginalSourceComputer = GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSourceComputable

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalCellGridWordTM.physicalCellGridPrefixComputer : BitTM BinaryEncoding.lengthPrefixedWord

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalCellGridWordTM.physicalCellGridPrefixComputer = GapCVP.CLStructuralPrefixWriter.structuralPrefixWriterComputable

@[irreducible]

noncomputable def GapCVP.BinaryPhysicalCellGridWordTM.physicalCellGridAppendComputer {first second : List Bool → List Bool} (firstComputer : BitTM first) (secondComputer : BitTM second) : BitTM fun (input : List Bool) => first input ++ second input

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalCellGridWordTM.physicalCellGridAppendComputer firstComputer secondComputer = GapCVP.CNFFlatPhysicalBinaryAppendTM.pointwiseAppendComputable firstComputer secondComputer

def GapCVP.BinaryRadiusTM.squareRootAccumulator (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryRadiusTM.squareRootAccumulator input = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input

noncomputable def GapCVP.BinaryRadiusTM.squareRootAccumulatorComputable : BitTM squareRootAccumulator

GapCVP reduction support.

Equations

• GapCVP.BinaryRadiusTM.squareRootAccumulatorComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryRadiusTM.squareRootTarget (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryRadiusTM.squareRootTarget input = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents (GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix input)

noncomputable def GapCVP.BinaryRadiusTM.squareRootTargetComputable : BitTM squareRootTarget

GapCVP reduction support.

Equations

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

def GapCVP.BinaryRadiusTM.squareRootAnchor (target : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryRadiusTM.squareRootAnchor target = GapCVP.BinaryEncoding.lengthPrefixedWord target ++ target

def GapCVP.BinaryRadiusTM.squareRootFoldPreparation (target : 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.BinaryRadiusTM.squareRootFoldPreparationComputable {target : List Bool → List Bool} (computer : BitTM target) : BitTM (squareRootFoldPreparation target)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryRadiusTM.ceilSquareRootAtomicRationalOutput (target : 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.BinaryRadiusTM.ceilSquareRootAtomicRationalComputable {target : List Bool → List Bool} (computer : BitTM target) : BitTM (ceilSquareRootAtomicRationalOutput target)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryRadiusTM.ceilSquareRootAtomicRationalOutput_valid (target : List Bool → List Bool) (input : List Bool) (weight : ℕ) (hweight : target input = List.replicate weight true) : ceilSquareRootAtomicRationalOutput target input = BinaryEncoding.encodeAtomic ↑⌈√↑weight⌉₊

def GapCVP.GaussianPivotScheduleTM.binaryGaussianPivotWord (candidates : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianPivotScheduleTM.binaryGaussianPivotWord candidates = match List.findIdx? id candidates with | none => [false] | some index => true :: List.replicate index true

def GapCVP.GaussianPivotScheduleTM.tacticBinaryGaussianPivotStepTac : Lean.ParserDescr

Executes the binaryGaussianPivotStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.GaussianPivotScheduleTM.binaryGaussianPivotComputable : BitTM binaryGaussianPivotWord

GapCVP reduction support.

Equations

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

def GapCVP.GaussianPivotScheduleTM.effectiveGaussianPivotCandidates {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (column : Fin n) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianPivotScheduleTM.effectiveGaussianPivotCandidates state column = List.map (fun (row : Fin m) => decide (state.nextPivot ≤ ↑row ∧ state.system.check row column = 1)) (List.finRange m)

def GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotCandidateOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotRowQuery (eligible entry : Bool) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotRowQuery eligible entry source = eligible :: entry :: source

def GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotColumnWord (rows : List (Bool × Bool)) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotCandidateOutput_valid (rows : List (Bool × Bool)) (source : List Bool) : binaryGaussianPackedPivotCandidateOutput (binaryGaussianPackedPivotColumnWord rows source) = List.map (fun (row : Bool × Bool) => row.1 && row.2) rows

def GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianDynamicBranchOutput (selector : List Bool → Bool) (valid fallback : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianDynamicBranchOutput selector valid fallback input = if selector input = true then valid input else fallback input

noncomputable def GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianDynamicBranchComputable {selector : List Bool → Bool} {valid fallback : List Bool → List Bool} (selection : BitTM fun (input : List Bool) => selector input :: input) (hvalid : BitTM valid) (hfallback : BitTM fallback) : BitTM (binaryGaussianDynamicBranchOutput selector valid fallback)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianIndexedBatchOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianIndexedBatchComputable : BitTM binaryGaussianIndexedBatchOutput

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianPivotBatchStream (batches : List (List Bool)) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianPivotBatchStream batches = GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixOriginalSourceQueryStream batches

theorem GapCVP.GaussianAdaptivePivotStepTM.binaryGaussianIndexedBatchOutput_valid (batches : List (List Bool)) (suffix : List Bool) (index : ℕ) (hindex : index < batches.length) : binaryGaussianIndexedBatchOutput (OutputBoundedDependentRecordFold.unaryBoundedFoldWord index (binaryGaussianPivotBatchStream batches ++ suffix)) = batches[index]

def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankUnary (query : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankUnary query = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents query

noncomputable def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankUnaryComputable : BitTM structuralRankUnary

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankUnaryComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource (query : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource query = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix (GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix query)

noncomputable def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSourceComputable : BitTM structuralRankOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryGaussianStructuralAtomTM.structuralRankUnary_query (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : structuralRankUnary (BinaryStructuralRecordTM.constructiveStructuralRankQuery dimension input rank) = List.replicate rank true

@[simp]

theorem GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource_query (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : structuralRankOriginalSource (BinaryStructuralRecordTM.constructiveStructuralRankQuery dimension input rank) = input

def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankLessBit (bound : List Bool → List Bool) (query : List Bool) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankLessSelectionComputable {bound : List Bool → List Bool} (hbound : BitTM bound) : BitTM fun (query : List Bool) => structuralRankLessBit bound query :: query

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryGaussianStructuralAtomTM.structuralRankLessBit_valid (bound : List Bool → List Bool) (query : List Bool) (rank ceiling : ℕ) (hrank : structuralRankUnary query = List.replicate rank true) (hbound : bound query = List.replicate ceiling true) : structuralRankLessBit bound query = decide (rank < ceiling)

def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOneBound (_query : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOneBound _query = [true]

noncomputable def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOneBoundComputable : BitTM structuralRankOneBound

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOneBoundComputable = GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable [true]

def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankTwoBound (_query : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankTwoBound _query = [true, true]

noncomputable def GapCVP.BinaryGaussianStructuralAtomTM.structuralRankTwoBoundComputable : BitTM structuralRankTwoBound

GapCVP reduction support.

Equations

• GapCVP.BinaryGaussianStructuralAtomTM.structuralRankTwoBoundComputable = GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable [true, true]

theorem GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOneDecision_query (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : structuralRankLessBit structuralRankOneBound (BinaryStructuralRecordTM.constructiveStructuralRankQuery dimension input rank) = decide (rank < 1)

theorem GapCVP.BinaryGaussianStructuralAtomTM.structuralRankTwoDecision_query (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : structuralRankLessBit structuralRankTwoBound (BinaryStructuralRecordTM.constructiveStructuralRankQuery dimension input rank) = decide (rank < 2)

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceVectorStructuralRecords_getD {α : Type u_1} [Encodable α] (n : ℕ) (values : Fin n → α) (index : Fin n) : (SourceWholeOutputAssemblyTM.sourceVectorStructuralRecords n values).getD ↑index [] = BinaryEncoding.encodeAtomic (values index)

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceMatrixStructuralRecords_getD (m n : ℕ) (matrix : Fin m → Fin n → ℤ) (row : Fin m) (column : Fin n) : (SourceWholeOutputAssemblyTM.sourceMatrixStructuralRecords m n matrix).getD (↑row * n + ↑column) [] = BinaryEncoding.encodeAtomic (matrix row column)

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceLatticeStructuralRecords_getD_dimension (lattice : GapCVPInstance) : (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).getD 0 [] = BinaryEncoding.encodeAtomic lattice.dimension

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceLatticeStructuralRecords_getD_radius (lattice : GapCVPInstance) : (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).getD 1 [] = BinaryEncoding.encodeAtomic lattice.radius

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceLatticeStructuralRecords_getD_target (lattice : GapCVPInstance) (index : Fin lattice.dimension) : (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).getD (2 + ↑index) [] = BinaryEncoding.encodeAtomic (lattice.target index)

theorem GapCVP.BinaryGaussianStructuralRecordIndex.sourceLatticeStructuralRecords_getD_basis (lattice : GapCVPInstance) (row column : Fin lattice.dimension) : (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).getD (2 + lattice.dimension + ↑row * lattice.dimension + ↑column) [] = BinaryEncoding.encodeAtomic (lattice.basis row column)

def GapCVP.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryQuotient (dividend modulus : 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.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryQuotientComputable {dividend modulus : List Bool → List Bool} (hdividend : BitTM dividend) (hmodulus : BitTM modulus) : BitTM (sourcePhysicalComputedUnaryQuotient dividend modulus)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryQuotient_valid (dividend modulus : List Bool → List Bool) (input : List Bool) (first second : ℕ) (hpositive : 0 < second) (hdividend : dividend input = List.replicate first true) (hmodulus : modulus input = List.replicate second true) : sourcePhysicalComputedUnaryQuotient dividend modulus input = List.replicate (first / second) true

def GapCVP.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryRemainder (dividend modulus : 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.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryRemainderComputable {dividend modulus : List Bool → List Bool} (hdividend : BitTM dividend) (hmodulus : BitTM modulus) : BitTM (sourcePhysicalComputedUnaryRemainder dividend modulus)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalRowBasisDivisionTM.sourcePhysicalComputedUnaryRemainder_valid (dividend modulus : List Bool → List Bool) (input : List Bool) (first second : ℕ) (hpositive : 0 < second) (hdividend : dividend input = List.replicate first true) (hmodulus : modulus input = List.replicate second true) : sourcePhysicalComputedUnaryRemainder dividend modulus input = List.replicate (first % second) true

def GapCVP.GaussianPhysicalWordRankIndexTM.factor400PhysicalWordGaussianTargetCoordinateUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianPhysicalWordRankIndexTM.factor400PhysicalWordGaussianTargetCoordinateComputable : BitTM factor400PhysicalWordGaussianTargetCoordinateUnary

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianPhysicalWordRankIndexTM.factor400PhysicalWordGaussianTargetCoordinateUnary_query (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : factor400PhysicalWordGaussianTargetCoordinateUnary (BinaryStructuralRecordTM.constructiveStructuralRankQuery dimension input rank) = List.replicate (rank - 2) true

def GapCVP.GaussianReducedConsistencyTM.binaryGaussianReducedConsistencyWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianReducedConsistencyTM.binaryGaussianReducedConsistencyComputable : BitTM binaryGaussianReducedConsistencyWord

GapCVP reduction support.

Equations

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

def GapCVP.GaussianReducedConsistencyTM.effectiveGaussianReducedConsistencyQuery (system : Core.BinaryAffineSystem) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianReducedConsistencyTM.binaryGaussianReducedConsistencyWord_effective (system : Core.BinaryAffineSystem) (source : List Bool) : binaryGaussianReducedConsistencyWord (effectiveGaussianReducedConsistencyQuery system source) = [system.effectiveReducedConsistent]

theorem GapCVP.GaussianAdaptiveEliminationCorrectness.finRange_idxOfOption_eq_some {count : ℕ} (row : Fin count) : List.idxOf? row (List.finRange count) = some ↑row

theorem GapCVP.GaussianAdaptiveEliminationCorrectness.binaryGaussianPivotWord_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (column : Fin n) : GaussianPivotScheduleTM.binaryGaussianPivotWord (GaussianPivotScheduleTM.effectiveGaussianPivotCandidates state column) = match Core.EffectiveBinaryGaussian.findPivotOption state column with | none => [false] | some row => true :: List.replicate (↑row) true

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedCheckBits {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedRhsBits {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedRhsBits state = List.map (fun (row : Fin m) => decide (state.system.rhs row = 1)) (List.finRange m)

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStatePivotRowOption {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (column : Fin n) : Option (Fin m)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStatePivotWord {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (column : Fin n) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStateReducedConsistencyRows {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : List (Bool × Bool)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStateReducedConsistencyQuery {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStatePivotRow_effective (system : Core.BinaryAffineSystem) (column : Fin system.dimension) : effectiveGaussianStatePivotRowOption system.effectiveGaussianState column = system.effectivePivotRowOption column

theorem GapCVP.GaussianAdaptiveEliminationCorrectness.effectiveGaussianStateReducedConsistencyQuery_effective (system : Core.BinaryAffineSystem) (source : List Bool) : effectiveGaussianStateReducedConsistencyQuery system.effectiveGaussianState source = GaussianReducedConsistencyTM.effectiveGaussianReducedConsistencyQuery system source

theorem GapCVP.BinaryPhysicalWordEntries.binaryFieldParityMatrix_apply_basisCoordinate {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {degree fieldRowCount dimension : ℕ} (basis : Module.Basis (Fin degree) (ZMod 2) K) (checks : Matrix (Fin fieldRowCount) (Fin dimension) K) (row : Fin fieldRowCount) (coordinate : Fin degree) (column : Fin dimension) : Core.binaryFieldParityMatrix basis checks (row, coordinate) column = basis.equivFun (checks row column) coordinate

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldQuery (lower left right source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLowerBits : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLowerBits = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLeftBits : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLeftBits = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceRightBits : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldSuffix : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceLowerBitsComputable : BitTM factor400BinarySourceLowerBits

GapCVP reduction support.

Equations

• GapCVP.BinarySourceFieldMultiplicationTM.binarySourceLowerBitsComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceLeftBitsComputable : BitTM factor400BinarySourceLeftBits

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceRightBitsComputable : BitTM factor400BinarySourceRightBits

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldSuffixComputable : BitTM factor400BinarySourceFieldSuffix

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLowerBits_query (lower left right source : List Bool) : factor400BinarySourceLowerBits (factor400BinarySourceFieldQuery lower left right source) = lower

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceLeftBits_query (lower left right source : List Bool) : factor400BinarySourceLeftBits (factor400BinarySourceFieldQuery lower left right source) = left

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceRightBits_query (lower left right source : List Bool) : factor400BinarySourceRightBits (factor400BinarySourceFieldQuery lower left right source) = right

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourceFieldSuffix_query (lower left right source : List Bool) : factor400BinarySourceFieldSuffix (factor400BinarySourceFieldQuery lower left right source) = source

def GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourcePaddedWord (degree : ℕ) (bits : List Bool) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourcePaddedWord degree bits position = bits.getD (↑position) false

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinaryFiniteWordBits_length {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) : (BinaryModularReductionTM.finiteWordBits word).length = degree

@[simp]

theorem GapCVP.BinarySourceFieldMultiplicationTM.factor400BinarySourcePaddedWord_finiteWordBits {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) : factor400BinarySourcePaddedWord degree (BinaryModularReductionTM.finiteWordBits word) = word

def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceMultiplyModWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySourceFieldMultiplicationTM.binarySourceMultiplyModWord_valid {degree : ℕ} (lower left right : Core.EffectiveBinaryField.Word degree) (source : List Bool) : binarySourceMultiplyModWord (factor400BinarySourceFieldQuery (BinaryModularReductionTM.finiteWordBits lower) (BinaryModularReductionTM.finiteWordBits left) (BinaryModularReductionTM.finiteWordBits right) source) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyMod lower left right)

def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductAccumulator (state : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductAccumulatorComputable : BitTM sourcePhysicalLagrangeProductAccumulator

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductFoldOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductFoldComputable (multiplyComputer : BitTM BinarySourceFieldMultiplicationTM.binarySourceMultiplyModWord) : BitTM sourcePhysicalLagrangeProductFoldOutput

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangePackedFactorWords {degree : ℕ} (factors : List (Core.EffectiveBinaryField.Word degree)) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductSourceAnchor {degree : ℕ} (lower : Core.EffectiveBinaryField.Word degree) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductFoldWord {degree : ℕ} (lower initial : Core.EffectiveBinaryField.Word degree) (factors : List (Core.EffectiveBinaryField.Word degree)) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangeProductFoldOutput_valid {degree : ℕ} (lower initial : Core.EffectiveBinaryField.Word degree) (factors : List (Core.EffectiveBinaryField.Word degree)) (source : List Bool) : sourcePhysicalLagrangeProductFoldOutput (sourcePhysicalLagrangeProductFoldWord lower initial factors source) = BinaryEncoding.lengthPrefixedWord (sourcePhysicalLagrangeProductSourceAnchor lower source) ++ BinaryEncoding.lengthPrefixedWord (BinaryModularReductionTM.finiteWordBits (List.foldl (Core.EffectiveBinaryField.multiplyMod lower) initial factors))

def GapCVP.BinaryFieldInverseAlgebra.zeroWord (degree : ℕ) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseAlgebra.zeroWord degree x✝ = false

def GapCVP.BinaryFieldInverseAlgebra.oneWord (degree : ℕ) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseAlgebra.oneWord degree bit = decide (↑bit = 0)

theorem GapCVP.BinaryFieldInverseAlgebra.wordPolynomial_zeroWord (degree : ℕ) : Core.EffectiveBinaryField.wordPolynomial (zeroWord degree) = 0

theorem GapCVP.BinaryFieldInverseAlgebra.wordPolynomial_shiftXor {e : ℕ} (lower : Core.EffectiveBinaryField.Word e) (degree : ℕ) (word : Core.EffectiveBinaryField.Word (2 * e)) (hdegree : e ≤ degree ∧ degree < 2 * e) : Core.EffectiveBinaryField.wordPolynomial (Core.EffectiveBinaryField.shiftXor lower degree word) = Core.EffectiveBinaryField.wordPolynomial word + Polynomial.X ^ (degree - e) * Core.EffectiveBinaryField.wordPolynomial lower

def GapCVP.BinaryFieldInverseAlgebra.reducePrefix {e : ℕ} (lower : Core.EffectiveBinaryField.Word e) (count : ℕ) (word : Core.EffectiveBinaryField.Word (2 * e)) : Core.EffectiveBinaryField.Word (2 * e)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryFieldInverseAlgebra.reducePrefix_succ {e : ℕ} (lower : Core.EffectiveBinaryField.Word e) (count : ℕ) (word : Core.EffectiveBinaryField.Word (2 * e)) : reducePrefix lower (count + 1) word = Core.EffectiveBinaryField.reduceAt lower (2 * e - 1 - count) (reducePrefix lower count word)

def GapCVP.BinaryFieldInverseAlgebra.truncateWord {e : ℕ} (word : Core.EffectiveBinaryField.Word (2 * e)) : Core.EffectiveBinaryField.Word e

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseAlgebra.truncateWord word i = word ⟨↑i, ⋯⟩

noncomputable def GapCVP.BinaryFieldInverseAlgebra.sourceWordValue (encodingLength : ℕ) (formula : Core.Formula) (word : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) : Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryFieldInverseAlgebra.sourceWordValue_oneWord (encodingLength : ℕ) (formula : Core.Formula) : sourceWordValue encodingLength formula (oneWord (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) = 1

theorem GapCVP.BinaryFieldInverseAlgebra.sourceWordValue_multiplyMod (encodingLength : ℕ) (formula : Core.Formula) (left right : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) : sourceWordValue encodingLength formula (Core.EffectiveBinaryField.multiplyMod (Core.EffectiveBinaryField.irreducibleWord (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) left right) = sourceWordValue encodingLength formula left * sourceWordValue encodingLength formula right

def GapCVP.BinaryFieldInverseAlgebra.sourceWordPow {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) : ℕ → Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.BinaryFieldInverseAlgebra.sourceWordPow word 0 = GapCVP.BinaryFieldInverseAlgebra.oneWord degree

theorem GapCVP.BinaryFieldInverseAlgebra.sourceWordValue_sourceWordPow (encodingLength : ℕ) (formula : Core.Formula) (word : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) (power : ℕ) : sourceWordValue encodingLength formula (sourceWordPow word power) = sourceWordValue encodingLength formula word ^ power

def GapCVP.BinaryFieldInverseAlgebra.sourceInverseWord {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldInverseAlgebra.sourceInverseWord word = GapCVP.BinaryFieldInverseAlgebra.sourceWordPow word (2 ^ degree - 2)

theorem GapCVP.BinaryFieldInverseAlgebra.sourceWordValue_sourceInverseWord (encodingLength : ℕ) (formula : Core.Formula) (word : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) (hnonzero : sourceWordValue encodingLength formula word ≠ 0) : sourceWordValue encodingLength formula (sourceInverseWord word) = (sourceWordValue encodingLength formula word)⁻¹