GapCVP proof, part 10

noncomputable def GapCVP.SourceFactor400BinaryConstructionABounds.gapFactor400 (dimension : ℕ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.SourceFactor400BinaryConstructionABounds.gapFactor400 dimension = ↑dimension ^ (1 / 400)

theorem GapCVP.SourceFactor400BinaryConstructionABounds.gapFactor400_sq (dimension : ℕ) : gapFactor400 dimension ^ 2 = ↑dimension ^ (1 / 200)

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormula_gapFactor400_eighty_mul_size_lt_fourth_power (encodingLength : ℕ) (F : Core.Formula) : 80 * SourceFactor400BinaryConstructionABounds.gapFactor400 (sourceFormulaDimension encodingLength F) ^ 2 * ↑(Core.sourceSizeParameter encodingLength F) < ↑(Core.sourceSizeParameter encodingLength F) ^ 4

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormula_satisfiable_of_short_signed_solution (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (hshort : 10 * Core.integerSquaredNorm z ≤ Fintype.card (sourceFormulaField encodingLength F) * Core.sourceSizeParameter encodingLength F ^ 4) : F.Satisfiable = true

theorem GapCVP.BinaryExplicitSourceSoundness.sourceFormulaExplicitBinarySystem_signedSolution_of_satisfiable (encodingLength : ℕ) (formula : Core.Formula) (hsatisfiable : formula.Satisfiable = true) : ∃ (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → ℤ), (BinaryExplicitAffineSystem.sourceFormulaExplicitBinarySystem encodingLength formula).Solves vector = true ∧ ↑(Core.integerSquaredNorm vector) ≤ ↑(Core.sourceOneHotCompletenessRadius formula (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength formula)) ^ 2

theorem GapCVP.BinaryExplicitSourceSoundness.sourceFormulaExplicitBinarySystem_squaredNorm_gt_factor400_of_unsatisfiable (encodingLength : ℕ) (formula : Core.Formula) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → ℤ) (hsolve : (BinaryExplicitAffineSystem.sourceFormulaExplicitBinarySystem encodingLength formula).Solves vector = true) (hunsatisfiable : ¬formula.Satisfiable = true) : (SourceFactor400BinaryConstructionABounds.gapFactor400 (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) * ↑(Core.sourceOneHotCompletenessRadius formula (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength formula))) ^ 2 < ↑(Core.integerSquaredNorm vector)

@[reducible, inline]

abbrev GapCVP.Factor400BinaryInstanceBridge.adaptGapCVPInstance (I : Core.GapCVPInstance) : GapCVPInstance

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryInstanceBridge.adaptGapCVPInstance I = { dimension := I.dimension, basis := I.basis, target := I.target, radius := I.radius }

theorem GapCVP.Factor400BinaryInstanceBridge.adaptGapCVPInstance_gapYES400_iff_metricYes (I : Core.GapCVPInstance) : gapYES400 (adaptGapCVPInstance I) = true ↔ I.IsYes = true

theorem GapCVP.Factor400BinaryInstanceBridge.adaptGapCVPInstance_gapNO400_iff_metricNo (I : Core.GapCVPInstance) : gapNO400 (adaptGapCVPInstance I) = true ↔ Core.GapCVPInstance.IsNo (1 / 400) I = true

def GapCVP.Factor400BinaryInstanceBridge.effectiveGapCVPInstance (H : Core.BinaryAffineSystem) (hdimension : 0 < H.dimension) (radius : ℚ) (hradius : 0 < radius) : GapCVPInstance

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryInstanceBridge.effectiveGapCVPInstance_wellFormed (H : Core.BinaryAffineSystem) (hdimension : 0 < H.dimension) (radius : ℚ) (hradius : 0 < radius) : gapCVPWellFormed (effectiveGapCVPInstance H hdimension radius hradius) = true

def GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveBasisPackedAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveBasisPackedAtomComputable : BitTM effectiveBasisPackedAtom

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveBasisPackedAtom_zero (suffix : List Bool) : effectiveBasisPackedAtom (false :: suffix) = BinaryEncoding.encodeAtomic 0

@[simp]

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveBasisPackedAtom_one (suffix : List Bool) : effectiveBasisPackedAtom (true :: false :: suffix) = BinaryEncoding.encodeAtomic 1

@[simp]

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveBasisPackedAtom_two (suffix : List Bool) : effectiveBasisPackedAtom (true :: true :: suffix) = BinaryEncoding.encodeAtomic 2

def GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveTargetPackedAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveTargetPackedAtomComputable : BitTM effectiveTargetPackedAtom

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveTargetPackedAtom_false (suffix : List Bool) : effectiveTargetPackedAtom (false :: suffix) = BinaryEncoding.encodeAtomic 0

@[simp]

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveTargetPackedAtom_true (suffix : List Bool) : effectiveTargetPackedAtom (true :: suffix) = BinaryEncoding.encodeAtomic 1

def GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveSourceSerializerOutput (counter descriptors : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryEffectiveBasisSerializerTM.effectiveSourceSerializerOutput_eq_flatten (counter descriptors : List Bool → List Bool) (records : List Bool → List (List Bool)) (input : List Bool) (hcounter : counter input = List.replicate (records input).length true) (hdescriptors : descriptors input = SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptorStream (records input)) : effectiveSourceSerializerOutput counter descriptors input = (records input).flatten

structure GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth : Type 1

GapCVP reduction support.

• output : List Bool → List Bool

  GapCVP reduction support.

• computer : BitTM self.output

  GapCVP reduction support.

def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.sourceQaryMaskDynamicGridBaseSource (width : SourceQaryMaskDynamicGridWidth) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.sourceQaryMaskDynamicGridBaseSource width input = GapCVP.BinaryEncoding.lengthPrefixedWord (width.output input) ++ input

noncomputable def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridBaseSourceComputable (width : SourceQaryMaskDynamicGridWidth) : BitTM (sourceQaryMaskDynamicGridBaseSource width)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridCandidateCatalogueOutput (width : SourceQaryMaskDynamicGridWidth) {candidate : List Bool → List Bool} (computer : BitTM candidate) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridCandidateCatalogueComputable (width : SourceQaryMaskDynamicGridWidth) {candidate : List Bool → List Bool} (computer : BitTM candidate) : BitTM (maskDynamicGridCandidateCatalogueOutput width computer)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridCandidateCatalogueOutput_valid (width : SourceQaryMaskDynamicGridWidth) {candidate : List Bool → List Bool} (computer : BitTM candidate) (input : List Bool) (count : ℕ) (hwidth : width.output input = List.replicate count true) : maskDynamicGridCandidateCatalogueOutput width computer input = List.flatMap (fun (rank : ℕ) => BinaryEncoding.lengthPrefixedWord (candidate (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ sourceQaryMaskDynamicGridBaseSource width input))) (List.range count)

noncomputable def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridRecordCatalogueOutput (width : SourceQaryMaskDynamicGridWidth) {record : List Bool → List Bool} (computer : BitTM record) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridRecordCatalogueComputable (width : SourceQaryMaskDynamicGridWidth) {record : List Bool → List Bool} (computer : BitTM record) : BitTM (maskDynamicGridRecordCatalogueOutput width computer)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridRecordCatalogueOutput_valid (width : SourceQaryMaskDynamicGridWidth) {record : List Bool → List Bool} (computer : BitTM record) (input : List Bool) (count : ℕ) (hwidth : width.output input = List.replicate count true) : maskDynamicGridRecordCatalogueOutput width computer input = List.flatMap (fun (rank : ℕ) => record (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ sourceQaryMaskDynamicGridBaseSource width input)) (List.range count)

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralRecordCountOutput (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryStructuralRecordTM.constructiveStructuralRecordCountOutput_valid (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (n : ℕ) (hdimension : dimension.output input = List.replicate n true) : constructiveStructuralRecordCountOutput dimension input = List.replicate (2 + n + n * n) true

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralRecordWidth (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

Internal support shared across GapCVP continuation modules.

Equations

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

structure GapCVP.BinaryStructuralRecordTM.ConstructiveStructuralAtomComputer : Type 1

GapCVP reduction support.

• output : List Bool → List Bool

  GapCVP reduction support.

• computer : BitTM self.output

  GapCVP reduction support.

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralRankQuery (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (input : List Bool) (rank : ℕ) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralDescriptorOutput (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (atom : ConstructiveStructuralAtomComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryStructuralRecordTM.constructiveStructuralDescriptorOutput_eq_records (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (atom : ConstructiveStructuralAtomComputer) (input : List Bool) (n : ℕ) (records : List (List Bool)) (hdimension : dimension.output input = List.replicate n true) (hcount : records.length = 2 + n + n * n) (hatoms : ∀ rank < records.length, atom.output (constructiveStructuralRankQuery dimension input rank) = records.getD rank []) : constructiveStructuralDescriptorOutput dimension atom input = SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptorStream records

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralSourceWord (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (atom : ConstructiveStructuralAtomComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryStructuralRecordTM.constructiveStructuralSourceWordComputable (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (atom : ConstructiveStructuralAtomComputer) : BitTM (constructiveStructuralSourceWord dimension atom)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryStructuralRecordTM.constructiveStructuralSourceWord_eq_encodeGapCVPInstance (dimension : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) (atom : ConstructiveStructuralAtomComputer) (input : List Bool) (lattice : GapCVPInstance) (hdimension : dimension.output input = List.replicate lattice.dimension true) (hatoms : ∀ rank < (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).length, atom.output (constructiveStructuralRankQuery dimension input rank) = (SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords lattice).getD rank []) : constructiveStructuralSourceWord dimension atom input = BinaryEncoding.encodeGapCVPInstance lattice

noncomputable def GapCVP.Core.EffectiveBinaryGaussian.System.InKernel {m n : ℕ} (system : System m n) (assignment : Fin n → ZMod 2) : Bool

GapCVP reduction support.

Equations

• system.InKernel assignment = decide (system.check.mulVec assignment = 0)

theorem GapCVP.Core.EffectiveBinaryGaussian.RowOperation.inKernel_iff {m n : ℕ} (operation : RowOperation m) (system : System m n) (assignment : Fin n → ZMod 2) : (operation.apply system).InKernel assignment = true ↔ system.InKernel assignment = true

theorem GapCVP.Core.BinaryAffineSystem.effectiveGaussian_kernel_iff (H : BinaryAffineSystem) (assignment : Fin H.dimension → ZMod 2) : H.effectiveGaussianState.system.check.mulVec assignment = 0 ↔ H.check.mulVec assignment = 0

theorem GapCVP.Core.BinaryAffineSystem.effectiveGaussian_signedKernel_iff (H : BinaryAffineSystem) (z : Fin H.dimension → ℤ) : H.effectiveGaussianState.system.check.mulVec (binaryResidue z) = 0 ↔ H.InLattice z = true

theorem GapCVP.Core.BinaryAffineSystem.effectivePivotRow_some_mem (H : BinaryAffineSystem) (column : Fin H.dimension) (row : Fin H.rowCount) (hrow : H.effectivePivotRowOption column = some row) : (row, column) ∈ H.effectiveGaussianState.pivots

theorem GapCVP.Core.BinaryAffineSystem.effectivePivotRow_eq_some_of_mem (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (column : Fin H.dimension) (row : Fin H.rowCount) (hmember : (row, column) ∈ H.effectiveGaussianState.pivots) : H.effectivePivotRowOption column = some row

theorem GapCVP.Core.BinaryAffineSystem.effectiveReducedRow_mulVec (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (bits : Fin H.dimension → ZMod 2) (pivotColumn : Fin H.dimension) (pivotRow : Fin H.rowCount) (hpivot : H.effectivePivotRowOption pivotColumn = some pivotRow) : H.effectiveGaussianState.system.check.mulVec bits pivotRow = bits pivotColumn + ∑ column : Fin H.dimension, if H.effectivePivotRowOption column = none then H.effectiveGaussianState.system.check pivotRow column * bits column else 0

theorem GapCVP.Core.BinaryAffineSystem.effectiveSquareBasisMatrix_mulVec_pivot_full (H : BinaryAffineSystem) (coefficients : Fin H.dimension → ℤ) (row : Fin H.dimension) (pivot : Fin H.rowCount) (hrow : H.effectivePivotRowOption row = some pivot) : H.effectiveSquareBasisMatrix.mulVec coefficients row = (∑ column : Fin H.dimension, if H.effectivePivotRowOption column = none then ↑(H.effectiveGaussianState.system.check pivot column).val * coefficients column else 0) + 2 * coefficients row

theorem GapCVP.Core.BinaryAffineSystem.effectiveGaussian_kernel_iff_graph_of_normal (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (bits : Fin H.dimension → ZMod 2) : H.effectiveGaussianState.system.check.mulVec bits = 0 ↔ ∀ (pivotColumn : Fin H.dimension) (pivotRow : Fin H.rowCount), H.effectivePivotRowOption pivotColumn = some pivotRow → bits pivotColumn = ∑ column : Fin H.dimension, if H.effectivePivotRowOption column = none then H.effectiveGaussianState.system.check pivotRow column * bits column else 0

def GapCVP.Core.BinaryAffineSystem.effectiveFreeLiftSum (H : BinaryAffineSystem) (row : Fin H.rowCount) (z : Fin H.dimension → ℤ) : ℤ

GapCVP reduction support.

Equations

• H.effectiveFreeLiftSum row z = ∑ column : Fin H.dimension, if H.effectivePivotRowOption column = none then ↑(H.effectiveGaussianState.system.check row column).val * z column else 0

theorem GapCVP.Core.BinaryAffineSystem.effectiveFreeLiftSum_cast (H : BinaryAffineSystem) (row : Fin H.rowCount) (z : Fin H.dimension → ℤ) : ↑(H.effectiveFreeLiftSum row z) = ∑ column : Fin H.dimension, if H.effectivePivotRowOption column = none then H.effectiveGaussianState.system.check row column * ↑(z column) else 0

def GapCVP.Core.BinaryAffineSystem.effectiveBasisCoefficients (H : BinaryAffineSystem) (z : Fin H.dimension → ℤ) : Fin H.dimension → ℤ

GapCVP reduction support.

Equations

• H.effectiveBasisCoefficients z column = match H.effectivePivotRowOption column with | none => z column | some row => (z column - H.effectiveFreeLiftSum row z) / 2

theorem GapCVP.Core.BinaryAffineSystem.effectiveBasis_two_dvd_of_normal (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (z : Fin H.dimension → ℤ) (hz : H.InLattice z = true) (column : Fin H.dimension) (row : Fin H.rowCount) (hpivot : H.effectivePivotRowOption column = some row) : 2 ∣ z column - H.effectiveFreeLiftSum row z

theorem GapCVP.Core.BinaryAffineSystem.effectiveBasis_mulVec_coefficients_of_normal (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (z : Fin H.dimension → ℤ) (hz : H.InLattice z = true) : H.effectiveSquareBasisMatrix.mulVec (H.effectiveBasisCoefficients z) = z

theorem GapCVP.Core.BinaryAffineSystem.effectiveBasis_mulVec_mem_lattice_of_normal (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (coefficients : Fin H.dimension → ℤ) : H.InLattice (H.effectiveSquareBasisMatrix.mulVec coefficients) = true

theorem GapCVP.Core.BinaryAffineSystem.inLattice_iff_exists_effectiveBasis_of_normal (H : BinaryAffineSystem) (hnormal : EffectiveBinaryGaussian.PrefixNormal (List.finRange H.dimension).reverse H.effectiveGaussianState = true) (hunique : ∀ (first second : Fin H.rowCount × Fin H.dimension), first ∈ H.effectiveGaussianState.pivots → second ∈ H.effectiveGaussianState.pivots → first.1 = second.1 → first.2 = second.2) (z : Fin H.dimension → ℤ) : H.InLattice z = true ↔ ∃ (coefficients : Fin H.dimension → ℤ), H.effectiveSquareBasisMatrix.mulVec coefficients = z

theorem GapCVP.Core.BinaryAffineSystem.effectivePivotRows_unique (H : BinaryAffineSystem) (first second : Fin H.rowCount × Fin H.dimension) (hfirst : first ∈ H.effectiveGaussianState.pivots) (hsecond : second ∈ H.effectiveGaussianState.pivots) (hrow : first.1 = second.1) : first.2 = second.2

theorem GapCVP.Core.BinaryAffineSystem.inLattice_iff_exists_effectiveSquareBasisMatrix (H : BinaryAffineSystem) (z : Fin H.dimension → ℤ) : H.InLattice z = true ↔ ∃ (coefficients : Fin H.dimension → ℤ), H.effectiveSquareBasisMatrix.mulVec coefficients = z

def GapCVP.Core.BinaryAffineSystem.effectiveReducedConsistent (H : BinaryAffineSystem) : Bool

GapCVP reduction support.

Equations

• H.effectiveReducedConsistent = decide (∀ (row : Fin H.rowCount), H.effectiveGaussianState.nextPivot ≤ ↑row → H.effectiveGaussianState.system.rhs row = 0)

@[simp]

theorem GapCVP.Core.BinaryAffineSystem.effectiveReducedConsistent_iff (H : BinaryAffineSystem) : H.effectiveReducedConsistent = true ↔ ∀ (row : Fin H.rowCount), H.effectiveGaussianState.nextPivot ≤ ↑row → H.effectiveGaussianState.system.rhs row = 0

theorem GapCVP.Core.BinaryAffineSystem.effectiveAffineBits_satisfies (H : BinaryAffineSystem) (hconsistent : H.effectiveReducedConsistent = true) : H.effectiveGaussianState.system.Satisfies H.effectiveAffineBits = true

theorem GapCVP.Core.BinaryAffineSystem.effectiveAffineRepresentative_solves (H : BinaryAffineSystem) (hconsistent : H.effectiveReducedConsistent = true) : H.Solves H.effectiveAffineRepresentative = true

theorem GapCVP.Core.BinaryAffineSystem.effectiveReducedConsistent_iff_solvable (H : BinaryAffineSystem) : H.effectiveReducedConsistent = true ↔ ∃ (z : Fin H.dimension → ℤ), H.Solves z = true

theorem GapCVP.Core.effectiveConstructionAInstance_solution_coset (H : BinaryAffineSystem) (hconsistent : H.effectiveReducedConsistent = true) (z : Fin H.dimension → ℤ) : H.Solves (H.effectiveAffineRepresentative - z) = true ↔ ∃ (coefficients : Fin H.dimension → ℤ), H.effectiveSquareBasisMatrix.mulVec coefficients = z

theorem GapCVP.Core.effectiveConstructionAInstance_yes_iff_signedSolution (H : BinaryAffineSystem) (hdimension : 0 < H.dimension) (hconsistent : H.effectiveReducedConsistent = true) (radius : ℚ) (hradius : 0 < radius) : (effectiveConstructionAInstance H hdimension radius hradius).IsYes = true ↔ ∃ (v : Fin H.dimension → ℤ), H.Solves v = true ∧ ↑(integerSquaredNorm v) ≤ ↑radius ^ 2

theorem GapCVP.Core.effectiveConstructionAInstance_no_iff_signedSolutionNorm (H : BinaryAffineSystem) (hdimension : 0 < H.dimension) (hconsistent : H.effectiveReducedConsistent = true) (radius : ℚ) (hradius : 0 < radius) (exponent : ℝ) : GapCVPInstance.IsNo exponent (effectiveConstructionAInstance H hdimension radius hradius) = true ↔ ∀ (v : Fin H.dimension → ℤ), H.Solves v = true → (↑H.dimension ^ exponent * ↑radius) ^ 2 < ↑(integerSquaredNorm v)

def GapCVP.Factor400BinaryPhysicalWorkers.factor400KeepFirstDropSecondWord : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryPhysicalWorkers.factor400KeepFirstDropSecondWord [] = []
• GapCVP.Factor400BinaryPhysicalWorkers.factor400KeepFirstDropSecondWord (marker :: remaining) = marker :: remaining.tail

noncomputable def GapCVP.Factor400BinaryPhysicalWorkers.factor400KeepFirstDropSecondComputable : BitTM factor400KeepFirstDropSecondWord

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryPhysicalWorkers.factor400KeepFirstDropSecondComputable = GapCVP.CNFGuardedFiveFamilyTagDispatchTM.keepFirstDropSecondComputable

def GapCVP.BinaryDimensionTM.sourceClauseCountUnary (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryDimensionTM.sourceClauseCountUnaryComputable : BitTM sourceClauseCountUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.BinaryDimensionTM.sourceClauseCountUnary_valid (formula : ThreeCNF) : sourceClauseCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (List.length formula) true

def GapCVP.BinaryDimensionTM.sourceInputLengthUnary (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryDimensionTM.sourceInputLengthUnary input = List.replicate input.length true

noncomputable def GapCVP.BinaryDimensionTM.sourceInputLengthUnaryComputable : BitTM sourceInputLengthUnary

GapCVP reduction support.

Equations

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

def GapCVP.BinaryDimensionTM.nextPowerUnaryOutput (target : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryDimensionTM.nextPowerUnaryComputable {target : List Bool → List Bool} (computer : BitTM target) : BitTM (nextPowerUnaryOutput target)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryDimensionTM.nextPowerUnaryOutput_valid (target : List Bool → List Bool) (input : List Bool) (n : ℕ) (htarget : target input = List.replicate n true) (hn : 0 < n) : nextPowerUnaryOutput target input = List.replicate (2 ^ Nat.clog 2 n) true

def GapCVP.BinaryDimensionTM.unarySubtractionOutput (base subtract : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryDimensionTM.unarySubtractionComputable {base subtract : List Bool → List Bool} (hbase : BitTM base) (hsubtract : BitTM subtract) : BitTM (unarySubtractionOutput base subtract)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryDimensionTM.unarySubtractionOutput_valid (base subtract : List Bool → List Bool) (input : List Bool) (first second : ℕ) (hbase : base input = List.replicate first true) (hsubtract : subtract input = List.replicate second true) : unarySubtractionOutput base subtract input = List.replicate (first - second) true

def GapCVP.SourceMixedRadixMaskSelectedRankTaggedSquareBasisPairTM.maskComputedWordEquality (first second : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMixedRadixMaskSelectedRankTaggedSquareBasisPairTM.maskComputedWordEqualityComputable {first second : List Bool → List Bool} (hfirst : BitTM first) (hsecond : BitTM second) : BitTM (maskComputedWordEquality first second)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceMixedRadixMaskSelectedRankTaggedSquareBasisPairTM.sourceQaryMaskSquareComputedWordEquality_valid (first second : List Bool → List Bool) (input : List Bool) : maskComputedWordEquality first second input = [decide (first input = second input)]