GapCVP proof, part 14

theorem GapCVP.BinarySelectedIrreducibleWordOrderCorrectness.finiteWordBits_monicWord {degree : ℕ} (hdegree : 0 < degree) (lower : Core.EffectiveBinaryField.Word degree) : BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.monicWord lower) = BinaryModularReductionTM.finiteWordBits lower ++ ([true] ++ List.replicate (degree - 1) false)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.BinarySelectedIrreducibleWordOrderCorrectness.exists_first_source_irreducible_rank (degree : ℕ) (hdegree : 0 < degree) : ∃ (rank : Fin (2 ^ degree)), List.findIdx? id (BinarySelectedIrreducibleWordTM.binaryIndexedIrreducibleCandidateMarkers degree) = some ↑rank ∧ BinaryFieldBasis.indexedWord degree rank = Core.EffectiveBinaryField.irreducibleWord degree

Internal support shared across GapCVP continuation modules.

@[reducible, inline]

abbrev GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleRankDegreeUnary : List Bool → List Bool

Encode the irreducible candidate rank's degree in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleRankDegreeUnaryComputable : BitTM sourceIrreducibleRankDegreeUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleRankCoefficientWord : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleRankCoefficientWordComputable : BitTM sourceIrreducibleRankCoefficientWord

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleRankCoefficientWord_eq_indexedWord (formula : ThreeCNF) (rank : Fin (2 ^ sourceIrreducibleFormulaDegree formula)) (auxiliary : List Bool) : sourceIrreducibleRankCoefficientWord (BinaryEncoding.lengthPrefixedWord (List.replicate (↑rank) true) ++ BinaryEncoding.lengthPrefixedWord auxiliary ++ BinaryEncoding.encodeThreeCNF formula) = BinaryModularReductionTM.finiteWordBits (BinaryFieldBasis.indexedWord (sourceIrreducibleFormulaDegree formula) rank)

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleCandidateWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleCandidateWidth_output (input : List Bool) : sourceIrreducibleCandidateWidth.output input = PhysicalFamilyRowTM.physicalFamilyFieldCardinalityUnary input

Internal support shared across GapCVP continuation modules.