diff --git a/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean b/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean index 05156e441..d03f0d10a 100644 --- a/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean +++ b/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean @@ -43,6 +43,8 @@ Arora, Lund, Motwani, Sudan and Szegedy [AroraLundMotwaniSudanSzegedy1998]. ## Main results * `Cslib.PCP.Encoded.Graph.div_le_unsatVal_toThreeSAT_toCNF`: the gap-preserving bound. +* `Cslib.Complexity.polyTimeReducible_GapTwoCSP_GapThreeSAT`: MAX-2CSP reduces to MAX-3SAT in + polynomial time, preserving a gap. * `Cslib.Complexity.GapThreeSAT_npHard`: distinguishing satisfiable 3CNF formulas from those in which every assignment satisfies at most the proportion `1 - 1 / (3 * 2 ^ 77)` of the clauses is NP-hard. diff --git a/Complexity/Computability/PCP/Encoded/Amplification/Iteration.lean b/Complexity/Computability/PCP/Encoded/Amplification/Iteration.lean index 8ab37a61e..682ed1c10 100644 --- a/Complexity/Computability/PCP/Encoded/Amplification/Iteration.lean +++ b/Complexity/Computability/PCP/Encoded/Amplification/Iteration.lean @@ -33,6 +33,9 @@ certificates need no completeness assumption on those lists; gap and satisfiabil * `Cslib.PCP.Encoded.Graph.isPolyTime_amplifyIter_clog`: a certificate for logarithmically many rounds, including their full intermediate and output table encodings. * `Cslib.PCP.Encoded.Graph.satisfiable_amplifyIter_iff`: complete rounds preserve satisfiability. +* `Cslib.PCP.Encoded.Graph.min_le_unsatVal_amplifyIter`, + `Cslib.PCP.Encoded.Graph.gap_le_unsatVal_amplifyIter`: complete rounds double the value up to + the fixed threshold, so `k` rounds with at most `2 ^ k` edges reach the gap. * `Cslib.PCP.Encoded.Graph.gap_le_unsatVal_amplifyIter_clog`: logarithmically many complete rounds give a fixed positive gap on every unsatisfiable input. diff --git a/Complexity/Computability/PCP/Encoded/Composition.lean b/Complexity/Computability/PCP/Encoded/Composition.lean index f415bff2d..0a8a04e54 100644 --- a/Complexity/Computability/PCP/Encoded/Composition.lean +++ b/Complexity/Computability/PCP/Encoded/Composition.lean @@ -40,6 +40,8 @@ written in the client's input representation. * `Cslib.PCP.Encoded.Graph.toGraph_compose`: exact agreement with mathematical composition. * `Cslib.PCP.Encoded.Graph.le_unsatVal_compose`: the existing `1/476` gap bound transfers. * `Cslib.PCP.Encoded.Graph.satisfiable_composeTabulated_iff`: satisfiability is preserved. +* `Cslib.PCP.Encoded.Graph.unsatVal_composeTabulated_eq`: tabulating the output constraints + preserves the value of the composition. ## References diff --git a/Complexity/Computability/PCP/Encoded/Constraints.lean b/Complexity/Computability/PCP/Encoded/Constraints.lean index 2f1721183..e202064c9 100644 --- a/Complexity/Computability/PCP/Encoded/Constraints.lean +++ b/Complexity/Computability/PCP/Encoded/Constraints.lean @@ -33,6 +33,8 @@ No decidability or efficiency is inferred for arbitrary proposition-valued const * `Cslib.PCP.Encoded.Graph.toGraph_mapConstraints`: exact interpretation after descriptor change. * `Cslib.PCP.Encoded.Graph.isPolyTime_tabulateConstraints`: materializing all finite tables is polynomial-time, including the unchanged endpoints and graph storage. +* `Cslib.PCP.Encoded.Graph.length_encoding_tabulateConstraints_le`: tabulation adds at most a + constant number of bits per edge. ## References diff --git a/Complexity/Computability/PCP/Encoded/Preprocess.lean b/Complexity/Computability/PCP/Encoded/Preprocess.lean index cc158e343..5acb97aff 100644 --- a/Complexity/Computability/PCP/Encoded/Preprocess.lean +++ b/Complexity/Computability/PCP/Encoded/Preprocess.lean @@ -37,6 +37,8 @@ proofs reuse the existing degree-reduction argument and exact laws for appending * `Cslib.PCP.Encoded.Graph.unsatVal_preprocess`: adding family edges and loops halves the degree-reduced graph's value. * `Cslib.PCP.Encoded.Graph.le_unsatVal_preprocess`: the existing Dinur gap bound for the program. +* `Cslib.PCP.Encoded.Graph.spectralExpansion_regularPreprocess_le`: the spectral bound of + preprocessing, for the program's own vertex numbering. ## References diff --git a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean index 455cc5c53..1e7bd2191 100644 --- a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean +++ b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean @@ -33,6 +33,8 @@ complete Boolean tables on the eight-symbol alphabet `Fin 3 → Bool`. ## Main results * `Cslib.PCP.Encoded.Graph.isPolyTime_ofCompactCNF`: charge renaming, enumeration, and truth tables. +* `Cslib.PCP.Encoded.Graph.toGraph_ofCNF`, `Cslib.PCP.Encoded.Graph.unsatVal_ofCNF`: the graph + is the mathematical graph of the formula, with the same unsatisfied value. ## References @@ -149,7 +151,7 @@ def cnfVertexNumber {m : ℕ} : ℕ ⊕ Fin m → ℕ | .inr j => 2 * j.val + 1 /-- The numbering separates all variable vertices and clause vertices. -/ -theorem cnfVertexNumber_injective (m : ℕ) : +private theorem cnfVertexNumber_injective (m : ℕ) : Function.Injective (cnfVertexNumber (m := m)) := by intro v w h cases v with diff --git a/Complexity/Computability/PCP/Encoded/Verifier.lean b/Complexity/Computability/PCP/Encoded/Verifier.lean index 0328d14d1..c1b4ecfeb 100644 --- a/Complexity/Computability/PCP/Encoded/Verifier.lean +++ b/Complexity/Computability/PCP/Encoded/Verifier.lean @@ -35,6 +35,10 @@ large unary indices. The alphabet decoder and block width are fixed before the r binary query indices, and verdict on arbitrary inputs. * `Cslib.PCP.Encoded.Graph.edgeVerifier_accepts`: the exact constraint checked for every proof. * `Cslib.PCP.Encoded.Graph.accepts_proofOfLabels`: a satisfying labelling gives a finite proof. +* `Cslib.PCP.Encoded.Edge.proofVerdict_answers`: the verdict on the answers to `proofQueries` is + the constraint evaluated on the two decoded endpoint blocks. +* `Cslib.PCP.Encoded.Graph.proofLabels_proofOfLabels`: every declared vertex recovers its label from + the packed proof. ## References diff --git a/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean b/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean index 4ba67cb94..0fbd21b5d 100644 --- a/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean +++ b/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean @@ -30,6 +30,8 @@ consistent labelling. Random strings of arbitrary length remain covered by the c ## Main results +* `Cslib.PCP.Encoded.Graph.polyTime_reductionVerifier`: the verifier is polynomial-time when the + graph construction and the constraint evaluation are. * `Cslib.PCP.Encoded.Graph.mem_PCP_of_gapReduction`: a positive-gap reduction gives membership in `PCP(log n, 1)`. diff --git a/Complexity/Computability/PCP/Preprocess.lean b/Complexity/Computability/PCP/Preprocess.lean index 9b22a5be4..5bf4c37a7 100644 --- a/Complexity/Computability/PCP/Preprocess.lean +++ b/Complexity/Computability/PCP/Preprocess.lean @@ -65,6 +65,11 @@ not require the executable numberings to equal a choice made on arbitrary finite * `Cslib.PCP.ConstraintGraph.spectralExpansion_preprocess_expanderFamily_le`, `Cslib.PCP.ConstraintGraph.le_unsatVal_preprocess_expanderFamily`: the constants for the non-explicit family of expanders. +* `Cslib.PCP.ConstraintGraph.unsatVal_preprocessWith`, + `Cslib.PCP.ConstraintGraph.unsatVal_preprocessWith_le`: for any specified rotations, the value + is exactly half that of the degree-reduced graph, and at most that of `G`. +* `Cslib.PCP.ConstraintGraph.preprocessWith_ofFamily`: rotations from a family recover + `preprocess`. ## References