Documentation

LeanPool.GapCVP.Part16A

GapCVP proof, part 16 #

source
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.

source
noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseQueryComputable :
BitTM GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseQuery✝

GapCVP reduction support.

Equations
Instances For
    source
    noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedPrefixIndexedClauseWeightUnaryComputable :
    BitTM GapCVP.ShiftedClauseOffsetTM.paperShiftedPrefixIndexedClauseWeightUnary✝

    GapCVP reduction support.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def GapCVP.ShiftedClauseOffsetTM.paperVariableArityShiftedSelectedOriginalClauseWordComputable :
      BitTM GapCVP.ShiftedClauseOffsetTM.paperShiftedSelectedOriginalClauseWord✝

      GapCVP reduction support.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[irreducible]
        noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowMixedTagComputable :
        BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowMixedTagWord✝

        GapCVP reduction support.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[irreducible]
          noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowRetainedCountComputable :
          BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowRetainedCountWord✝

          GapCVP reduction support.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[irreducible]
            noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateCellComputable :
            BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateCell✝

            GapCVP reduction support.

            Equations
            Instances For
              source
              @[irreducible]
              noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateClauseEnvelopeComputable :
              BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateClauseEnvelope✝

              GapCVP reduction support.

              Instances For
                source
                @[simp]
                theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateClauseEnvelope_query (formula : ThreeCNF) (row column rank : ℕ) :
                GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateClauseEnvelope✝ (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateRankEnvelope✝ formula row column rank) = GapCVP.ShiftedClauseOffsetTM.paperShiftedClauseRankEnvelope✝ formula rank
                source
                @[irreducible]
                noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixComputable :
                BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidatePrefixWord✝

                GapCVP reduction support.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[irreducible]
                  noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateMixedTagComputable :
                  BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateMixedTagWord✝

                  GapCVP reduction support.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidateMixedTagWord_query (formula : ThreeCNF) (row column rank : ℕ) :
                    GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateMixedTagWord✝ (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidateRankEnvelope✝ formula row column rank) = List.replicate (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowMixedTag✝ formula row) true
                    source
                    @[irreducible]
                    noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixMarkerComputable :
                    BitTM GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixMarker✝

                    GapCVP reduction support.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[irreducible]
                      noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowCandidatePrefixRecordComputable :
                      BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowCandidatePrefixRecord✝

                      GapCVP reduction support.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[irreducible]
                        noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowAcceptedPrefixCountComputable :
                        BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowAcceptedPrefixCountWord✝

                        GapCVP reduction support.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[irreducible]
                          noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowClauseRankComputable :
                          BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRankWord✝

                          GapCVP reduction support.

                          Instances For
                            source
                            @[irreducible]
                            noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClauseEnvelopeComputable :
                            BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClauseEnvelope✝

                            GapCVP reduction support.

                            Instances For
                              source
                              @[irreducible]
                              noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClauseArityComputable :
                              BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClauseArityWord✝

                              GapCVP reduction support.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[irreducible]
                                noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowSelectedClausePrefixComputable :
                                BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowSelectedClausePrefixWord✝

                                GapCVP reduction support.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[irreducible]
                                  noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowLocalTagComputable :
                                  BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowLocalTagWord✝

                                  GapCVP reduction support.

                                  Instances For
                                    source
                                    @[irreducible]
                                    noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputable :
                                    BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowTupleRankWord✝

                                    GapCVP reduction support.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      @[irreducible]
                                      noncomputable def GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowVariablePositionComputable :
                                      BitTM GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowVariablePositionWord✝

                                      GapCVP reduction support.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[simp]
                                        theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputers_clause_query (formula : ThreeCNF) (row column : ℕ) :
                                        GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowTupleRankComputers✝.clause.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank✝ formula row) true
                                        source
                                        theorem GapCVP.PhysicalShiftedRowTupleRankTM.paperVariableArityPhysicalShiftedRowTupleRankComputers_variablePosition_query (formula : ThreeCNF) (row column : ℕ) (hbound : GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank✝ formula row < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) :
                                        GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowTupleRankComputers✝.variablePosition.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowVariablePosition✝ formula row hbound) true
                                        source
                                        @[irreducible]
                                        noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.paperVariableArityPhysicalShiftedExpectedLocalTypePrefixComputable :
                                        BitTM GapCVP.PhysicalShiftedExpectedTypeRankTM.physicalShiftedExpectedLocalTypePrefixWord✝

                                        GapCVP reduction support.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          @[irreducible]
                                          noncomputable def GapCVP.PhysicalShiftedExpectedTypeRankTM.paperVariableArityPhysicalShiftedExpectedTableTypeRankComputable :
                                          BitTM GapCVP.PhysicalShiftedExpectedTypeRankTM.physicalShiftedExpectedTableTypeRankWord✝

                                          GapCVP reduction support.

                                          Instances For
                                            source
                                            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.
                                            Instances For
                                              source
                                              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.
                                              Instances For
                                                source
                                                theorem GapCVP.PhysicalShiftedInterpolationBaseSourceFieldCorrectness.paperVariableArityPhysicalShiftedCanonicalInterpolationBaseSourceWord_sourceField (formula : ThreeCNF) (row column : ℕ) (bounded : GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank✝ formula row < List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) :
                                                BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (GapCVP.PhysicalShiftedInterpolationBaseInstantiation.physicalShiftedCanonicalInterpolationBaseSourceWord✝ formula row column bounded) = (BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnValueSourceWord formula column) - Core.sourceSATFieldBit (GapCVP.PhysicalShiftedInterpolationBaseInstantiation.physicalShiftedRowBetaBit✝ formula row bounded)) / (BinarySourceCoordinateOrder.sourceFormulaEvaluationWord (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (PhysicalShiftedInterpolationBaseTM.physicalShiftedColumnGridIndex formula column) - Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (ShiftedTupleAnchorSourceFieldCorrectness.paperShiftedTupleSelectedSourceVariableIndex formula (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowClauseRank✝ formula row) bounded (GapCVP.PhysicalShiftedRowTupleRankTM.physicalShiftedRowVariablePosition✝ formula row bounded) ⋯))
                                                source
                                                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)
                                                source
                                                theorem GapCVP.PhysicalShiftedCanonicalInterpolationBaseSemanticCorrectness.paperVariableArityPhysicalShiftedFiniteRowCanonicalBaseSourceWord_eq_decodedSourceRatio (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) :
                                                BinaryFieldInverseAlgebra.sourceWordValue (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) (GapCVP.PhysicalShiftedInterpolationParityMaskedFieldCorrectness.physicalShiftedFiniteRowCanonicalBaseSourceWord✝ formula row column inShifted) = (((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.2 - Core.sourceSATFieldBit (↑(GapCVP.PhysicalShiftedInterpolationRowFieldCorrectness.physicalShiftedSourceRowTuple✝ formula row inShifted) (GapCVP.PhysicalShiftedInterpolationRowFieldCorrectness.physicalShiftedSourceRowLocalVariable✝ formula row inShifted))) / (↑((SourceOrder.sourceCoordinateWordOrder (BinaryEncoding.encodeThreeCNF formula).length formula) column).2.1 - Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula) ↑(GapCVP.PhysicalShiftedInterpolationRowFieldCorrectness.physicalShiftedSourceRowLocalVariable✝ formula row inShifted))
                                                source
                                                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.