From 9a725b0e0575c6c195f6c7977530574969d784f9 Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sun, 25 Oct 2026 09:24:47 +0000 Subject: [PATCH 1/2] doc(PCP): document or privatize declarations left without outside references (#949 item 8) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Item 8 of #949, area Computability.PCP, entries marked † but not ‡. Twelve declarations are API: their docstrings already state their purpose, and they get Main entries. Three are proof plumbing used only in their own file and become private: cnfVertexNumber_injective, Edge.proofVerdict_answers and Graph.proofLabels_proofOfLabels. No statement changes. Co-Authored-By: Claude Opus 5.5 --- Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean | 2 ++ .../Computability/PCP/Encoded/Amplification/Iteration.lean | 3 +++ Complexity/Computability/PCP/Encoded/Composition.lean | 2 ++ Complexity/Computability/PCP/Encoded/Constraints.lean | 2 ++ Complexity/Computability/PCP/Encoded/Preprocess.lean | 2 ++ Complexity/Computability/PCP/Encoded/ThreeSAT.lean | 4 +++- Complexity/Computability/PCP/Encoded/Verifier.lean | 4 ++-- Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean | 2 ++ Complexity/Computability/PCP/Preprocess.lean | 5 +++++ 9 files changed, 23 insertions(+), 3 deletions(-) diff --git a/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean b/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean index 05156e441c..d03f0d10ac 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 8ab37a61e2..682ed1c101 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 f415bff2d2..0a8a04e54a 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 2f17211831..e202064c9f 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 cc158e3437..5acb97aff6 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 455cc5c53c..1e7bd2191e 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 0328d14d17..cb49c0f5ec 100644 --- a/Complexity/Computability/PCP/Encoded/Verifier.lean +++ b/Complexity/Computability/PCP/Encoded/Verifier.lean @@ -69,7 +69,7 @@ theorem length_proofQueries (width : ℕ) (edge : Edge C) : simp [proofQueries, two_mul] /-- Reading the query list returns exactly the two endpoint bit blocks, including repeated bits. -/ -theorem proofVerdict_answers (width : ℕ) (decode : (Fin width → Bool) → α) +private theorem proofVerdict_answers (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (edge : Edge C) (proof : List Bool) : edge.proofVerdict width decode eval (PCPVerifier.answers proof (edge.proofQueries width)) = eval edge.constraint (decode fun i => proof.getD (width * edge.src + i.val) false) @@ -156,7 +156,7 @@ def proofOfLabels (width vertices : ℕ) (encode : α → Fin width → Bool) (l List.ofFn (BitString.blocksEquiv.symm (fun vertex : Fin vertices => encode (labels vertex))) /-- Every declared vertex recovers its original label from the packed proof. -/ -theorem proofLabels_proofOfLabels (width vertices : ℕ) +private theorem proofLabels_proofOfLabels (width vertices : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) (labels : ℕ → α) {vertex : ℕ} (hvertex : vertex < vertices) : diff --git a/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean b/Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean index 4ba67cb94f..0fbd21b5d5 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 9b22a5be48..5bf4c37a72 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 From bd3b6889e5e5223b13c277c80efed6a5eaf47829 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 09:01:18 -0400 Subject: [PATCH 2/2] doc(PCP): keep the proof-evaluation and round-trip laws public (#926) Edge.proofVerdict_answers and Graph.proofLabels_proofOfLabels state the evaluation law of proofQueries and the round trip of proofOfLabels/proofLabels; both are API under privatize-by-intent, so they stay public with Main entries, per reviewer-claude-c4b0c164-18. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Computability/PCP/Encoded/Verifier.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/PCP/Encoded/Verifier.lean b/Complexity/Computability/PCP/Encoded/Verifier.lean index cb49c0f5ec..c1b4ecfeb9 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 @@ -69,7 +73,7 @@ theorem length_proofQueries (width : ℕ) (edge : Edge C) : simp [proofQueries, two_mul] /-- Reading the query list returns exactly the two endpoint bit blocks, including repeated bits. -/ -private theorem proofVerdict_answers (width : ℕ) (decode : (Fin width → Bool) → α) +theorem proofVerdict_answers (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (edge : Edge C) (proof : List Bool) : edge.proofVerdict width decode eval (PCPVerifier.answers proof (edge.proofQueries width)) = eval edge.constraint (decode fun i => proof.getD (width * edge.src + i.val) false) @@ -156,7 +160,7 @@ def proofOfLabels (width vertices : ℕ) (encode : α → Fin width → Bool) (l List.ofFn (BitString.blocksEquiv.symm (fun vertex : Fin vertices => encode (labels vertex))) /-- Every declared vertex recovers its original label from the packed proof. -/ -private theorem proofLabels_proofOfLabels (width vertices : ℕ) +theorem proofLabels_proofOfLabels (width vertices : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) (labels : ℕ → α) {vertex : ℕ} (hvertex : vertex < vertices) :