GapCVP proof, part 14, continuation 02

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleCandidateCardinalityComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleCandidateCardinalityUnary✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairWidthComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairWidthOutput✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairCardinalityComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairCardinalityUnary✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairDivisionQueryComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairDivisionQuery✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairOdometerComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairOdometer✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairFirstRankComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairFirstRank✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairSecondRankComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairSecondRank✝

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairLowerWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairLowerWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairFirstWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairFirstWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairSecondWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairSecondWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairProductQueryComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairProductQuery✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairProductWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairProductWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairDegreeUnaryComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairDegreeUnary✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWidthComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWidthOutput✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleMonicZeroWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleMonicZeroWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMonicWordComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairMonicWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMarkerComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairMarker✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleFactorPairMarkerStreamComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleFactorPairMarkerStream✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleProperFactorExistsComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleProperFactorExistsWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceIrreducibleNoProperFactorComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceIrreducibleNoProperFactorWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleCandidateMarkerStreamComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceActualIrreducibleCandidateMarkerStream✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleFirstCandidateComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceActualIrreducibleFirstCandidateWord✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.sourceActualIrreducibleSelectedRankUnary✝

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankQueryComputable : BitTM GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceActualIrreducibleSelectedRankQuery✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldArithmeticMachine.paperVariableAritySourceSelectedIrreducibleWordComputable : BitTM sourceSelectedIrreducibleWord

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixFieldDegreeComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalMatrixCellTM.physicalMatrixSelectedBasisRankComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

def GapCVP.PhysicalMatrixCellTM.physicalMatrixGuardedFourFamilyCheck (global refinement ordinary shifted : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalMatrixCellTM.paperVariableArityPhysicalMatrixGuardedFourFamilyCheckComputable (global refinement ordinary shifted : List Bool → List Bool) (globalComputer : BitTM global) (refinementComputer : BitTM refinement) (ordinaryComputer : BitTM ordinary) (shiftedComputer : BitTM shifted) : BitTM (physicalMatrixGuardedFourFamilyCheck global refinement ordinary shifted)

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalCoefficientFieldCardinalityUnaryComputable : BitTM GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientFieldCardinalityUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalCoefficientGridCardinalityUnaryComputable : BitTM GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalCoefficientGridCardinalityUnary✝

GapCVP reduction support.

Equations

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

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

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnFieldValueRankUnaryComputable : BitTM physicalColumnFieldValueRankUnary

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalColumnGridRankUnaryComputable : BitTM physicalColumnGridRankUnary

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalColumnTypeRankUnaryComputable : BitTM physicalColumnTypeRankUnary

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalRowFieldRankUnaryComputable : BitTM GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalGlobalRowFieldRankUnary✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalFamilyCoefficientWordComputable : BitTM GapCVP.PhysicalGlobalRefinementCoefficientTM.physicalGlobalFamilyCoefficientWord✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalGlobalRefinementCoefficientTM.paperVariableArityPhysicalGlobalCheckBitComputable : BitTM physicalGlobalCheckBit

GapCVP reduction support.

Equations

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

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

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

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

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

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

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

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

@[reducible, inline]

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

GapCVP reduction support.

Equations

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

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

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

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

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

GapCVP reduction support.

Equations

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

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

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixRankWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixIndexedClauseQueryComputable : BitTM paperRefinementPrefixIndexedClauseQuery

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementPrefixIndexedClauseWeightUnaryComputable : BitTM GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixIndexedClauseWeightUnary✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.RefinementClauseOffsetTM.paperVariableArityRefinementClauseOffsetUnaryComputable : BitTM paperRefinementClauseOffsetUnary

GapCVP reduction support.

Equations

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

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowLocalRankUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowLocalRankUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldQuotientUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowFieldQuotientUnary✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowFieldValueRankUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowFieldValueRankUnary✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowGridQuotientUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowGridQuotientUnary✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementRowGridRankUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementRowGridRankUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseRankUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseRankUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseRankEnvelopeOutputComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseRankEnvelopeOutput✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseOffsetUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseOffsetUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseWidthUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseWidthUnary✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementColumnLocalTagUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementColumnLocalTagUnary✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementClauseLocalTagUpperUnaryComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementClauseLocalTagUpperUnary✝

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagBelowPrefixBitComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagBelowPrefixBit✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagBelowUpperBitComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagBelowUpperBit✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementClauseLocalTagTM.paperVariableArityPhysicalRefinementLocalTagMarkerComputable : BitTM GapCVP.PhysicalRefinementClauseLocalTagTM.physicalRefinementLocalTagMarker✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementGridMatchBitComputable : BitTM GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementGridMatchBit✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementFieldValueMatchBitComputable : BitTM GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementFieldValueMatchBit✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementAllowedTypeBitComputable : BitTM GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementAllowedTypeBit✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementFamilyCoefficientWordComputable : BitTM GapCVP.PhysicalRefinementCheckSourceCorrectness.physicalRefinementFamilyCoefficientWord✝

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRefinementCheckSourceCorrectness.paperVariableArityPhysicalRefinementCheckBitComputable : BitTM physicalRefinementCheckBit

GapCVP reduction support.

Equations

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

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

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableAritySourceFieldOperationsMachine.paperVariableAritySourceSelectedFieldInverseComputable : BitTM sourceSelectedFieldInverseWord

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCellComputable : BitTM GapCVP.BinaryCompactPhysicalFieldWordXorTM.compactPhysicalFieldWordXorOriginalCell✝

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

@[reducible, inline]

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientTM.paperVariableArityPhysicalInterpolationDegreeWordComputable : BitTM GapCVP.PhysicalOrdinaryShiftedCoefficientTM.physicalInterpolationDegreeWord✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationVariableCountWordComputable : BitTM GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationVariableCountWord✝

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.paperVariableArityPhysicalInterpolationShiftedVariableCountWordComputable : BitTM GapCVP.PhysicalOrdinaryShiftedCoefficientSumTM.physicalInterpolationShiftedVariableCountWord✝

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeRankComputable : BitTM compactPhysicalLagrangeNestedNodeRank

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOuterCellComputable : BitTM compactPhysicalLagrangeNestedNodeOuterCell

GapCVP reduction support.

Equations

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

@[simp]

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeOriginalSourceComputable : BitTM compactPhysicalLagrangeNestedNodeOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherActualCellComputable : BitTM compactPhysicalLagrangeNestedOtherActualCell

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherOriginalSourceComputable : BitTM compactPhysicalLagrangeNestedOtherOriginalSource

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRankComputable : BitTM compactPhysicalLagrangeNestedAnchorRank

GapCVP reduction support.

Equations

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

@[simp]

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedNodeSourceWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherSourceWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedOtherRankWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryCompactPhysicalLagrangeNestedNodeTM.compactPhysicalLagrangeNestedAnchorRankWordComputer : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[simp]

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

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellDegreeUnaryComputable : BitTM GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellDegreeUnary✝

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

• GapCVP.SourceFieldMomentOperationsTM.physicalMomentCellGridCardinalityUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyRowTM.physicalFamilyGridCardinalityUnary

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellGridCardinalityUnaryComputable : BitTM physicalMomentCellGridCardinalityUnary

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.SourceFieldMomentOperationsTM.paperVariableArityPhysicalMomentCellMomentCountUnaryComputable : BitTM physicalMomentCellMomentCountUnary

GapCVP reduction support.

Equations

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

@[simp]

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[simp]

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

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