Sundogcert/MatchingNPHard.lean — the KARP-LAYER EXTENSION of the formalized hardness chain: 3-DIMENSIONAL MATCHING (3DM) reduces to EXACT-COVER-BY-3-SETS (X3C), composed through frontier #1's reduction_iff into bounded-weight GF(2) decoding. (Lean 4 / mathlib v4.30.0.)

WHAT THIS FILE PROVES (pure combinatorics — the reduction CORRECTNESS, no gadgets): * ThreeDM t — a perfect 3-dimensional matching among the s triples t : Fin s → W×X×Y: a selection T of triples covering each W-, X-, and Y-element exactly once. * reduce3DM t — the Karp reduction: each triple (w,x,y) becomes its 3-element set {inl w, inr (inl x), inr (inr y)} in the X3C universe W ⊕ X ⊕ Y. * threeDM_iff_X3C (THE HEADLINE) — ThreeDM t ↔ X3C (reduce3DM t), machine-checked. Both sides are ∃ T, <cond>; the X3C exact-cover condition over W ⊕ X ⊕ Y decomposes (via Sum.forall, twice) into exactly the three per-part "covered once" conditions of ThreeDM. No gadgets — the equivalence is the Sum-universe bookkeeping, nothing more. * reduce3DM_card — every reduce-set is a genuine 3-set (the three Sum-tagged elements are pairwise distinct: inl ≠ inr, and the two inr-branches differ by inl ≠ inr again). * reduce3DM_univ_card — with |W| = |X| = |Y| = q, the universe W ⊕ X ⊕ Y has 3q points. * threeDM_iff_Decodes (THE COMPOSITION / PAYOFF) — chaining the headline through frontier #1's PROVED reduction_iff (whose hypotheses (c i).card = 3 and |universe| = 3q are discharged by the two card lemmas) yields ThreeDM t ↔ Decodes (reduce3DM t) q. The hardness chain 3DM ≤ X3C ≤ Decodes is now formalized end to end.

THE IMPORTED WALL (named, NOT proved — mathlib has no complexity framework): * the NP complexity class itself, and poly-time-ness of this reduction (it is visibly local — each triple maps to one 3-set — but "polynomial" is unformalized); * 3DM's OWN NP-hardness (Garey–Johnson problem GT2, via 3SAT ≤ 3DM, NOT yet formalized — the next milestone; this file only relates 3DM to X3C, it does not prove 3DM hard from scratch); * the DEEP TERMINAL WALL = SAT's NP-hardness (Cook–Levin), a multi-year formalization, named forever as the ultimate source of every Karp-reduction hardness claim in this chain. STANDING LIMIT (unchanged): NP-hardness is CONDITIONAL on P≠NP — never absolute. What this file adds is one Karp layer of REACH: it pushes the imported wall outward from "X3C is hard" to "3DM is hard", since 3DM ↔ X3C (the reduction is an equivalence — reduce3DM is essentially a relabeling). A small but composable, de-risking step toward the genuine gadget reduction 3SAT ≤ 3DM that would discharge 3DM's hardness internally.

The two problems and the reduction.

def Sundog.MatchingNPHard.ThreeDM {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) : Prop

Perfect 3-dimensional matching among the s triples: a selection T of triple-indices covering each W-element, each X-element, and each Y-element exactly once.

Equations

• One or more equations did not get rendered due to their size.

def Sundog.MatchingNPHard.reduce3DM {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) : Fin s → Finset (W ⊕ X ⊕ Y)

The reduction. Each triple (w, x, y) becomes its 3-element set in the X3C universe W ⊕ X ⊕ Y: the W-, X-, Y-coordinates are tagged into the three disjoint summands.

Equations

• Sundog.MatchingNPHard.reduce3DM t i = {Sum.inl (t i).1, Sum.inr (Sum.inl (t i).2.1), Sum.inr (Sum.inr (t i).2.2)}

Membership lemmas — each Sum-tagged point lands in exactly its coordinate's slot.

theorem Sundog.MatchingNPHard.mem_reduce_inl {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (i : Fin s) (w : W) : Sum.inl w ∈ reduce3DM t i ↔ (t i).1 = w

A W-tagged point inl w is in the reduce-set of triple i iff that triple's W-coordinate is w (the other two slots are inr, never equal to inl w).

theorem Sundog.MatchingNPHard.mem_reduce_inr_inl {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (i : Fin s) (x : X) : Sum.inr (Sum.inl x) ∈ reduce3DM t i ↔ (t i).2.1 = x

An X-tagged point inr (inl x) is in the reduce-set of triple i iff that triple's X-coordinate is x.

theorem Sundog.MatchingNPHard.mem_reduce_inr_inr {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (i : Fin s) (y : Y) : Sum.inr (Sum.inr y) ∈ reduce3DM t i ↔ (t i).2.2 = y

A Y-tagged point inr (inr y) is in the reduce-set of triple i iff that triple's Y-coordinate is y.

The cover counts of the reduced instance ARE the per-part filter counts.

theorem Sundog.MatchingNPHard.coverCount_inl {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (T : Finset (Fin s)) (w : W) : DecodingNPHard.coverCount (reduce3DM t) T (Sum.inl w) = {i ∈ T | (t i).1 = w}.card

The X3C cover count of a W-tagged point equals the W-part matching count.

theorem Sundog.MatchingNPHard.coverCount_inr_inl {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (T : Finset (Fin s)) (x : X) : DecodingNPHard.coverCount (reduce3DM t) T (Sum.inr (Sum.inl x)) = {i ∈ T | (t i).2.1 = x}.card

The X3C cover count of an X-tagged point equals the X-part matching count.

theorem Sundog.MatchingNPHard.coverCount_inr_inr {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (T : Finset (Fin s)) (y : Y) : DecodingNPHard.coverCount (reduce3DM t) T (Sum.inr (Sum.inr y)) = {i ∈ T | (t i).2.2 = y}.card

The X3C cover count of a Y-tagged point equals the Y-part matching count.

THE HEADLINE — reduction correctness.

theorem Sundog.MatchingNPHard.threeDM_iff_X3C {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) : ThreeDM t ↔ DecodingNPHard.X3C (reduce3DM t)

THE REDUCTION CORRECTNESS (machine-checked, pure combinatorics). ThreeDM t holds iff the reduced X3C instance reduce3DM t has an exact cover. Both sides are ∃ T, <cond>; for a fixed T, the X3C exact-cover condition ∀ u : W ⊕ X ⊕ Y, coverCount … u = 1 decomposes via Sum.forall (applied twice, for W ⊕ (X ⊕ Y)) into the three slots, and the cover-count lemmas rewrite each slot into the corresponding per-part matching count. So the X3C condition is EXACTLY ThreeDM's three-fold "covered once" condition — no gadgets, just the Sum bookkeeping.

Card lemmas — the hypotheses frontier #1 needs.

theorem Sundog.MatchingNPHard.reduce3DM_card {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (i : Fin s) : (reduce3DM t i).card = 3

Each reduce-set is a genuine 3-set: its three Sum-tagged elements are pairwise distinct.

theorem Sundog.MatchingNPHard.reduce3DM_univ_card {W : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype W] [Fintype X] [Fintype Y] (q : ℕ) (hW : Fintype.card W = q) (hX : Fintype.card X = q) (hY : Fintype.card Y = q) : Fintype.card (W ⊕ X ⊕ Y) = 3 * q

With each part of size q, the X3C universe W ⊕ X ⊕ Y has 3q points.

THE COMPOSITION — chain extended to the certificate.

theorem Sundog.MatchingNPHard.threeDM_iff_Decodes {W : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype W] [Fintype X] [Fintype Y] [DecidableEq W] [DecidableEq X] [DecidableEq Y] {s : ℕ} (t : Fin s → W × X × Y) (q : ℕ) (hW : Fintype.card W = q) (hX : Fintype.card X = q) (hY : Fintype.card Y = q) : ThreeDM t ↔ DecodingNPHard.Decodes (reduce3DM t) q

THE COMPOSITION (the payoff). Chaining the headline threeDM_iff_X3C through frontier #1's PROVED reduction_iff — whose two hypotheses (each set has card 3; the universe has 3q points) are discharged by reduce3DM_card and reduce3DM_univ_card — yields ThreeDM t ↔ Decodes (reduce3DM t) q. The formalized hardness chain 3DM ≤ X3C ≤ Decodes is now complete end to end; only the COMPLEXITY WRAPPING (NP class, poly-time-ness, 3DM's own NP-hardness Garey–Johnson GT2, ultimately Cook–Levin) stays the named imported wall.

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