GapCVP proof, part 16

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalOrdinaryCheckBit_valid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : physicalOrdinaryCheckBit (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)]

Internal support shared across GapCVP continuation modules.

def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseQuery (input : List Bool) : List Bool

The indexed-clause query used to compute a shifted prefix weight.

Equations

• GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseQuery input = GapCVP.RefinementClauseOffsetTM.paperRefinementPrefixIndexedClauseQuery input

noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseQueryComputable : BitTM paperVariableArityShiftedPrefixIndexedClauseQuery

GapCVP reduction support.

noncomputable def GapCVP.ShiftedClauseOffsetTM.paperShiftedClauseRankEnvelope (formula : ThreeCNF) (rank : ℕ) : List Bool

Pair a clause rank with the retained-source grid envelope.

Equations

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

def GapCVP.ShiftedClauseOffsetTM.paperShiftedPrefixIndexedClauseWeightUnary : List Bool → List Bool

Read the shifted weight of the indexed clause in a prefix query.

Equations

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

noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseWeightUnaryComputable : BitTM paperShiftedPrefixIndexedClauseWeightUnary

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedClauseOffsetTM.paperShiftedSelectedOriginalClauseWord : List Bool → List Bool

Read the original clause selected by a shifted indexed-clause query.

Equations

• GapCVP.ShiftedClauseOffsetTM.paperShiftedSelectedOriginalClauseWord = GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseOutput ∘ GapCVP.ShiftedTupleTM.paperShiftedIndexedClauseQuery

noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedSelectedOriginalClauseWordComputable : BitTM paperShiftedSelectedOriginalClauseWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowMixedTagWord : List Bool → List Bool

Compute the shifted row's mixed tag from its grid quotient and moment count.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowMixedTagComputable : BitTM physicalShiftedRowMixedTagWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowRetainedCountWord : List Bool → List Bool

Read the retained clause count from the shifted row's original source.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowRetainedCountComputable : BitTM physicalShiftedRowRetainedCountWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowMixedTag (formula : ThreeCNF) (row : ℕ) : ℕ

The mixed tag of a shifted row after removing degree, grid, and moment coordinates.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateRankEnvelope (formula : ThreeCNF) (row column rank : ℕ) : List Bool

Pair a candidate clause rank with the shifted row's retained-source grid envelope.

Equations

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

def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateCell : List Bool → List Bool

Recover the cell query after dropping two fields from a candidate envelope.

Equations

• GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateCell = GapCVP.SourcePreprocessingTM.paperSourcePreprocessingSuffixAt 2

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateCellComputable : BitTM physicalShiftedRowCandidateCell

GapCVP reduction support.

Equations

• GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateCellComputable = GapCVP.SourcePreprocessingTM.paperPreprocessingSuffixAtComputable 2

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateClauseEnvelope (input : List Bool) : List Bool

Rebuild the candidate clause envelope over the cell's original source.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateClauseEnvelopeComputable : BitTM physicalShiftedRowCandidateClauseEnvelope

GapCVP reduction support.

@[simp]

theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateClauseEnvelope_query (formula : ThreeCNF) (row column rank : ℕ) : physicalShiftedRowCandidateClauseEnvelope (physicalShiftedRowCandidateRankEnvelope formula row column rank) = ShiftedClauseOffsetTM.paperShiftedClauseRankEnvelope formula rank

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidatePrefixWord : List Bool → List Bool

Read the shifted prefix offset of a candidate clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixComputable : BitTM physicalShiftedRowCandidatePrefixWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateMixedTagWord : List Bool → List Bool

Read the mixed row tag from a candidate's cell query.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateMixedTagComputable : BitTM physicalShiftedRowCandidateMixedTagWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateMixedTagWord_query (formula : ThreeCNF) (row column rank : ℕ) : physicalShiftedRowCandidateMixedTagWord (physicalShiftedRowCandidateRankEnvelope formula row column rank) = List.replicate (physicalShiftedRowMixedTag formula row) true

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixMarker : List Bool → List Bool

Test whether the mixed row tag reaches the candidate clause's prefix offset.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixMarkerComputable : BitTM paperVariableArityPhysicalShiftedRowCandidatePrefixMarker

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidatePrefixRecord : List Bool → List Bool

Emit one unary marker when the candidate clause's prefix is accepted.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixRecordComputable : BitTM physicalShiftedRowCandidatePrefixRecord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowAcceptedPrefixCountWord : List Bool → List Bool

Count accepted candidate prefixes using the retained-clause catalogue.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowAcceptedPrefixCountComputable : BitTM physicalShiftedRowAcceptedPrefixCountWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRankWord : List Bool → List Bool

Subtract one from the accepted prefix count to obtain the selected clause rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowClauseRankComputable : BitTM physicalShiftedRowClauseRankWord

GapCVP reduction support.

def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank (formula : ThreeCNF) (row : ℕ) : ℕ

The clause rank selected by the shifted row's accepted prefix count.

Equations

• GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank formula row = GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowAcceptedPrefixCount✝ formula row - 1

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClauseEnvelope (input : List Bool) : List Bool

Pair the selected clause rank with the retained-source envelope.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClauseEnvelopeComputable : BitTM physicalShiftedRowSelectedClauseEnvelope

GapCVP reduction support.

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClauseArityWord : List Bool → List Bool

Read the arity of the shifted row's selected clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClauseArityComputable : BitTM physicalShiftedRowSelectedClauseArityWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClausePrefixWord : List Bool → List Bool

Read the shifted prefix offset of the selected clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClausePrefixComputable : BitTM physicalShiftedRowSelectedClausePrefixWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowLocalTagWord : List Bool → List Bool

Subtract the selected clause's prefix offset from the mixed row tag.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowLocalTagComputable : BitTM physicalShiftedRowLocalTagWord

GapCVP reduction support.

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowTupleRankWord : List Bool → List Bool

Divide the local tag by the selected clause's arity to obtain the tuple rank.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputable : BitTM physicalShiftedRowTupleRankWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowVariablePositionWord : List Bool → List Bool

Take the local tag modulo the selected clause's arity to obtain its variable position.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowVariablePositionComputable : BitTM physicalShiftedRowVariablePositionWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowVariablePosition (formula : ThreeCNF) (row : ℕ) (hbound : physicalShiftedRowClauseRank formula row < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : ℕ

The variable position within the shifted row's selected clause.

Equations

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

noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowTupleRankComputers : ShiftedTupleBetaTM.PaperVariableArityShiftedTupleRankComputers

Collect the clause, tuple, and variable-position computers for a shifted row.

Equations

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

@[simp]

theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputers_clause_query (formula : ThreeCNF) (row column : ℕ) : physicalShiftedRowTupleRankComputers.clause.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (physicalShiftedRowClauseRank formula row) true

theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputers_variablePosition_query (formula : ThreeCNF) (row column : ℕ) (hbound : physicalShiftedRowClauseRank formula row < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : physicalShiftedRowTupleRankComputers.variablePosition.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (physicalShiftedRowVariablePosition formula row hbound) true

noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.physicalShiftedExpectedLocalTypePrefixWord : List Bool → List Bool

Read the refinement type prefix for the shifted row's selected clause.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.paperVariableArityPhysicalShiftedExpectedLocalTypePrefixComputable : BitTM physicalShiftedExpectedLocalTypePrefixWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.physicalShiftedExpectedTableTypeRankWord : List Bool → List Bool

Assemble the expected table-type rank from the local prefix and row coordinates.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.paperVariableArityPhysicalShiftedExpectedTableTypeRankComputable : BitTM physicalShiftedExpectedTableTypeRankWord

GapCVP reduction support.

def GapCVP.PhysicalShiftedInterpolationBaseInstantiation.physicalShiftedCanonicalInterpolationBaseSourceWord (formula : ThreeCNF) (row column : ℕ) (bounded : PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank formula row < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)

The canonical interpolation base word for a shifted row with a valid clause rank.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalShiftedCheckBitComputable : BitTM physicalShiftedCheckBit

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.PhysicalShiftedInterpolationParityMaskedFieldCorrectness.physicalShiftedFiniteRowCanonicalBaseSourceWord (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula))) (inShifted : PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ ↑row) : Core.EffectiveBinaryField.Word (PhysicalFamilyRowTM.physDegree formula)

The canonical shifted interpolation base word at finite row and column indices.

Equations

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

theorem GapCVP.PhysicalShiftedCanonicalRetainedClauseSourceCorrectness.paperFormulaRetainedClause_retainedOriginal (formula : ThreeCNF) (original : Fin (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula))) : ↑(SourceOrder.paperFormulaRetainedClause formula ((CanonicalOffsetIdentity.paperRetainedOriginalClauseIndexOrder formula) original)) = SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) original)

theorem GapCVP.PhysicalOrdinaryShiftedCheckBitInstantiation.paperVariableArityPhysicalShiftedCheckBit_valid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : physicalShiftedCheckBit (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ ↑row) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]

Internal support shared across GapCVP continuation modules.