feat(coding-theory): constructors for the Grand List-Decoding witnesses - #792
Open
aryaethn wants to merge 2 commits into
Open
feat(coding-theory): constructors for the Grand List-Decoding witnesses#792aryaethn wants to merge 2 commits into
aryaethn wants to merge 2 commits into
Conversation
…itnesses `GrandChallenges.lean` carried `ListLowerWitness` and `ListUpperWitness` with no constructor for either, so neither side of the Grand List-Decoding Challenge could be witnessed for any concrete code. Add, in `GrandChallenges.lean`: - `ListLowerWitness.ofLe` and `ListUpperWitness.ofGt`, the generic shapes, mirroring the existing `McaLowerWitness.ofLe` / `McaUpperWitness.ofGt`. - `ListUpperWitness.ofEncardGt`, reducing an unsafe witness to a single word with an oversized point list. `Lambda` is a supremum over words, so one such word suffices; this is the shape a concrete large-list construction actually produces. Add, in the new `GrandChallenges/ListDecoding.lean`: - `relUDR_interleavedCode_eq` and `lambda_interleavedCode_le_one_of_le_relUDR`, supporting `ListLowerWitness.ofUniqueDecodingRange` — the first constructor for either list witness type. Interleaving preserves minimum distance, hence the unique-decoding radius, and inside that radius the interleaved point lists are subsingletons, so `Λ(C^⋈m, δ) ≤ 1`. The new module is axiom-clean (axiomsweep: 3 declarations, 0 tainted), as is all of `GrandChallenges.lean` (214 declarations, 0 tainted). This mirrors `McaLowerWitness.ofUniqueDecodingRange` on the MCA side and shares its trade-off: the unique-decoding radius falls well short of the Johnson and capacity radii, so it is not a route to the prize thresholds. A Johnson-radius list witness is reachable without new admits, since `CodingTheory.johnson_bound_lambda_le_ell` is stated over an arbitrary finite alphabet and is itself axiom-clean; that is left as follow-up work. `docs/kb/papers/ABF26.md` records the new constructors and the remaining gaps, keeping the two upper-witness items separate from the prize resolutions, which are the open research question rather than a formalization backlog. Refs Verified-zkEVM#789
…tness `ListLowerWitness.ofUniqueDecodingRange` only certifies radii up to half the minimum distance. Add `ListLowerWitness.ofJohnsonBound`, which reaches the Johnson radius and is likewise admit-free. `CodingTheory.johnson_bound_lambda_le_ell` is stated over an arbitrary finite alphabet, so it applies to `C^⋈(Fin m)` at alphabet `Fin m → F` with no specialization. `lambda_interleavedCode_le_of_le_johnson` re-expresses its two code-dependent inputs on the base code: the alphabet size becomes `|F|^m`, and the minimum distance is unchanged (`Code.minDist_interleavedCodeSet`). Stating the radius on `C` rather than on the interleaved code is what makes the constructor usable, since a caller has `C` in hand. The Johnson radius is computed at `q = |F|^m`, not `|F|`. That widens the usable radius rather than narrowing it, since `q/(q-1)` decreases in `q`, while the relative minimum distance is untouched. The module docstring records this so it is not later "corrected" to `|F|`. Both list witnesses are axiom-clean (axiomsweep: 5 declarations, 0 tainted). Note the asymmetry with the MCA side: `McaLowerWitness.ofJohnsonRangeBound` is sorry-tainted through the external [BCHKS25] admit `rs_mcaError_le_in_johnson_range`, whereas the list-side Johnson witness rests on an in-tree axiom-clean bound. `docs/kb/papers/ABF26.md` is corrected accordingly: the previous gap note said no list witness reached past the unique-decoding radius, which this makes false. The sharpened statement is that both constructors bound `Λ` by a fixed `ℓ`, whereas a prize resolution needs `Λ ≤ ε* · |F|` — the obstacle is the shape of the bound, not the radius. Refs Verified-zkEVM#789 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Contributor
🤖 PR SummaryNO Statistics
Lean Declarations ✏️ Added: 8 declaration(s)
📋 **Additional Analysis**Two style violations: missing citation key in a docstring, and a remark about 'L2.10' using an author-year suffix. Everything else (title format, naming, syntax, docs) is clean. 📄 **Per-File Summaries**
Last updated: 2026-08-22 06:38 UTC. |
Contributor
Build Timing Report
Incremental Rebuild Signal
This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark. Slowest Current Clean-Build FilesShowing 20 slowest current targets, with comparison against the selected baseline when available.
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
GrandChallenges.leandefinesListLowerWitnessandListUpperWitnessfor the GrandList-Decoding Challenge, together with the boundary lemmas relating them to a
GrandListResolution— but ships no constructor for either, so neither side of thechallenge could be witnessed for any concrete code. (The MCA side, by contrast, has three
McaLowerWitnessconstructors.)This adds four constructors, all axiom-clean.
What's added
In
GrandChallenges.lean— the generic shapes, mirroring the existingMcaLowerWitness.ofLe/McaUpperWitness.ofGt:ListLowerWitness.ofLeListUpperWitness.ofGtListUpperWitness.ofEncardGt— reduces an unsafe witness to a single word with anoversized point list.
Lambdais a supremum over words, so one such word suffices, and thisis the shape a concrete large-list construction actually produces.
In the new
GrandChallenges/ListDecoding.lean— the two substantive ones:ListLowerWitness.ofUniqueDecodingRangerelUDR_interleavedCode_eq,lambda_interleavedCode_le_one_of_le_relUDRListLowerWitness.ofJohnsonBoundlambda_interleavedCode_le_of_le_johnsonThe unique-decoding one is the floor, mirroring
McaLowerWitness.ofUniqueDecodingRange:interleaving preserves minimum distance (
Code.minDist_interleavedCodeSet), hence theunique-decoding radius, and inside that radius the interleaved point lists are subsingletons
(
Code.isUniquelyDecodable_relativeUniqueDecodingRadius), soΛ(C^⋈m, δ) ≤ 1.The Johnson one reaches much further.
CodingTheory.johnson_bound_lambda_le_ellis stated overan arbitrary finite alphabet, so it applies to
C^⋈(Fin m)at alphabetFin m → Fwith nospecialization; the supporting lemma re-expresses its two code-dependent inputs on the base
code, so a caller can discharge the hypothesis with the
Cthey actually hold.Two points a reviewer may want to check
The Johnson radius is computed at
q = |F|^m, not|F|. This is deliberate and is theinterleaved code's own alphabet. It widens the usable radius rather than narrowing it, since
q/(q-1)decreases inq, while the relative minimum distance is unchanged. The moduledocstring records this so it is not later "corrected" to
|F|.The list side now has an admit-free Johnson-range witness where the MCA side does not.
McaLowerWitness.ofJohnsonRangeBoundis sorry-tainted inscripts/axiom_baseline.jsonthroughthe external [BCHKS25] admit
rs_mcaError_le_in_johnson_range. The list-side Johnson witnessrests on
johnson_bound_lambda_le_ell, which is in-tree and axiom-clean, so it needs no admit.Flagging this as a genuine asymmetry rather than leaving it to be noticed.
Provenance
./scripts/validate.sh --axiomspasses end to end: build,ArkLib/Datawarning budget(no non-sorry warnings), toy-problem runtime, umbrella imports, docs integrity, knowledge-base
lint, axiom-sweep fixture matrix, and the axiom/sorry regression baseline (no new taint).
What this does not do
mcaPrize/listDecodingPrizeremain unproved at every rate, andnothing here approaches them. Both new constructors bound
Λby a fixedℓ, whereas aresolution needs
Λ ≤ ε* · |F|— the obstacle is the shape of the bound, not the radius.Nothing outside
GrandChallenges.leaninstantiatesprizeDimension/prizeRateat anyj : Fin 4, so the rates1/4,1/8,1/16are still untouched.ListUpperWitness.ofGtand.ofEncardGtaregeneric shapes awaiting a real large-list construction;
ofEncardGtis the intended entrypoint for one.
docs/kb/papers/ABF26.mdis updated to record the new constructors and to restate theremaining gaps in these terms.
Note on style
The three new
defs inGrandChallenges.leanwrite the interleaving asC^⋈(Fin m)withoutspaces, which differs from the ~20 spaced
C ^⋈ (Fin m)occurrences elsewhere in that file.This is forced, not a preference: Mathlib's whitespace linter diffs source against the
pretty-printed form, and
notation:20 C "^⋈" κcarries no spaces, so the spaced form warns —and
ArkLib/Datais under a zero-warning gate. The existing occurrences do not warn becausethey sit in
structurefields andtheoremstatements; these are the file's firstdefs usingthe notation.
Closes #789