GapCVP proof, part 09 #

GapCVP.BinaryReedSolomonParity.orderedInterpolationPrefix hdegree = { toFun := fun (values : Fin p → K) (index : Fin (D + 1)) => values (Fin.castLE ⋯ index), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

noncomputable def GapCVP.BinaryReedSolomonParity.orderedInterpolationPolynomial {K : Type u_1} [Field K] {p D : ℕ} (points : Fin p → K) (hdegree : D < p) (values : Fin p → K) :

Polynomial K

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryReedSolomonParity.constructiveParityLinearMap {K : Type u_1} [Field K] {p D : ℕ} (points : Fin p → K) (hdegree : D < p) :

(Fin p → K) →ₗ[K] Fin p → K

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryReedSolomonParity.constructiveParityMatrix {K : Type u_1} [Field K] {p D : ℕ} (points : Fin p → K) (hdegree : D < p) :

Matrix (Fin p) (Fin p) K

GapCVP reduction support.

Equations

GapCVP.BinaryReedSolomonParity.constructiveParityMatrix points hdegree = LinearMap.toMatrix' (GapCVP.BinaryReedSolomonParity.constructiveParityLinearMap points hdegree)

Instances For

source

@[simp]

theorem GapCVP.BinaryReedSolomonParity.constructiveParityLinearMap_apply {K : Type u_1} [Field K] {p D : ℕ} (points : Fin p → K) (hdegree : D < p) (values : Fin p → K) (index : Fin p) :

(constructiveParityLinearMap points hdegree) values index = values index - Polynomial.eval (points index) (orderedInterpolationPolynomial points hdegree values)

source

theorem GapCVP.Core.functionFieldPolynomial_algebraMap_injective {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra (RatFunc K) E] [Algebra (Polynomial K) E] [IsScalarTower (Polynomial K) (RatFunc K) E] :

Function.Injective ⇑(algebraMap (Polynomial K) E)

source

noncomputable def GapCVP.Core.functionFieldExtendedValuation {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra (RatFunc K) E] [Algebra (Polynomial K) E] [IsScalarTower (Polynomial K) (RatFunc K) E] [FiniteDimensional (RatFunc K) E] [Algebra.IsSeparable (RatFunc K) E] (a : K) :

Valuation E (WithZero (Multiplicative ℤ))

GapCVP reduction support.

Equations

GapCVP.Core.functionFieldExtendedValuation a = GapCVP.Core.functionFieldPlaceValuation✝ (GapCVP.Core.functionFieldHeightOnePlace✝ a)

Instances For

source

theorem GapCVP.Core.functionFieldExtendedValuation_place_lt_one {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra (RatFunc K) E] [Algebra (Polynomial K) E] [IsScalarTower (Polynomial K) (RatFunc K) E] [FiniteDimensional (RatFunc K) E] [Algebra.IsSeparable (RatFunc K) E] (a : K) :

(functionFieldExtendedValuation a) ((algebraMap (Polynomial K) E) (Polynomial.X - Polynomial.C a)) < 1

source

def GapCVP.Core.rootMoment {K : Type u_1} [Field K] {h : ℕ} (roots : Fin h → K) (j : ℕ) :

GapCVP reduction support.

Equations

GapCVP.Core.rootMoment roots j = ∑ i : Fin h, roots i ^ j

Instances For

source

noncomputable def GapCVP.Core.rootSupportPolynomial {K : Type u_1} [Field K] {h : ℕ} (roots : Fin h → K) :

Polynomial K

GapCVP reduction support.

Equations

GapCVP.Core.rootSupportPolynomial roots = ∏ i : Fin h, (Polynomial.X - Polynomial.C (roots i))

Instances For

source

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

Polynomial K

GapCVP reduction support.

Equations

GapCVP.Core.genericHankelDenominator h moments = GapCVP.Core.leadingHankelDet✝ moments h

Instances For

source

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

ℕ

GapCVP reduction support.

Equations

GapCVP.Core.maximalGenericHankelRank moments rankBound = GapCVP.Core.maximalLeadingHankelRank✝ moments rankBound

Instances For

source

theorem GapCVP.Core.maximalGenericHankelRank_spec {K : Type u_1} [Field K] (moments : ℕ → Polynomial K) (rankBound : ℕ) :

maximalGenericHankelRank moments rankBound ≤ rankBound ∧ genericHankelDenominator (maximalGenericHankelRank moments rankBound) moments ≠ 0

source

noncomputable def GapCVP.Core.familySplittingPolynomial {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (family : ι → Polynomial F) :

Polynomial F

GapCVP reduction support.

Equations

GapCVP.Core.familySplittingPolynomial family = ∏ i : ι, family i

Instances For

source

@[reducible, inline]

noncomputable abbrev GapCVP.Core.CommonAmbientSplittingField {F : Type u_1} [Field F] {t : ℕ} (polynomials : Fin t → Polynomial F) :

Type u_1

GapCVP reduction support.

Equations

GapCVP.Core.CommonAmbientSplittingField polynomials = GapCVP.Core.CommonSplittingField✝ polynomials

Instances For

source

noncomputable def GapCVP.Core.enumeratedRootSupport {E : Type u_2} {h : ℕ} (roots : Fin h → E) :

Finset E

GapCVP reduction support.

Equations

GapCVP.Core.enumeratedRootSupport roots = Finset.image roots Finset.univ

Instances For

source

theorem GapCVP.Core.functionFieldExtendedValuation_polynomial_le_one {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra (RatFunc K) E] [Algebra (Polynomial K) E] [IsScalarTower (Polynomial K) (RatFunc K) E] [FiniteDimensional (RatFunc K) E] [Algebra.IsSeparable (RatFunc K) E] (a : K) (f : Polynomial K) :

(functionFieldExtendedValuation a) ((algebraMap (Polynomial K) E) f) ≤ 1

source

theorem GapCVP.Core.sourceOneHotCompletenessRadius_squared_le_four_weight (F : Formula) {α : Type u_1} (points : Finset α) (hpoints : 0 < points.card) :

↑(sourceOneHotCompletenessRadius F points) ^ 2 ≤ 4 * ↑((F.clauses.length + 1) * points.card)

source

theorem GapCVP.Core.source_oneHot_weight_four_mul_le {N q ell points : ℕ} (hN : 100 ≤ N) (hell : ell ≤ N) (hpoints : points ≤ q) :

4 * ((ell + 1) * points) ≤ 8 * q * N

source

noncomputable def GapCVP.Core.inverseTransposeVandermonde {E : Type u_1} [Field E] {h : ℕ} (roots : Fin h → E) :

Matrix (Fin h) (Fin h) E

GapCVP reduction support.

Equations

GapCVP.Core.inverseTransposeVandermonde roots = (Matrix.vandermonde roots).transpose⁻¹

Instances For

source

theorem GapCVP.Core.valuation_roots_integral_of_shifted_moments {E : Type u_1} {Γ₀ : Type u_2} [Field E] [LinearOrderedCommMonoidWithZero Γ₀] {h : ℕ} (valuation : Valuation E Γ₀) (roots : Fin h → E) (hroots : Function.Injective roots) (bound : Γ₀) (z : ℕ) (hinverse : ∀ (i j : Fin h), valuation (inverseTransposeVandermonde roots i j) ≤ bound) (hmoments : ∀ (r : Fin h), valuation (∑ i : Fin h, roots i ^ (z + ↑r)) ≤ 1) (hseparation : ∀ (i : Fin h), 1 < valuation (roots i) → bound < valuation (roots i ^ z)) (i : Fin h) :

valuation (roots i) ≤ 1

source

theorem GapCVP.Core.mem_enumeratedRootSupport_iff {E : Type u_1} {h : ℕ} (roots : Fin h → E) (value : E) :

value ∈ enumeratedRootSupport roots ↔ ∃ (index : Fin h), roots index = value

source

theorem GapCVP.Core.functionFieldExtendedValuation_shiftedVandermonde_det_inv_le_place_inv_pow {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra (RatFunc K) E] [Algebra (Polynomial K) E] [IsScalarTower (Polynomial K) (RatFunc K) E] [FiniteDimensional (RatFunc K) E] [Algebra.IsSeparable (RatFunc K) E] (a : K) (moments : ℕ → Polynomial K) (d : ℕ) {h : ℕ} (roots : Fin h → E) (bit : E) (hmoments : ∀ j < 2 * h, (algebraMap (Polynomial K) E) (moments j) = rootMoment roots j) (hdegrees : ∀ (j : ℕ), (moments j).natDegree ≤ d * j) (hdenominator : genericHankelDenominator h moments ≠ 0) :

((functionFieldExtendedValuation a) (Matrix.vandermonde fun (i : Fin h) => (roots i - bit) / (algebraMap (Polynomial K) E) (Polynomial.X - Polynomial.C a)).det)⁻¹ ≤ ((functionFieldExtendedValuation a) ((algebraMap (Polynomial K) E) (Polynomial.X - Polynomial.C a)) ^ (d * h * h))⁻¹

source

def GapCVP.Core.bitInField {E : Type u_1} [Field E] (b : Bool) :

GapCVP reduction support.

Equations

GapCVP.Core.bitInField b = if b = true then 1 else 0

Instances For

source

theorem GapCVP.Core.satisfiable_of_common_valuation_root {E : Type u_1} {Γ₀ : Type u_2} [Field E] [LinearOrderedCommMonoidWithZero Γ₀] (formula : Formula) (valuation : Fin formula.variableCount → Valuation E Γ₀) (commonRoot : E) (localAssignment : Fin formula.clauses.length → Fin formula.variableCount → Bool) (local_satisfies : ∀ (C : Fin formula.clauses.length), (formula.clauses.get C).Satisfied (localAssignment C) = true) (local_close : ∀ (C : Fin formula.clauses.length), ∀ literal ∈ (formula.clauses.get C).literals, (valuation literal.variableIndex) (commonRoot - bitInField (localAssignment C literal.variableIndex)) < 1) :

formula.Satisfiable = true

source

theorem GapCVP.Core.functionFieldExtendedValuation_shiftedGenericRoot_le_place_inv_pow {k : Type u_1} {E : Type u_2} [Field k] [Field E] [Algebra k E] [Algebra (RatFunc k) E] [Algebra (Polynomial k) E] [IsScalarTower k (Polynomial k) E] [IsScalarTower (Polynomial k) (RatFunc k) E] [FiniteDimensional (RatFunc k) E] [Algebra.IsSeparable (RatFunc k) E] (moments : ℕ → Polynomial k) (d h : ℕ) (hmoments : ∀ (j : ℕ), (moments j).natDegree ≤ d * j) (hdenominator : genericHankelDenominator h moments ≠ 0) (roots : Fin h → E) (hroots : Polynomial.map (algebraMap (RatFunc k) E) (GapCVP.Core.genericMomentSupportPolynomial✝ h moments) = rootSupportPolynomial roots) (place bit : k) (index : Fin h) :

(functionFieldExtendedValuation place) ((roots index - (algebraMap k E) bit) / (algebraMap (Polynomial k) E) (Polynomial.X - Polynomial.C place)) ≤ ((functionFieldExtendedValuation place) ((algebraMap (Polynomial k) E) (Polynomial.X - Polynomial.C place)) ^ (d * h * (h - 1) + 1))⁻¹

source

theorem GapCVP.Core.valuation_inverseTransposeVandermonde_le_place_inv_pow {E : Type u_1} {Γ₀ : Type u_2} [Field E] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation E Γ₀) {h : ℕ} (roots : Fin h → E) (p : Γ₀) (hp : 0 < p) (hpone : p ≤ 1) (A B : ℕ) (hroots : ∀ (i : Fin h), v (roots i) ≤ (p ^ A)⁻¹) (hdet : (v (Matrix.vandermonde roots).det)⁻¹ ≤ (p ^ B)⁻¹) (i j : Fin h) :

v (inverseTransposeVandermonde roots i j) ≤ (p ^ (B + A * h * h))⁻¹

source

@[reducible, inline]

abbrev GapCVP.Core.BinaryAffineSystem.effectiveGaussianSystem (H : BinaryAffineSystem) :

EffectiveBinaryGaussian.System H.rowCount H.dimension

GapCVP reduction support.

Equations

H.effectiveGaussianSystem = { check := H.check, rhs := H.rightHandSide }

Instances For

source

@[reducible, inline]

abbrev GapCVP.Core.BinaryAffineSystem.effectiveGaussianState (H : BinaryAffineSystem) :

EffectiveBinaryGaussian.State H.rowCount H.dimension

GapCVP reduction support.

Equations

H.effectiveGaussianState = GapCVP.Core.EffectiveBinaryGaussian.eliminate H.effectiveGaussianSystem

Instances For

source

theorem GapCVP.Core.BinaryAffineSystem.effectiveGaussian_solves_iff (H : BinaryAffineSystem) (z : Fin H.dimension → ℤ) :

H.effectiveGaussianState.system.Satisfies (binaryResidue z) = true ↔ H.Solves z = true

source

def GapCVP.Core.BinaryAffineSystem.effectivePivotRowOption (H : BinaryAffineSystem) (column : Fin H.dimension) :

Option (Fin H.rowCount)

GapCVP reduction support.

Equations

H.effectivePivotRowOption column = Option.map Prod.fst (List.find? (fun (pivot : Fin H.rowCount × Fin H.dimension) => decide (pivot.2 = column)) H.effectiveGaussianState.pivots)

Instances For

source

def GapCVP.Core.BinaryAffineSystem.effectiveAffineBits (H : BinaryAffineSystem) :

Fin H.dimension → ZMod 2

GapCVP reduction support.

Equations

H.effectiveAffineBits column = match H.effectivePivotRowOption column with | some row => H.effectiveGaussianState.system.rhs row | none => 0

Instances For

source

def GapCVP.Core.BinaryAffineSystem.effectiveAffineRepresentative (H : BinaryAffineSystem) :

Fin H.dimension → ℤ

GapCVP reduction support.

Equations

H.effectiveAffineRepresentative column = ↑(H.effectiveAffineBits column).val

Instances For

source

@[simp]

theorem GapCVP.Core.BinaryAffineSystem.effectiveAffineRepresentative_residue (H : BinaryAffineSystem) :

binaryResidue H.effectiveAffineRepresentative = H.effectiveAffineBits

source

theorem GapCVP.Core.effectiveBinary_eq_zero_or_one (bit : ZMod 2) :

bit = 0 ∨ bit = 1

source

theorem GapCVP.Core.BinaryAffineSystem.effectiveAffineRepresentative_eq_zero_or_one (H : BinaryAffineSystem) (column : Fin H.dimension) :

H.effectiveAffineRepresentative column = 0 ∨ H.effectiveAffineRepresentative column = 1

source

def GapCVP.Core.BinaryAffineSystem.effectiveSquareBasisMatrix (H : BinaryAffineSystem) :

Matrix (Fin H.dimension) (Fin H.dimension) ℤ

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Core.BinaryAffineSystem.effectiveSquareBasisMatrix_mulVec_free (H : BinaryAffineSystem) (coefficients : Fin H.dimension → ℤ) (row : Fin H.dimension) (hrow : H.effectivePivotRowOption row = none) :

H.effectiveSquareBasisMatrix.mulVec coefficients row = coefficients row

source

theorem GapCVP.Core.BinaryAffineSystem.effectiveSquareBasisMatrix_mulVec_pivot (H : BinaryAffineSystem) (coefficients : Fin H.dimension → ℤ) (row : Fin H.dimension) (pivot : Fin H.rowCount) (hrow : H.effectivePivotRowOption row = some pivot) (hfree : ∀ (column : Fin H.dimension), H.effectivePivotRowOption column = none → coefficients column = 0) :

H.effectiveSquareBasisMatrix.mulVec coefficients row = 2 * coefficients row

source

theorem GapCVP.Core.BinaryAffineSystem.effectiveSquareBasisMatrix_det_ne_zero (H : BinaryAffineSystem) :

H.effectiveSquareBasisMatrix.det ≠ 0

source

def GapCVP.Core.effectiveConstructionAInstance (H : 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.

Instances For

source

@[simp]

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

(clearTargets pivot column targets state).pivots = state.pivots

source

noncomputable def GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal {m n : ℕ} (scanned : List (Fin n)) (state : State m n) :

Bool

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal.nextPivot_le {m n : ℕ} {scanned : List (Fin n)} {state : State m n} (normal : PrefixNormal scanned state = true) :

state.nextPivot ≤ m

source

theorem GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal.pivot_below {m n : ℕ} {scanned : List (Fin n)} {state : State m n} (normal : PrefixNormal scanned state = true) (pair : Fin m × Fin n) (hpair : pair ∈ state.pivots) :

↑pair.1 < state.nextPivot

source

theorem GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal.pivot_complete {m n : ℕ} {scanned : List (Fin n)} {state : State m n} (normal : PrefixNormal scanned state = true) (row : Fin m) (hrow : ↑row < state.nextPivot) :

∃ (column : Fin n), (row, column) ∈ state.pivots

source

theorem GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal.pivot_unit {m n : ℕ} {scanned : List (Fin n)} {state : State m n} (normal : PrefixNormal scanned state = true) (pair : Fin m × Fin n) (hpair : pair ∈ state.pivots) (row : Fin m) :

state.system.check row pair.2 = if row = pair.1 then 1 else 0

source

theorem GapCVP.Core.EffectiveBinaryGaussian.PrefixNormal.scanned_lower_zero {m n : ℕ} {scanned : List (Fin n)} {state : State m n} (normal : PrefixNormal scanned state = true) (column : Fin n) (hcolumn : column ∈ scanned) (row : Fin m) (hrow : state.nextPivot ≤ ↑row) :

state.system.check row column = 0

source

theorem GapCVP.Core.EffectiveBinaryGaussian.initialState_prefixNormal {m n : ℕ} (system : System m n) :

PrefixNormal [] (initialState system) = true

source

theorem GapCVP.Factor400BinarySourceTM.boundedFoldStates_of_nonexpansive {worker : List Bool → List Bool} (hworker : ∀ (state : List Bool), (worker state).length ≤ state.length) :

OutputBoundedDependentRecordFold.PolynomiallyBoundedFoldStates worker Polynomial.X = true

source

noncomputable def GapCVP.Factor400BinarySourceTM.nonexpansiveBoundedWorkerComputable {worker : List Bool → List Bool} (computer : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding worker) (hworker : ∀ (state : List Bool), (worker state).length ≤ state.length) :

Turing.TM2ComputableInPolyTime bitEncoding bitEncoding (OutputBoundedDependentRecordFold.boundedRecordFoldOutput worker)

GapCVP reduction support.

Equations

GapCVP.Factor400BinarySourceTM.nonexpansiveBoundedWorkerComputable computer hworker = GapCVP.Factor400BinarySourceTM.boundedWorkerComputable✝ computer Polynomial.X ⋯

Instances For

source

def GapCVP.Factor400BinaryPreservingXorWorker.tacticPreservingXorStepTac :

Lean.ParserDescr

Executes the preservingXorStepTac machine-step simplifier.

Equations

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

Instances For

source

def GapCVP.Factor400BinaryPhysicalParityTM.prefixParityOutput :

List Bool → List Bool

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.Factor400BinaryPhysicalParityTM.prefixParityComputable :

Turing.TM2ComputableInPolyTime bitEncoding bitEncoding prefixParityOutput

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Factor400BinaryPhysicalParityTM.prefixParityOutput_valid (first : Bool) (remaining suffix : List Bool) :

prefixParityOutput (OutputBoundedDependentRecordFold.unaryBoundedFoldWord remaining.length (first :: (remaining ++ suffix))) = List.foldl xor first remaining :: suffix

source

def GapCVP.BinaryCoefficientTM.convolutionCoefficientOutput :

List Bool → List Bool

GapCVP reduction support.

Equations

GapCVP.BinaryCoefficientTM.convolutionCoefficientOutput = GapCVP.Factor400BinaryPhysicalParityTM.prefixParityOutput ∘ GapCVP.BinaryCoefficientTM.convolutionProductRecordFoldOutput✝

Instances For

source

noncomputable def GapCVP.BinaryCoefficientTM.convolutionCoefficientComputable :

BitTM convolutionCoefficientOutput

GapCVP reduction support.

Equations

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

Instances For

source

def GapCVP.BinaryCoefficientTM.convolutionCoefficientQuery (queries : List (List Bool)) :

List Bool

GapCVP reduction support.

Equations

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

Instances For

source

def GapCVP.BinaryCoefficientTM.wordConvolutionQueries {e : ℕ} (left right : Core.EffectiveBinaryField.Word e) (coefficient : Fin (2 * e)) :

List (List Bool)

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.BinaryCoefficientTM.wordConvolutionQueries_length {e : ℕ} (left right : Core.EffectiveBinaryField.Word e) (coefficient : Fin (2 * e)) :

(wordConvolutionQueries left right coefficient).length = e * e

source

def GapCVP.BinaryCoefficientTM.wordConvolutionCoefficientQuery {e : ℕ} (left right : Core.EffectiveBinaryField.Word e) (coefficient : Fin (2 * e)) :

List Bool

GapCVP reduction support.

Equations

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

Instances For

source

@[simp]

theorem GapCVP.BinaryCoefficientTM.convolutionCoefficientOutput_word {e : ℕ} (left right : Core.EffectiveBinaryField.Word e) (coefficient : Fin (2 * e)) :

convolutionCoefficientOutput (wordConvolutionCoefficientQuery left right coefficient) = [Core.EffectiveBinaryField.multiplyWords left right coefficient]

source

def GapCVP.GaussianXorWorker.binaryGaussianXorHeadWord :

List Bool → List Bool

GapCVP reduction support.

Equations

GapCVP.GaussianXorWorker.binaryGaussianXorHeadWord (first :: second :: remaining) = [first ^^ second]
GapCVP.GaussianXorWorker.binaryGaussianXorHeadWord x✝ = []

Instances For

source

def GapCVP.GaussianXorWorker.tacticBinaryGaussianXorStepTac :

Lean.ParserDescr

Executes the binaryGaussianXorStepTac machine-step simplifier.

Equations

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

Instances For

source

noncomputable def GapCVP.GaussianXorWorker.binaryGaussianXorHeadComputable :

Turing.TM2ComputableInPolyTime bitEncoding bitEncoding binaryGaussianXorHeadWord

GapCVP reduction support.

Equations

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

Instances For

source

def GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord :

List Bool → List Bool

GapCVP reduction support.

Equations

GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord = GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (fun (x : List Bool) => [true ]) [false ]

Instances For

source

noncomputable def GapCVP.GaussianRowWorker.binaryGaussianFirstCellComputable :

BitTM binaryGaussianFirstCellWord

GapCVP reduction support.

Equations

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

Instances For

source

@[simp]

theorem GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord_valid (first : Bool) (remaining : List Bool) :

binaryGaussianFirstCellWord (first :: remaining) = [first]

source

def GapCVP.BinaryModularReductionTM.modularReductionCellOutput :

List Bool → List Bool

GapCVP reduction support.

Equations

GapCVP.BinaryModularReductionTM.modularReductionCellOutput = GapCVP.GaussianXorWorker.binaryGaussianXorHeadWord ∘ GapCVP.BinaryModularReductionTM.modularReductionPackedXorInput✝

Instances For

source

@[simp]

theorem GapCVP.BinaryModularReductionTM.modularReductionCellOutput_valid (gate mask destination : Bool) :

modularReductionCellOutput [gate, mask, destination] = [gate && mask ^^ destination]

source

theorem GapCVP.BinaryModularReductionTM.modularReductionCellOutput_length (input : List Bool) :

(modularReductionCellOutput input).length = 1

source

def GapCVP.BinaryModularReductionTM.modularReductionWordRowOutput :

List Bool → List Bool

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryModularReductionTM.modularReductionWordRowComputable :

BitTM modularReductionWordRowOutput

GapCVP reduction support.

Equations

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

Instances For

source

def GapCVP.BinaryModularReductionTM.finiteWordBits {d : ℕ} (word : Core.EffectiveBinaryField.Word d) :

List Bool

GapCVP reduction support.

Equations

GapCVP.BinaryModularReductionTM.finiteWordBits word = List.map word (List.finRange d)

Instances For

source

def GapCVP.BinaryExplicitAffineSystem.explicitMomentBudget (encodingLength : ℕ) (formula : Core.Formula) :

ℕ

GapCVP reduction support.

Equations

GapCVP.BinaryExplicitAffineSystem.explicitMomentBudget encodingLength formula = GapCVP.Core.sourceSizeParameter encodingLength formula ^ 30

Instances For

source

@[reducible, inline]

abbrev GapCVP.BinaryExplicitAffineSystem.ExplicitConstraintFamily (encodingLength : ℕ) (formula : Core.Formula) :

Type

GapCVP reduction support.

Equations

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

Instances For

source

@[reducible, inline]

abbrev GapCVP.BinaryExplicitAffineSystem.ExplicitGridPoint (encodingLength : ℕ) (formula : Core.Formula) :

Type

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder (encodingLength : ℕ) (formula : Core.Formula) :

Fin (Fintype.card (ExplicitGridPoint encodingLength formula)) ≃ ExplicitGridPoint encodingLength formula

GapCVP reduction support.

Equations

GapCVP.BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength formula = (finCongr ⋯).trans (GapCVP.BinarySourceCoordinateOrder.sourceFormulaGridOrder encodingLength formula)

Instances For

source

@[reducible, inline]

noncomputable abbrev GapCVP.BinaryExplicitAffineSystem.explicitFamilyRowCount (encodingLength : ℕ) (formula : Core.Formula) (family : ExplicitConstraintFamily encodingLength formula) :

ℕ

GapCVP reduction support.

Equations

One or more equations did not get rendered due to their size.
GapCVP.BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength formula (Sum.inl val) = Fintype.card (GapCVP.BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength formula)

Instances For

source

theorem GapCVP.BinaryExplicitAffineSystem.explicitOrdinaryDegree_lt_grid (encodingLength : ℕ) (formula : Core.Formula) (index : Fin (explicitMomentBudget encodingLength formula + 1)) :

formula.variableCount * ↑index < Fintype.card (ExplicitGridPoint encodingLength formula)

source

theorem GapCVP.BinaryExplicitAffineSystem.explicitShiftedDegree_lt_grid (encodingLength : ℕ) (formula : Core.Formula) (index : Fin (explicitMomentBudget encodingLength formula + 1)) :

(formula.variableCount - 1) * ↑index < Fintype.card (ExplicitGridPoint encodingLength formula)

source

noncomputable def GapCVP.BinaryExplicitAffineSystem.explicitFamilyLinearMap (encodingLength : ℕ) (formula : Core.Formula) (family : ExplicitConstraintFamily encodingLength formula) :

(Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula) →ₗ[Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula] Fin (explicitFamilyRowCount encodingLength formula family) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryExplicitAffineSystem.explicitFamilyTarget (encodingLength : ℕ) (formula : Core.Formula) (family : ExplicitConstraintFamily encodingLength formula) :

Fin (explicitFamilyRowCount encodingLength formula family) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula

GapCVP reduction support.

Equations

GapCVP.BinaryExplicitAffineSystem.explicitFamilyTarget encodingLength formula (Sum.inl val) x_1 = 1
GapCVP.BinaryExplicitAffineSystem.explicitFamilyTarget encodingLength formula (Sum.inr val) x_1 = 0

Instances For

source

@[reducible, inline]

noncomputable abbrev GapCVP.BinaryExplicitAffineSystem.sourceFormulaExplicitBinarySystem (encodingLength : ℕ) (formula : Core.Formula) :

Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.BinaryExplicitAffineSystem.sourceFormulaExplicitBinarySystem_solves_iff_family (encodingLength : ℕ) (formula : Core.Formula) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → ℤ) :

(sourceFormulaExplicitBinarySystem encodingLength formula).Solves values = true ↔ ∀ (family : ExplicitConstraintFamily encodingLength formula), ((explicitFamilyLinearMap encodingLength formula family) fun (position : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula)) => (algebraMap (ZMod 2) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula)) ↑(values position)) = explicitFamilyTarget encodingLength formula family

source

noncomputable def GapCVP.BinarySourceRowOrder.sourceFormulaExplicitRefinementOrder (encodingLength : ℕ) (formula : Core.Formula) :

Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength formula × Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula)) ≃ BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength formula × Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula

GapCVP reduction support.

Equations

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

Instances For

source

@[reducible, inline]

noncomputable abbrev GapCVP.BinaryOrderedAssembly.assembledBinaryAffineSystemOrdered {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {degree dimension rowCount : ℕ} (basis : Module.Basis (Fin degree) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin dimension) K) (targets : (family : ι) → Fin (rowCounts family) → K) (rowOrder : Fin rowCount ≃ Core.assembledBinaryRow rowCounts degree) :

Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.BinaryOrderedAssembly.assembledBinaryAffineSystemOrdered_solves_iff {ι : Type u_1} {K : Type u_2} [Field K] [Algebra (ZMod 2) K] {degree dimension rowCount : ℕ} (basis : Module.Basis (Fin degree) (ZMod 2) K) (rowCounts : ι → ℕ) (checks : (family : ι) → Matrix (Fin (rowCounts family)) (Fin dimension) K) (targets : (family : ι) → Fin (rowCounts family) → K) (rowOrder : Fin rowCount ≃ Core.assembledBinaryRow rowCounts degree) (values : Fin dimension → ℤ) :

(assembledBinaryAffineSystemOrdered basis rowCounts checks targets rowOrder).Solves values = true ↔ ∀ (family : ι), ((checks family).mulVec fun (position : Fin dimension) => (algebraMap (ZMod 2) K) ↑(values position)) = targets family

source

noncomputable def GapCVP.BinaryOrderedRefinement.sourceFormulaPhysicalFamilyLinearMap (encodingLength : ℕ) (formula : Core.Formula) (family : BinaryExplicitAffineSystem.ExplicitConstraintFamily encodingLength formula) :

(Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula) →ₗ[Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula] Fin (BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength formula family) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.BinaryOrderedRefinement.sourceFormulaPhysicalFamilyFieldMatrix (encodingLength : ℕ) (formula : Core.Formula) (family : BinaryExplicitAffineSystem.ExplicitConstraintFamily encodingLength formula) :

Matrix (Fin (BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength formula family)) (Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula)) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula)

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.BinaryOrderedRefinement.sourceFormulaPhysicalFamilyLinearMap_eq_iff_explicit (encodingLength : ℕ) (formula : Core.Formula) (family : BinaryExplicitAffineSystem.ExplicitConstraintFamily encodingLength formula) (values : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula) :

(sourceFormulaPhysicalFamilyLinearMap encodingLength formula family) values = BinaryExplicitAffineSystem.explicitFamilyTarget encodingLength formula family ↔ (BinaryExplicitAffineSystem.explicitFamilyLinearMap encodingLength formula family) values = BinaryExplicitAffineSystem.explicitFamilyTarget encodingLength formula family

source

theorem GapCVP.BinaryExplicitFourFamilyKernel.sourceFormulaExplicitBinarySystem_solves_iff_concreteSATFieldChecks (encodingLength : ℕ) (formula : Core.Formula) (z : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → ℤ) :

(BinaryExplicitAffineSystem.sourceFormulaExplicitBinarySystem encodingLength formula).Solves z = true ↔ (Core.concreteSATFieldChecks formula (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace encodingLength formula) (Core.sourceSizeParameter encodingLength formula ^ 30) fun (position : Fin (Core.sourceSATTableDimension formula (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength formula))) => (algebraMap (ZMod 2) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula)) ↑(z position)) = true

source

theorem GapCVP.BinaryExplicitFourFamilyKernel.integerSquaredNorm_wordOrder {newDimension oldDimension : ℕ} (columnOrder : Fin newDimension ≃ Fin oldDimension) (vector : Fin newDimension → ℤ) :

(Core.integerSquaredNorm fun (column : Fin oldDimension) => vector (columnOrder.symm column)) = Core.integerSquaredNorm vector

source

@[reducible, inline]

abbrev GapCVP.BinaryExplicitFourFamilyKernel.reindexBinaryAffineSystem {rowCount dimension : ℕ} (system : Core.BinaryAffineSystem) (rowOrder : Fin rowCount ≃ Fin system.rowCount) (columnOrder : Fin dimension ≃ Fin system.dimension) :

Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.BinaryExplicitFourFamilyKernel.reindexBinaryAffineSystem_solves_iff {rowCount dimension : ℕ} (system : Core.BinaryAffineSystem) (rowOrder : Fin rowCount ≃ Fin system.rowCount) (columnOrder : Fin dimension ≃ Fin system.dimension) (vector : Fin dimension → ℤ) :

(reindexBinaryAffineSystem system rowOrder columnOrder).Solves vector = true ↔ (system.Solves fun (column : Fin system.dimension) => vector (columnOrder.symm column)) = true

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaSignedTableOrdinaryMomentPolynomials (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) :

ℕ → Polynomial (sourceFormulaField encodingLength F)

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaSignedTableOrdinaryMomentPolynomials_natDegree (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) (j : ℕ) :

(sourceFormulaSignedTableOrdinaryMomentPolynomials encodingLength F z hz tableType j).natDegree ≤ F.variableCount * j

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaSignedTableShiftedMomentPolynomials (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (clause : Fin F.clauses.length) (tuple : (F.clauses.get clause).SatisfyingLocalTuple) (localVar : (F.clauses.get clause).LocalVariable) :

ℕ → Polynomial (sourceFormulaField encodingLength F)

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGenericRank (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) :

ℕ

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGenericSupportPolynomial (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) :

Polynomial (RatFunc (sourceFormulaField encodingLength F))

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGenericRank_le (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) :

sourceFormulaGenericRank encodingLength F z hz tableType ≤ Core.sourceSizeParameter encodingLength F ^ 4

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGenericSupportFamily (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) :

Fin (Fintype.card (Core.sourceSATTableType F)) → Polynomial (RatFunc (sourceFormulaField encodingLength F))

GapCVP reduction support.

Equations

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

Instances For

source

@[reducible, inline]

noncomputable abbrev GapCVP.Factor400BinaryConstructiveSourcePlaces.SourceFormulaCommonSeparableSplittingField (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) :

IntermediateField (RatFunc (sourceFormulaField encodingLength F)) (Core.CommonAmbientSplittingField (sourceFormulaGenericSupportFamily encodingLength F z hz))

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRoots (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) (tableType : Core.sourceSATTableType F) :

Fin (sourceFormulaGenericRank encodingLength F z hz tableType) → ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)

GapCVP reduction support.

Equations

GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRoots encodingLength F z hz hshort tableType = Classical.choose ⋯

Instances For

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRoots_injective (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) (tableType : Core.sourceSATTableType F) :

Function.Injective (sourceFormulaCommonRoots encodingLength F z hz hshort tableType)

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRoots_rootSupport (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) (tableType : Core.sourceSATTableType F) :

Polynomial.map (algebraMap (RatFunc (sourceFormulaField encodingLength F)) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (sourceFormulaGenericSupportPolynomial encodingLength F z hz tableType) = Core.rootSupportPolynomial (sourceFormulaCommonRoots encodingLength F z hz hshort tableType)

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRootSupport (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) (tableType : Core.sourceSATTableType F) :

Finset ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)

GapCVP reduction support.

Equations

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

Instances For

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGlobalGenericRoot (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) :

↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaCommonRoots_moment (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) (tableType : Core.sourceSATTableType F) (j : ℕ) (hj : j ≤ Core.sourceSizeParameter encodingLength F ^ 30) :

(algebraMap (RatFunc (sourceFormulaField encodingLength F)) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) ((algebraMap (Polynomial (sourceFormulaField encodingLength F)) (RatFunc (sourceFormulaField encodingLength F))) (sourceFormulaSignedTableOrdinaryMomentPolynomials encodingLength F z hz tableType j)) = Core.rootMoment (sourceFormulaCommonRoots encodingLength F z hz hshort tableType) j

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGlobalGenericRoot_mem_satisfyingSubtype (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) (clause : Fin F.clauses.length) :

∃ (tuple : (F.clauses.get clause).SatisfyingLocalTuple), sourceFormulaGlobalGenericRoot encodingLength F z hz hshort ∈ sourceFormulaCommonRootSupport encodingLength F z hz hshort (Sum.inr ⟨clause, tuple⟩)

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaShiftedCommonRoot_highPower_separation (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) (clause : Fin F.clauses.length) (tuple : (F.clauses.get clause).SatisfyingLocalTuple) (localVar : (F.clauses.get clause).LocalVariable) (exponent : ℕ) (index : Fin (sourceFormulaGenericRank encodingLength F z hz (Sum.inr ⟨clause, tuple⟩))) (hlarge : 1 < (Core.functionFieldExtendedValuation (sourceFormulaVariablePlace encodingLength F ↑localVar)) ((sourceFormulaCommonRoots encodingLength F z hz hshort (Sum.inr ⟨clause, tuple⟩) index - (algebraMap (sourceFormulaField encodingLength F) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (Core.sourceSATFieldBit (↑tuple localVar))) / (algebraMap (Polynomial (sourceFormulaField encodingLength F)) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (Polynomial.X - Polynomial.C (sourceFormulaVariablePlace encodingLength F ↑localVar)))) :

((Core.functionFieldExtendedValuation (sourceFormulaVariablePlace encodingLength F ↑localVar)) ((algebraMap (Polynomial (sourceFormulaField encodingLength F)) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (Polynomial.X - Polynomial.C (sourceFormulaVariablePlace encodingLength F ↑localVar))) ^ exponent)⁻¹ < (Core.functionFieldExtendedValuation (sourceFormulaVariablePlace encodingLength F ↑localVar)) (((sourceFormulaCommonRoots encodingLength F z hz hshort (Sum.inr ⟨clause, tuple⟩) index - (algebraMap (sourceFormulaField encodingLength F) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (Core.sourceSATFieldBit (↑tuple localVar))) / (algebraMap (Polynomial (sourceFormulaField encodingLength F)) ↥(SourceFormulaCommonSeparableSplittingField encodingLength F z hz)) (Polynomial.X - Polynomial.C (sourceFormulaVariablePlace encodingLength F ↑localVar))) ^ (sourceFormulaGenericRank encodingLength F z hz (Sum.inr ⟨clause, tuple⟩) * exponent + 1))

source

def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceValuationInverseExponent (d h : ℕ) :

ℕ

GapCVP reduction support.

Equations

GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceValuationInverseExponent d h = d * h * h + (d * h * (h - 1) + 1) * h * h

Instances For

source

noncomputable def GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaValuationInverseExponent (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) :

ℕ

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaValuationInverseExponent_shifted_index_le_budget (encodingLength : ℕ) (F : Core.Formula) (z : Fin (sourceFormulaDimension encodingLength F) → ℤ) (hz : (sourceFormulaBinarySystem encodingLength F).Solves z = true) (tableType : Core.sourceSATTableType F) (row : Fin (sourceFormulaGenericRank encodingLength F z hz tableType)) :

sourceFormulaGenericRank encodingLength F z hz tableType * sourceFormulaValuationInverseExponent encodingLength F z hz tableType + 1 + ↑row ≤ Core.sourceSizeParameter encodingLength F ^ 30

source

Core.rootMoment (fun (index : Fin (Core.maximalGenericHankelRank (sourceFormulaSignedTableOrdinaryMomentPolynomials encodingLength F z hz (Sum.inr ⟨clause, tuple⟩)) (Core.sourceSizeParameter encodingLength F ^ 4))) => (roots index - (algebraMap (sourceFormulaField encodingLength F) E) (Core.sourceSATFieldBit (↑tuple localVar))) / (algebraMap (Polynomial (sourceFormulaField encodingLength F)) E) (Polynomial.X - Polynomial.C (sourceFormulaVariablePlace encodingLength F ↑localVar))) j = (algebraMap (Polynomial (sourceFormulaField encodingLength F)) E) (sourceFormulaSignedTableShiftedMomentPolynomials encodingLength F z hz clause tuple localVar j)

Documentation

LeanPool.GapCVP.Part09

GapCVP proof, part 09 #