Error-Sensitive Alignment Bounds for Affine-Line Decoding: A Lean-Verified Refinement

Goyal and Guruswami derive mutual correlated agreement (MCA) for the affine-line generator from line decodability, requiring n + 1 aligned challenges, where n is the block length. We prove that max(⌊δn⌋ + 2, 3) aligned challenges suffice when n < |F|, where δ is the proximity parameter. Using a classical counting argument, we replace an injection of challenges into coordinates with a double count of mismatch coordinates. This refinement improves the capacity-regime MCA upper bound for folded Reed–Solomon codes from (nt + 3t³)/|F| to ((δn + 2)t + 3t³)/|F|, where δ = 1 − ρ − 2/t, under the stated hypotheses. The counting technique has precedents in Ligero, Ben-Sasson–Kopparty–Saraf, and Haböck. Our contribution is applying it to the alignment argument of GG25, deriving the improved FRS bound, and formally verifying the resulting theorems in Lean 4 using ArkLib. Version 1.0.1 adds prior-art citations and clarifies the contribution. The mathematical results and Lean proofs are unchanged from version 1.0.0. Independent research preprint. Not peer reviewed.