feat(ReedSolomon): decode-outcome iff for Gao decoding

[alexanderlhicks]

Quick follow-up to #267: combines decode_eq_none and decode_none_farness
into a single outcome characterization decode_eq_none_iff — Gao.decode returns none iff the received word is beyond the guaranteed radius ⌊(n-k)/2⌋ of every codeword.

[github-actions]

🤖 PR Summary

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

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

---

Lean Declarations

✏️ Added: 1 declaration(s)

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

• theorem decode_eq_none_iff [Field F]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean: This change adds decode_eq_none_iff, a new iff theorem that characterizes when Gao.decode returns none as ∀ msg, D.n - k < 2 * hammingDist r.get (encode D msg).get. It is proven by combining the existing decode_none_farness and decode_eq_none (which gave the two directions separately), thereby providing a complete equivalence for the failure case of the decoder.

---

Last updated: 2026-07-12 01:35 UTC.

[github-actions]

🤖 AI Review

Overall Summary:

---

Errors during review:

• Agent B failed for CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean

---

📄 **Review for `CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean`**

An error occurred while analyzing CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

[github-actions]

Build Timing Report

• Commit: f49fb84
• Message: Merge 56a921f into 95569c0
• Ref: feat/gao-decode-none-iff
• Comparison baseline: e95ba1b from the latest successful master run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	391.67	292.69	-98.98	ok
Warm rebuild	1.60	1.43	-0.17	ok
Test path	34.38	26.66	-7.72	ok

Incremental Rebuild Signal

• Warm rebuild saved 291.26s vs clean (204.68x faster).

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 Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
38.00	45.00	-7.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
35.00	54.00	-19.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
31.00	48.00	-17.00	CompPoly/Univariate/DivisionCorrectness.lean
24.00	34.00	-10.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
20.00	30.00	-10.00	CompPoly/Bivariate/Deriv.lean
19.00	28.00	-9.00	CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Correctness.lean
17.00	25.00	-8.00	CompPoly/Bivariate/ToPoly.lean
14.00	19.00	-5.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIF.lean
13.00	18.00	-5.00	CompPoly/Univariate/Raw/Proofs.lean
13.00	16.00	-3.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
12.00	18.00	-6.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIT.lean
11.00	12.00	-1.00	CompPoly/Univariate/NTT/Forward.lean
11.00	16.00	-5.00	CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean
11.00	16.00	-5.00	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Divisibility.lean
10.00	16.00	-6.00	CompPoly/Fields/KoalaBear/Fast.lean
10.00	11.00	-1.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
10.00	17.00	-7.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
10.00	13.00	-3.00	CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Correctness.lean
9.60	12.00	-2.40	CompPoly/Bivariate/Factor.lean
9.10	11.00	-1.90	CompPoly/Univariate/NTTFast/Correctness/DIF.lean