GapCVP proof, part 15

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalInterpolationDirectMomentBitTM.paperVariableArityPhysicalInterpolationDirectGridMatchBitComputable (family : Fin 4) : BitTM (GapCVP.PhysicalInterpolationDirectMomentBitTM.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) : GapCVP.PhysicalInterpolationDirectMomentBitTM.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]

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationOuterColumnGridRankComputable : BitTM GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationOuterColumnGridRank✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationNodeColumnGridMaskComputable : BitTM GapCVP.PhysicalMaskedInterpolationNodeParityTM.physicalInterpolationNodeColumnGridMask✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalInterpolationNestedBasisRankWordComputable : BitTM GapCVP.PhysicalMaskedInterpolationNodeParityTM.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, ⋯⟩

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalMaskedInterpolationNodeParityTM.paperVariableArityPhysicalMaskedNodeInterpolationBitComputable (weight : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalMaskedInterpolationNodeParityTM.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.

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherSelfMaskComputable : BitTM GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherSelfMask✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationCellFieldOneWordComputable : BitTM GapCVP.PhysicalInterpolationNodeGridMaskTM.physicalInterpolationCellFieldOneWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeGridMaskTM.paperVariableArityPhysicalInterpolationNestedOtherFieldOneWordComputable : BitTM GapCVP.PhysicalInterpolationNodeGridMaskTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationCellRowGridRankWordComputable (family : Fin 4) : BitTM (GapCVP.PhysicalInterpolationNodeFactorTM.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) : GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationCellRowGridRankWord✝ family (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (↑(physicalInterpolationFamilyRowGridPosition family row formula)) true

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedRowGridRankWordComputable (family : Fin 4) : BitTM (GapCVP.PhysicalInterpolationNodeFactorTM.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) : GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedRowGridRankWord✝ family (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = List.replicate (↑(physicalInterpolationFamilyRowGridPosition family row formula)) true

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedOtherDegreeWordComputable : BitTM GapCVP.PhysicalInterpolationNodeFactorTM.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) : GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedOtherDegreeWord✝ (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope innerWidth other (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)))) = List.replicate (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula) true

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedDifferenceWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalInterpolationNodeFactorTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseSelectionComputable : BitTM GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNestedEraseSelection✝

GapCVP reduction support.

@[simp]

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOneBranchComputable : BitTM GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNestedEraseOneBranch✝

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationNumeratorNodeFactorWordComputable (family : Fin 4) : BitTM (GapCVP.PhysicalInterpolationNodeFactorTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeFactorTM.paperVariableArityPhysicalInterpolationDenominatorNodeFactorWordComputable : BitTM GapCVP.PhysicalInterpolationNodeFactorTM.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) : GapCVP.PhysicalInterpolationNodeFactorTM.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 (GapCVP.PhysicalInterpolationNodeFactorTM.physicalInterpolationNodeGridWord✝ formula node) (GapCVP.PhysicalInterpolationNodeFactorTM.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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeSelectedModulusComputable : BitTM GapCVP.PhysicalInterpolationNestedNodeProductTM.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 = GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeSelectedModulusWord✝ input

@[simp]

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeFieldOneComputable : BitTM GapCVP.PhysicalInterpolationNestedNodeProductTM.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) : GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNodeFieldOneWord✝ (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope width node (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (BinaryFieldInverseAlgebra.oneWord (Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFormulaDegree formula))

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeInverseWordComputable (operand : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalInterpolationNestedNodeProductTM.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.

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNodeMultiplyWordComputable (left right : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalInterpolationNestedNodeProductTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductComputable (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BitTM (GapCVP.PhysicalInterpolationNestedNodeProductTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNestedNodeProductTM.paperVariableArityPhysicalInterpolationNestedDenominatorNodeProductComputable (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : BitTM (GapCVP.PhysicalInterpolationNestedNodeProductTM.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) : GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedNumeratorNodeProductWord✝ family width (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.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) : GapCVP.PhysicalInterpolationNestedNodeProductTM.physicalInterpolationNestedDenominatorNodeProductWord✝ width (BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeEnvelope outerWidth (↑node) (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula))) = BinaryModularReductionTM.finiteWordBits (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.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

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNestedNodeMomentWordComputable (family : Fin 4) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalInterpolationNodeWeightTM.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.

@[irreducible]

noncomputable def GapCVP.PhysicalInterpolationNodeWeightTM.paperVariableArityPhysicalInterpolationNodeWeightWordComputable (family : Fin 4) (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (base : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (GapCVP.PhysicalInterpolationNodeWeightTM.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 (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.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 (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.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)) (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNumeratorNodeFactorValues✝ formula (Fin.castLE bounded node) (PhysicalInterpolationNodeFactorTM.physicalInterpolationFamilyRowGridPosition family row formula) count)) (BinaryFieldInverseAlgebra.sourceInverseWord (GapCVP.PhysicalLagrangeNodeProductAlgebra.physicalLagrangeNodeSelectedWordProduct✝ formula (GapCVP.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.paperVariableArityPhysicalInterpolationColumnFieldWordComputable : BitTM GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.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.paperVariableArityPhysicalInterpolationFamilyTypeRankUnaryComputable (family : Fin 4) : BitTM (GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.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.

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRetainedSourceComputable : BitTM GapCVP.ShiftedTupleBetaTM.paperShiftedTupleRetainedSource✝

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleOriginalClauseWordComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (GapCVP.ShiftedTupleBetaTM.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)

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

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 (GapCVP.ShiftedTupleBetaTM.paperShiftedTupleSelectedSourceBit✝ marker first second)

GapCVP reduction support.

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 (GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedSignWord✝ ranks position)

GapCVP reduction support.

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 (GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedPositionBit✝ ranks position)

GapCVP reduction support.

@[irreducible]

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

GapCVP reduction support.

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleRejectedRankUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (GapCVP.ShiftedTupleBetaTM.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.

@[irreducible]

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

GapCVP reduction support.

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.ShiftedTupleBetaTM.paperVariableArityShiftedTupleSatisfyingPositionDigitUnaryComputable (ranks : PaperVariableArityShiftedTupleRankComputers) : BitTM (GapCVP.ShiftedTupleBetaTM.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), GapCVP.ShiftedTupleBetaTM.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

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

GapCVP reduction support.

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 (GapCVP.ShiftedTupleBetaSourceCorrectness.paperShiftedTupleSelectedSourceWord✝ marker first second)

GapCVP reduction support.

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 (GapCVP.ShiftedTupleBetaSourceCorrectness.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) : GapCVP.ShiftedTupleBetaTM.paperShiftedTupleNormalizedSignWord✝ ranks position (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [(paperShiftedTuplePotentialNormalizedLiteral (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) ⟨rank, hbound⟩) position).2]

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleBetaSourceCorrectness.paperVariableArityShiftedTupleRetainedAnchorRankUnaryComputable (ranks : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers) : BitTM (GapCVP.ShiftedTupleBetaSourceCorrectness.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.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)]