GapCVP proof, part 08, continuation 04

def GapCVP.CNFFiveFamilySourceIndexedORGadgetFoldCoreTM.flatAnnotatedIndexedORGadgetState (clauseIndex prefixWord pending active emitted count : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilySourceIndexedORGadgetFinalCert.actualWholeStructuralCNFOutputComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.gapFactor400 (I : GapCVPInstance) : ℝ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.gapYES400 (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.gapYES400 I = decide (GapCVP.gapCVPWellFormed I = true ∧ ∃ (z : Fin I.dimension → ℤ), GapCVP.distanceSquared I z ≤ ↑I.radius ^ 2)

noncomputable def GapCVP.gapNO400 (I : GapCVPInstance) : Bool

GapCVP reduction support.

Equations

• GapCVP.gapNO400 I = decide (GapCVP.gapCVPWellFormed I = true ∧ ∀ (z : Fin I.dimension → ℤ), (GapCVP.gapFactor400 I * ↑I.radius) ^ 2 < GapCVP.distanceSquared I z)

theorem GapCVP.gapYES400_not_gapNO400 (I : GapCVPInstance) (hyes : gapYES400 I = true) (hno : gapNO400 I = true) : False

noncomputable def GapCVP.gapCVP400Promise : PromiseProblem

GapCVP reduction support.

Equations

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

theorem GapCVP.gapYES400_iff_gapYES (I : GapCVPInstance) : gapYES400 I = true ↔ gapYES I = true

@[reducible, inline]

abbrev GapCVP.Factor400BinaryCanonicalNo.adaptedCanonicalNoInstance : GapCVPInstance

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryCanonicalNo.adaptedCanonicalNoWord : List Bool

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCanonicalNo.adaptedCanonicalNoWord = (GapCVP.binaryFinEncoding GapCVP.GapCVPInstance).encode GapCVP.Factor400BinaryCanonicalNo.adaptedCanonicalNoInstance

theorem GapCVP.Factor400BinaryCanonicalNo.adaptedCanonicalNoWord_mem_no : gapCVP400Promise.no adaptedCanonicalNoWord = true

structure GapCVP.Core.Literal (variableCount : ℕ) : Type

GapCVP reduction support.

• variableIndex : Fin variableCount

  GapCVP reduction support.

• satisfyingValue : Bool

  GapCVP reduction support.

def GapCVP.Core.instDecidableEqLiteral.decEq {variableCount✝ : ℕ} (x✝ x✝¹ : Literal variableCount✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GapCVP.Core.instDecidableEqLiteral {variableCount✝ : ℕ} : DecidableEq (Literal variableCount✝)

Equations

• GapCVP.Core.instDecidableEqLiteral = GapCVP.Core.instDecidableEqLiteral.decEq

structure GapCVP.Core.Clause (variableCount : ℕ) : Type

GapCVP reduction support.

• literals : Finset (Literal variableCount)

  GapCVP reduction support.

• nonempty : self.literals.Nonempty
• size_le_three : self.literals.card ≤ 3

structure GapCVP.Core.Formula : Type

GapCVP reduction support.

• variableCount : ℕ

  GapCVP reduction support.

• clauses : List (Clause self.variableCount)

  GapCVP reduction support.

noncomputable def GapCVP.Core.Clause.Satisfied {variableCount : ℕ} (clause : Clause variableCount) (assignment : Fin variableCount → Bool) : Bool

GapCVP reduction support.

Equations

• clause.Satisfied assignment = decide (∃ literal ∈ clause.literals, assignment literal.variableIndex = literal.satisfyingValue)

noncomputable def GapCVP.Core.Formula.Satisfied (formula : Formula) (assignment : Fin formula.variableCount → Bool) : Bool

GapCVP reduction support.

Equations

• formula.Satisfied assignment = decide (∀ (i : Fin formula.clauses.length), (formula.clauses.get i).Satisfied assignment = true)

noncomputable def GapCVP.Core.Formula.Satisfiable (formula : Formula) : Bool

GapCVP reduction support.

Equations

• formula.Satisfiable = decide (∃ (assignment : Fin formula.variableCount → Bool), formula.Satisfied assignment = true)

theorem GapCVP.Factor400FormulaBridge.formula_satisfied_iff_forall_mem (formula : Core.Formula) (assignment : Fin formula.variableCount → Bool) : formula.Satisfied assignment = true ↔ ∀ clause ∈ formula.clauses, clause.Satisfied assignment = true

def GapCVP.BinarySourceVariableCompaction.occurringVariables (formula : ThreeCNF) : List ℕ

GapCVP reduction support.

Equations

• GapCVP.BinarySourceVariableCompaction.occurringVariables formula = (GapCVP.SourceMachineCert.formulaVariables formula).eraseDups

def GapCVP.BinarySourceVariableCompaction.occurringVariableCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.BinarySourceVariableCompaction.occurringVariableCount formula = (GapCVP.BinarySourceVariableCompaction.occurringVariables formula).length

theorem GapCVP.BinarySourceVariableCompaction.mem_occurringVariables_iff (formula : ThreeCNF) (name : ℕ) : name ∈ occurringVariables formula ↔ name ∈ SourceMachineCert.formulaVariables formula

theorem GapCVP.BinarySourceVariableCompaction.eraseDups_nodup (names : List ℕ) : names.eraseDups.Nodup

theorem GapCVP.BinarySourceVariableCompaction.occurringVariables_nodup (formula : ThreeCNF) : (occurringVariables formula).Nodup

def GapCVP.BinarySourceVariableCompaction.compactVariableRank (formula : ThreeCNF) (name : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.BinarySourceVariableCompaction.compactVariableRank formula name = List.idxOf name (GapCVP.BinarySourceVariableCompaction.occurringVariables formula)

theorem GapCVP.BinarySourceVariableCompaction.mem_formulaVariables_iff_exists_literal (formula : ThreeCNF) (name : ℕ) : name ∈ SourceMachineCert.formulaVariables formula ↔ ∃ clause ∈ formula, ∃ (index : Fin 3), (clause index).1 = name

structure GapCVP.Core.EffectiveBinaryGaussian.System (m n : ℕ) : Type

GapCVP reduction support.

• check : Matrix (Fin m) (Fin n) (ZMod 2)

  GapCVP reduction support.

• rhs : Fin m → ZMod 2

  GapCVP reduction support.

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

GapCVP reduction support.

Equations

• system.Satisfies assignment = decide (system.check.mulVec assignment = system.rhs)

def GapCVP.Core.EffectiveBinaryGaussian.swapRows {m n : ℕ} (system : System m n) (left right : Fin m) : System m n

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryGaussian.swapRows_satisfies_iff {m n : ℕ} (system : System m n) (left right : Fin m) (assignment : Fin n → ZMod 2) : (swapRows system left right).Satisfies assignment = true ↔ system.Satisfies assignment = true

def GapCVP.Core.EffectiveBinaryGaussian.addRow {m n : ℕ} (system : System m n) (source target : Fin m) : System m n

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryGaussian.binary_add_self (value : ZMod 2) : value + value = 0

theorem GapCVP.Core.EffectiveBinaryGaussian.binary_eq_zero_of_ne_one (value : ZMod 2) (hne : value ≠ 1) : value = 0

theorem GapCVP.Core.EffectiveBinaryGaussian.addRow_satisfies_iff {m n : ℕ} (system : System m n) (source target : Fin m) (hne : source ≠ target) (assignment : Fin n → ZMod 2) : (addRow system source target).Satisfies assignment = true ↔ system.Satisfies assignment = true

inductive GapCVP.Core.EffectiveBinaryGaussian.RowOperation (m : ℕ) : Type

GapCVP reduction support.

• swap {m : ℕ} (left right : Fin m) : RowOperation m
• add {m : ℕ} (source target : Fin m) (distinct : source ≠ target) : RowOperation m

def GapCVP.Core.EffectiveBinaryGaussian.RowOperation.apply {m n : ℕ} (operation : RowOperation m) (system : System m n) : System m n

GapCVP reduction support.

Equations

• (GapCVP.Core.EffectiveBinaryGaussian.RowOperation.swap left right).apply system = GapCVP.Core.EffectiveBinaryGaussian.swapRows system left right
• (GapCVP.Core.EffectiveBinaryGaussian.RowOperation.add source target distinct).apply system = GapCVP.Core.EffectiveBinaryGaussian.addRow system source target

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

structure GapCVP.Core.EffectiveBinaryGaussian.State (m n : ℕ) : Type

GapCVP reduction support.

• system : System m n

  GapCVP reduction support.

• nextPivot : ℕ

  GapCVP reduction support.

• pivots : List (Fin m × Fin n)

  GapCVP reduction support.

• operations : List (RowOperation m)

  GapCVP reduction support.

def GapCVP.Core.EffectiveBinaryGaussian.initialState {m n : ℕ} (system : System m n) : State m n

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryGaussian.initialState system = { system := system, nextPivot := 0, pivots := [], operations := [] }

def GapCVP.Core.EffectiveBinaryGaussian.applyOperation {m n : ℕ} (state : State m n) (operation : RowOperation m) : State m n

GapCVP reduction support.

Equations

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

def GapCVP.Core.EffectiveBinaryGaussian.findPivotOption {m n : ℕ} (state : State m n) (column : Fin n) : Option (Fin m)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryGaussian.findPivotOption state column = List.find? (fun (row : Fin m) => decide (state.nextPivot ≤ ↑row ∧ state.system.check row column = 1)) (List.finRange m)

theorem GapCVP.Core.EffectiveBinaryGaussian.findPivotOption_some {m n : ℕ} (state : State m n) (column : Fin n) (row : Fin m) (h : findPivotOption state column = some row) : state.nextPivot ≤ ↑row ∧ state.system.check row column = 1

def GapCVP.Core.EffectiveBinaryGaussian.clearTarget {m n : ℕ} (pivot : Fin m) (column : Fin n) (state : State m n) (target : Fin m) : State m n

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryGaussian.clearTarget_check_pivot {m n : ℕ} (pivot : Fin m) (column otherColumn : Fin n) (state : State m n) (target : Fin m) : (clearTarget pivot column state target).system.check pivot otherColumn = state.system.check pivot otherColumn

theorem GapCVP.Core.EffectiveBinaryGaussian.clearTarget_rhs_pivot {m n : ℕ} (pivot : Fin m) (column : Fin n) (state : State m n) (target : Fin m) : (clearTarget pivot column state target).system.rhs pivot = state.system.rhs pivot

def GapCVP.Core.EffectiveBinaryGaussian.clearTargets {m n : ℕ} (pivot : Fin m) (column : Fin n) (targets : List (Fin m)) (state : State m n) : State m n

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryGaussian.clearTargets pivot column targets state = List.foldl (GapCVP.Core.EffectiveBinaryGaussian.clearTarget pivot column) state targets

def GapCVP.Core.EffectiveBinaryGaussian.columnStep {m n : ℕ} (state : State m n) (column : Fin n) : State m n

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryGaussian.columnStep_pivot_column {m n : ℕ} (state : State m n) (column : Fin n) (hrow : state.nextPivot < m) (candidate : Fin m) (hfound : findPivotOption state column = some candidate) (row : Fin m) : (columnStep state column).system.check row column = if row = ⟨state.nextPivot, hrow⟩ then 1 else 0

theorem GapCVP.Core.EffectiveBinaryGaussian.clearTargets_check_of_pivot_zero {m n : ℕ} (pivot : Fin m) (pivotColumn oldColumn : Fin n) (targets : List (Fin m)) (state : State m n) (hzero : state.system.check pivot oldColumn = 0) (row : Fin m) : (clearTargets pivot pivotColumn targets state).system.check row oldColumn = state.system.check row oldColumn

def GapCVP.Core.EffectiveBinaryGaussian.runColumns {m n : ℕ} (columns : List (Fin n)) (state : State m n) : State m n

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryGaussian.runColumns columns state = List.foldl GapCVP.Core.EffectiveBinaryGaussian.columnStep state columns

def GapCVP.Core.EffectiveBinaryGaussian.eliminate {m n : ℕ} (system : System m n) : State m n

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryGaussian.eliminate system = GapCVP.Core.EffectiveBinaryGaussian.runColumns (List.finRange n) (GapCVP.Core.EffectiveBinaryGaussian.initialState system)

theorem GapCVP.Core.EffectiveBinaryGaussian.eliminate_satisfies_iff {m n : ℕ} (system : System m n) (assignment : Fin n → ZMod 2) : (eliminate system).system.Satisfies assignment = true ↔ system.Satisfies assignment = true

@[reducible, inline]

abbrev GapCVP.Core.EffectiveBinaryField.Word (e : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.Word e = (Fin e → Bool)

def GapCVP.Core.EffectiveBinaryField.allWords (e : ℕ) : List (Word e)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.Core.EffectiveBinaryField.allWords 0 = [fun (i : Fin 0) => i.elim0]

theorem GapCVP.Core.EffectiveBinaryField.mem_allWords {e : ℕ} (word : Word e) : word ∈ allWords e

def GapCVP.Core.EffectiveBinaryField.bitValue (bit : Bool) : ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.bitValue bit = if bit = true then 1 else 0

theorem GapCVP.Core.EffectiveBinaryField.bitValue_xor (left right : Bool) : bitValue (left ^^ right) = bitValue left + bitValue right

noncomputable def GapCVP.Core.EffectiveBinaryField.wordPolynomial {e : ℕ} (word : Word e) : Polynomial (ZMod 2)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.wordPolynomial word = ∑ i : Fin e, (Polynomial.monomial ↑i) (GapCVP.Core.EffectiveBinaryField.bitValue (word i))

@[simp]

theorem GapCVP.Core.EffectiveBinaryField.wordPolynomial_coeff_fin {e : ℕ} (word : Word e) (i : Fin e) : (wordPolynomial word).coeff ↑i = bitValue (word i)

theorem GapCVP.Core.EffectiveBinaryField.wordPolynomial_coeff_eq_zero {e : ℕ} (word : Word e) (k : ℕ) (hk : e ≤ k) : (wordPolynomial word).coeff k = 0

theorem GapCVP.Core.EffectiveBinaryField.wordPolynomial_degree_lt {e : ℕ} (word : Word e) : (wordPolynomial word).degree < ↑e

noncomputable def GapCVP.Core.EffectiveBinaryField.monicPolynomial {e : ℕ} (word : Word e) : Polynomial (ZMod 2)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.monicPolynomial word = Polynomial.X ^ e + GapCVP.Core.EffectiveBinaryField.wordPolynomial word

noncomputable def GapCVP.Core.EffectiveBinaryField.coefficientWord (e : ℕ) (p : Polynomial (ZMod 2)) : Word e

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.coefficientWord e p i = decide (p.coeff ↑i = 1)

def GapCVP.Core.EffectiveBinaryField.multiplyWords {e : ℕ} (left right : Word e) : Word (2 * e)

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryField.wordPolynomial_multiplyWords {e : ℕ} (left right : Word e) : wordPolynomial (multiplyWords left right) = wordPolynomial left * wordPolynomial right

def GapCVP.Core.EffectiveBinaryField.monicWord {e : ℕ} (lower : Word e) : Word (2 * e)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.monicWord lower i = if h : ↑i < e then lower ⟨↑i, h⟩ else decide (↑i = e)

theorem GapCVP.Core.EffectiveBinaryField.bitValue_injective : Function.Injective bitValue

def GapCVP.Core.EffectiveBinaryField.noProperFactors (e : ℕ) (lower : Word e) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.EffectiveBinaryField.noProperFactors_eq_true_iff {e : ℕ} (lower : Word e) : noProperFactors e lower = true ↔ ∀ (left right : Word e), multiplyWords left right ≠ monicWord lower

def GapCVP.Core.EffectiveBinaryField.findIrreducibleWordOption (e : ℕ) : Option (Word e)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.findIrreducibleWordOption e = List.find? (GapCVP.Core.EffectiveBinaryField.noProperFactors e) (GapCVP.Core.EffectiveBinaryField.allWords e)

theorem GapCVP.Core.EffectiveBinaryField.findIrreducibleWordOption_exists (e : ℕ) (he : 0 < e) : ∃ (word : Word e), findIrreducibleWordOption e = some word ∧ Irreducible (monicPolynomial word)

def GapCVP.Core.EffectiveBinaryField.irreducibleWord (e : ℕ) : Word e

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.irreducibleWord e = (GapCVP.Core.EffectiveBinaryField.findIrreducibleWordOption e).getD fun (x : Fin e) => false

def GapCVP.Core.EffectiveBinaryField.xorAt {d : ℕ} (word : Word d) (index : Fin d) (bit : Bool) : Word d

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.xorAt word index bit i = if i = index then word i ^^ bit else word i

theorem GapCVP.Core.EffectiveBinaryField.wordPolynomial_xorAt {d : ℕ} (word : Word d) (index : Fin d) (bit : Bool) : wordPolynomial (xorAt word index bit) = wordPolynomial word + (Polynomial.monomial ↑index) (bitValue bit)

def GapCVP.Core.EffectiveBinaryField.shiftXor {e : ℕ} (lower : Word e) (degree : ℕ) (word : Word (2 * e)) : Word (2 * e)

GapCVP reduction support.

Equations

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

def GapCVP.Core.EffectiveBinaryField.reduceAt {e : ℕ} (lower : Word e) (degree : ℕ) (word : Word (2 * e)) : Word (2 * e)

GapCVP reduction support.

Equations

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

def GapCVP.Core.EffectiveBinaryField.reduceProduct {e : ℕ} (lower : Word e) (word : Word (2 * e)) : Word (2 * e)

GapCVP reduction support.

Equations

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

def GapCVP.Core.EffectiveBinaryField.multiplyMod {e : ℕ} (lower left right : Word e) : Word e

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.multiplyMod lower left right i = GapCVP.Core.EffectiveBinaryField.reduceProduct lower (GapCVP.Core.EffectiveBinaryField.multiplyWords left right) ⟨↑i, ⋯⟩

noncomputable def GapCVP.Core.EffectiveBinaryField.selectedPolynomial (e : ℕ) : Polynomial (ZMod 2)

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.selectedPolynomial e = GapCVP.Core.EffectiveBinaryField.monicPolynomial (GapCVP.Core.EffectiveBinaryField.irreducibleWord e)

theorem GapCVP.Core.EffectiveBinaryField.selectedPolynomial_monic (e : ℕ) : (selectedPolynomial e).Monic

theorem GapCVP.Core.EffectiveBinaryField.selectedPolynomial_natDegree (e : ℕ) : (selectedPolynomial e).natDegree = e

@[reducible, inline]

abbrev GapCVP.Core.EffectiveBinaryField.Extension (e : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.Extension e = AdjoinRoot (GapCVP.Core.EffectiveBinaryField.selectedPolynomial e)

noncomputable def GapCVP.Core.EffectiveBinaryField.extensionBasis (e : ℕ) : Module.Basis (Fin e) (ZMod 2) (Extension e)

Power basis of the selected binary field extension, reindexed by its degree.

Equations

• GapCVP.Core.EffectiveBinaryField.extensionBasis e = (AdjoinRoot.powerBasisAux' ⋯).reindex (finCongr ⋯)

@[instance_reducible]

noncomputable instance GapCVP.Core.EffectiveBinaryField.extensionFintype (e : ℕ) : Fintype (Extension e)

Equations

• GapCVP.Core.EffectiveBinaryField.extensionFintype e = Fintype.ofEquiv (Fin e → ZMod 2) (GapCVP.Core.EffectiveBinaryField.extensionBasis e).equivFun.toEquiv.symm

noncomputable def GapCVP.Core.EffectiveBinaryField.extensionAlgEquivGaloisField (e : ℕ) (he : 0 < e) : Extension e ≃ₐ[ZMod 2] GaloisField 2 e

GapCVP reduction support.

Equations

• GapCVP.Core.EffectiveBinaryField.extensionAlgEquivGaloisField e he = GaloisField.algEquivGaloisFieldOfFintype 2 e ⋯

def GapCVP.BinaryFieldBasis.indexedWord (degree : ℕ) (index : Fin (2 ^ degree)) : Core.EffectiveBinaryField.Word degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.indexedWord degree index bit = (↑index).testBit ↑bit

theorem GapCVP.BinaryFieldBasis.indexedWord_injective (degree : ℕ) : Function.Injective (indexedWord degree)

def GapCVP.BinaryFieldBasis.boundedWordIndex {degree count : ℕ} (hcount : count ≤ 2 ^ degree) : Fin count ↪ Fin (2 ^ degree)

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.boundedWordIndex hcount = Fin.castLEEmb hcount

def GapCVP.BinaryFieldBasis.evaluationWordIndex {degree count : ℕ} (hcount : count ≤ 2 ^ degree) : Fin (2 ^ degree - count) ↪ Fin (2 ^ degree)

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.evaluationWordIndex hcount = (Fin.natAddEmb count).trans (finCongr ⋯).toEmbedding

@[instance_reducible, instance 100]

noncomputable instance GapCVP.BinaryFieldBasis.factor400GaloisFieldFintype (degree : ℕ) : Fintype (GaloisField 2 degree)

Equations

• GapCVP.BinaryFieldBasis.factor400GaloisFieldFintype degree = Fintype.ofFinite (GaloisField 2 degree)

noncomputable def GapCVP.BinaryFieldBasis.wordElement {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) : Core.EffectiveBinaryField.Extension degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.wordElement word = (AdjoinRoot.mk (GapCVP.Core.EffectiveBinaryField.selectedPolynomial degree)) (GapCVP.Core.EffectiveBinaryField.wordPolynomial word)

theorem GapCVP.BinaryFieldBasis.wordElement_injective (degree : ℕ) : Function.Injective wordElement

noncomputable def GapCVP.BinaryFieldBasis.effectiveExtensionBasis (degree : ℕ) : Module.Basis (Fin degree) (ZMod 2) (Core.EffectiveBinaryField.Extension degree)

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.effectiveExtensionBasis degree = GapCVP.Core.EffectiveBinaryField.extensionBasis degree

noncomputable def GapCVP.BinaryFieldBasis.effectiveFieldBasis (degree : ℕ) (hdegree : 0 < degree) : Module.Basis (Fin degree) (ZMod 2) (GaloisField 2 degree)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryFieldBasis.effectiveFieldBasis_coordinates_transport (degree : ℕ) (hdegree : 0 < degree) (value : Core.EffectiveBinaryField.Extension degree) : (effectiveFieldBasis degree hdegree).equivFun ((Core.EffectiveBinaryField.extensionAlgEquivGaloisField degree hdegree) value) = (effectiveExtensionBasis degree).equivFun value

noncomputable def GapCVP.BinaryFieldBasis.indexedFieldEquiv (degree : ℕ) (hdegree : 0 < degree) : Fin (2 ^ degree) ≃ GaloisField 2 degree

GapCVP reduction support.

Equations

• GapCVP.BinaryFieldBasis.indexedFieldEquiv degree hdegree = Equiv.ofBijective (GapCVP.BinaryFieldBasis.indexedFieldElement✝ degree hdegree) ⋯

theorem GapCVP.BinaryFieldBasis.indexedFieldEquiv_apply (degree : ℕ) (hdegree : 0 < degree) (index : Fin (2 ^ degree)) : (indexedFieldEquiv degree hdegree) index = (Core.EffectiveBinaryField.extensionAlgEquivGaloisField degree hdegree) (wordElement (indexedWord degree index))

The indexed field equivalence evaluates the corresponding binary word.

noncomputable def GapCVP.BinaryFieldBasis.effectiveAnchor (degree : ℕ) (hdegree : 0 < degree) {count : ℕ} (hcount : count ≤ 2 ^ degree) : Fin count ↪ GaloisField 2 degree

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.BinaryFieldBasis.effectiveEvaluationEmbedding (degree : ℕ) (hdegree : 0 < degree) {count : ℕ} (hcount : count ≤ 2 ^ degree) : Fin (2 ^ degree - count) ↪ GaloisField 2 degree

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryFieldBasis.effectiveAnchor_apply (degree : ℕ) (hdegree : 0 < degree) {count : ℕ} (hcount : count ≤ 2 ^ degree) (index : Fin count) : (effectiveAnchor degree hdegree hcount) index = (Core.EffectiveBinaryField.extensionAlgEquivGaloisField degree hdegree) (wordElement (indexedWord degree ((boundedWordIndex hcount) index)))

The anchor embedding evaluates the indexed binary word in the extension field.

theorem GapCVP.BinaryFieldBasis.effectiveEvaluationEmbedding_apply (degree : ℕ) (hdegree : 0 < degree) {count : ℕ} (hcount : count ≤ 2 ^ degree) (index : Fin (2 ^ degree - count)) : (effectiveEvaluationEmbedding degree hdegree hcount) index = (Core.EffectiveBinaryField.extensionAlgEquivGaloisField degree hdegree) (wordElement (indexedWord degree ((evaluationWordIndex hcount) index)))

The evaluation embedding evaluates the indexed binary word in the extension field.

theorem GapCVP.BinaryFieldBasis.effectiveEvaluationEmbedding_ne_anchor (degree : ℕ) (hdegree : 0 < degree) {count : ℕ} (hcount : count ≤ 2 ^ degree) (point : Fin (2 ^ degree - count)) (anchor : Fin count) : (effectiveEvaluationEmbedding degree hdegree hcount) point ≠ (effectiveAnchor degree hdegree hcount) anchor

noncomputable def GapCVP.Core.binaryFieldVectorEquiv {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {e : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (dimension : ℕ) : (Fin dimension → K) ≃ₗ[ZMod 2] Fin dimension × Fin e → ZMod 2

GapCVP reduction support.

Equations

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

def GapCVP.Core.binaryFieldBitEmbedding {K : Type u_1} [Field K] [Algebra (ZMod 2) K] (dimension : ℕ) : (Fin dimension → ZMod 2) →ₗ[ZMod 2] Fin dimension → K

GapCVP reduction support.

Equations

• GapCVP.Core.binaryFieldBitEmbedding dimension = LinearMap.pi fun (i : Fin dimension) => Algebra.linearMap (ZMod 2) K ∘ₗ LinearMap.proj i

noncomputable def GapCVP.Core.binaryFieldParityLinearMap {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {e m n : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (checks : Matrix (Fin m) (Fin n) K) : (Fin n → ZMod 2) →ₗ[ZMod 2] Fin m × Fin e → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Core.binaryFieldParityLinearMap basis checks = ↑(GapCVP.Core.binaryFieldVectorEquiv basis m) ∘ₗ ↑(ZMod 2) checks.mulVecLin ∘ₗ GapCVP.Core.binaryFieldBitEmbedding n

noncomputable def GapCVP.Core.binaryFieldParityMatrix {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {e m n : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (checks : Matrix (Fin m) (Fin n) K) : Matrix (Fin m × Fin e) (Fin n) (ZMod 2)

GapCVP reduction support.

Equations

• GapCVP.Core.binaryFieldParityMatrix basis checks = LinearMap.toMatrix' (GapCVP.Core.binaryFieldParityLinearMap basis checks)

def GapCVP.Core.binaryResidue {n : ℕ} (z : Fin n → ℤ) : Fin n → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Core.binaryResidue z i = ↑(z i)

theorem GapCVP.Core.binaryResidue_sub {n : ℕ} (x y : Fin n → ℤ) : binaryResidue (x - y) = binaryResidue x - binaryResidue y

structure GapCVP.Core.BinaryAffineSystem : Type

GapCVP reduction support.

• rowCount : ℕ

  GapCVP reduction support.

• dimension : ℕ

  GapCVP reduction support.

• check : Matrix (Fin self.rowCount) (Fin self.dimension) (ZMod 2)

  GapCVP reduction support.

• rightHandSide : Fin self.rowCount → ZMod 2

  GapCVP reduction support.

noncomputable def GapCVP.Core.BinaryAffineSystem.Solves (system : BinaryAffineSystem) (z : Fin system.dimension → ℤ) : Bool

GapCVP reduction support.

Equations

• system.Solves z = decide (system.check.mulVec (GapCVP.Core.binaryResidue z) = system.rightHandSide)

noncomputable def GapCVP.Core.BinaryAffineSystem.InLattice (system : BinaryAffineSystem) (z : Fin system.dimension → ℤ) : Bool

GapCVP reduction support.

Equations

• system.InLattice z = decide (system.check.mulVec (GapCVP.Core.binaryResidue z) = 0)

theorem GapCVP.Core.BinaryAffineSystem.solves_sub_iff_inLattice (system : BinaryAffineSystem) {u : Fin system.dimension → ℤ} (hu : system.Solves u = true) (z : Fin system.dimension → ℤ) : system.Solves (u - z) = true ↔ system.InLattice z = true

@[reducible, inline]

abbrev GapCVP.Core.assembledBinaryRow {ι : Type u_1} (rowCounts : ι → ℕ) (e : ℕ) : Type u_1

GapCVP reduction support.

Equations

• GapCVP.Core.assembledBinaryRow rowCounts e = ((family : ι) × Fin (rowCounts family) × Fin e)

noncomputable def GapCVP.Core.assembledBinaryParityMatrix {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e n : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin n) K) : Matrix (assembledBinaryRow rowCounts e) (Fin n) (ZMod 2)

GapCVP reduction support.

Equations

• GapCVP.Core.assembledBinaryParityMatrix basis rowCounts checks row column = GapCVP.Core.binaryFieldParityMatrix basis (checks row.fst) row.snd column

noncomputable def GapCVP.Core.assembledBinaryRightHandSide {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (targets : (family : ι) → Fin (rowCounts family) → K) : assembledBinaryRow rowCounts e → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Core.assembledBinaryRightHandSide basis rowCounts targets row = (GapCVP.Core.binaryFieldVectorEquiv basis (rowCounts row.fst)) (targets row.fst) row.snd

@[simp]

theorem GapCVP.Core.assembledBinaryParityMatrix_mulVec_apply {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e n : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin n) K) (bits : Fin n → ZMod 2) (row : assembledBinaryRow rowCounts e) : (assembledBinaryParityMatrix basis rowCounts checks).mulVec bits row = (binaryFieldParityMatrix basis (checks row.fst)).mulVec bits row.snd

theorem GapCVP.Core.assembledBinaryParityMatrix_mulVec_eq_iff {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e n : ℕ} (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin n) K) (bits : Fin n → ZMod 2) (targets : (family : ι) → Fin (rowCounts family) → K) : (assembledBinaryParityMatrix basis rowCounts checks).mulVec bits = assembledBinaryRightHandSide basis rowCounts targets ↔ ∀ (family : ι), ((checks family).mulVec fun (position : Fin n) => (algebraMap (ZMod 2) K) (bits position)) = targets family

@[reducible, inline]

noncomputable abbrev GapCVP.Core.assembledBinaryAffineSystem {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e n : ℕ} [Fintype ι] (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin n) K) (targets : (family : ι) → Fin (rowCounts family) → K) : BinaryAffineSystem

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.assembledBinaryAffineSystem_solves_iff {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {e n : ℕ} [Fintype ι] (basis : Module.Basis (Fin e) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin n) K) (targets : (family : ι) → Fin (rowCounts family) → K) (z : Fin n → ℤ) : (assembledBinaryAffineSystem basis rowCounts checks targets).Solves z = true ↔ ∀ (family : ι), ((checks family).mulVec fun (position : Fin n) => (algebraMap (ZMod 2) K) ↑(z position)) = targets family

theorem GapCVP.Core.source_moment_degree_le {N d : ℕ} (hd : d ≤ N) : d * N ^ 30 ≤ N ^ 31

def GapCVP.Core.sourcePuncturedGrid {k : Type u_1} [Fintype k] [DecidableEq k] (variablePlaces : Finset k) : Finset k

GapCVP reduction support.

Equations

• GapCVP.Core.sourcePuncturedGrid variablePlaces = Finset.univ \ variablePlaces

theorem GapCVP.Core.source_moment_degree_lt_actual_grid {k : Type u_1} [Fintype k] [DecidableEq k] {N : ℕ} (variablePlaces : Finset k) (hN : 100 ≤ N) (hq : N ^ 200 ≤ Fintype.card k) (hplaces : variablePlaces.card ≤ N) : N ^ 31 < (sourcePuncturedGrid variablePlaces).card

theorem GapCVP.Core.source_cleared_moment_degree_lt_half_field_size {N q : ℕ} (hN : 100 ≤ N) (hq : N ^ 200 ≤ q) : 2 * N ^ 39 < q / 2

theorem GapCVP.Core.source_clause_support_lt_moment_budget {N : ℕ} (hN : 100 ≤ N) : 9 * N ^ 4 < N ^ 30

theorem GapCVP.Core.source_valuation_index_lt_moment_budget {N h U : ℕ} (hN : 100 ≤ N) (hh : h ≤ N ^ 4) (hU : U ≤ 4 * N ^ 17) : h * U + h < N ^ 30

theorem GapCVP.Core.source_cleared_moment_degree_le {N d h j : ℕ} (hd : d ≤ N) (hh : h ≤ N ^ 4) (hj : j ≤ N ^ 30) : 2 * d * h ^ 2 * j ≤ 2 * N ^ 39

@[irreducible]

def GapCVP.Core.sourceFieldExponent (N : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.Core.sourceFieldExponent N = Nat.clog 2 (N ^ 200)

theorem GapCVP.Core.sourceFieldExponent_eq (N : ℕ) : sourceFieldExponent N = Nat.clog 2 (N ^ 200)

@[reducible, inline]

abbrev GapCVP.Core.SourceFiniteField (N : ℕ) : Type

GapCVP reduction support.

Equations

• GapCVP.Core.SourceFiniteField N = GaloisField 2 (GapCVP.Core.sourceFieldExponent N)

@[instance_reducible]

noncomputable instance GapCVP.Core.sourceFiniteFieldFintype (N : ℕ) : Fintype (SourceFiniteField N)

Equations

• GapCVP.Core.sourceFiniteFieldFintype N = Fintype.ofFinite (GapCVP.Core.SourceFiniteField N)

theorem GapCVP.Core.sourceFieldExponent_pos {N : ℕ} (hN : 100 ≤ N) : 0 < sourceFieldExponent N

theorem GapCVP.Core.sourceFiniteField_card {N : ℕ} (hN : 100 ≤ N) : Fintype.card (SourceFiniteField N) = 2 ^ sourceFieldExponent N

theorem GapCVP.Core.sourceFiniteField_card_lower {N : ℕ} (hN : 100 ≤ N) : N ^ 200 ≤ Fintype.card (SourceFiniteField N)

theorem GapCVP.Core.sourceFiniteField_card_upper {N : ℕ} (hN : 100 ≤ N) : Fintype.card (SourceFiniteField N) < 2 * N ^ 200

theorem GapCVP.Core.hankel_det_eq_vandermonde_det_sq {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → R) : (Matrix.of fun (i j : Fin n) => ∑ k : Fin n, v k ^ (↑i + ↑j)).det = (Matrix.vandermonde v).det ^ 2

theorem GapCVP.Core.hankel_det_ne_zero_of_injective {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {v : Fin n → R} (hv : Function.Injective v) : (Matrix.of fun (i j : Fin n) => ∑ k : Fin n, v k ^ (↑i + ↑j)).det ≠ 0

theorem GapCVP.Core.polynomial_eq_of_agree_on_points {K : Type u_1} [Field K] (points : Finset K) (f g : Polynomial K) (hdeg : max f.natDegree g.natDegree < points.card) (hagree : ∀ x ∈ points, Polynomial.eval x f = Polynomial.eval x g) : f = g

noncomputable def GapCVP.Core.supportMoment {K : Type u_1} [Field K] (support : Finset K) (j : ℕ) : K

GapCVP reduction support.

Equations

• GapCVP.Core.supportMoment support j = ∑ a ∈ support, a ^ j

def GapCVP.Core.paritySupport {K : Type u_1} [DecidableEq K] : List (Finset K) → Finset K

GapCVP reduction support.

Equations

• GapCVP.Core.paritySupport [] = ∅
• GapCVP.Core.paritySupport (s :: supports) = symmDiff s (GapCVP.Core.paritySupport supports)

theorem GapCVP.Core.global_root_mem_subtype_of_moment_refinement {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] (global : Finset K) (subtypes : List (Finset K)) (hmoments : ∀ j < global.card + (paritySupport subtypes).card, supportMoment global j = (List.map (fun (s : Finset K) => supportMoment s j) subtypes).sum) {a : K} (ha : a ∈ global) : ∃ s ∈ subtypes, a ∈ s

theorem GapCVP.Core.scaled_shifted_supportMoment {K : Type u_1} [Field K] (support : Finset K) (β π : K) (j : ℕ) (hπ : π ≠ 0) : π ^ j * ∑ w ∈ support, ((w - β) / π) ^ j = ∑ l ∈ Finset.range (j + 1), ↑(j.choose l) * (-β) ^ (j - l) * supportMoment support l

noncomputable def GapCVP.Core.shiftedMomentCombination {K : Type u_1} [Field K] (moments : ℕ → Polynomial K) (β : K) (j : ℕ) : Polynomial K

GapCVP reduction support.

Equations

• GapCVP.Core.shiftedMomentCombination moments β j = ∑ l ∈ Finset.range (j + 1), Polynomial.C (↑(j.choose l) * (-β) ^ (j - l)) * moments l

def GapCVP.Core.sourceSizeParameter (encodingLength : ℕ) (formula : Formula) : ℕ

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSizeParameter encodingLength formula = 100 + encodingLength + formula.variableCount + formula.clauses.length

theorem GapCVP.Core.sourceSizeParameter_ge_one_hundred (encodingLength : ℕ) (formula : Formula) : 100 ≤ sourceSizeParameter encodingLength formula

theorem GapCVP.Core.source_variableCount_le_size (encodingLength : ℕ) (formula : Formula) : formula.variableCount ≤ sourceSizeParameter encodingLength formula

theorem GapCVP.Core.source_clauseCount_le_size (encodingLength : ℕ) (formula : Formula) : formula.clauses.length ≤ sourceSizeParameter encodingLength formula

def GapCVP.Core.Clause.variableSet {m : ℕ} (C : Clause m) : Finset (Fin m)

GapCVP reduction support.

Equations

• C.variableSet = Finset.image (fun (literal : GapCVP.Core.Literal m) => literal.variableIndex) C.literals

theorem GapCVP.Core.Clause.variableSet_card_le_three {m : ℕ} (C : Clause m) : C.variableSet.card ≤ 3

@[reducible, inline]

abbrev GapCVP.Core.Clause.LocalVariable {m : ℕ} (C : Clause m) : Type

GapCVP reduction support.

Equations

• C.LocalVariable = ↥C.variableSet

@[reducible, inline]

abbrev GapCVP.Core.Clause.LocalAssignment {m : ℕ} (C : Clause m) : Type

GapCVP reduction support.

Equations

• C.LocalAssignment = (C.LocalVariable → Bool)

noncomputable def GapCVP.Core.Clause.LocalSatisfied {m : ℕ} (C : Clause m) (assignment : C.LocalAssignment) : Bool

GapCVP reduction support.

Equations

• C.LocalSatisfied assignment = decide (∃ (literal : GapCVP.Core.Literal m) (hliteral : literal ∈ C.literals), assignment ⟨literal.variableIndex, ⋯⟩ = literal.satisfyingValue)

@[reducible, inline]

abbrev GapCVP.Core.Clause.SatisfyingLocalTuple {m : ℕ} (C : Clause m) : Type

GapCVP reduction support.

Equations

• C.SatisfyingLocalTuple = { assignment : C.LocalAssignment // C.LocalSatisfied assignment = true }

@[instance_reducible]

noncomputable instance GapCVP.Core.Clause.instFintypeSatisfyingLocalTuple {m : ℕ} (C : Clause m) : Fintype C.SatisfyingLocalTuple

Equations

• C.instFintypeSatisfyingLocalTuple = Fintype.ofFinite C.SatisfyingLocalTuple

theorem GapCVP.Core.Clause.satisfyingLocalTuple_card_le_eight {m : ℕ} (C : Clause m) : Fintype.card C.SatisfyingLocalTuple ≤ 8

def GapCVP.Core.Clause.restrictAssignment {m : ℕ} (C : Clause m) (assignment : Fin m → Bool) : C.LocalAssignment

GapCVP reduction support.

Equations

• C.restrictAssignment assignment i = assignment ↑i

theorem GapCVP.Core.Clause.localSatisfied_restrict_iff {m : ℕ} (C : Clause m) (assignment : Fin m → Bool) : C.LocalSatisfied (C.restrictAssignment assignment) = true ↔ C.Satisfied assignment = true

def GapCVP.Core.Clause.satisfyingLocalTupleOfAssignment {m : ℕ} (C : Clause m) (assignment : Fin m → Bool) (h : C.Satisfied assignment = true) : C.SatisfyingLocalTuple

GapCVP reduction support.

Equations

• C.satisfyingLocalTupleOfAssignment assignment h = ⟨C.restrictAssignment assignment, ⋯⟩

@[reducible, inline]

abbrev GapCVP.Core.sourceSATTableType (F : Formula) : Type

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATTableType F = (Unit ⊕ (C : Fin F.clauses.length) × (F.clauses.get C).SatisfyingLocalTuple)

@[reducible, inline]

abbrev GapCVP.Core.sourceSATGridPoint {K : Type u_1} (points : Finset K) : Type u_1

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATGridPoint points = ↥points

@[reducible, inline]

abbrev GapCVP.Core.sourceSATTableCoordinate (F : Formula) (K : Type u_1) (points : Finset K) : Type u_1

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATTableCoordinate F K points = (GapCVP.Core.sourceSATTableType F × GapCVP.Core.sourceSATGridPoint points × K)

noncomputable def GapCVP.Core.sourceSATTableDimension (F : Formula) (K : Type u_1) [Fintype K] (points : Finset K) : ℕ

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATTableDimension F K points = Fintype.card (GapCVP.Core.sourceSATTableCoordinate F K points)

theorem GapCVP.Core.sourceSATTableDimension_eq (F : Formula) (K : Type u_1) [Fintype K] (points : Finset K) : sourceSATTableDimension F K points = Fintype.card (sourceSATTableType F) * points.card * Fintype.card K

theorem GapCVP.Core.sourceSATTableDimension_le (F : Formula) (K : Type u_1) [Fintype K] (points : Finset K) (N : ℕ) (hN : 100 ≤ N) (hclauses : F.clauses.length ≤ N) (hgrid : points.card ≤ Fintype.card K) (hfield : Fintype.card K < 2 * N ^ 200) : sourceSATTableDimension F K points ≤ 40 * N ^ 401

noncomputable def GapCVP.Core.sourceReedSolomonCode {K : Type u_1} [Field K] (points : Finset K) (degreeBound : ℕ) : Submodule K (sourceSATGridPoint points → K)

GapCVP reduction support.

Equations

• GapCVP.Core.sourceReedSolomonCode points degreeBound = (GapCVP.Core.sourceGridEvaluationLinearMap✝ points ∘ₗ (Polynomial.degreeLE K ↑degreeBound).subtype).range

theorem GapCVP.Core.sourceReedSolomonCode_mem_iff {K : Type u_1} [Field K] (points : Finset K) (degreeBound : ℕ) (values : sourceSATGridPoint points → K) : values ∈ sourceReedSolomonCode points degreeBound ↔ ∃ (polynomial : Polynomial K), polynomial.natDegree ≤ degreeBound ∧ ∀ (point : sourceSATGridPoint points), Polynomial.eval (↑point) polynomial = values point

noncomputable def GapCVP.Core.sourceFiniteReindexLinearEquiv {K : Type u_1} [Field K] (α : Type u_2) [Fintype α] : (α → K) ≃ₗ[K] Fin (Fintype.card α) → K

GapCVP reduction support.

Equations

• GapCVP.Core.sourceFiniteReindexLinearEquiv α = LinearEquiv.funCongrLeft K K (Fintype.equivFin α).symm

noncomputable def GapCVP.Core.sourceSATColumnIndex {K : Type u_1} (F : Formula) [Fintype K] (points : Finset K) (tableType : sourceSATTableType F) (point : sourceSATGridPoint points) (value : K) : Fin (sourceSATTableDimension F K points)

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATColumnIndex F points tableType point value = (Fintype.equivFin (GapCVP.Core.sourceSATTableCoordinate F K points)) (tableType, point, value)

noncomputable def GapCVP.Core.sourceGlobalNormalizationMap {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) : (Fin (sourceSATTableDimension F K points) → K) →ₗ[K] sourceSATGridPoint points → K

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Core.sourceClauseRefinementMap {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (clause : Fin F.clauses.length) : (Fin (sourceSATTableDimension F K points) → K) →ₗ[K] sourceSATGridPoint points × K → K

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Core.sourceOrdinaryMomentMap {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (tableType : sourceSATTableType F) (j : ℕ) : (Fin (sourceSATTableDimension F K points) → K) →ₗ[K] sourceSATGridPoint points → K

GapCVP reduction support.

Equations

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

def GapCVP.Core.sourceSATFieldBit {K : Type u_1} [Field K] (bit : Bool) : K

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATFieldBit bit = if bit = true then 1 else 0

noncomputable def GapCVP.Core.sourceShiftedMomentMap {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (variablePlace : Fin F.variableCount → K) (clause : Fin F.clauses.length) (tuple : (F.clauses.get clause).SatisfyingLocalTuple) (localVar : (F.clauses.get clause).LocalVariable) (j : ℕ) : (Fin (sourceSATTableDimension F K points) → K) →ₗ[K] sourceSATGridPoint points → K

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.Core.sourceSATConstraintFamily (F : Formula) (momentBudget : ℕ) : Type

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Core.sourceSATFamilyRowCount {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (momentBudget : ℕ) (family : sourceSATConstraintFamily F momentBudget) : ℕ

Number of field checks contributed by one SAT constraint family.

Equations

• GapCVP.Core.sourceSATFamilyRowCount F points momentBudget (Sum.inl val) = Fintype.card (GapCVP.Core.sourceSATGridPoint points)
• GapCVP.Core.sourceSATFamilyRowCount F points momentBudget (Sum.inr (Sum.inl val)) = Fintype.card (GapCVP.Core.sourceSATGridPoint points × K)
• GapCVP.Core.sourceSATFamilyRowCount F points momentBudget (Sum.inr (Sum.inr (Sum.inl (fst, j)))) = GapCVP.Core.sourceReedSolomonCodimension✝ points (F.variableCount * ↑j)
• GapCVP.Core.sourceSATFamilyRowCount F points momentBudget (Sum.inr (Sum.inr (Sum.inr ⟨fst, ⟨fst_1, (fst_2, j)⟩⟩))) = GapCVP.Core.sourceReedSolomonCodimension✝ points ((F.variableCount - 1) * ↑j)

def GapCVP.Core.sourceSATFamilyTarget {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (momentBudget : ℕ) (family : sourceSATConstraintFamily F momentBudget) : Fin (sourceSATFamilyRowCount F points momentBudget family) → K

Target values for the field checks of one SAT constraint family.

Equations

• GapCVP.Core.sourceSATFamilyTarget F points momentBudget (Sum.inl val) x_1 = 1
• GapCVP.Core.sourceSATFamilyTarget F points momentBudget (Sum.inr val) x_1 = 0

noncomputable def GapCVP.Core.sourceSATFamilyFieldMatrix {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (variablePlace : Fin F.variableCount → K) (momentBudget : ℕ) (family : sourceSATConstraintFamily F momentBudget) : Matrix (Fin (sourceSATFamilyRowCount F points momentBudget family)) (Fin (sourceSATTableDimension F K points)) K

Matrix of field checks for one SAT constraint family.

Equations

• GapCVP.Core.sourceSATFamilyFieldMatrix F points variablePlace momentBudget family = LinearMap.toMatrix' (GapCVP.Core.sourceSATFamilyLinearMap✝ F points variablePlace momentBudget family)

noncomputable def GapCVP.Core.concreteSATBinaryAffineSystem {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [Fintype K] (F : Formula) {e : ℕ} (fieldBasis : Module.Basis (Fin e) (ZMod 2) K) (points : Finset K) (variablePlace : Fin F.variableCount → K) (momentBudget : ℕ) : BinaryAffineSystem

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Core.concreteSATFieldChecks {K : Type u_1} [Field K] (F : Formula) [Fintype K] (points : Finset K) (variablePlace : Fin F.variableCount → K) (momentBudget : ℕ) (values : Fin (sourceSATTableDimension F K points) → K) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.concreteSATBinaryAffineSystem_solves_iff {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [Fintype K] (F : Formula) {e : ℕ} (fieldBasis : Module.Basis (Fin e) (ZMod 2) K) (points : Finset K) (variablePlace : Fin F.variableCount → K) (momentBudget : ℕ) (z : Fin (sourceSATTableDimension F K points) → ℤ) : (concreteSATBinaryAffineSystem F fieldBasis points variablePlace momentBudget).Solves z = true ↔ (concreteSATFieldChecks F points variablePlace momentBudget fun (position : Fin (sourceSATTableDimension F K points)) => (algebraMap (ZMod 2) K) ↑(z position)) = true

noncomputable def GapCVP.Core.sourceSATPuncturedGrid {K : Type u_1} (F : Formula) [Fintype K] (variablePlace : Fin F.variableCount → K) : Finset K

GapCVP reduction support.

Equations

• GapCVP.Core.sourceSATPuncturedGrid F variablePlace = GapCVP.Core.sourcePuncturedGrid (Finset.image variablePlace Finset.univ)

theorem GapCVP.Core.sourceSATPuncturedGrid_card {K : Type u_1} (F : Formula) [Fintype K] (variablePlace : Fin F.variableCount → K) (hinjective : Function.Injective variablePlace) : (sourceSATPuncturedGrid F variablePlace).card = Fintype.card K - F.variableCount

theorem GapCVP.Core.sourceSATPuncturedGrid_sub_ne_zero {K : Type u_1} [Field K] (F : Formula) [Fintype K] (variablePlace : Fin F.variableCount → K) (point : sourceSATGridPoint (sourceSATPuncturedGrid F variablePlace)) (i : Fin F.variableCount) : ↑point - variablePlace i ≠ 0

@[reducible, inline]

abbrev GapCVP.Core.sourceFormulaField (encodingLength : ℕ) (F : Formula) : Type

GapCVP reduction support.

Equations

• GapCVP.Core.sourceFormulaField encodingLength F = GapCVP.Core.SourceFiniteField (GapCVP.Core.sourceSizeParameter encodingLength F)

def GapCVP.Core.sourceActiveLocalTuple (F : Formula) (assignment : Fin F.variableCount → Bool) (hsatisfies : F.Satisfied assignment = true) (clause : Fin F.clauses.length) : (F.clauses.get clause).SatisfyingLocalTuple

GapCVP reduction support.

Equations

• GapCVP.Core.sourceActiveLocalTuple F assignment hsatisfies clause = (F.clauses.get clause).satisfyingLocalTupleOfAssignment assignment ⋯

theorem GapCVP.Core.exists_sourceSAT_assignment_interpolant_of_injective {K : Type u_1} [Field K] (F : Formula) (variablePlace : Fin F.variableCount → K) (hinjective : Function.Injective variablePlace) (assignment : Fin F.variableCount → Bool) : ∃ (interpolant : Polynomial K), interpolant.natDegree ≤ F.variableCount - 1 ∧ ∀ (i : Fin F.variableCount), Polynomial.eval (variablePlace i) interpolant = sourceSATFieldBit (assignment i)

noncomputable def GapCVP.Core.sourceOneHotSignedTable {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (F : Formula) (points : Finset K) (assignment : Fin F.variableCount → Bool) (hsatisfies : F.Satisfied assignment = true) (interpolant : Polynomial K) : Fin (sourceSATTableDimension F K points) → ℤ

GapCVP reduction support.

Equations

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

theorem GapCVP.Core.sourceOneHot_solves_concreteSATBinaryAffineSystem {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [Algebra (ZMod 2) K] (F : Formula) {e : ℕ} (fieldBasis : Module.Basis (Fin e) (ZMod 2) K) (points : Finset K) (variablePlace : Fin F.variableCount → K) (assignment : Fin F.variableCount → Bool) (hsatisfies : F.Satisfied assignment = true) (interpolant : Polynomial K) (hdegree : interpolant.natDegree ≤ F.variableCount - 1) (hinterpolant : ∀ (i : Fin F.variableCount), Polynomial.eval (variablePlace i) interpolant = sourceSATFieldBit (assignment i)) (hplaces : ∀ (point : sourceSATGridPoint points) (i : Fin F.variableCount), ↑point - variablePlace i ≠ 0) (momentBudget : ℕ) : (concreteSATBinaryAffineSystem F fieldBasis points variablePlace momentBudget).Solves (sourceOneHotSignedTable F points assignment hsatisfies interpolant) = true

theorem GapCVP.Core.sourceOneHotSignedTable_squaredNorm {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (F : Formula) (points : Finset K) (assignment : Fin F.variableCount → Bool) (hsatisfies : F.Satisfied assignment = true) (interpolant : Polynomial K) : ∑ position : Fin (sourceSATTableDimension F K points), (sourceOneHotSignedTable F points assignment hsatisfies interpolant position).natAbs ^ 2 = (F.clauses.length + 1) * points.card

def GapCVP.Core.integerSquaredNorm {n : ℕ} (z : Fin n → ℤ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.Core.integerSquaredNorm z = ∑ i : Fin n, (z i).natAbs ^ 2

noncomputable def GapCVP.Core.sourceOneHotCompletenessRadius (F : Formula) {α : Type u_2} (points : Finset α) : ℚ

GapCVP reduction support.

Equations

• GapCVP.Core.sourceOneHotCompletenessRadius F points = ↑⌈√↑((F.clauses.length + 1) * points.card)⌉₊

theorem GapCVP.Core.sourceOneHotCompletenessRadius_pos (F : Formula) {α : Type u_2} (points : Finset α) (hpoints : 0 < points.card) : 0 < sourceOneHotCompletenessRadius F points

theorem GapCVP.Core.sourceOneHotCompletenessRadius_squared_bound (F : Formula) {α : Type u_2} (points : Finset α) : ↑((F.clauses.length + 1) * points.card) ≤ ↑(sourceOneHotCompletenessRadius F points) ^ 2