Documentation

LeanPool.GapCVP.Part17

GapCVP proof, part 17 #

source
theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalSystem_satisfiable_of_scaled_hamming (encodingLength : ℕ) (formula : ThreeCNF) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (solution : (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalSystem✝ encodingLength formula).Solves values = true) (short : ↑(Core.integerSquaredNorm values) ≤ 2 * Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) * ↑(FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula)) :
∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true
source
theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalSystem_satisfiable_of_finiteP_short (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (solution : (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalSystem✝ encodingLength formula).Solves values = true) (short : (Factor400FinitePNormCorollary.finitePNorm p fun (index : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) => ↑(values index)) ≤ Factor400FinitePNormCorollary.finitePGapFactor p (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula) * ↑(Factor400FinitePNormCorollary.finitePRadius p (FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula))) :
∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true
source
theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalFormulaInstance_close_of_satisfiable (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) (satisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) :
∃ (coefficients : Fin (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula).dimension → ℤ), Factor400FinitePNormCorollary.finitePLatticeDistance p (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula) coefficients ≤ ↑(GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula).radius
source
theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalFormulaInstance_far_of_unsatisfiable (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) (consistent : (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalSystem✝ encodingLength formula).effectiveReducedConsistent = true) (unsatisfiable : ¬∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) (coefficients : Fin (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula).dimension → ℤ) :
Factor400FinitePNormCorollary.finitePGapFactor p (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula) * ↑(GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula).radius < Factor400FinitePNormCorollary.finitePLatticeDistance p (GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance✝ p hp encodingLength formula) coefficients
source
@[irreducible]
noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePThresholdUnaryComputable (p : ℚ) :
BitTM (GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePThresholdUnary✝ p)

GapCVP reduction support.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePNumeratorUnaryComputable (p : ℚ) :
    BitTM (GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePNumeratorUnary✝ p)

    GapCVP reduction support.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[irreducible]
      noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePRadiusAtomicComputable (p : ℚ) :
      BitTM (GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePRadiusAtomicOutput✝ p)

      GapCVP reduction support.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[irreducible]
        noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePPhysicalStructuralOutputComputable (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) :
        BitTM (GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePPhysicalStructuralOutput✝ p cell)

        GapCVP reduction support.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[irreducible]
          noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePPhysicalRoutedOutputComputable (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) :
          BitTM (GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePPhysicalRoutedOutput✝ p cell)

          GapCVP reduction support.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePNPHardPromise (p : ℚ) (hp : 1 ≤ p) :
            NPHardPromise (Factor400FinitePNormCorollary.finitePGapCVPPromise p hp) = true
            source
            @[irreducible]
            noncomputable def GapCVP.PaperNearestStructuralAtom.paperVariableArityNearestStructuralAtomComputer (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {reduced : List Bool → List Bool} (computer : BitTM reduced) :
            BinaryStructuralRecordTM.ConstructiveStructuralAtomComputer

            GapCVP reduction support.

            Instances For
              source
              theorem GapCVP.Factor400PaperVariableArityNearestUnconditional.binaryNearestCodeword_nphard_unconditional :
              NPHardPromise Factor400BinaryDecodingPromiseHardness.binaryNearestCodewordPromise = true