GapCVP proof, part 14, continuation 02

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

Encode the number of irreducibility candidates in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleCandidateCardinalityComputable : BitTM sourceIrreducibleCandidateCardinalityUnary

GapCVP reduction support.

Equations

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

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

Compute the encoded width of an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairWidthComputable : BitTM paperVariableAritySourceIrreducibleFactorPairWidthOutput

GapCVP reduction support.

Equations

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

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

Encode the number of irreducibility factor pairs in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairCardinalityComputable : BitTM sourceIrreducibleFactorPairCardinalityUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairDivisionQuery (input : List Bool) : List Bool

Prepare the division query for an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairDivisionQueryComputable : BitTM sourceIrreducibleFactorPairDivisionQuery

GapCVP reduction support.

Equations

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

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

Decode a factor-pair index into a mixed-radix row-major pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairOdometerComputable : BitTM sourceIrreducibleFactorPairOdometer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairFirstRank (input : List Bool) : List Bool

Read the first factor rank from a factor-pair state.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairFirstRankComputable : BitTM sourceIrreducibleFactorPairFirstRank

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairSecondRank (input : List Bool) : List Bool

Read the second factor rank from a factor-pair state.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairSecondRankComputable : BitTM sourceIrreducibleFactorPairSecondRank

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorRankQuery (rank : List Bool → List Bool) (input : List Bool) : List Bool

Prepare the query for a factor's rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorRankQueryComputable {rank : List Bool → List Bool} (computer : BitTM rank) : BitTM (sourceIrreducibleFactorRankQuery rank)

GapCVP reduction support.

Equations

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

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

Extract the lower word of an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairLowerWordComputable : BitTM sourceIrreducibleFactorPairLowerWord

GapCVP reduction support.

Equations

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

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

Extract the first word of an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairFirstWordComputable : BitTM sourceIrreducibleFactorPairFirstWord

GapCVP reduction support.

Equations

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

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

Extract the second word of an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairSecondWordComputable : BitTM sourceIrreducibleFactorPairSecondWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairProductQuery (input : List Bool) : List Bool

Prepare the product query for an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairProductQueryComputable : BitTM sourceIrreducibleFactorPairProductQuery

GapCVP reduction support.

Equations

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

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

Compute the product word of an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairProductWordComputable : BitTM sourceIrreducibleFactorPairProductWord

GapCVP reduction support.

Equations

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

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

Encode the degree of an irreducibility factor pair in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairDegreeUnaryComputable : BitTM sourceIrreducibleFactorPairDegreeUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWidthOutput (input : List Bool) : List Bool

Compute the width of the monic zero word.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWidthComputable : BitTM paperVariableAritySourceIrreducibleMonicZeroWidthOutput

GapCVP reduction support.

Equations

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

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

Construct the monic zero word for an irreducibility test.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWordComputable : BitTM sourceIrreducibleMonicZeroWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairMonicWord (input : List Bool) : List Bool

Construct the monic word for an irreducibility factor pair.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMonicWordComputable : BitTM sourceIrreducibleFactorPairMonicWord

GapCVP reduction support.

Equations

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

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

Mark factor pairs whose product equals the candidate monic word.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMarkerComputable : BitTM sourceIrreducibleFactorPairMarker

GapCVP reduction support.

Equations

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

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

Concatenate markers for enumerated factor pairs.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMarkerStreamComputable : BitTM sourceIrreducibleFactorPairMarkerStream

GapCVP reduction support.

Equations

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

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

Encode whether a proper irreducibility factor exists.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleProperFactorExistsComputable : BitTM paperVariableAritySourceIrreducibleProperFactorExistsWord

GapCVP reduction support.

Equations

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

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

Encode the absence of a proper factor.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleNoProperFactorComputable : BitTM sourceIrreducibleNoProperFactorWord

GapCVP reduction support.

Equations

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

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

Concatenate markers for actual irreducible candidates.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleCandidateMarkerStreamComputable : BitTM sourceActualIrreducibleCandidateMarkerStream

GapCVP reduction support.

Equations

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

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

Select the first marked irreducible candidate word.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleFirstCandidateComputable : BitTM sourceActualIrreducibleFirstCandidateWord

GapCVP reduction support.

Equations

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

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

Encode the selected irreducible candidate rank in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankComputable : BitTM sourceActualIrreducibleSelectedRankUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankQuery (input : List Bool) : List Bool

Prepare the selected irreducible candidate rank query.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankQueryComputable : BitTM paperVariableAritySourceActualIrreducibleSelectedRankQuery

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceSelectedIrreducibleWordComputable : BitTM sourceSelectedIrreducibleWord

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceSelectedIrreducibleWord_valid (formula : ThreeCNF) : sourceSelectedIrreducibleWord (BinaryEncoding.encodeThreeCNF formula) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.irreducibleWord (sourceIrreducibleFormulaDegree formula))

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixBasisRankComputer (degree : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixBasisRankComputer_query (degree : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (fieldDegree : ℕ) (positive : 0 < fieldDegree) (correctDegree : degree.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate fieldDegree true) : (physicalMatrixBasisRankComputer degree).output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (row % fieldDegree) true

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixFieldDegreeComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixFieldDegreeComputer_query (row column : ℕ) (formula : ThreeCNF) : physicalMatrixFieldDegreeComputer.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physDegree formula) true

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixSelectedBasisRankComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

• GapCVP.PhysicalMatrixCellTM.physicalMatrixSelectedBasisRankComputer = GapCVP.PhysicalMatrixCellTM.physicalMatrixBasisRankComputer GapCVP.PhysicalMatrixCellTM.physicalMatrixFieldDegreeComputer

@[simp]

theorem GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixSelectedBasisRankComputer_query (row column : ℕ) (formula : ThreeCNF) : physicalMatrixSelectedBasisRankComputer.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (row % PhysicalFamilyRowTM.physDegree formula) true

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixCoefficientBit (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalMatrixCellTM.physicalMatrixCoefficientBit basisRank coefficient = GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientCellBit basisRank coefficient

noncomputable def GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixCoefficientBitComputable (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalMatrixCoefficientBit basisRank coefficient)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixCoefficientBit_valid {degree : ℕ} (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (word : Core.EffectiveBinaryField.Word degree) (position : ℕ) (bounded : position < degree) (correctRank : basisRank.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate position true) (correctCoefficient : coefficient.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits word) : physicalMatrixCoefficientBit basisRank coefficient (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [word ⟨position, bounded⟩]

def GapCVP.PhysicalMatrixCellTM.physicalMatrixGuardedFourFamilyCheck (global refinement ordinary shifted : 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.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixGuardedFourFamilyCheckComputable (global refinement ordinary shifted : List Bool → List Bool) (globalComputer : BitTM global) (refinementComputer : BitTM refinement) (ordinaryComputer : BitTM ordinary) (shiftedComputer : BitTM shifted) : BitTM (physicalMatrixGuardedFourFamilyCheck global refinement ordinary shifted)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixGuardedFourFamilyCheck_valid (global refinement ordinary shifted : List Bool → List Bool) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) (correctGlobal : global (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (↑row < PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctRefinement : refinement (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctOrdinary : ordinary (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctShifted : shifted (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ ↑row) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) : physicalMatrixGuardedFourFamilyCheck global refinement ordinary shifted (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]

noncomputable def GapCVP.PhysicalMatrixCellTM.paperVariableArityCanonicalPhysicalMatrixCellComputerOfCheck (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (check : List Bool → List Bool) (checkComputer : BitTM check) (correctCheck : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), check (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientFieldCardinalityUnary : List Bool → List Bool

Encode the physical coefficient field cardinality in unary form.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalCoefficientFieldCardinalityUnaryComputable : BitTM physicalCoefficientFieldCardinalityUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientGridCardinalityUnary : List Bool → List Bool

Encode the physical coefficient grid cardinality in unary form.

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalCoefficientGridCardinalityUnaryComputable : BitTM physicalCoefficientGridCardinalityUnary

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientFieldCardinality_pos (formula : ThreeCNF) : 0 < PhysicalFamilyRowTM.physFieldCard formula

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientGridCardinality_pos (formula : ThreeCNF) : 0 < PhysicalFamilyRowTM.physGridCard formula

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalColumnFieldValueRankUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnFieldValueRankUnaryComputable : BitTM physicalColumnFieldValueRankUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnFieldValueRankUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalColumnFieldValueRankUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (column % PhysicalFamilyRowTM.physFieldCard formula) true

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalColumnGridRankUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalColumnGridRankUnaryComputable : BitTM physicalColumnGridRankUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnGridRankUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalColumnGridRankUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (column / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula) true

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalColumnTypeRankUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnTypeRankUnaryComputable : BitTM physicalColumnTypeRankUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnTypeRankUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalColumnTypeRankUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (column / PhysicalFamilyRowTM.physFieldCard formula / PhysicalFamilyRowTM.physGridCard formula) true

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalGlobalRowFieldRankUnary : List Bool → List Bool

Encode a global row's field rank in unary form.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalRowFieldRankUnaryComputable : BitTM physicalGlobalRowFieldRankUnary

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientUnaryEquality (first second : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientUnaryEquality first second = GapCVP.SourceMixedRadixMaskSelectedRankTaggedSquareBasisPairTM.maskComputedWordEquality first second

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalCoefficientUnaryEqualityComputable {first second : List Bool → List Bool} (firstComputer : BitTM first) (secondComputer : BitTM second) : BitTM (physicalCoefficientUnaryEquality first second)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientUnaryEquality_valid (first second : List Bool → List Bool) (input : List Bool) (left right : ℕ) (firstValid : first input = List.replicate left true) (secondValid : second input = List.replicate right true) : physicalCoefficientUnaryEquality first second input = [decide (left = right)]

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalGlobalFamilyCoefficientWord : List Bool → List Bool

Compute a coefficient word for the global physical family.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalFamilyCoefficientWordComputable : BitTM physicalGlobalFamilyCoefficientWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalGlobalCheckBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalCheckBitComputable : BitTM physicalGlobalCheckBit

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalColumnOrderProjection.paperVariableAritySourceCoordinateFieldWordRank (encodingLength : ℕ) (formula : ThreeCNF) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) : ↑((BinarySourceCoordinateOrder.sourceFormulaFieldCardOrder encodingLength (FormulaBridge.srcFormula formula)).symm ((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).2.2) = ↑column % Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula))

theorem GapCVP.PhysicalColumnOrderProjection.sourceCoordinateGridWordRank (encodingLength : ℕ) (formula : ThreeCNF) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) : ↑((BinarySourceCoordinateOrder.sourceFormulaGridOrder encodingLength (FormulaBridge.srcFormula formula)).symm ((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).2.1) = ↑column / Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) % (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula)).card

theorem GapCVP.PhysicalColumnOrderProjection.sourceCoordinateTypeWordRank (encodingLength : ℕ) (formula : ThreeCNF) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) : ↑((SourceOrder.sourceTypeCardWordOrder formula).symm ((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).1) = ↑column / Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) / (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula)).card

theorem GapCVP.PhysicalColumnOrderProjection.physicalFormulaFieldCardinality_eq_card (formula : ThreeCNF) : Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)) = PhysicalFamilyRowTM.physFieldCard formula

theorem GapCVP.PhysicalColumnOrderProjection.physicalFormulaGridCardinality_eq_card (formula : ThreeCNF) : (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).card = PhysicalFamilyRowTM.physGridCard formula

theorem GapCVP.PhysicalGlobalCoefficientCorrectness.paperVariableArityPhysicalGlobalCheckBit_valid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : PhysicalGlobalRefinementCoefficientTM.physicalGlobalCheckBit (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (↑row < PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]

theorem GapCVP.PhysicalRefinementRowProjection.physicalRefinementGridCard_eq (formula : ThreeCNF) : Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)) = PhysicalFamilyRowTM.physGridCard formula

@[reducible, inline]

abbrev GapCVP.PhysicalRefinementRowProjection.physicalRefinementBlockWidth (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalRefinementRowProjection.physicalRefinementDegree_pos (formula : ThreeCNF) : 0 < PhysicalFamilyRowTM.physDegree formula

theorem GapCVP.PhysicalRefinementRowProjection.physicalRefinementGridCard_pos (formula : ThreeCNF) : 0 < PhysicalFamilyRowTM.physGridCard formula

theorem GapCVP.PhysicalRefinementRowProjection.physicalRefinementFamilySourceBlockCount (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) : SourceOrder.paperExplicitBinaryFamilyBlockCount (BinaryEncoding.encodeThreeCNF formula).length formula (PhysicalRowOrderProjection.physicalRefinementFamilyIndex (BinaryEncoding.encodeThreeCNF formula).length formula clause) = physicalRefinementBlockWidth formula

def GapCVP.SourceClausePrefixBridge.sourceRetainedPrefixIndex (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) (index : Fin ↑clause) : Fin (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula))

GapCVP reduction support.

Equations

• GapCVP.SourceClausePrefixBridge.sourceRetainedPrefixIndex formula clause index = Fin.cast ⋯ (Fin.castLE ⋯ index)

theorem GapCVP.SourceClausePrefixBridge.paperVariableAritySourceDependentClausePrefix_eq_weightSum (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) : ∑ index : Fin ↑clause, (2 ^ SourceOrder.paperFormulaClauseWidth formula (Fin.castLE ⋯ index) - 1) = ClauseOffsetTM.sourceClauseWeightSum (List.take (↑clause) (BinarySourceTautologyNormalizationExact.noTautClauses formula))

theorem GapCVP.PhysicalRefinementColumnTagSourceCorrectness.paperVariableAritySourceLocalTypeWordRank (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) (tuple : ((FormulaBridge.srcFormula formula).clauses.get clause).SatisfyingLocalTuple) : ↑((SourceOrder.sourceTypeCardWordOrder formula).symm (Sum.inr ⟨clause, tuple⟩)) = 1 + ↑(finSigmaFinEquiv ⟨clause, (SourceOrder.paperFormulaClauseTupleWordOrder formula clause).symm tuple⟩)

noncomputable def GapCVP.RefinementClauseOffsetTM.paperRefinementClauseRankEnvelope (formula : ThreeCNF) (rank : ℕ) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixRankWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixRankWidth_output (input : List Bool) : paperRefinementPrefixRankWidth.output input = SourceFormulaStructuralDecoder.firstFieldContents input

The refinement prefix-width computer reads the leading unary field.

noncomputable def GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixRankEnvelope (formula : ThreeCNF) (outer inner : ℕ) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixIndexedClauseQuery (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixIndexedClauseQueryComputable : BitTM paperRefinementPrefixIndexedClauseQuery

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixIndexedClauseQuery_valid (formula : ThreeCNF) (outer inner : ℕ) : paperRefinementPrefixIndexedClauseQuery (paperRefinementPrefixRankEnvelope formula outer inner) = SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseQuery inner (BinarySourceTautologyNormalizationExact.noTautClauses formula)

def GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixIndexedClauseWeightUnary : List Bool → List Bool

Encode the indexed clause weight in a refinement prefix.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixIndexedClauseWeightUnaryComputable : BitTM paperRefinementPrefixIndexedClauseWeightUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperRefinementClauseOffsetUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementClauseOffsetUnaryComputable : BitTM paperRefinementClauseOffsetUnary

GapCVP reduction support.

Equations

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

theorem GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementClauseOffsetUnary_valid (formula : ThreeCNF) (rank : ℕ) (hbound : rank ≤ List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : paperRefinementClauseOffsetUnary (paperRefinementClauseRankEnvelope formula rank) = List.replicate (ClauseOffsetTM.sourceClauseWeightSum (List.take rank (BinarySourceTautologyNormalizationExact.noTautClauses formula))) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowLocalRankUnary : List Bool → List Bool

Encode the refinement row's local rank in unary form.

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowLocalRankUnaryComputable : BitTM physicalRefinementRowLocalRankUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowFieldQuotientUnary : List Bool → List Bool

Encode the refinement row's field quotient in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldQuotientUnaryComputable : BitTM physicalRefinementRowFieldQuotientUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldQuotientUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementRowFieldQuotientUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((row - PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) / PhysicalFamilyRowTM.physDegree formula) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowFieldValueRankUnary : List Bool → List Bool

Encode the refinement row's field-value rank in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldValueRankUnaryComputable : BitTM physicalRefinementRowFieldValueRankUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldValueRankUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementRowFieldValueRankUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((row - PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) / PhysicalFamilyRowTM.physDegree formula % PhysicalFamilyRowTM.physFieldCard formula) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowGridQuotientUnary : List Bool → List Bool

Encode the refinement row's grid quotient in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowGridQuotientUnaryComputable : BitTM physicalRefinementRowGridQuotientUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowGridQuotientUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementRowGridQuotientUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((row - PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) / PhysicalFamilyRowTM.physDegree formula / PhysicalFamilyRowTM.physFieldCard formula) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowGridRankUnary : List Bool → List Bool

Encode the refinement row's grid rank in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowGridRankUnaryComputable : BitTM physicalRefinementRowGridRankUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseRankUnary : List Bool → List Bool

Encode the refinement clause rank in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseRankUnaryComputable : BitTM physicalRefinementClauseRankUnary

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowClauseRank (row : ℕ) (formula : ThreeCNF) : ℕ

Compute the clause rank of a physical refinement row.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseRankEnvelopeOutput (input : List Bool) : List Bool

Construct the refinement clause-rank envelope word.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseRankEnvelopeOutputComputable : BitTM physicalRefinementClauseRankEnvelopeOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseRankEnvelopeOutput_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementClauseRankEnvelopeOutput (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = RefinementClauseOffsetTM.paperRefinementClauseRankEnvelope formula (physicalRefinementRowClauseRank row formula)

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseOffsetUnary : List Bool → List Bool

Encode the refinement clause offset in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseOffsetUnaryComputable : BitTM physicalRefinementClauseOffsetUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseWidthUnary : List Bool → List Bool

Encode the refinement clause width in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseWidthUnaryComputable : BitTM physicalRefinementClauseWidthUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementColumnLocalTagUnary : List Bool → List Bool

Encode the refinement column's local tag in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementColumnLocalTagUnaryComputable : BitTM physicalRefinementColumnLocalTagUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementColumnLocalTagUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementColumnLocalTagUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (column / PhysicalFamilyRowTM.physFieldCard formula / PhysicalFamilyRowTM.physGridCard formula - 1) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseLocalTagUpperUnary : List Bool → List Bool

Encode the upper local tag for a refinement clause.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseLocalTagUpperUnaryComputable : BitTM physicalRefinementClauseLocalTagUpperUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseLocalTagUpperUnary_query (row column : ℕ) (formula : ThreeCNF) (hbound : physicalRefinementRowClauseRank row formula < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : physicalRefinementClauseLocalTagUpperUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (ClauseOffsetTM.sourceClauseWeightSum (List.take (physicalRefinementRowClauseRank row formula) (BinarySourceTautologyNormalizationExact.noTautClauses formula)) + ClauseOffsetTM.sourceClauseWeight (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨physicalRefinementRowClauseRank row formula, hbound⟩)) true

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagBelowPrefixBit : List Bool → List Bool

Test whether the local tag lies below the prefix boundary.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagBelowPrefixBitComputable : BitTM physicalRefinementLocalTagBelowPrefixBit

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagBelowUpperBit : List Bool → List Bool

Test whether the local tag lies below the upper boundary.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagBelowUpperBitComputable : BitTM physicalRefinementLocalTagBelowUpperBit

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagMarker : List Bool → List Bool

Mark a local tag inside the refinement interval.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagMarkerComputable : BitTM physicalRefinementLocalTagMarker

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementColumnTypeRank (column : ℕ) (formula : ThreeCNF) : ℕ

Compute the type rank of a physical refinement column.

Equations

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

def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementSourceLocalTagInRange (row column : ℕ) (formula : ThreeCNF) (hbound : PhysicalRefinementClauseLocalTagTM.physicalRefinementRowClauseRank row formula < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : Bool

Test whether a source local tag is in refinement range.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementGridMatchBit : List Bool → List Bool

Test whether a refinement grid coordinate matches.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementGridMatchBitComputable : BitTM physicalRefinementGridMatchBit

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementFieldValueMatchBit : List Bool → List Bool

Test whether a refinement field value matches.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementFieldValueMatchBitComputable : BitTM physicalRefinementFieldValueMatchBit

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementAllowedTypeBit : List Bool → List Bool

Test whether a refinement type is allowed.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementAllowedTypeBitComputable : BitTM physicalRefinementAllowedTypeBit

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementFamilyCoefficientWord : List Bool → List Bool

Compute the coefficient word for a refinement family.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementFamilyCoefficientWordComputable : BitTM physicalRefinementFamilyCoefficientWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementFamilyCoefficientWord_query (row column : ℕ) (formula : ThreeCNF) (hbound : PhysicalRefinementClauseLocalTagTM.physicalRefinementRowClauseRank row formula < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : physicalRefinementFamilyCoefficientWord (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (column / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula = (row - PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) / PhysicalFamilyRowTM.physDegree formula / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula) && (decide (column % PhysicalFamilyRowTM.physFieldCard formula = (row - PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) / PhysicalFamilyRowTM.physDegree formula % PhysicalFamilyRowTM.physFieldCard formula) && (decide (physicalRefinementColumnTypeRank column formula = 0) || decide (physicalRefinementSourceLocalTagInRange row column formula hbound = true)))]

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementCheckBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementCheckBitComputable : BitTM physicalRefinementCheckBit

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalRefinementGuardAbsorption.paperVariableArityPhysicalRefinementCheckBit_valid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : PhysicalRefinementCheckSourceCorrectness.physicalRefinementCheckBit (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]

@[reducible, inline]

abbrev GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.physicalFieldFormulaDegree (formula : ThreeCNF) : ℕ

Compute the physical field degree associated with a formula.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableArityPhysicalSourceWordValue_injective (encodingLength : ℕ) (formula : Core.Formula) : Function.Injective (BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula)

def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableAritySourceSelectedFieldOperandQuery (operand source : List Bool) : List Bool

Prepare the operand query for a selected source-field value.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.sourceSelectedFieldInverseWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableAritySourceSelectedFieldInverseComputable : BitTM sourceSelectedFieldInverseWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableAritySourceSelectedFieldInverseWord_valid (formula : ThreeCNF) (operand : Core.EffectiveBinaryField.Word (physicalFieldFormulaDegree formula)) : sourceSelectedFieldInverseWord (paperVariableAritySourceSelectedFieldOperandQuery (BinaryModularReductionTM.finiteWordBits operand) (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.sourceInverseWord operand)

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.physicalCellInverseWord (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableArityPhysicalCellInverseComputer (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableArityPhysicalCellInverseComputer_output (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : (paperVariableArityPhysicalCellInverseComputer operand).output input = physicalCellInverseWord operand input

The physical cell inverse computer returns the declared inverse word.

@[simp]

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableArityPhysicalCellInverseWord_valid (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (value : Core.EffectiveBinaryField.Word (physicalFieldFormulaDegree formula)) (hvalue : operand.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits value) : physicalCellInverseWord operand (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.sourceInverseWord value)

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.physicalCellFieldWordAt (rank : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.physicalCellFieldWordAtComputable (rank : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalCellFieldWordAt rank)

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.physicalCellFieldWordAt_valid (rank : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (index : Fin (2 ^ Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)) (hrank : rank.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (↑index) true) : physicalCellFieldWordAt rank (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryFieldBasis.indexedWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) index)

def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorValue {degree : ℕ} (left right : Core.EffectiveBinaryField.Word degree) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorValue left right position = (left position ^^ right position)

theorem GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorValue_sourceWordValue_sub (encodingLength : ℕ) (formula : Core.Formula) (left right : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) : BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula (compactPhysicalFieldWordXorValue left right) = BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula left - BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula right

def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCell : List Bool → List Bool

Read the original cell for a compact field-word XOR.

Equations

• GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCell = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCellComputable : BitTM compactPhysicalFieldWordXorOriginalCell

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateOperand (worker : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Read the candidate operand for a compact field-word XOR.

Equations

• GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateOperand worker = worker.output ∘ GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCell

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateOperandComputable (worker : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldWordXorCandidateOperand worker)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateBit (worker : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Compute a candidate bit for the compact field-word XOR.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateBitComputable (worker : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldWordXorCandidateBit worker)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidate (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Construct the candidate compact field-word XOR output.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorCandidateComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldWordXorCandidate left right)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorWithDegree (degree left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorWithDegreeComputable (degree left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldWordXorWithDegree degree left right)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorWithDegree_valid (degreeWorker left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) (degree : ℕ) (leftWord rightWord : Core.EffectiveBinaryField.Word degree) (hdegree : degreeWorker.output input = List.replicate degree true) (hleft : left.output input = BinaryModularReductionTM.finiteWordBits leftWord) (hright : right.output input = BinaryModularReductionTM.finiteWordBits rightWord) : compactPhysicalFieldWordXorWithDegree degreeWorker left right input = BinaryModularReductionTM.finiteWordBits (compactPhysicalFieldWordXorValue leftWord rightWord)

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeNodeFactorCatalogue (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeNodeFactorQuery (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeNodeFactorCatalogue_valid (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) (count : ℕ) (hwidth : width.output input = List.replicate count true) : compactPhysicalLagrangeNodeFactorCatalogue width factor input = List.flatMap (fun (rank : ℕ) => BinaryEncoding.lengthPrefixedWord (factor.output (compactPhysicalLagrangeNodeFactorQuery width input rank))) (List.range count)

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeFactorProductPreparation (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (lower initial source factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

Prepare the product query for compact physical Lagrange factors.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeFactorProductPreparationComputable (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (lower initial source factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalLagrangeFactorProductPreparation width lower initial source factor)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeFactorProductWord (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (lower initial source factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeFactorProductComputable (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (lower initial source factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalLagrangeFactorProductWord width lower initial source factor)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalLagrangeFactorStreamTM.compactPhysicalLagrangeFactorProductWord_valid {degree : ℕ} (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (lower initial source factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) (lowerWord initialWord : Core.EffectiveBinaryField.Word degree) (factors : List (Core.EffectiveBinaryField.Word degree)) (original : List Bool) (hwidth : width.output input = List.replicate factors.length true) (hlower : lower.output input = BinaryModularReductionTM.finiteWordBits lowerWord) (hinitial : initial.output input = BinaryModularReductionTM.finiteWordBits initialWord) (hsource : source.output input = original) (hfactors : compactPhysicalLagrangeNodeFactorCatalogue width factor input = BinaryPhysicalLagrangeProductFoldTM.sourcePhysicalLagrangePackedFactorWords factors) : compactPhysicalLagrangeFactorProductWord width lower initial source factor input = BinaryModularReductionTM.finiteWordBits (List.foldl (Core.EffectiveBinaryField.multiplyMod lowerWord) initialWord factors)

@[reducible, inline]

abbrev GapCVP.PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord (formula : ThreeCNF) : Type

GapCVP reduction support.

Equations

• GapCVP.PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula = GapCVP.Core.EffectiveBinaryField.Word (GapCVP.PhysicalFamilyRowTM.physDegree formula)

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.physicalInterpolationDegreeWord : List Bool → List Bool

Read the field degree from the original source of a physical interpolation query.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDegreeWordComputable : BitTM physicalInterpolationDegreeWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.physicalInterpolationDifferenceWord (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Compute the field-word difference of the outputs of two interpolation computers.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDifferenceWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationDifferenceWord left right)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDifferenceComputer (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDifferenceComputer_output (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : (paperVariableArityPhysicalInterpolationDifferenceComputer left right).output = physicalInterpolationDifferenceWord left right

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDifferenceWord_valid (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (leftWord rightWord : PaperVariableArityPhysicalInterpolationWord formula) (hleft : left.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits leftWord) (hright : right.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits rightWord) : physicalInterpolationDifferenceWord left right (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorValue leftWord rightWord)

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationProductWord (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationProductWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (paperVariableArityPhysicalInterpolationProductWord left right)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationProductWord_valid (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (leftWord rightWord : PaperVariableArityPhysicalInterpolationWord formula) (hleft : left.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits leftWord) (hright : right.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits rightWord) : paperVariableArityPhysicalInterpolationProductWord left right (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyMod (Core.EffectiveBinaryField.irreducibleWord (PhysicalFamilyRowTM.physDegree formula)) leftWord rightWord)

def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationVariableCountWord : List Bool → List Bool

Encode the physical interpolation variable count.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationVariableCountWordComputable : BitTM physicalInterpolationVariableCountWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationShiftedVariableCountWord : List Bool → List Bool

Encode the shifted interpolation variable count.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationShiftedVariableCountWordComputable : BitTM physicalInterpolationShiftedVariableCountWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationShiftedVariableCountWord_valid (row column : ℕ) (formula : ThreeCNF) : physicalInterpolationShiftedVariableCountWord (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaVariableCount formula - 1) true

def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalOrdinaryNodePrefixWord (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalOrdinaryNodePrefixWord_valid (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (momentRank : ℕ) (hmoment : moment.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate momentRank true) : physicalOrdinaryNodePrefixWord moment (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaVariableCount formula * momentRank + 1) true

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalOrdinaryNodePrefixWidth (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalOrdinaryNodePrefixWidth_output (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : (physicalOrdinaryNodePrefixWidth moment).output = physicalOrdinaryNodePrefixWord moment

def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalShiftedNodePrefixWord (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalShiftedNodePrefixWord_valid (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (momentRank : ℕ) (hmoment : moment.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate momentRank true) : physicalShiftedNodePrefixWord moment (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((PhysicalFamilyRowTM.physicalFormulaVariableCount formula - 1) * momentRank + 1) true

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalShiftedNodePrefixWidth (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalShiftedNodePrefixWidth_output (moment : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : (physicalShiftedNodePrefixWidth moment).output = physicalShiftedNodePrefixWord moment

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationNodeParity (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) {term : List Bool → List Bool} (computer : BitTM term) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationNodeParity width computer = GapCVP.BinaryCompactPhysicalNodeParityTM.compactPhysicalNodeParity✝ width computer

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationNodeParityComputable (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) {term : List Bool → List Bool} (computer : BitTM term) : BitTM (physicalInterpolationNodeParity width computer)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationNodeParity_valid (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) {term : List Bool → List Bool} (computer : BitTM term) (input : List Bool) (count : ℕ) (value : ℕ → Bool) (hwidth : width.output input = List.replicate count true) (hterm : ∀ rank ∈ List.range count, term (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ SourceMixedRadixMaskSelectedFlatPreparationTM.sourceQaryMaskDynamicGridBaseSource width input) = [value rank]) : physicalInterpolationNodeParity width computer input = [List.foldl xor false (List.map value (List.range count))]

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (rank : ℕ) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRank : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRank = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRankComputable : BitTM compactPhysicalLagrangeNestedNodeRank

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRankComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOuterCell : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOuterCellComputable : BitTM compactPhysicalLagrangeNestedNodeOuterCell

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRank_query (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (rank : ℕ) (source : List Bool) : compactPhysicalLagrangeNestedNodeRank (compactPhysicalLagrangeNestedNodeEnvelope width rank source) = List.replicate rank true

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOuterCell_query (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (rank : ℕ) (source : List Bool) : compactPhysicalLagrangeNestedNodeOuterCell (compactPhysicalLagrangeNestedNodeEnvelope width rank source) = source

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOriginalSource : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOriginalSourceComputable : BitTM compactPhysicalLagrangeNestedNodeOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOriginalSource_query (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (node row column : ℕ) (formula : ThreeCNF) : compactPhysicalLagrangeNestedNodeOriginalSource (compactPhysicalLagrangeNestedNodeEnvelope width node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryEncoding.encodeThreeCNF formula

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherActualCell : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherActualCellComputable : BitTM compactPhysicalLagrangeNestedOtherActualCell

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherActualCell_query (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node : ℕ) (cell : List Bool) : compactPhysicalLagrangeNestedOtherActualCell (compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (compactPhysicalLagrangeNestedNodeEnvelope outerWidth node cell)) = cell

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherOriginalSource : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherOriginalSourceComputable : BitTM compactPhysicalLagrangeNestedOtherOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherOriginalSource_query (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node row column : ℕ) (formula : ThreeCNF) : compactPhysicalLagrangeNestedOtherOriginalSource (compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (compactPhysicalLagrangeNestedNodeEnvelope outerWidth node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = BinaryEncoding.encodeThreeCNF formula

def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRank : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRankComputable : BitTM compactPhysicalLagrangeNestedAnchorRank

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRank_query (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node : ℕ) (cell : List Bool) : compactPhysicalLagrangeNestedAnchorRank (compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (compactPhysicalLagrangeNestedNodeEnvelope outerWidth node cell)) = List.replicate node true

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeSourceWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherSourceWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherRankWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRankWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeSourceWordComputer_output (input : List Bool) : compactPhysicalLagrangeNestedNodeSourceWordComputer.output input = compactPhysicalLagrangeNestedNodeOriginalSource input

The nested node source computer returns its declared source word.

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherSourceWordComputer_output (input : List Bool) : compactPhysicalLagrangeNestedOtherSourceWordComputer.output input = compactPhysicalLagrangeNestedOtherOriginalSource input

The nested other-source computer returns its declared source word.

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherRankWordComputer_output (input : List Bool) : compactPhysicalLagrangeNestedOtherRankWordComputer.output input = compactPhysicalLagrangeNestedNodeRank input

The nested other-rank computer returns the encoded node rank.

theorem GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRankWordComputer_output (input : List Bool) : compactPhysicalLagrangeNestedAnchorRankWordComputer.output input = compactPhysicalLagrangeNestedAnchorRank input

The nested anchor-rank computer returns the encoded anchor rank.

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNodeProductTM.compactPhysicalLagrangeNestedNodePrefixWidth (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryCompactPhysicalLagrangeNodeProductTM.compactPhysicalLagrangeNestedNodePrefixWidth_valid (inner outer : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (node : ℕ) (cell : List Bool) : (compactPhysicalLagrangeNestedNodePrefixWidth inner).output (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outer node cell) = inner.output cell

theorem GapCVP.BinaryCompactPhysicalLagrangeMomentWeightTM.compactPhysicalLagrangeIndexedOneWord (degree : ℕ) (hdegree : 0 < degree) : BinaryFieldBasis.indexedWord degree ⟨1, ⋯⟩ = BinaryFieldInverseAlgebra.oneWord degree

def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyStart (family : Fin 4) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyStartUnary (family : Fin 4) : List Bool → List Bool

Encode the start index of a physical family in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyStartUnaryComputable (family : Fin 4) : BitTM (physicalFamilyStartUnary family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellDegreeUnary : List Bool → List Bool

Encode a physical moment cell's degree in unary form.

Equations

• GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellDegreeUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyRowTM.physicalFamilyFieldDegreeUnary

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellDegreeUnaryComputable : BitTM physicalMomentCellDegreeUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellGridCardinalityUnary : List Bool → List Bool

GapCVP reduction support.

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellGridCardinalityUnaryComputable : BitTM physicalMomentCellGridCardinalityUnary

GapCVP reduction support.

@[simp]

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellGridCardinalityUnary_valid (row column : ℕ) (formula : ThreeCNF) : physicalMomentCellGridCardinalityUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physGridCard formula) true

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellMomentCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellMomentCountUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyRowTM.physicalFamilyMomentCountUnary

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellMomentCountUnaryComputable : BitTM physicalMomentCellMomentCountUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellMomentCountUnary_valid (row column : ℕ) (formula : ThreeCNF) : physicalMomentCellMomentCountUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaMomentCount formula) true

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowLocalOffsetWord (family : Fin 4) : List Bool → List Bool

Encode the local offset of a physical family row.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowLocalOffsetComputable (family : Fin 4) : BitTM (physicalFamilyRowLocalOffsetWord family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowFieldRankWord (family : Fin 4) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowFieldRankComputable (family : Fin 4) : BitTM (physicalFamilyRowFieldRankWord family)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowFieldRankWord_valid (family : Fin 4) (row column : ℕ) (formula : ThreeCNF) : physicalFamilyRowFieldRankWord family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((row - physicalFamilyStart family formula) / PhysicalFamilyRowTM.physDegree formula) true

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowGridQuotientWord (family : Fin 4) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowGridQuotientComputable (family : Fin 4) : BitTM (physicalFamilyRowGridQuotientWord family)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowGridQuotientWord_valid (family : Fin 4) (row column : ℕ) (formula : ThreeCNF) : physicalFamilyRowGridQuotientWord family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate ((row - physicalFamilyStart family formula) / PhysicalFamilyRowTM.physDegree formula / PhysicalFamilyRowTM.physGridCard formula) true

def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowMoment (family : Fin 4) (row : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFieldMomentOperationsTM.physicalFormulaMomentCount_pos (formula : ThreeCNF) : 0 < PhysicalFamilyRowTM.physicalFormulaMomentCount formula

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowMomentRankWord (family : Fin 4) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowMomentRankComputable (family : Fin 4) : BitTM (physicalFamilyRowMomentRankWord family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowMomentRankComputer (family : Fin 4) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyRowMomentRankWord_valid (family : Fin 4) (row column : ℕ) (formula : ThreeCNF) : physicalFamilyRowMomentRankWord family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (physicalFamilyRowMoment family row formula) true

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyMomentPowerWord (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyMomentPowerComputable (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalFamilyMomentPowerWord family base)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFieldMomentOperationsTM.physicalFamilyMomentPowerComputer (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalFamilyMomentPowerWord_valid (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (value : Core.EffectiveBinaryField.Word (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)) (hvalue : base.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits value) : physicalFamilyMomentPowerWord family base (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.sourceWordPow value (physicalFamilyRowMoment family row formula))