Sundogcert/DecodingNPHard.lean — the DEDUCTIVE CORE of NP-hardness of SYNDROME DECODING over GF(2), via the reduction from EXACT-COVER-BY-3-SETS (EC3S / X3C). (Lean 4 / mathlib v4.30.0. Berlekamp–McEliece–van Tilborg route.)

WHAT THIS FILE PROVES (the deductive core — MILESTONES 1 AND 2 BOTH DONE): * the reduction is laid out exactly as designed: an EC3S instance (c : Fin s → Finset X) becomes a parity-check matrix Hmat c over ZMod 2 with target syndrome allOnes, and a bounded-weight decoding question Decodes c q. * the KEY CONNECTION (connection): for the indicator error eOf T, the syndrome Hmat c *ᵥ eOf T is the mod-2 cast of the cover count — so "syndrome = allOnes" is exactly "every point is covered an ODD number of times". An exact cover (count = 1) is odd. * the DOUBLE-COUNT (incidence_double_count): ∑ i∈T, (c i).card = ∑ x, coverCount c T x, which with hc (each 3-set has card 3) and hX (|X| = 3q) pins T.card = q. * reduction_forward (PROVED): an exact cover yields a weight-≤ q decoding witness. * reduction_backward (PROVED, MILESTONE 2): a weight-≤ q decoding witness MUST be a 0/1 exact-cover indicator. Over ZMod 2 the error is 0/1, so its support T has eOf T = e and |T| ≤ q; "syndrome = allOnes" forces every cover count ODD hence ≥ 1, and the double-count ∑ coverCount = 3|T| ≥ |X| = 3q pins |T| = q; equal sums with the pointwise ≥ 1 bound force every cover count = 1 — an exact cover. * reduction_iff (UNCONDITIONAL): the full X3C c ↔ Decodes c q, both directions now machine-checked (⟨reduction_forward, reduction_backward⟩) — NO hypothesis, NO sorry, NO axiom. The reduction's correctness is FULLY proved; only the COMPLEXITY WRAPPING remains the named imported wall (below).

WIRE-IN TO THE CERTIFICATE. Decodes c q is EXACTLY the decision form of Sundog.Certificate.CertWall.minCosetWeight (Hmat c) allOnes ≤ q — we use the EXISTENTIAL form (∃ e, Hmat *ᵥ e = allOnes ∧ hammingNorm e ≤ q) rather than minCosetWeight ≤ q to dodge the sInf-of-empty-coset pitfall (safe_iff_minCosetWeight_le in CertWall is the bridge when the coset is nonempty). So this reduction LANDS on the certificate's imported hardness wall: CertWall's minCosetWeight is the very quantity an EC3S→decoding reduction makes NP-hard.

THE IMPORTED WALL (named, NOT proved — mathlib has no complexity framework): * the NP complexity class itself; * poly-time-ness of this reduction (it is visibly local, but "polynomial" is unformalized); * EC3S's own NP-hardness (Karp 1972). STANDING LIMIT. With milestone 2 done, this proves "decoding is NP-hard CONDITIONAL on P≠NP" — hardness is never absolute, and this limit is UNCHANGED by completing the backward direction. What IS proved (now in full) is that bounded-weight GF(2) decoding is exactly as hard as a canonical NP-hard problem (EC3S): the reduction correctness X3C c ↔ Decodes c q is fully machine-checked; only the complexity wrapping above stays imported.

CORRECTNESS NOTE (a wrong reduction is the failure mode). Decoding is over GF(2), so H *ᵥ e is a MOD-2 (XOR) sum. EC3S is the right source problem because GF(2) is the natural operation for COVERING (odd-cover) — unlike subset-sum, which needs integer carries and is WRONG over GF(2). The connection lemma makes the odd-cover ⇔ syndrome=allOnes equivalence explicit.

The reduction's definitions.

def Sundog.DecodingNPHard.coverCount {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (T : Finset (Fin s)) (x : X) : ℕ

coverCount c T x — how many SELECTED 3-sets (indices in T) contain the point x.

Equations

• Sundog.DecodingNPHard.coverCount c T x = {i ∈ T | x ∈ c i}.card

def Sundog.DecodingNPHard.IsExactCover {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (T : Finset (Fin s)) : Prop

T is an exact cover: every point is covered by exactly one selected set.

Equations

• Sundog.DecodingNPHard.IsExactCover c T = ∀ (x : X), Sundog.DecodingNPHard.coverCount c T x = 1

def Sundog.DecodingNPHard.X3C {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) : Prop

EC3S / X3C: an exact cover exists. (The source NP-hard problem; Karp 1972.)

Equations

• Sundog.DecodingNPHard.X3C c = ∃ (T : Finset (Fin s)), Sundog.DecodingNPHard.IsExactCover c T

def Sundog.DecodingNPHard.Hmat {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) : Matrix X (Fin s) (ZMod 2)

The parity-check matrix of the reduction: column i is the GF(2) indicator of the 3-set c i. Rows are points of X, columns are the s sets.

Equations

• Sundog.DecodingNPHard.Hmat c = Matrix.of fun (x : X) (i : Fin s) => if x ∈ c i then 1 else 0

def Sundog.DecodingNPHard.allOnes {X : Type u_1} : X → ZMod 2

The all-ones target syndrome — "cover every point".

Equations

• Sundog.DecodingNPHard.allOnes = Function.const X 1

def Sundog.DecodingNPHard.Decodes {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (q : ℕ) : Prop

The decoding question (decision form of minCosetWeight (Hmat c) allOnes ≤ q): is there a GF(2) error pattern e of weight ≤ q whose syndrome is the all-ones vector? Existential form, NOT minCosetWeight ≤ q, to dodge the sInf-of-empty-coset pitfall.

Equations

• Sundog.DecodingNPHard.Decodes c q = ∃ (e : Fin s → ZMod 2), (Sundog.DecodingNPHard.Hmat c).mulVec e = Sundog.DecodingNPHard.allOnes ∧ hammingNorm e ≤ q

def Sundog.DecodingNPHard.eOf {s : ℕ} (T : Finset (Fin s)) : Fin s → ZMod 2

The 0/1 indicator error pattern of a selection T (a column-selection of Hmat).

Equations

• Sundog.DecodingNPHard.eOf T i = if i ∈ T then 1 else 0

The KEY CONNECTION — syndrome of eOf T is the mod-2 cast of the cover count.

theorem Sundog.DecodingNPHard.syndrome_eq_coverCount_cast {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (T : Finset (Fin s)) (x : X) : (Hmat c).mulVec (eOf T) x = ↑(coverCount c T x)

For each point x, the syndrome coordinate (Hmat c *ᵥ eOf T) x equals the mod-2 cast of coverCount c T x: each selected set containing x contributes a 1, all summed in ZMod 2, so the parity of the cover count is exactly the syndrome bit.

theorem Sundog.DecodingNPHard.hammingNorm_eOf {s : ℕ} (T : Finset (Fin s)) : hammingNorm (eOf T) = T.card

The Hamming weight of the indicator error equals the size of the selection.

theorem Sundog.DecodingNPHard.syndrome_eOf_eq_allOnes {X : Type u_1} [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (T : Finset (Fin s)) (hT : IsExactCover c T) : (Hmat c).mulVec (eOf T) = allOnes

An EXACT cover makes the syndrome the all-ones vector: count 1 is odd, so its mod-2 cast is 1 at every point.

The DOUBLE-COUNT — incidence count, two ways.

theorem Sundog.DecodingNPHard.incidence_double_count {X : Type u_1} [Fintype X] [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (T : Finset (Fin s)) : ∑ i ∈ T, (c i).card = ∑ x : X, coverCount c T x

Incidence double-count. Summing set-sizes over selected sets equals summing cover-counts over points: both count the incidence pairs (i, x) with i ∈ T and x ∈ c i. Proved by Finset.sum_comm after writing each card as a sum of 0/1 indicators.

theorem Sundog.DecodingNPHard.exactCover_card_eq {X : Type u_1} [Fintype X] [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (q : ℕ) (hc : ∀ (i : Fin s), (c i).card = 3) (hX : Fintype.card X = 3 * q) (T : Finset (Fin s)) (hT : IsExactCover c T) : T.card = q

With each 3-set of card 3, an exact cover of an X of size 3q selects exactly q sets. 3 * T.card = ∑ i∈T, 3 = ∑ i∈T, (c i).card = ∑ x, coverCount = ∑ x, 1 = |X| = 3q.

THE THEOREMS.

theorem Sundog.DecodingNPHard.reduction_forward {X : Type u_1} [Fintype X] [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (q : ℕ) (hc : ∀ (i : Fin s), (c i).card = 3) (hX : Fintype.card X = 3 * q) (h : X3C c) : Decodes c q

FORWARD (PROVED). An EC3S exact cover yields a bounded-weight GF(2) decoding witness: the column-selection eOf T has syndrome allOnes (connection lemma) and weight T.card = q ≤ q (double-count).

theorem Sundog.DecodingNPHard.reduction_backward {X : Type u_1} [Fintype X] [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (q : ℕ) (hc : ∀ (i : Fin s), (c i).card = 3) (hX : Fintype.card X = 3 * q) (h : Decodes c q) : X3C c

BACKWARD (PROVED, MILESTONE 2). A bounded-weight GF(2) decoding witness MUST be a 0/1 exact-cover indicator. Over ZMod 2 every coordinate of e is 0 or 1, so for its support T := {i | e i ≠ 0} we have e = eOf T and |T| = hammingNorm e ≤ q. "Syndrome = allOnes" casts each cover count to 1 in ZMod 2, forcing it ODD hence ≥ 1; the double-count plus hc gives ∑ coverCount = 3|T|, and pointwise ≥ 1 summed gives ∑ coverCount ≥ |X| = 3q, pinning |T| = q. Finally equal sums against the pointwise ≥ 1 bound force every cover count to be EXACTLY 1 — an exact cover.

theorem Sundog.DecodingNPHard.reduction_iff {X : Type u_1} [Fintype X] [DecidableEq X] {s : ℕ} (c : Fin s → Finset X) (q : ℕ) (hc : ∀ (i : Fin s), (c i).card = 3) (hX : Fintype.card X = 3 * q) : X3C c ↔ Decodes c q

THE REDUCTION IFF (UNCONDITIONAL). Both directions are now machine-checked: forward is the PROVED reduction_forward, backward is the PROVED reduction_backward (milestone 2). This is the full EC3S ⇔ bounded-weight-GF(2)-decoding equivalence — the reduction's correctness, NO hypothesis, NO sorry, NO axiom — landing on CertWall's minCosetWeight imported wall. Only the COMPLEXITY WRAPPING (NP class, poly-time-ness, EC3S's own NP-hardness, Karp 1972) stays the named imported wall; the standing limit (NP-hard CONDITIONAL on P≠NP) is unchanged.

Axiom audit on the two headline theorems (expect propext/Classical.choice/Quot.sound).