GapCVP proof, part 17

@[reducible, inline]

noncomputable abbrev GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalSystem (encodingLength : ℕ) (formula : ThreeCNF) : Core.BinaryAffineSystem

The binary affine system associated with the physically encoded formula.

Equations

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

noncomputable def GapCVP.PaperFinitePNormSourceReduction.paperFinitePPhysicalFormulaInstance (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) : GapCVPInstance

Construct the finite-p GapCVP instance of a physically encoded formula.

Equations

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

theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalSystem_satisfiable_of_scaled_hamming (encodingLength : ℕ) (formula : ThreeCNF) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (solution : (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

theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalSystem_satisfiable_of_finiteP_short (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (solution : (paperFinitePPhysicalSystem encodingLength formula).Solves values = true) (short : (Factor400FinitePNormCorollary.finitePNorm p fun (index : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) => ↑(values index)) ≤ Factor400FinitePNormCorollary.finitePGapFactor p (paperFinitePPhysicalFormulaInstance p hp encodingLength formula) * ↑(Factor400FinitePNormCorollary.finitePRadius p (FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula))) : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

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 (paperFinitePPhysicalFormulaInstance p hp encodingLength formula).dimension → ℤ), Factor400FinitePNormCorollary.finitePLatticeDistance p (paperFinitePPhysicalFormulaInstance p hp encodingLength formula) coefficients ≤ ↑(paperFinitePPhysicalFormulaInstance p hp encodingLength formula).radius

theorem GapCVP.PaperFinitePNormSourceReduction.paperVariableArityFinitePPhysicalFormulaInstance_far_of_unsatisfiable (p : ℚ) (hp : 1 ≤ p) (encodingLength : ℕ) (formula : ThreeCNF) (consistent : (paperFinitePPhysicalSystem encodingLength formula).effectiveReducedConsistent = true) (unsatisfiable : ¬∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) (coefficients : Fin (paperFinitePPhysicalFormulaInstance p hp encodingLength formula).dimension → ℤ) : Factor400FinitePNormCorollary.finitePGapFactor p (paperFinitePPhysicalFormulaInstance p hp encodingLength formula) * ↑(paperFinitePPhysicalFormulaInstance p hp encodingLength formula).radius < Factor400FinitePNormCorollary.finitePLatticeDistance p (paperFinitePPhysicalFormulaInstance p hp encodingLength formula) coefficients

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePThresholdUnary (p : ℚ) (input : List Bool) : List Bool

Encode the scaled finite-p radius threshold in unary.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePThresholdUnaryComputable (p : ℚ) : BitTM (paperFinitePThresholdUnary p)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePNumeratorUnary (p : ℚ) : List Bool → List Bool

Compute the unary root used as the finite-p radius numerator.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePNumeratorUnaryComputable (p : ℚ) : BitTM (paperFinitePNumeratorUnary p)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePRadiusAtomicOutput (p : ℚ) : List Bool → List Bool

Encode the reduced rational finite-p radius as an atomic source word.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePRadiusAtomicComputable (p : ℚ) : BitTM (paperVariableArityFinitePRadiusAtomicOutput p)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePPhysicalStructuralOutput (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

Assemble the finite-p physical source word from the Gaussian matrix and radius data.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePPhysicalStructuralOutputComputable (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperFinitePPhysicalStructuralOutput p cell)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperFinitePPhysicalRoutedOutput (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (input : List Bool) : List Bool

Route the source to the canonical or structural finite-p output according to its guards.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePPhysicalRoutedOutputComputable (p : ℚ) {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperFinitePPhysicalRoutedOutput p cell)

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400PaperVariableArityFinitePNormUnconditional.paperVariableArityFinitePNPHardPromise (p : ℚ) (hp : 1 ≤ p) : NPHardPromise (Factor400FinitePNormCorollary.finitePGapCVPPromise p hp) = true

@[irreducible]

noncomputable def GapCVP.PaperNearestStructuralAtom.paperVariableArityNearestStructuralAtomComputer (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {reduced : List Bool → List Bool} (computer : BitTM reduced) : BinaryStructuralRecordTM.ConstructiveStructuralAtomComputer

GapCVP reduction support.

theorem GapCVP.Factor400PaperVariableArityNearestUnconditional.binaryNearestCodeword_nphard_unconditional : NPHardPromise Factor400BinaryDecodingPromiseHardness.binaryNearestCodewordPromise = true