GapCVP proof, part 15

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.physicalInterpolationRowGridRankWord (family : Fin 4) : List Bool → List Bool

The unary grid rank of an interpolation row within its family.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.paperVariableArityPhysicalInterpolationRowGridRankWordComputable (family : Fin 4) : BitTM (physicalInterpolationRowGridRankWord family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.physicalInterpolationDirectGridMatchBit (family : Fin 4) : List Bool → List Bool

Compare the interpolation row's grid rank with the column's grid rank.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.paperVariableArityPhysicalInterpolationDirectGridMatchBitComputable (family : Fin 4) : BitTM (physicalInterpolationDirectGridMatchBit family)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalInterpolationDirectMomentBitTM.paperVariableArityPhysicalInterpolationDirectGridMatchBit_valid (family : Fin 4) (row column : ℕ) (formula : ThreeCNF) : physicalInterpolationDirectGridMatchBit family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide ((row - SourceFieldMomentOperationsTM.physicalFamilyStart family formula) / PhysicalFamilyRowTM.physDegree formula % PhysicalFamilyRowTM.physGridCard formula = column / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula)]

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.physicalFamilyDirectMomentBit (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.

theorem GapCVP.PhysicalInterpolationDirectMomentBitTM.paperVariableArityPhysicalFamilyDirectMomentBit_valid (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (value : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) (index : Fin (PhysicalFamilyRowTM.physDegree formula)) (hindex : ↑index = row % PhysicalFamilyRowTM.physDegree formula) (hvalue : base.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits value) : physicalFamilyDirectMomentBit family base (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide ((row - SourceFieldMomentOperationsTM.physicalFamilyStart family formula) / PhysicalFamilyRowTM.physDegree formula % PhysicalFamilyRowTM.physGridCard formula = column / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula) && BinaryFieldInverseAlgebra.sourceWordPow value (SourceFieldMomentOperationsTM.physicalFamilyRowMoment family row formula) index]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationOuterColumnGridRank : List Bool → List Bool

Read the outer cell's column grid rank from a nested node query.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationOuterColumnGridRankComputable : BitTM physicalInterpolationOuterColumnGridRank

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationNodeColumnGridMask : List Bool → List Bool

Test whether the nested node rank matches the outer column's grid rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationNodeColumnGridMaskComputable : BitTM physicalInterpolationNodeColumnGridMask

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationNestedBasisRankWord : List Bool → List Bool

Read the outer cell's matrix basis rank from a nested node query.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationNestedBasisRankWordComputable : BitTM physicalInterpolationNestedBasisRankWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationRowBasisIndex (row : ℕ) (formula : ThreeCNF) : Fin (PhysicalFamilyRowTM.physDegree formula)

GapCVP reduction support.

Equations

• GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationRowBasisIndex row formula = ⟨row % GapCVP.PhysicalFamilyRowTM.physDegree formula, ⋯⟩

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationNodeWeightBasisBit (weight : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Extract the prepared field coefficient of a weighted interpolation node.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationNodeWeightBasisBitComputable (weight : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNodeWeightBasisBit weight)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalMaskedNodeInterpolationBit (weight : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Restrict a weighted interpolation node's coefficient to its matching column.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalMaskedNodeInterpolationBitComputable (weight : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalMaskedNodeInterpolationBit weight)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalOrdinaryInterpolationMomentComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

• GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalOrdinaryInterpolationMomentComputer = GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowMomentRankComputer 2

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalShiftedInterpolationMomentComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

• GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalShiftedInterpolationMomentComputer = GapCVP.SourceFieldMomentOperationsTM.physicalFamilyRowMomentRankComputer 3

def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalOrdinaryInterpolationNodeCount (row : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalShiftedInterpolationNodeCount (row : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalOrdinaryInterpolationNodeWidth_valid (row column : ℕ) (formula : ThreeCNF) : (PhysicalOrdinaryShiftedCoefficientSumTM.physicalOrdinaryNodePrefixWidth physicalOrdinaryInterpolationMomentComputer).output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (physicalOrdinaryInterpolationNodeCount row formula) true

theorem GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalShiftedInterpolationNodeWidth_valid (row column : ℕ) (formula : ThreeCNF) : (PhysicalOrdinaryShiftedCoefficientSumTM.physicalShiftedNodePrefixWidth physicalShiftedInterpolationMomentComputer).output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (physicalShiftedInterpolationNodeCount row formula) true

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableArityPhysicalCellVariableCountLiftComputable : BitTM (PhysicalFamilyMarkerTM.physicalCellSourceLift PhysicalFamilyRowTM.physicalFamilyVariableCountUnary)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalInterpolationNodeGridMaskTM.PaperVariableArityPhysicalInterpolationGridIndex (formula : ThreeCNF) : Type

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeGridMaskTM.physicalInterpolationRebuiltGridCell (rank source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

Rebuild a grid-cell query from computed rank and source words.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationRebuiltGridCellComputable (rank source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationRebuiltGridCell rank source)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.physicalInterpolationRebuiltGridWord (rank source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Read the field word at the grid cell rebuilt from computed rank and source words.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationRebuiltGridWordComputable (rank source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationRebuiltGridWord rank source)

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherSelfMask : List Bool → List Bool

Compare the nested node rank with its anchor rank.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherSelfMaskComputable : BitTM paperVariableArityPhysicalInterpolationNestedOtherSelfMask

GapCVP reduction support.

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.physicalInterpolationCellFieldOneWord : List Bool → List Bool

Read the field word representing one at an interpolation cell.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationCellFieldOneWordComputable : BitTM physicalInterpolationCellFieldOneWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.physicalInterpolationNestedOtherFieldOneWord : List Bool → List Bool

Read the field word representing one from the nested query's actual cell.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherFieldOneWordComputable : BitTM physicalInterpolationNestedOtherFieldOneWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition (family : Fin 4) (row : ℕ) (formula : ThreeCNF) : PhysicalInterpolationNodeGridMaskTM.PaperVariableArityPhysicalInterpolationGridIndex formula

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationCellRowGridRankWord (family : Fin 4) : List Bool → List Bool

Compute a cell row's grid rank modulo the grid cardinality.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationCellRowGridRankWordComputable (family : Fin 4) : BitTM (physicalInterpolationCellRowGridRankWord family)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationCellRowGridRankWord_valid (family : Fin 4) (row column : ℕ) (formula : ThreeCNF) : physicalInterpolationCellRowGridRankWord family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (↑(physicalInterpolationFamilyRowGridPosition family row formula)) true

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedRowGridRankWord (family : Fin 4) : List Bool → List Bool

Read a family row's grid rank from the nested query's actual cell.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedRowGridRankWordComputable (family : Fin 4) : BitTM (physicalInterpolationNestedRowGridRankWord family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedRowGridRankComputer (family : Fin 4) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedRowGridRankWord_valid (family : Fin 4) (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node row column : ℕ) (formula : ThreeCNF) : physicalInterpolationNestedRowGridRankWord family (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = List.replicate (↑(physicalInterpolationFamilyRowGridPosition family row formula)) true

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedOtherDegreeWord : List Bool → List Bool

Read the field degree from the nested query's original source.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedOtherDegreeWordComputable : BitTM physicalInterpolationNestedOtherDegreeWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedOtherDegreeComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedOtherDegreeWord_valid (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node row column : ℕ) (formula : ThreeCNF) : physicalInterpolationNestedOtherDegreeWord (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = List.replicate (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) true

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedDifferenceWord (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

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

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedDifferenceWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNestedDifferenceWord left right)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedDifferenceComputer (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedEraseSelection : List Bool → List Bool

Prefix the nested query with the marker selecting its anchor node.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseSelectionComputable : BitTM physicalInterpolationNestedEraseSelection

GapCVP reduction support.

@[simp]

theorem GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseSelection_valid (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (other node : ℕ) (cell : List Bool) : physicalInterpolationNestedEraseSelection (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node cell)) = BinaryEncoding.lengthPrefixedWord [decide (other = node)] ++ BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node cell)

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOneBranch : List Bool → List Bool

Emit the field word one for the selected anchor node.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOneBranchComputable : BitTM paperVariableArityPhysicalInterpolationNestedEraseOneBranch

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOtherBranch (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Emit the supplied factor for a node other than the selected anchor.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOtherBranchComputable (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (paperVariableArityPhysicalInterpolationNestedEraseOtherBranch factor)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedEraseFactorWord (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

Replace the selected anchor's factor with one, retaining every other factor.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseFactorWordComputable (factor : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNestedEraseFactorWord factor)

GapCVP reduction support.

@[reducible, inline]

abbrev GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNodeGridWord (formula : ThreeCNF) (point : PhysicalInterpolationNodeGridMaskTM.PaperVariableArityPhysicalInterpolationGridIndex formula) : Core.EffectiveBinaryField.Word (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)

The finite field word indexed by an interpolation grid point.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNumeratorNodeDifferenceComputer (family : Fin 4) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationDenominatorNodeDifferenceComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNumeratorNodeFactorWord (family : Fin 4) : List Bool → List Bool

The numerator factor for a nested node, with the anchor factor replaced by one.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNumeratorNodeFactorWordComputable (family : Fin 4) : BitTM (physicalInterpolationNumeratorNodeFactorWord family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNumeratorNodeFactorComputer (family : Fin 4) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationDenominatorNodeFactorWord : List Bool → List Bool

The denominator factor for a nested node, with the anchor factor replaced by one.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationDenominatorNodeFactorWordComputable : BitTM physicalInterpolationDenominatorNodeFactorWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationDenominatorNodeFactorComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationDenominatorNodeFactorWord_valid (innerWidth outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (other node : PhysicalInterpolationNodeGridMaskTM.PaperVariableArityPhysicalInterpolationGridIndex formula) : physicalInterpolationDenominatorNodeFactorWord (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth (↑other) (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = BinaryModularReductionTM.finiteWordBits (if other = node then BinaryFieldInverseAlgebra.oneWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) else BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorValue (physicalInterpolationNodeGridWord formula node) (physicalInterpolationNodeGridWord formula other))

@[reducible, inline]

abbrev GapCVP.PhysicalLagrangeNodeProductAlgebra.PaperVariableArityPhysicalLagrangeNodeGridIndex (formula : ThreeCNF) : Type

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeEvaluationWord (formula : ThreeCNF) (point : PaperVariableArityPhysicalLagrangeNodeGridIndex formula) : PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeEvaluationWord_sourceField (formula : ThreeCNF) (point : PaperVariableArityPhysicalLagrangeNodeGridIndex formula) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (physicalLagrangeNodeEvaluationWord formula point) = BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) point

def GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct (formula : ThreeCNF) (factors : List (PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula)) : PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula

Multiply a list of interpolation words modulo the selected irreducible polynomial.

Equations

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

def GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNumeratorNodeFactorValues (formula : ThreeCNF) (node point : PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (count : ℕ) : List (PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula)

List the numerator factor values for the initial interpolation nodes.

Equations

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

def GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeDenominatorNodeFactorValues (formula : ThreeCNF) (node : PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (count : ℕ) : List (PhysicalOrdinaryShiftedCoefficientTM.PaperVariableArityPhysicalInterpolationWord formula)

List the denominator factor values for the initial interpolation nodes.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeSelectedModulusWord : List Bool → List Bool

Read the selected irreducible modulus from a nested node's original source.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusComputable : BitTM physicalInterpolationNestedNodeSelectedModulusWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusComputer_output (input : List Bool) : paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusComputer.output input = physicalInterpolationNestedNodeSelectedModulusWord input

@[simp]

theorem GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusWord_valid (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (node row column : ℕ) (formula : ThreeCNF) : physicalInterpolationNestedNodeSelectedModulusWord (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope width node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.irreducibleWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula))

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeFieldOneWord : List Bool → List Bool

Read the field word one from a nested node's outer cell.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeFieldOneComputable : BitTM physicalInterpolationNestedNodeFieldOneWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeFieldOneComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeFieldOneWord_valid (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (node row column : ℕ) (formula : ThreeCNF) : physicalInterpolationNestedNodeFieldOneWord (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope width node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.oneWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula))

def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeInverseQuery (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

Pair a computed operand with the nested node's original source for inversion.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeInverseQueryComputable (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (paperVariableArityPhysicalInterpolationNestedNodeInverseQuery operand)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeInverseWord (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Invert a computed operand using the nested node's selected field.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeInverseWordComputable (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNestedNodeInverseWord operand)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeInverseComputer (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

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

Assemble a field-multiplication query from the computed modulus and operands.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeMultiplyQueryComputable (lower left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (paperVariableArityPhysicalInterpolationNestedNodeMultiplyQuery lower left right)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeMultiplyWord (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Multiply two computed words in the nested node's selected field.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeMultiplyWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNestedNodeMultiplyWord left right)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeMultiplyComputer (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNumeratorNodeProductWord (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : List Bool → List Bool

Multiply the numerator node factors over the supplied grid width.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductComputable (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BitTM (physicalInterpolationNestedNumeratorNodeProductWord family width)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductComputer (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedDenominatorNodeProductWord (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : List Bool → List Bool

Multiply the denominator node factors over the supplied grid width.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedDenominatorNodeProductComputable (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BitTM (physicalInterpolationNestedDenominatorNodeProductWord width)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedDenominatorNodeProductComputer (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductWord_valid (family : Fin 4) (width outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (node : PhysicalLagrangeNodeProductAlgebra.PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) : physicalInterpolationNestedNumeratorNodeProductWord family width (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNumeratorNodeFactorValues formula node (PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition family row formula) count))

theorem GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedDenominatorNodeProductWord_valid (width outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (node : PhysicalLagrangeNodeProductAlgebra.PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) : physicalInterpolationNestedDenominatorNodeProductWord width (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeDenominatorNodeFactorValues formula node count))

theorem GapCVP.PhysicalLagrangeNodeDenominatorNonzero.paperVariableArityPhysicalLagrangeNodeEvaluationSourceValue_ne_variableAnchor (formula : ThreeCNF) (point : PhysicalLagrangeNodeProductAlgebra.PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (anchor : Fin (FormulaBridge.srcFormula formula).variableCount) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeEvaluationWord formula point) ≠ Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) anchor

theorem GapCVP.PhysicalLagrangeNodeDenominatorNonzero.paperVariableArityPhysicalLagrangeNodeEvaluationSourceValue_sub_variableAnchor_ne_zero (formula : ThreeCNF) (point : PhysicalLagrangeNodeProductAlgebra.PaperVariableArityPhysicalLagrangeNodeGridIndex formula) (anchor : Fin (FormulaBridge.srcFormula formula).variableCount) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeEvaluationWord formula point) - Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) anchor ≠ 0

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

Raise a computed base to the outer cell's family moment.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedNodeMomentWordComputable (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNestedNodeMomentWord family base)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedNodeMomentComputer (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedDenominatorInverseComputer (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNodeWeightWord (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

Compute the weighted Lagrange contribution of a nested interpolation node.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNodeWeightWordComputable (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (paperVariableArityPhysicalInterpolationNodeWeightWord family width base)

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalInterpolationNodeWeightTM.physicalInterpolationNodeWeightSourceWord (family : Fin 4) (row : ℕ) (formula : ThreeCNF) (count : ℕ) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (node : Fin count) (value : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedDenominatorInverseComputer_valid (width outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (node : Fin count) : (paperVariableArityPhysicalInterpolationNestedDenominatorInverseComputer width).output (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.sourceInverseWord (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeDenominatorNodeFactorValues formula (Fin.castLE bounded node) count)))

theorem GapCVP.PhysicalInterpolationNodeWeightCorrectness.paperVariableArityPhysicalInterpolationNestedNumeratorNodeComputer_valid (family : Fin 4) (width outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (node : Fin count) : (PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductComputer family width).output (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNumeratorNodeFactorValues formula (Fin.castLE bounded node) (PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition family row formula) count))

theorem GapCVP.PhysicalInterpolationNodeWeightCorrectness.paperVariableArityPhysicalInterpolationNestedNumeratorInverseComputer_valid (family : Fin 4) (width outerWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (row column : ℕ) (formula : ThreeCNF) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (node : Fin count) : (PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeMultiplyComputer (PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductComputer family width) (PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedDenominatorInverseComputer width)).output (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (Core.EffectiveBinaryField.multiplyMod (Core.EffectiveBinaryField.irreducibleWord (PhysicalFamilyRowTM.physDegree formula)) (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNumeratorNodeFactorValues formula (Fin.castLE bounded node) (PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition family row formula) count)) (BinaryFieldInverseAlgebra.sourceInverseWord (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct formula (PhysicalLagrangeNodeProductAlgebra.physicalLagrangeDenominatorNodeFactorValues formula (Fin.castLE bounded node) count))))

def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalBooleanXorOutput (first second : 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.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationColumnFieldWord : List Bool → List Bool

Read the field word indexed by an interpolation column.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalInterpolationColumnFieldWordComputable : BitTM physicalInterpolationColumnFieldWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationColumnFieldComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationFamilyTypeRankUnary (family : Fin 4) : List Bool → List Bool

Compute a family's type rank from its row grid quotient and moment count.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalInterpolationFamilyTypeRankUnaryComputable (family : Fin 4) : BitTM (physicalInterpolationFamilyTypeRankUnary family)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationFamilyTypeRankComputer (family : Fin 4) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationExpectedTypeMatchBit (expected : 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.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalInterpolationExpectedTypeMatchBitComputable (expected : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationExpectedTypeMatchBit expected)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationNodeCorrectionBit (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (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.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalInterpolationNodeCorrectionBitComputable (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalInterpolationNodeCorrectionBit family width base)

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalInterpolationNodeSourceWord (family : Fin 4) (row : ℕ) (formula : ThreeCNF) (count : ℕ) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (value : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) (node : ℕ) : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalSourceInterpolationFamilyCheckBit (family : Fin 4) (marker : List Bool → List Bool) (expected : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (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.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalSourceInterpolationFamilyCheckBitComputable (family : Fin 4) (marker : List Bool → List Bool) (markerComputer : BitTM marker) (expected : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (physicalSourceInterpolationFamilyCheckBit family marker expected width base)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalSourceInterpolationFamilyCheckBit_bits (family : Fin 4) (marker : List Bool → List Bool) (expected : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) (markerBit expectedBit directBit correctionBit : Bool) (markerCorrect : marker input = [markerBit]) (expectedCorrect : physicalInterpolationExpectedTypeMatchBit expected input = [expectedBit]) (directCorrect : PhysicalInterpolationDirectMomentBitTM.physicalFamilyDirectMomentBit family base input = [directBit]) (correctionCorrect : physicalInterpolationNodeCorrectionBit family width base input = [correctionBit]) : physicalSourceInterpolationFamilyCheckBit family marker expected width base input = [markerBit && (expectedBit && (directBit ^^ correctionBit))]

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.physicalOrdinaryCheckBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryCheckBitComputable : BitTM physicalOrdinaryCheckBit

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalLagrangeParityEntry.constructiveParityMatrix_apply_eq_orderedNodeProducts {K : Type u_1} [Field K] {gridCardinality degreeBound : ℕ} (points : Fin gridCardinality → K) (hdegree : degreeBound < gridCardinality) (row column : Fin gridCardinality) : BinaryReedSolomonParity.constructiveParityMatrix points hdegree row column = (if row = column then 1 else 0) - ∑ node : Fin (degreeBound + 1), (if Fin.castLE ⋯ node = column then 1 else 0) * ∏ other ∈ Finset.univ.erase node, (points (Fin.castLE ⋯ node) - points (Fin.castLE ⋯ other))⁻¹ * (points row - points (Fin.castLE ⋯ other))

theorem GapCVP.PhysicalSelectedInterpolationCoefficientProjection.paperVariableArityPhysicalWordShiftedFieldCoefficient_eq_selectedCoordinate (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) (tuple : ((FormulaBridge.srcFormula formula).clauses.get clause).SatisfyingLocalTuple) (localVariable : ((FormulaBridge.srcFormula formula).clauses.get clause).LocalVariable) (moment : Fin (BinaryExplicitAffineSystem.explicitMomentBudget encodingLength (FormulaBridge.srcFormula formula) + 1)) (row : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension encodingLength formula)) : MatrixEntrySemantics.physicalWordFamilyFieldCoefficient encodingLength formula (Sum.inr (Sum.inr (Sum.inr ⟨clause, ⟨tuple, (localVariable, moment)⟩⟩))) row column = if Sum.inr ⟨clause, tuple⟩ = ((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).1 then BinaryReedSolomonParity.constructiveParityMatrix (fun (index : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) => ↑((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) index)) ⋯ row ((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)).symm ((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).2.1) * ((((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).2.2 - Core.sourceSATFieldBit (↑tuple localVariable)) / (↑((SourceOrder.sourceCoordinateWordOrder encodingLength formula) column).2.1 - Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace encodingLength (FormulaBridge.srcFormula formula) ↑localVariable)) ^ ↑moment else 0

theorem GapCVP.PhysicalInterpolationNodeWeightSourceFieldCorrectness.paperVariableArityPhysicalInterpolationNodeWeightSourceWord_sourceField (family : Fin 4) (row : ℕ) (formula : ThreeCNF) (count : ℕ) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (node : Fin count) (value : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalInterpolationNodeWeightTM.physicalInterpolationNodeWeightSourceWord family row formula count bounded node value) = (∏ other ∈ Finset.univ.erase node, (BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition family row formula) - BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (Fin.castLE bounded other))) * (∏ other ∈ Finset.univ.erase node, (BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (Fin.castLE bounded node) - BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (Fin.castLE bounded other)))⁻¹ * BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) value ^ SourceFieldMomentOperationsTM.physicalFamilyRowMoment family row formula

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalInterpolationNodeCorrectionBit_sourceField_valid (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (count : ℕ) (correctWidth : width.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate count true) (bounded : count ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount) (value : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) (correctBase : base.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits value) : physicalInterpolationNodeCorrectionBit family width base (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide ((Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).equivFun (List.map (fun (node : ℕ) => if node = column / PhysicalFamilyRowTM.physFieldCard formula % PhysicalFamilyRowTM.physGridCard formula then BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (physicalInterpolationNodeSourceWord family row formula count bounded value node) else 0) (List.range count)).sum (PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationRowBasisIndex row formula) = 1)]

structure GapCVP.ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers : Type 1

GapCVP reduction support.

• clause : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

  GapCVP reduction support.

• tuple : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

  GapCVP reduction support.

• variablePosition : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

  GapCVP reduction support.

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRetainedSource : List Bool → List Bool

Read the filtered formula from a shifted tuple query's original source.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRetainedSourceComputable : BitTM paperShiftedTupleRetainedSource

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleClauseQuery (ranks : PaperVariableArityShiftedTupleRankComputers) (input : List Bool) : List Bool

Pair the computed clause rank with the retained source formula.

Equations

• GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleClauseQuery ranks input = ranks.clause.output input ++ false :: GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRetainedSource input

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleClauseQueryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperVariableArityShiftedTupleClauseQuery ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleOriginalClauseWord (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Read the original clause selected by the tuple's computed clause rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleOriginalClauseWordComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleOriginalClauseWord ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedArityUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleNormalizedArityUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleNormalizedArityUnary ranks)

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleNormalizedArityUnary_query (ranks : PaperVariableArityShiftedTupleRankComputers) (row column : ℕ) (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (hrank : ranks.clause.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate rank true) : paperShiftedTupleNormalizedArityUnary ranks (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩)).length true

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleGuardedSourceWord (marker selected : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleBetaTM.paperShiftedTupleGuardedSourceWord marker selected input = GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput selected [] (marker input ++ input)

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleGuardedSourceWordComputable {marker selected : List Bool → List Bool} (hmarker : BitTM marker) (hselected : BitTM selected) : BitTM (paperShiftedTupleGuardedSourceWord marker selected)

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleBetaTM.paperShiftedTupleGuardedSourceWord_valid (marker selected : List Bool → List Bool) (input : List Bool) (bit : Bool) (hmarker : marker input = [bit]) : paperShiftedTupleGuardedSourceWord marker selected input = if bit = true then selected input else []

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleConstantUnary (value : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleBetaTM.paperShiftedTupleConstantUnary value x✝ = List.replicate value true

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleConstantUnaryComputable (value : ℕ) : BitTM (paperShiftedTupleConstantUnary value)

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleConstantUnaryComputable value = GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable (List.replicate value true)

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleOriginalSignWord (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Read one literal sign from the tuple's original clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleOriginalSignWordComputable (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleOriginalSignWord ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleOriginalSecondKeepBit (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Read the marker deciding whether the original clause's second literal is retained.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleOriginalSecondKeepBitComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleOriginalSecondKeepBit ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleSelectedSourceBit (marker first second : List Bool → List Bool) : List Bool → List Bool

Select between two computed bits using a computed marker.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSelectedSourceBitComputable {marker first second : List Bool → List Bool} (hmarker : BitTM marker) (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (paperShiftedTupleSelectedSourceBit marker first second)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedSignWord (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Read the literal sign at a position in the tuple's normalized clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleNormalizedSignWordComputable (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleNormalizedSignWord ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedPositionBit (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Test whether a literal position lies below the normalized clause's arity.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleNormalizedPositionBitComputable (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleNormalizedPositionBit ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRejectedPositionBit (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Mark a normalized clause position whose literal rejects the corresponding bit.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRejectedPositionBitComputable (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleRejectedPositionBit ranks position)

GapCVP reduction support.

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRejectedWeightedUnary (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Encode a rejected literal position's binary weight in unary.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRejectedWeightedUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleRejectedWeightedUnary ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRejectedRankUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Sum the rejected literal positions' binary weights to obtain the rejected rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRejectedRankUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleRejectedRankUnary ranks)

GapCVP reduction support.

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRejectedNatural (arity : ℕ) (sign : Fin 3 → Bool) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleBeforeRejectedBit (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Test whether the tuple rank precedes the clause's rejected assignment rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleBeforeRejectedBitComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperVariableArityShiftedTupleBeforeRejectedBit ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleSkipUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Encode whether the tuple rank must skip the rejected assignment.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSkipUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleSkipUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleSatisfyingWordRankUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Adjust the tuple rank to skip the clause's rejected assignment.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingWordRankUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleSatisfyingWordRankUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleLocalPowerNumeratorUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Compute the unary numerator used for the tuple position's local power.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleLocalPowerNumeratorUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleLocalPowerNumeratorUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleLocalBinaryPowerUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Divide the local power numerator by two in unary.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleLocalBinaryPowerUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleLocalBinaryPowerUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingPositionQuotientUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Divide the satisfying assignment rank by the position's local binary power.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingPositionQuotientUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperVariableArityShiftedTupleSatisfyingPositionQuotientUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingPositionDigitUnary (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Extract the satisfying assignment's position digit by taking the quotient modulo two.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingPositionDigitUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperVariableArityShiftedTupleSatisfyingPositionDigitUnary ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaTM.paperShiftedTupleBetaBit (ranks : PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleBetaBitComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleBetaBit ranks)

GapCVP reduction support.

theorem GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleBetaBit_valid (ranks : PaperVariableArityShiftedTupleRankComputers) (input : List Bool) (arity tuple position : ℕ) (sign : Fin 3 → Bool) (hposition : position < 3) (harity : paperShiftedTupleNormalizedArityUnary ranks input = List.replicate arity true) (hsign : ∀ (slot : Fin 3), paperShiftedTupleNormalizedSignWord ranks slot input = [sign slot]) (htuple : ranks.tuple.output input = List.replicate tuple true) (hlocal : ranks.variablePosition.output input = List.replicate position true) : paperShiftedTupleBetaBit ranks input = [(tuple + if tuple < paperShiftedTupleRejectedNatural arity sign then 0 else 1).testBit position]

def GapCVP.SatisfyingWordSourceRankSemantics.paperVariableArityBoundedSourceSign (arity : ℕ) (harity : arity ≤ 3) (sign : Fin 3 → Bool) : Fin arity → Bool

GapCVP reduction support.

Equations

• GapCVP.SatisfyingWordSourceRankSemantics.paperVariableArityBoundedSourceSign arity harity sign position = sign ⟨↑position, ⋯⟩

theorem GapCVP.SatisfyingWordSourceRankSemantics.paperVariableAritySatisfyingWordOrder_apply_eq_shiftedTupleBetaBit (arity : ℕ) (harity : arity ≤ 3) (sign : Fin 3 → Bool) (tuple : Fin (2 ^ arity - 1)) (position : Fin arity) : ↑((SourceOrder.paperSatisfyingWordOrder arity (paperVariableArityBoundedSourceSign arity harity sign)) tuple) position = (↑tuple + if ↑tuple < ShiftedTupleBetaTM.paperShiftedTupleRejectedNatural arity sign then 0 else 1).testBit ↑position

@[reducible, inline]

abbrev GapCVP.PhysicalInterpolationRowFamilyProjection.physicalInterpolationMomentBudget (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalInterpolationRowFamilyProjection.physicalShiftedInterpolationTagCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalInterpolationRowFamilyProjection.physicalInterpolationBlockWidth (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalInterpolationRowFamilyProjection.physicalInterpolationBlockWidth formula = GapCVP.PhysicalFamilyRowTM.physGridCard formula * GapCVP.PhysicalFamilyRowTM.physDegree formula

def GapCVP.PhysicalInterpolationRowFamilyProjection.physicalShiftedDependentFamilyIndex (formula : ThreeCNF) (tag : Fin (physicalShiftedInterpolationTagCount formula)) : Fin (SourceOrder.paperExplicitFamilyTagCount (BinaryEncoding.encodeThreeCNF formula).length formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationRowFamilyProjection.paperVariableArityPhysicalShiftedDependentFamilyWordOrder (formula : ThreeCNF) (tag : Fin (physicalShiftedInterpolationTagCount formula)) : (SourceOrder.paperExplicitFamilyWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) (physicalShiftedDependentFamilyIndex formula tag) = Sum.inr (Sum.inr (Sum.inr ((SourceOrder.paperShiftedFamilyWordOrder formula (physicalInterpolationMomentBudget formula)) tag)))

theorem GapCVP.PhysicalInterpolationRowFamilyProjection.paperVariableArityPhysicalShiftedDependentFamilyBlockCount (formula : ThreeCNF) (tag : Fin (physicalShiftedInterpolationTagCount formula)) : SourceOrder.paperExplicitBinaryFamilyBlockCount (BinaryEncoding.encodeThreeCNF formula).length formula (physicalShiftedDependentFamilyIndex formula tag) = physicalInterpolationBlockWidth formula

theorem GapCVP.PhysicalInterpolationRowFamilyProjection.paperVariableArityPhysicalInterpolationRowCount_eq (formula : ThreeCNF) : SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula = PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula + physicalShiftedInterpolationTagCount formula * physicalInterpolationBlockWidth formula

theorem GapCVP.PhysicalInterpolationRowFamilyProjection.paperVariableArityPhysicalShiftedDependentFamilyPrefix (formula : ThreeCNF) (tag : Fin (physicalShiftedInterpolationTagCount formula)) : PhysicalRowOrderProjection.physicalSigmaPrefix (SourceOrder.paperExplicitBinaryFamilyBlockCount (BinaryEncoding.encodeThreeCNF formula).length formula) (physicalShiftedDependentFamilyIndex formula tag) = PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula + ↑tag * physicalInterpolationBlockWidth formula

noncomputable def GapCVP.PhysicalOrdinaryInterpolationCheckFieldCorrectness.physicalOrdinarySourceRowTableMoment (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : Core.sourceSATTableType (FormulaBridge.srcFormula formula) × Fin (PhysicalInterpolationRowFamilyProjection.physicalInterpolationMomentBudget formula + 1)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryInterpolationCheckFieldCorrectness.physicalOrdinarySourceRowGrid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)))

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalOrdinaryInterpolationCheckFieldCorrectness.paperVariableArityPhysicalOrdinarySourceRowFieldCoefficient_eq_selected (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : MatrixEntrySemantics.physicalWordFamilyFieldCoefficient (BinaryEncoding.encodeThreeCNF formula).length formula (MatrixEntrySemantics.physicalWordDecodedRow (BinaryEncoding.encodeThreeCNF formula).length formula row).fst (MatrixEntrySemantics.physicalWordDecodedRow (BinaryEncoding.encodeThreeCNF formula).length formula row).snd.1 column = if (physicalOrdinarySourceRowTableMoment formula row inOrdinary).1 = ((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).1 then BinaryReedSolomonParity.constructiveParityMatrix (fun (index : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)))) => ↑((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)) index)) ⋯ (physicalOrdinarySourceRowGrid formula row inOrdinary) ((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).symm ((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.1) * ((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.2 ^ ↑(physicalOrdinarySourceRowTableMoment formula row inOrdinary).2 else 0

theorem GapCVP.PhysicalOrdinaryInterpolationRowGridBasisCorrectness.paperVariableArityPhysicalOrdinarySourceRowGrid_val (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : ↑(PhysicalOrdinaryInterpolationCheckFieldCorrectness.physicalOrdinarySourceRowGrid formula row inOrdinary) = (↑row - PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) / PhysicalFamilyRowTM.physDegree formula % PhysicalFamilyRowTM.physGridCard formula

theorem GapCVP.PhysicalOrdinaryInterpolationRowGridBasisCorrectness.paperVariableArityPhysicalOrdinarySourceRowBasis_val (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) : ↑(MatrixEntrySemantics.physicalWordDecodedRow (BinaryEncoding.encodeThreeCNF formula).length formula row).snd.2 = ↑row % PhysicalFamilyRowTM.physDegree formula

theorem GapCVP.PhysicalOrdinaryInterpolationRowGridBasisCorrectness.paperVariableArityPhysicalOrdinarySourceRowMoment_val (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : ↑(PhysicalOrdinaryInterpolationCheckFieldCorrectness.physicalOrdinarySourceRowTableMoment formula row inOrdinary).2 = (↑row - PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) / PhysicalFamilyRowTM.physDegree formula / PhysicalFamilyRowTM.physGridCard formula % PhysicalFamilyRowTM.physicalFormulaMomentCount formula

theorem GapCVP.PhysicalInterpolationNodeCountBounds.physicalInterpolationExplicitGridCardinality_eq (formula : ThreeCNF) : Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)) = 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount

theorem GapCVP.PhysicalInterpolationNodeCountBounds.physicalOrdinaryInterpolationNodeCount_le_grid (formula : ThreeCNF) (row : ℕ) : PhysicalMaskedInterpolationNodeParityTM.physicalOrdinaryInterpolationNodeCount row formula ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount

theorem GapCVP.PhysicalInterpolationNodeCountBounds.physicalShiftedInterpolationNodeCount_le_grid (formula : ThreeCNF) (row : ℕ) : PhysicalMaskedInterpolationNodeParityTM.physicalShiftedInterpolationNodeCount row formula ≤ 2 ^ PhysicalFamilyRowTM.physDegree formula - (FormulaBridge.srcFormula formula).variableCount

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleOriginalVariableWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Read the variable word at a literal position in the original clause.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleOriginalVariableWordComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleOriginalVariableWord ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleSelectedSourceWord (marker first second : List Bool → List Bool) (input : List Bool) : List Bool

Select one of two computed source words using a computed marker.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleSelectedSourceWordComputable {marker first second : List Bool → List Bool} (hmarker : BitTM marker) (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (paperShiftedTupleSelectedSourceWord marker first second)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleNormalizedVariableWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Read the variable word at a position in the normalized clause.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleNormalizedVariableWordComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleNormalizedVariableWord ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTuplePotentialNormalizedLiteral (clause : ThreeClause) (position : Fin 3) : Literal

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTuplePotentialNormalizedLiteral_get (clause : ThreeClause) (position : Fin 3) (hposition : ↑position < (SourcePreprocessingSemantics.paperSourceNormalizedClause clause).length) : paperShiftedTuplePotentialNormalizedLiteral clause position = (SourcePreprocessingSemantics.paperSourceNormalizedClause clause).get ⟨↑position, hposition⟩

theorem GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleNormalizedSignWord_potential_query (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (row column : ℕ) (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (hrank : ranks.clause.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate rank true) (position : Fin 3) : ShiftedTupleBetaTM.paperShiftedTupleNormalizedSignWord ranks position (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [(paperShiftedTuplePotentialNormalizedLiteral (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩) position).2]

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleLocalPositionMarker (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : List Bool → List Bool

Test whether the computed variable position equals a specified literal position.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleLocalPositionMarkerComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (position : Fin 3) : BitTM (paperShiftedTupleLocalPositionMarker ranks position)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleSelectedNormalizedVariableWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (input : List Bool) : List Bool

Select the normalized clause's variable word at the computed position.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleSelectedNormalizedVariableWordComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleSelectedNormalizedVariableWord ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorRankQuery (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (input : List Bool) : List Bool

Pair the selected normalized variable with the source used to locate its retained rank.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleRetainedAnchorRankQueryComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleRetainedAnchorRankQuery ranks)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorRankUnary (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

Compute the retained source rank of the selected normalized variable.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleRetainedAnchorRankUnaryComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleRetainedAnchorRankUnary ranks)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorFieldWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleRetainedAnchorFieldWordComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (paperShiftedTupleRetainedAnchorFieldWord ranks)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorFieldComputer (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorFieldComputer_output (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (input : List Bool) : (paperShiftedTupleRetainedAnchorFieldComputer ranks).output input = paperShiftedTupleRetainedAnchorFieldWord ranks input

The retained-anchor computer outputs its specified field word.

theorem GapCVP.ShiftedTupleAnchorSourceFieldCorrectness.paperShiftedTupleRetainedNormalizedClause_mem (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩) ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula

def GapCVP.ShiftedTupleAnchorSourceFieldCorrectness.paperShiftedTupleSelectedSourceVariableIndex (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (position : ℕ) (hposition : position < (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩)).length) : Fin (FormulaBridge.paperVariableArityVariableCount formula)

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleAnchorSourceFieldCorrectness.paperShiftedTupleSelectedSourceVariableWord (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (position : ℕ) (hposition : position < (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩)).length) : Core.EffectiveBinaryField.Word (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleAnchorSourceFieldCorrectness.paperVariableArityShiftedTupleRetainedAnchorFieldWord_query (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (row column : ℕ) (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (hrank : ranks.clause.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate rank true) (position : ℕ) (hposition : position < (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩)).length) (hlocal : ranks.variablePosition.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate position true) : ShiftedTupleBetaSourceCorrectness.paperShiftedTupleRetainedAnchorFieldWord ranks (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (paperShiftedTupleSelectedSourceVariableWord formula rank hbound position hposition)

theorem GapCVP.ShiftedTupleAnchorSourceFieldCorrectness.paperVariableArityShiftedTupleSelectedSourceVariableWord_sourceField (formula : ThreeCNF) (rank : ℕ) (hbound : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (position : ℕ) (hposition : position < (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩)).length) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (paperShiftedTupleSelectedSourceVariableWord formula rank hbound position hposition) = Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (paperShiftedTupleSelectedSourceVariableIndex formula rank hbound position hposition)

def GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperShiftedTupleBetaFieldIndex (formula : ThreeCNF) (bit : Bool) : Fin (2 ^ Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperShiftedTupleBetaFieldIndex formula bit = ⟨if bit = true then 1 else 0, ⋯⟩

noncomputable def GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperShiftedTupleBetaFieldWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperShiftedTupleBetaFieldComputer (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

theorem GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperVariableArityShiftedTupleBetaFieldComputer_output (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : (paperShiftedTupleBetaFieldComputer ranks).output = paperShiftedTupleBetaFieldWord ranks

theorem GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperVariableArityShiftedTupleBetaFieldWord_valid (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) (row column : ℕ) (formula : ThreeCNF) (bit : Bool) (hbit : ShiftedTupleBetaTM.paperShiftedTupleBetaBit ranks (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [bit]) : paperShiftedTupleBetaFieldWord ranks (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (BinaryFieldBasis.indexedWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) (paperShiftedTupleBetaFieldIndex formula bit))

theorem GapCVP.ShiftedTupleBetaSourceFieldCorrectness.paperVariableArityShiftedTupleBetaIndexedWord_sourceField (formula : ThreeCNF) (bit : Bool) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (BinaryFieldBasis.indexedWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) (paperShiftedTupleBetaFieldIndex formula bit)) = Core.sourceSATFieldBit bit

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedColumnValueWordComputable : BitTM physicalShiftedColumnValueWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueSourceWord (formula : ThreeCNF) (column : ℕ) : Core.EffectiveBinaryField.Word (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedColumnValueWord_valid (row column : ℕ) (formula : ThreeCNF) : physicalShiftedColumnValueWord (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (physicalShiftedColumnValueSourceWord formula column)

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedColumnGridWordComputable : BitTM physicalShiftedColumnGridWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridIndex (formula : ThreeCNF) (column : ℕ) : Fin (2 ^ Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula - (FormulaBridge.srcFormula formula).variableCount)

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridSourceWord (formula : ThreeCNF) (column : ℕ) : Core.EffectiveBinaryField.Word (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedColumnGridWord_valid (row column : ℕ) (formula : ThreeCNF) : physicalShiftedColumnGridWord (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (physicalShiftedColumnGridSourceWord formula column)

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedInterpolationNumeratorComputer (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedInterpolationDenominatorComputer (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedInterpolationBaseWord (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedInterpolationBaseWordComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (physicalShiftedInterpolationBaseWord ranks)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationBaseTM.paperVariableArityPhysicalShiftedInterpolationBaseComputer (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedInterpolationBaseTM.physicalShiftedInterpolationBaseSourceWord (formula : ThreeCNF) (column rank : ℕ) (bounded : rank < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (position : ℕ) (validPosition : position < (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, bounded⟩)).length) (bit : Bool) : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalInterpolationColumnSourceFieldCorrectness.paperVariableArityPhysicalInterpolationColumnValueSourceWord_sourceField (formula : ThreeCNF) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula))) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueSourceWord formula ↑column) = ((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.2

theorem GapCVP.PhysicalInterpolationColumnSourceFieldCorrectness.paperVariableArityPhysicalInterpolationColumnGridSourceWord_sourceField (formula : ThreeCNF) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula))) : BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridSourceWord formula ↑column) = ↑((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.1

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalSourceWordBasisCoordinate_decide (formula : ThreeCNF) (word : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)) (index : Fin (PhysicalFamilyRowTM.physDegree formula)) : decide ((Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).equivFun (BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) word) index = 1) = word index

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalSourceBasisCoordinate_sub_decide (formula : ThreeCNF) (first second : MatrixEntrySemantics.PaperVariableArityPhysicalWordField (BinaryEncoding.encodeThreeCNF formula).length formula) (index : Fin (PhysicalFamilyRowTM.physDegree formula)) : decide ((Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).equivFun (first - second) index = 1) = (decide ((Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).equivFun first index = 1) ^^ decide ((Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).equivFun second index = 1))

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryCheckBit_of_not_in_family (formula : ThreeCNF) (row column : ℕ) (outside : ¬(PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ row ∧ row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula)) : physicalOrdinaryCheckBit (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [false]

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryColumnFieldComputer_valid (formula : ThreeCNF) (row : ℕ) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : physicalInterpolationColumnFieldComputer.output (BinaryExplicitAffineRows.affineCellQuery row (↑column) (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits (PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueSourceWord formula ↑column)

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryFamilyStart_eq_refinement (formula : ThreeCNF) : SourceFieldMomentOperationsTM.physicalFamilyStart 2 formula = PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryExpectedTypeMatchBit_eq_sourceTable (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) (inOrdinary : PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) : physicalInterpolationExpectedTypeMatchBit (physicalInterpolationFamilyTypeRankComputer 2) (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((PhysicalOrdinaryInterpolationCheckFieldCorrectness.physicalOrdinarySourceRowTableMoment formula row inOrdinary).1 = ((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).1)]