GapCVP proof, part 16, continuation 02

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalMatrixCellInstantiation.paperVariableArityCanonicalPhysicalMatrixCellComputerOfGuardedFamilies (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (global refinement ordinary shifted : List Bool → List Bool) (globalComputer : BitTM global) (refinementComputer : BitTM refinement) (ordinaryComputer : BitTM ordinary) (shiftedComputer : BitTM shifted) (correctGlobal : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), global (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (↑row < PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctRefinement : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), refinement (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctOrdinary : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), ordinary (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)]) (correctShifted : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), shifted (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ ↑row) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalMatrixCellInstantiation.paperVariableArityCanonicalPhysicalMatrixCellComputerOfActualGlobal (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (refinement ordinary shifted : List Bool → List Bool) (refinementComputer : BitTM refinement) (ordinaryComputer : BitTM ordinary) (shiftedComputer : BitTM shifted) (correctRefinement : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), refinement (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula ≤ ↑row ∧ ↑row < PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) (correctOrdinary : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), ordinary (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)]) (correctShifted : ∀ (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)), shifted (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ ↑row) && decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]) : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalMatrixCellInstantiation.paperVariableArityCanonicalPhysicalMatrixCellComputer (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape

GapCVP reduction support.

noncomputable def GapCVP.Factor400BinaryPaperVariableArityUnconditionalPhysicalSourceMachine.HasIntegerTarget (record : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryPaperVariableArityUnconditionalPhysicalSourceMachine.HasIntegerTarget record = decide (∀ (index : Fin record.dimension), ∃ (value : ℤ), record.target index = ↑value)

noncomputable def GapCVP.Factor400BinaryPaperVariableArityUnconditionalPhysicalSourceMachine.integerTargetGapCVP400Promise : PromiseProblem

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryPaperVariableArityUnconditionalPhysicalSourceMachine.paperVariableArityPhysicalIntegerTargetNPHardPromise : NPHardPromise integerTargetGapCVP400Promise = true

theorem GapCVP.Factor400BinaryDecodingPromiseHardness.encodeBinaryNearestCodewordInstance_injective : Function.Injective Factor400BinaryDecodingPromiseReduction.encodeBinaryNearestCodewordInstance

theorem GapCVP.Factor400BinaryDecodingPromiseHardness.encodeBinarySyndromeDecodingInstance_injective : Function.Injective Factor400BinaryDecodingPromiseReduction.encodeBinarySyndromeDecodingInstance

noncomputable def GapCVP.Factor400BinaryDecodingPromiseHardness.binaryNearestCodewordPromise : PromiseProblem

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryDecodingPromiseHardness.binarySyndromeDecodingPromise : PromiseProblem

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryDecodingPromiseHardness.integerSquaredNorm_eq_hammingNorm_binaryResidue {n : ℕ} (vector : Fin n → ℤ) (hbinary : ∀ (index : Fin n), vector index = 0 ∨ vector index = 1) : Core.integerSquaredNorm vector = hammingNorm (Core.binaryResidue vector)

def GapCVP.Factor400BinaryDecodingPromiseHardness.canonicalBinaryNearestCodewordNo : Factor400BinaryDecodingPromiseReduction.BinaryNearestCodewordInstance

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryDecodingPromiseHardness.canonicalBinaryNearestCodewordNo_mem : binaryNearestCodewordPromise.no (Factor400BinaryDecodingPromiseReduction.encodeBinaryNearestCodewordInstance canonicalBinaryNearestCodewordNo) = true

def GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingBinaryBasisAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingBinaryBasisAtomComputable : BitTM compactPhysicalDecodingBinaryBasisAtom

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingBinaryBasisAtom_effective (system : Core.BinaryAffineSystem) (row column : Fin system.dimension) : compactPhysicalDecodingBinaryBasisAtom (GaussianPhysicalWordReducedAtomTM.effectiveGaussianStateBasisTag system.effectiveGaussianState row column) = BinaryEncoding.encodeAtomic ↑(↑(system.effectiveSquareBasisMatrix row column)).val

def GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingGaussianIntegerTargetAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingGaussianIntegerTargetAtomComputable : BitTM compactPhysicalDecodingGaussianIntegerTargetAtom

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryDecodingPhysicalWordSourceTM.compactPhysicalDecodingGaussianIntegerTargetAtom_effective (system : Core.BinaryAffineSystem) (column : Fin system.dimension) (source : List Bool) : compactPhysicalDecodingGaussianIntegerTargetAtom (GaussianPackedStateTargetAtomTM.gaussianPackedIndexedStateWord (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord system.effectiveGaussianState source)) = BinaryEncoding.encodeAtomic (system.effectiveAffineRepresentative column)

noncomputable def GapCVP.PaperBinaryCodingTM.paperCodingBlockLengthAtomic : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PaperBinaryCodingTM.paperVariableArityCodingBlockLengthAtomicComputable : BitTM paperCodingBlockLengthAtomic

GapCVP reduction support.

Equations

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

theorem GapCVP.PaperBinaryCodingTM.paperVariableArityCodingBlockLengthAtomic_valid (formula : ThreeCNF) : paperCodingBlockLengthAtomic (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.encodeAtomic (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension

noncomputable def GapCVP.PaperBinaryCodingTM.paperCodingRadiusAtomic : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PaperBinaryCodingTM.paperVariableArityCodingRadiusAtomicComputable : BitTM paperCodingRadiusAtomic

GapCVP reduction support.

Equations

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

theorem GapCVP.PaperBinaryCodingTM.paperVariableArityCodingRadiusAtomic_valid (formula : ThreeCNF) : paperCodingRadiusAtomic (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.encodeAtomic (FourFamilySoundness.paperVariableArityIntegerRadius (BinaryEncoding.encodeThreeCNF formula).length formula)

theorem GapCVP.Factor400BinaryDecodingPhysicalWordUnconditionalSyndromeFinal.binarySyndromeDecoding_nphard_unconditional : NPHardPromise Factor400BinaryDecodingPromiseHardness.binarySyndromeDecodingPromise = true

theorem GapCVP.Factor400FinitePNormPromiseReduction.finitePGapFactor_rpow (p : ℚ) (hp : 1 ≤ p) (I : GapCVPInstance) : Factor400FinitePNormCorollary.finitePGapFactor p I ^ ↑p = Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor I.dimension

@[reducible, inline]

abbrev GapCVP.Factor400FinitePNormPromiseReduction.finitePCanonicalNoInstance : GapCVPInstance

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormPromiseReduction.finitePCanonicalNoInstance = { dimension := 1, basis := !![2], target := fun (x : Fin 1) => 1, radius := 1 / 2 }

noncomputable def GapCVP.Factor400FinitePNormPromiseReduction.finitePCanonicalNoWord : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400FinitePNormPromiseReduction.finitePCanonicalNo_mem_no (p : ℚ) (hp : 1 ≤ p) : (Factor400FinitePNormCorollary.finitePGapCVPPromise p hp).no finitePCanonicalNoWord = true

def GapCVP.Factor400FinitePNormPromiseReduction.effectiveFinitePSignedDiscrepancy (H : Core.BinaryAffineSystem) (coefficients : Fin H.dimension → ℤ) : Fin H.dimension → ℤ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormPromiseReduction.effectiveFinitePSignedDiscrepancy H coefficients = H.effectiveAffineRepresentative - H.effectiveSquareBasisMatrix.mulVec coefficients

theorem GapCVP.Factor400FinitePNormPromiseReduction.effectiveFinitePSignedDiscrepancy_solves (H : Core.BinaryAffineSystem) (hconsistent : H.effectiveReducedConsistent = true) (coefficients : Fin H.dimension → ℤ) : H.Solves (effectiveFinitePSignedDiscrepancy H coefficients) = true

theorem GapCVP.Factor400FinitePNormPromiseReduction.finitePLatticeDistance_effective_eq_signed_norm (p : ℚ) (H : Core.BinaryAffineSystem) (hdimension : 0 < H.dimension) (radius : ℚ) (hradius : 0 < radius) (coefficients : Fin H.dimension → ℤ) : Factor400FinitePNormCorollary.finitePLatticeDistance p (Factor400BinaryInstanceBridge.effectiveGapCVPInstance H hdimension radius hradius) coefficients = Factor400FinitePNormCorollary.finitePNorm p fun (i : Fin H.dimension) => ↑(effectiveFinitePSignedDiscrepancy H coefficients i)