Coding theory basic proofs - #141
Merged
alexanderlhicks merged 3 commits intoSep 3, 2025
Merged
Conversation
…erified-zkEVM#110 theorem singletonBound [ArkLib/Data/CodingTheory/Basic.lean] Verified-zkEVM#109 theorem dist_eq_dist_from_HammingNorm [ArkLib/Data/CodingTheory/Basic.lean] Verified-zkEVM#108
Collaborator
|
Thank you! Hoping to review these tomorrow and merge. |
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
Verified-zkEVM#171) P2PartitionMatchScratch.lean held the only real code `sorry` in the tree: `theorem restrictedFaaDiBrunoMatchAt_proof … := by unfold …; sorry` — a placebo 'proof' of RestrictedFaaDiBrunoPartitionMatchAt (the open BCIKS20 A.4 combinatorial core, equivalent to mcaConjecture). It has zero consumers and cannot be honestly proven (it's an open research conjecture), so the honest move toward 'no sorries' is to remove the fake, not fabricate it. The genuine obligation remains tracked as the honest `def : Prop` named residual + its GitHub issues (Verified-zkEVM#139/Verified-zkEVM#141), not a sorry-keystone. Tree is now free of real code sorries. Refs Verified-zkEVM#171 Verified-zkEVM#169.
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): prove a general MCA lower bound + RS-structure necessity (no axioms/sorries) Novel, axiom-clean [propext, Classical.choice, Quot.sound], sorry-free: - epsMCA_ge_inv_card_of_mcaEvent: general reusable MCA lower bound -- if any word stack admits a bad scalar (mcaEvent fires), then epsMCA >= 1/|F|. - MCALowerExample.epsMCA_C0_ge_half: the zero linear code over ZMod 2 has epsMCA >= 1/2. Hence the Grand-Challenge-1 poly/q upper bound is FALSE for general linear codes -- it genuinely requires the Reed-Solomon structure hypothesis. A real necessity/negative result complementing the prize upper-bound development. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): add mcaEvent_prob_le_epsMCA primitive to the MCA lower-bound theory Refactor MCALowerBound.lean: expose the fundamental lower-bound primitive mcaEvent_prob_le_epsMCA (epsMCA dominates every stack`s bad-scalar probability, by def the sup), and derive epsMCA_ge_inv_card_of_mcaEvent from it. All sorry-free, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): epsMCA univ = 0 (full code has zero MCA error) — brackets the MCA extremes Adds epsMCA_univ_eq_zero: for C = univ every pair is jointly matchable, so mcaEvent never fires and epsMCA = 0. With epsMCA_C0_ge_half (zero code >= 1/2) this brackets the MCA error across the structural extremes, making precise that the prize`s poly/q smallness is a non-trivial structural property. Sorry-free, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…y-free build
Three tracked scratch files held `sorry` stubs attempting genuinely-OPEN
conjectures (not closeable by formalization):
- ArkLib/P2Scratch.lean (restrictedFaaDiBrunoMatch_proof — BCIKS20 P2 Hensel,
Verified-zkEVM#139/Verified-zkEVM#140; the residual was refuted as not-unconditionally-true)
- ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2PartitionMatchScratch.lean
(wrongly registered in the generated ArkLib.lean)
- ArkLib/GrandChallengesScratch.lean (uniformEpsMCAgsPrizeBoundConjecture —
the open uniform prize form, Verified-zkEVM#141)
None were imported or load-bearing (zero external references); only auto-sync
had touched them since landing. They were the last 3 live holes per
scripts/sorry_census.py. The open math stays tracked on Verified-zkEVM#139/Verified-zkEVM#140/Verified-zkEVM#141; the
production tree should not carry broken scratch attempts at open conjectures.
After removal + `scripts/update-lib.sh` regen of ArkLib.lean (835 imports):
- scripts/sorry_census.py: 0 holes (was 3)
- scripts/forbidden_tokens.py: clean (10 allowlisted external-paper axioms)
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…nditional MCA lower witness The genuine open prize IS the uniform (field-universal) form; the repo's epsMCAgs_prizeBound_conjecture domain m surface was a weaker fixed-field form mislabeled as the prize, now proven (epsMCAgs_prizeBound_conjecture_holds). Since that hypothesis is discharged, the flagship downstream consumer (exists_prize_mcaLowerWitness_unconditional) holds unconditionally in the conjecture: every ABF26 prize rate admits an MCALowerWitness given only the still-explicit GS faithfulness + numeric clearance. Mirrors the _of_uniformConjecture adapter with the conjecture hypothesis removed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
GrandChallenges.lean had no Verified-zkEVM#141 reference, so the abstract Grand Challenge 1 prize surface mcaConjecture was untracked at source. Add an explicit 'Tracking: Issue Verified-zkEVM#141' note plus the keep-as-named-hypothesis / no-laundering guidance and a pointer to the GS-exposed counterparts, so the prize surface is not silently buried (per Verified-zkEVM#141 Purpose). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
fix(Verified-zkEVM#141,Verified-zkEVM#171): replace unsound mcaForallDoubleCover axiom with a PROVED refutation; remove vacuous larp Per the Verified-zkEVM#171 state audit. Two integrity fixes, no new axioms/sorries: - PROVE mcaForallDoubleCover_not_universal: the global ABF26 T4.21 hypothesis MCAForallDoubleCover is NOT universally true (a ZMod 2 counterexample where mcaEvent fires). This replaces the unsound `axiom mcaForallDoubleCover_residual` (which asserted it for all codes/radii -> would derive False) and its fake re-export theorem mcaForallDoubleCover_holds. Axiom-clean [propext,Classical,Quot]. - Remove 8 vacuous `theorem ..._residual : True := by trivial` larps (0 consumers) that Verified-zkEVM#171/Verified-zkEVM#169 flagged as placebos named after hard open problems (Verified-zkEVM#14,Verified-zkEVM#114,Verified-zkEVM#116,Verified-zkEVM#112,Verified-zkEVM#113,Verified-zkEVM#29,Verified-zkEVM#13,Verified-zkEVM#62). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
… theorem; state the field-universal open prize The GS-exposed surface epsMCAgs_prizeBound_conjecture (field/domain/m fixed, constants before the quantifiers) is PROVABLE, not the open prize: since every prizeRates j >= 1/16, the radius constraint forces eta <= 1 - rho <= 15/16 uniformly, so a single exponent c3 = n with (15/16)^n <= 1/q inflates the bound past 1 for all (j, eta) at once, while epsMCAgs <= 1. The earlier 'open prize' reading missed that eta is bounded away from 1, not merely < 1. The genuinely open ABF26 prize is the field-universal form (epsMCAgsPrizeUniversalConjecture): constants quantified before the field so they cannot absorb q = |F|; as q -> infinity the bound -> 0 and inflation fails. Stated as the EXISTENCE of a faithful GS family (epsMCA <= epsMCAgs) meeting the bound -- a forall-L form is false (adversarial L keeps epsMCAgs = Omega(1)). Bridge epsMCA_le_of_universalGSConjecture transfers it to the abstract epsMCA prize. Axiom-clean. Tracking: Issue Verified-zkEVM#141. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…isolated open core Add UniversalGSListMassBound (the field-universal beyond-UDR Guruswami-Sudan list-mass hypothesis) and prove the universal prize follows from it via the already-PROVED pivot-covering bound epsMCAgs_le_listSize_div_of_pivotCovering plus le_trans. No laundering: the only open content is the existence of a uniform polynomial GS list family (the classical GS mass bound at radius 1-rho-eta, absent from mathlib); everything else is unconditional. Switches import to MCAGSWitness. Axiom-clean. Tracking: Issue Verified-zkEVM#141. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): characterize zero MCA error — epsMCA C delta = 0 iff no stack admits a bad scalar Adds epsMCA_eq_zero_iff (general, any field/code): the MCA error vanishes exactly when mcaEvent never fires for any word stack. Foundational characterization; generalizes epsMCA_univ_eq_zero. Sorry-free, axiom-clean [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…ze is vacuous without faithfulness (anti-vacuity guard) (Verified-zkEVM#192) New genuine result (not previously in tree): epsMCAgs C δ (fun _ => ∅) = 0, hence the bare 'exists L, epsMCAgs C δ L ≤ B' holds for ANY bound B (via the empty list family). This formally proves WHY the FaithfulGSFamily hypothesis used throughout GrandChallenge141PrizeMath.lean is mathematically indispensable: dropping it makes the GS-exposed Grand-Challenge-1 prize statement vacuous. mcaEventGSrow's witness must lie in L, so L=∅ kills every bad event. A structural anti-vacuity guard (Verified-zkEVM#121), not a closure of the open prize. VERIFICATION: proved sorry-free and axiom-clean [propext, Classical.choice, Quot.sound] via 'lake env lean' on content-identical theorems while the dependency oleans were consistent. A full-library re-verify is currently impossible because concurrent activity invalidated the Mathlib cache and the shared checkout is mid-rebuild (lean exiting code 143 / SIGTERM on Mathlib.Logic.Basic) — an infrastructure state, not a defect in this proof. Co-authored-by: ArkLib Agent <agent@arklib.local> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…(was `∃ℓ,∀w,True`) The GS-prize 'open core' RSListDecodingCapacityConjecture was defined with body `True` (a placeholder that slips past the :True larp gate via the ∃/∀ wrapper), so the prize's 'reduction to RS list-decoding capacity' reduced to nothing. Replace with the genuine proximity-ball count: there is a list-size bound ℓ such that every word has at most ℓ codewords of the rate-ρ RS code within relative distance RSCapacityRadius ρ η = 1-ρ-η, via ListDecodable.closeCodewordsRel ... .ncard ≤ ℓ. The ∃ℓ,∀w shape is preserved so the (content-ignoring) consumers (exists_listSize_bound_of_capacity_conjecture, epsMCAgsPrizeUniformConjecture_of_listSize_clears) still compile: the prize reduction is now HONEST (conditional on a real open statement) rather than vacuous. Build: lake build ...RSListDecodingBeyondJohnson exit 0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…_conjecture (was `∃ℓ,True`) Companion to the conjecture de-vacuification: this extraction API previously concluded the vacuous `∃ ℓ, True`. It now exposes the genuine list-size bound (closeCodewordsRel ncard ≤ ℓ over the capacity radius) — proved by `exact hConj`, since that IS the conjecture's content. Also clears the unused-ℓ lint warning. Build exit 0 (25s incremental). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): closed form epsMCA = (sup bad-scalar count)/|F| + positive characterization - epsMCA_eq_iSup_badCount_div: exact closed form — epsMCA equals the supremum over word stacks of the bad-scalar count, divided by |F| (via ENNReal.iSup_div pulling the constant denominator out). - epsMCA_pos_iff: 0 < epsMCA iff some stack admits a bad scalar (complements epsMCA_eq_zero_iff). Both sorry-free, axiom-clean [propext, Classical.choice, Quot.sound]. Verified after the toolchain rebuild settled. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): bridge bad-scalar-count bound to the prize-shape MCA bound epsMCA_le_of_badCount_le: if every word stack has <= l bad scalars, then epsMCA <= l/|F|. Via the closed form epsMCA_eq_iSup_badCount_div, this is the poly/q shape of Grand Challenge 1 -- the prize reduces to UNIFORMLY BOUNDING the bad-scalar count l (the proven GS list size in the Johnson window). Sorry-free, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): reduce the MCA prize to the proximity-gap line-close count - badCount_le_lineCloseCount: every bad scalar makes the line delta-close to C (mcaEvent_imp_relCloseToCode), so bad-scalar count <= line-close count. - epsMCA_le_of_lineCloseCount_le: hence if the line-close count is uniformly <= l, then epsMCA <= l/|F|. This reduces ABF26 Grand Challenge 1 EXACTLY to bounding the line-close count -- the proximity-gap/list-decoding quantity (proven in the Johnson window, open at capacity) -- precisely locating the open core within a fully proven framework. Sorry-free, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): maximal MCA error condition — epsMCA = 1 when a stack has all scalars bad epsMCA_eq_one_of_forall_mcaEvent: if some word stack has mcaEvent for every scalar, epsMCA = 1. Completes the MCA-error trichotomy with epsMCA_eq_zero_iff / epsMCA_pos_iff. Sorry-free, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…via projective injectivity
New self-contained mathlib-only file MCAMasterBound.lean:
- ncard_badScalars_le: for any field K, module M, syndromes s₀ s₁, and finite
subspace family 𝒱, the bad-scalar set {γ | ∃V∈𝒱, s₀+γ•s₁∈V ∧ s₁∉V} has
ncard ≤ 𝒱.card. One-line projective injectivity: distinct γ sharing a witness
V force (γ-γ')•s₁ ∈ V hence s₁∈V (γ-γ' invertible), contradiction.
- ncard_badScalars_le_choose: binomial master bound E(a) ≤ C(n,e*), valid in
EVERY agreement band, every MDS code, every domain — complements the exact
3e≤r UDR law and the CS25 volume bound; polynomial in the UDR band (the
mcaConjecture form). Verified against all 130 sweep data points (0 violations).
Both kernel-clean [propext, Classical.choice, Quot.sound], no sorry/axiom/native_decide.
Co-Authored-By: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): full maximal-error characterization epsMCA = 1 iff a stack has all scalars bad epsMCA_eq_one_iff: completes the MCA-error trichotomy as three iffs (=0 / >0 / =1). Forward via Finite.exists_max (sup attained over the finite stack type) + ENNReal.div_eq_one_iff. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…r bound
ncard_badScalars_le_one_of_dependent: if s₀ ∈ span{s₁} (degenerate pencil) the
bad-scalar set has ncard ≤ 1 (s₀+γ•s₁=(c+γ)•s₁∈V with s₁∉V pins γ=-c). Completes
the syndrome-plane pencil dichotomy with ncard_badScalars_le (rank-2 master bound)
— the 'WLOG genuine line' reduction of the UDR-ladder proof. Kernel-clean.
Co-Authored-By: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
feat(Verified-zkEVM#141,Verified-zkEVM#171): polynomial-method core — two close scalars sharing a witness ⇒ u1 vanishes on overlap mca_two_agree_imp_u1_vanish_on_inter: if a word w agrees with the line u0+gamma*u1 at two distinct scalars (on sets S, S`), then u1 = 0 on S cap S`. This is the mechanism limiting the bad-scalar count per witness (large agreement sets overlap on >= (1-2delta)n coords) -- the kernel of the proximity-gap / Schwartz-Zippel argument underlying the prize`s list-decoding core. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> @
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…d sharpening engine) card_indices_mem_le_of_general_position: if every (d+1)-subfamily of w : ι → M is linearly independent (the MDS-dual genericity: every r parity columns independent), any subspace W with finrank ≤ d contains at most d of the w i. Sharpens the master bound below capacity: at a=n-1 (e*=1) bad scalars inject into columns in the 2-dim syndrome pencil, and for r≥3 at most 2 columns lie there ⟹ secant value E(n-1)≤2, far below the master bound C(n,1)=n. Kernel-clean [propext, Classical.choice, Quot.sound]. Co-Authored-By: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…roximity gap in UDR (unconditional) Composition of epsMCAgs_restricted_le_epsCA and ahiv17_epsCA_bound_uniqueDecodingRegime: restricted GS-exposed MCA error <= errorBound = n/q for RS in the unique-decoding regime, any L. No new hypothesis, no axiom, no sorry. (Proximity-gap shape n/q, not the prize shape; honest.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 8, 2026
…Refutation.lean Proper tree module (namespace ProximityGap.MCAGSPrizeRefutation) proving the uniform prize conjecture FALSE. Verified axiom-clean [propext, Classical.choice, Quot.sound], 0 sorry. Removes the root scratch keep file. See Verified-zkEVM#141 for the full mathematical finding. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 8, 2026
…-final feat(Verified-zkEVM#141): refute the uniform GS prize conjecture (verified axiom-clean)
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 8, 2026
… multi-γ lower bound
Genuine new math for the Proximity Prize lower-bound side (ABF26 Grand MCA
Challenge). Two results, axiom-clean [propext, Classical.choice, Quot.sound]:
- epsMCA_ge_card_div_of_mcaEvent_set: the multi-scalar lower-bound engine —
a stack with |G| bad scalars gives ε_mca ≥ |G|/|F| (generalizes the
single-scalar 1/|F| bound to the n^{Ω(1)}/|F| near-capacity regime shape).
- unique_bad_gamma_common_witness: for ANY linear code, a fixed witness set S
admits at most one bad scalar (the two line equations force a
pairJointAgreesOn witness, which mcaEvent forbids). Consequence
(common_witness_badGamma_set_card_le_one): the prize's near-capacity lower
bound provably REQUIRES the witness sets to vary with γ — the list-decoding
spread. Honestly delineates the open lower-bound core (Verified-zkEVM#232/Verified-zkEVM#141).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 8, 2026
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
2 participants
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.
Closes the following proofs:
theorem singleton_bound_linear [ArkLib/Data/CodingTheory/Basic.lean] #110
theorem singletonBound [ArkLib/Data/CodingTheory/Basic.lean] #109
theorem dist_eq_dist_from_HammingNorm [ArkLib/Data/CodingTheory/Basic.lean] #108
theorem dist'_eq_dist [ArkLib/Data/CodingTheory/Basic.lean] #107
Note that we had to relax some theorems to make sure that they hold:
dist_eq_dist_from_HammingNorm, singletonBound and singleton_bound_linear generally only hold over commutative rings, not semirings.
singletonBound and singleton_bound_linear further require F to have strong rank condition.