feat(ReedSolomon): decoder refusal as a farness certificate for Gao decoding

[Abraxas1010]

Summary

One theorem, added to GaoCorrectness.lean beside the completeness/failure pair: decode_none_farness — if Gao.decode returns none, the received word is beyond the guaranteed radius ⌊(n-k)/2⌋ of every codeword:

Gao.decode k D r = none → ∀ msg, D.n - k < 2 * hammingDist r.get (encode D msg).get

It is the contrapositive of decode_eq_some, completing the square of decode-outcome characterizations (decode_sound / decode_eq_none already give the other diagonal): a decoder refusal is now positive, O(n²)-checkable evidence of proximity-gap-style farness from the code — the certificate shape proximity testing wants, produced by machinery the library already trusts.

#print axioms: [propext, Classical.choice, Quot.sound].

Validation performed (not in the diff)

Full lake build CompPoly green (2516 jobs, warning-free). Concrete check over ZMod 17, RS(8, 4), radius 2: the honest codeword #[10,15,7,13,15,11,6,16] decodes to some #[1,2,3,4] (its exact message), and a 3-position corruption of it decodes to none — on which the theorem certifies farness from the entire code.

Complements #266 (certified NTT encoder): together, fast-encode lands provably in the code and decoder-refusal provably certifies far from the code.

---

Contributed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[github-actions]

🤖 PR Summary

Reed–Solomon Decoder Refusal as a Farness Certificate for Gao Decoding

Mathematical Formalization

• Adds the theorem decode_none_farness to CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean.

Gao.decode k D r = none → ∀ msg, D.n - k < 2 * hammingDist r.get (encode D msg).get

• This theorem is the contrapositive of the existing decode_eq_some: if the Gao decoder returns none, the received word r is at Hamming distance strictly greater than ⌊(n−k)/2⌋ from every codeword in the Reed–Solomon code RS(D, k).
• Together with decode_sound and decode_eq_none, it completes the logical square of decoder-outcome characterizations:
  • decode_eq_some : if a codeword exists within radius, decode returns it.
  • decode_none_farness : if decode returns none, no codeword lies within radius.
• The theorem provides a certificate of farness in O(n²) time (the decoder’s own runtime) – a positive, checkable proof that the received word is outside the unique-decoding radius. This certificate shape is directly useful for proximity-testing protocols.

Proof Completion / Sorries

• The PR body and the displayed #print axioms ([propext, Classical.choice, Quot.sound]) indicate no added sorry or admit placeholders. The per‑file summary for GaoCorrectness.lean is unavailable due to a JSON parsing error, so the presence of any hidden sorries cannot be confirmed from the provided data; the reviewer should verify the actual file.

Infrastructure / CI

• A full lake build CompPoly (2516 jobs, warning‑free) passed, confirming the change compiles against the current library.
• A concrete test over ZMod 17, RS(8,4) (radius 2) is documented: an honest codeword decodes to some its message; a 3‑position corruption decodes to none, and the theorem then certifies farness from the entire code.

Relation to Prior Work

• Complements PR feat(ReedSolomon): certify the forward NTT as a Reed-Solomon encoder #266 (certified NTT encoder): that PR provides a provably correct encoding that lands in the code; this PR provides a provably correct decoder refusal that certifies far from the code.

Note on Per‑File Data

• The only substantive file change reported is GaoCorrectness.lean. The per‑file summary for that file could not be parsed (JSON validation error). The overview above is based on the PR body; the reviewer should inspect the diff directly to confirm the exact statement, any auxiliary lemmas, and the absence of placeholders.

Headers

• Mathematical Formalization
• Proof Completion (no sorries expected)
• Protocols / Soundness
• Infrastructure / CI
• Documentation (not applicable)

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	13
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 1 declaration(s)

CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean (1)

• theorem decode_none_farness [Field F]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a new theorem decode_none_farness that fully adheres to the CompPoly style guide and documentation standards. No violations were found.

---

📄 **Per-File Summaries**

• CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='添加了新定理 `deco...的正确性分析。', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid

---

Last updated: 2026-07-10 16:24 UTC.

[alexanderlhicks]

Thank you!

[Abraxas1010]

My pleasure.

…

On Sat, Jul 11, 2026 at 9:03 PM Alexander Hicks ***@***.***> wrote: *alexanderlhicks* left a comment (Verified-zkEVM/CompPoly#267) <#267 (comment)> Thank you! — Reply to this email directly, view it on GitHub <#267?email_source=notifications&email_token=ATMORT67PR7BG5U65ALK4UL5ELPVPA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOJUHE2DCMRTGI4KM4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KYZTPN52GK4S7MNWGSY3L#issuecomment-4949412328>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ATMORT3X7YXACSALJXX57KD5ELPVPAVCNFSNUABGKJSXA33TNF2G64TZHMYTAOBRGQ4DQMJRHA5US43TOVSTWNBYGU3DOOBQGAYTRILWAI> . Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/ATMORT3CQH2O647DRGTGAY35ELPVPA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOJUHE2DCMRTGI4KM4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KUZTPN52GK4S7NFXXG> and Android <https://github.com/notifications/mobile/android/ATMORT5OFTMGC3WKFLNC7ST5ELPVPA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOJUHE2DCMRTGI4KM4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2K4ZTPN52GK4S7MFXGI4TPNFSA>. Download it today! You are receiving this because you authored the thread.Message ID: ***@***.***>

-- This email and any attachments are confidential and may be protected by legal privilege. If you are not the intended recipient, be aware that disclosing, copying, distributing, or use of this email or any attachments is prohibited. If you have received this email in error, please notify me immediately and delete this copy from your system. Thank you for your cooperation.