|
| 1 | +/- |
| 2 | +Copyright (c) 2026 ArkLib Contributors. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: ArkLib Contributors |
| 5 | +-/ |
| 6 | +import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.WeightedAgreement |
| 7 | +import ArkLib.Data.CodingTheory.ProximityGap.MCABadCount |
| 8 | +import Mathlib.Tactic.Linarith |
| 9 | + |
| 10 | +/-! |
| 11 | +# Faithful ABF26 Theorem 4.21 — genuine GS list-size bound on the MCA bad-scalar count (#140) |
| 12 | +
|
| 13 | +The black-box form of ABF26 Theorem 4.21 (`lineDecodable_imp_epsMCA_le_target`) is |
| 14 | +**mathematically false** and is *proven* refuted in-tree (`LineDecodingRefutation.lean`). |
| 15 | +
|
| 16 | +The first repair attempt routed the conclusion `ε_mca C δ = 0` through the hypothesis |
| 17 | +`MCAForallDoubleCover C δ` (per-coordinate "double cover" by two distinct scalars). That repair |
| 18 | +is **circular**: two distinct scalars pin a degree-`≤1` line, so the double cover collapses to |
| 19 | +joint agreement, and the in-tree theorem `epsMCA_eq_zero_iff_MCAForallDoubleCover` proves |
| 20 | +
|
| 21 | + `MCAForallDoubleCover C δ ↔ epsMCA C δ = 0`. |
| 22 | +
|
| 23 | +The "repaired" hypothesis is therefore *goal-equivalent* to the conclusion — it assumes (an exact |
| 24 | +restatement of) what it sets out to prove, so it carries no content. |
| 25 | +
|
| 26 | +This module gives the **non-circular** repair. The genuine open Guruswami–Sudan content is |
| 27 | +exposed as honest interpolation data — a *single* candidate codeword-pair `v = (v₀, v₁) ∈ C²` |
| 28 | +whose affine line `v₀ + γ·v₁` `µ`-agrees (weight `≥ α`) with the received line `u₀ + γ·u₁` at |
| 29 | +*every* bad scalar `γ` — together with the genuine failure of correlated agreement for that pair. |
| 30 | +This hypothesis is **strictly weaker** than `epsMCA = 0`: it asserts the existence of a shared |
| 31 | +low-degree interpolant covering the bad scalars, *not* the absence of bad scalars. From it the |
| 32 | +**proven** BCIKS20 list-agreement-on-a-curve bound |
| 33 | +(`WeightedAgreement.sufficiently_large_list_agreement_on_curve_implies_correlated_agreement`) |
| 34 | +delivers a real list-size cap on the bad-scalar count: |
| 35 | +
|
| 36 | + `mcaBadCount C δ u₀ u₁ < M·n + 1`, |
| 37 | +
|
| 38 | +i.e. per stack `ε_mca`-contribution `< (M·n + 1)/|F|` — the authentic `a/|F|` shape of T4.21 |
| 39 | +(`l = 0` for the affine line, `M` the common denominator of the weight profile `µ`, `n = |ι|`). |
| 40 | +Contrapositive of the curve bound: were there `≥ M·n + 1` bad scalars sharing the interpolant, |
| 41 | +the curve lemma would force correlated agreement, contradicting its failure. |
| 42 | +
|
| 43 | +The remaining genuinely-open content is *constructing* the GS interpolant `v` (the |
| 44 | +Guruswami–Sudan list decoder of `u₀ + Z·u₁` over `F(Z)`); this module faithfully isolates that |
| 45 | +as the explicit, non-circular hypothesis `hcover`/`hfail`, with the extraction itself proven. |
| 46 | +
|
| 47 | +## References |
| 48 | +
|
| 49 | +- [ABF26] Arnon-Boneh-Fenzi. Theorem 4.21. *Open Problems in List Decoding and Correlated |
| 50 | + Agreement.* |
| 51 | +- [GG25] Goyal-Guruswami; [BCIKS20] Ben-Sasson et al. (the curve list-agreement bound). |
| 52 | +-/ |
| 53 | + |
| 54 | +set_option linter.unusedSectionVars false |
| 55 | + |
| 56 | +open Finset |
| 57 | +open scoped NNReal |
| 58 | + |
| 59 | +namespace ProximityGap |
| 60 | + |
| 61 | +open WeightedAgreement |
| 62 | + |
| 63 | +variable {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι] |
| 64 | +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] |
| 65 | + |
| 66 | +/-- **Faithful ABF26 Theorem 4.21 core — genuine GS list-size bound on the MCA bad-scalar count.** |
| 67 | +
|
| 68 | +The *non-circular* replacement for the refuted black-box `lineDecodable_imp_epsMCA_le_target` and |
| 69 | +for the circular `MCAForallDoubleCover` repair (whose hypothesis is provably equivalent to the |
| 70 | +conclusion `ε_mca = 0` via `epsMCA_eq_zero_iff_MCAForallDoubleCover`). The open Guruswami–Sudan |
| 71 | +content is exposed as genuine interpolation data — a *single* candidate codeword-pair |
| 72 | +`v = (v₀, v₁) ∈ C²` whose affine line `v₀ + γ·v₁` `µ`-agrees (weight `≥ α`) with the received |
| 73 | +line `u₀ + γ·u₁` at *every* bad scalar `γ` — together with the genuine failure of correlated |
| 74 | +agreement for that pair. From this the **proven** BCIKS20 list-agreement-on-a-curve bound |
| 75 | +(`sufficiently_large_list_agreement_on_curve_implies_correlated_agreement`) gives the real |
| 76 | +list-size cap |
| 77 | +
|
| 78 | + `mcaBadCount C δ u₀ u₁ < M·n + 1`, |
| 79 | +
|
| 80 | +i.e. per-stack `ε_mca`-contribution `< (M·n + 1)/|F|`, the genuine `a/|F|` shape of T4.21 |
| 81 | +(`l = 0` for the affine line; `M` the common denominator of the weight profile `µ`, `n = |ι|`). |
| 82 | +
|
| 83 | +The hypothesis is strictly weaker than the conclusion: it asserts a shared low-degree interpolant |
| 84 | +covering the bad scalars, **not** the absence of bad scalars. Contrapositive of the curve bound: |
| 85 | +were there `≥ M·n + 1` bad scalars, the curve lemma would force correlated agreement, |
| 86 | +contradicting `hfail`. -/ |
| 87 | +theorem mcaBadCount_lt_of_gs_curve_cover |
| 88 | + (C : Set (ι → F)) (δ : ℝ≥0) (u₀ u₁ : ι → F) |
| 89 | + (μ : ι → Set.Icc (0 : ℚ) 1) (M : ℕ) (hM : 0 < M) |
| 90 | + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) |
| 91 | + (α : ℝ≥0) (v : Fin 2 → ι → F) |
| 92 | + (hcover : ∀ γ : F, mcaEvent C δ u₀ u₁ γ → |
| 93 | + (α : ℝ) ≤ agree μ (fun x => Curve.polynomialCurveEval (F := F) (A := F) ![u₀, u₁] γ x) |
| 94 | + (fun x => Curve.polynomialCurveEval (F := F) (A := F) v γ x)) |
| 95 | + (hfail : mu_set μ { x : ι | ∀ i, (![u₀, u₁] : Fin 2 → ι → F) i x = v i x } < (α : ℝ)) : |
| 96 | + mcaBadCount (F := F) C δ u₀ u₁ < M * Fintype.card ι + 1 := by |
| 97 | + classical |
| 98 | + by_contra hge |
| 99 | + push_neg at hge |
| 100 | + -- `S'` is exactly the bad-scalar set; `mcaBadCount = S'.card`. |
| 101 | + set S' : Finset F := univ.filter (fun γ : F => mcaEvent C δ u₀ u₁ γ) with hS' |
| 102 | + have hcard : mcaBadCount (F := F) C δ u₀ u₁ = S'.card := rfl |
| 103 | + rw [hcard] at hge |
| 104 | + -- size hypotheses for the curve lemma, `l = 0` |
| 105 | + have hn_pos : 0 < Fintype.card ι := Fintype.card_pos |
| 106 | + have hMn : 2 ≤ M * Fintype.card ι + 1 := by |
| 107 | + have : 1 ≤ M * Fintype.card ι := Nat.one_le_iff_ne_zero.mpr (by positivity) |
| 108 | + omega |
| 109 | + have h1 : S'.card > 0 + 1 := by omega |
| 110 | + have h2 : S'.card ≥ (M * Fintype.card ι + 1) * (0 + 1) := by simpa using hge |
| 111 | + -- the cover gives curve-agreement at every bad scalar `z ∈ S'` |
| 112 | + have hagree : ∀ z ∈ S', |
| 113 | + (α : ℝ) ≤ agree μ |
| 114 | + (fun x => Curve.polynomialCurveEval (F := F) (A := F) ![u₀, u₁] z x) |
| 115 | + (fun x => Curve.polynomialCurveEval (F := F) (A := F) v z x) := by |
| 116 | + intro z hz |
| 117 | + exact hcover z (Finset.mem_filter.mp hz).2 |
| 118 | + -- proven BCIKS20 curve bound forces correlated agreement |
| 119 | + have hcorr : |
| 120 | + mu_set μ { x : ι | ∀ i, (![u₀, u₁] : Fin 2 → ι → F) i x = v i x } ≥ (α : ℝ) := |
| 121 | + sufficiently_large_list_agreement_on_curve_implies_correlated_agreement |
| 122 | + (l := 0) (u := ![u₀, u₁]) (μ := μ) (α := α) (M := M) hμ (v := v) (S' := S') |
| 123 | + h1 h2 hagree |
| 124 | + exact absurd hcorr (not_le.mpr hfail) |
| 125 | + |
| 126 | +end ProximityGap |
| 127 | + |
| 128 | +/-! ### `#print axioms` verification anchor -/ |
| 129 | + |
| 130 | +#print axioms ProximityGap.mcaBadCount_lt_of_gs_curve_cover |
0 commit comments