SamuelSchlesinger · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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