Documentation

LeanPool.GapCVP.Part12A

GapCVP proof, part 12 #

source
noncomputable def GapCVP.FourFamilySoundness.paperVariableArityIntegerRadius (encodingLength : ℕ) (formula : ThreeCNF) :
ℕ

GapCVP reduction support.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem GapCVP.FourFamilySoundness.paperVariableArityIntegerRadius_pos (encodingLength : ℕ) (formula : ThreeCNF) :
    0 < paperVariableArityIntegerRadius encodingLength formula
    source
    theorem GapCVP.FourFamilySoundness.paperVariableArityExplicitBinarySystem_oneHot_of_satisfiable (encodingLength : ℕ) (formula : ThreeCNF) (hsatisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) :
    ∃ (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ), (FormulaBridge.paperExplicitBinarySystem encodingLength formula).Solves vector = true ∧ (∀ (index : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))), vector index = 0 ∨ vector index = 1) ∧ Core.integerSquaredNorm vector = paperVariableArityIntegerRadius encodingLength formula

    Internal support shared across GapCVP continuation modules.

    source
    theorem GapCVP.FourFamilySoundness.paperVariableArityExplicitBinarySystem_satisfiable_of_scaled_hamming (encodingLength : ℕ) (formula : ThreeCNF) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (hsolve : (FormulaBridge.paperExplicitBinarySystem encodingLength formula).Solves vector = true) (hshort : ↑(Core.integerSquaredNorm vector) ≤ 2 * Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) * ↑(paperVariableArityIntegerRadius encodingLength formula)) :
    ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

    Internal support shared across GapCVP continuation modules.

    source
    theorem GapCVP.FourFamilySoundness.paperVariableArityExplicitBinarySystem_strict_factor400_of_unsatisfiable (encodingLength : ℕ) (formula : ThreeCNF) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (hsolve : (FormulaBridge.paperExplicitBinarySystem encodingLength formula).Solves vector = true) (hunsatisfiable : ¬∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) :
    (SourceFactor400BinaryConstructionABounds.gapFactor400 (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) * ↑(Core.sourceOneHotCompletenessRadius (FormulaBridge.srcFormula formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula)))) ^ 2 < ↑(Core.integerSquaredNorm vector)

    Internal support shared across GapCVP continuation modules.