Sundogcert/SATReductionReverse.lean — MILESTONE 7 of the 3SAT ≤ 3DM marathon: the REVERSE DIRECTION of the reduction's correctness.

WHAT THIS FILE PROVES (reverse): threeDMI (tripleFn φ) → Satisfiable φ — a perfect 3-dimensional matching of the gadget triple map yields a satisfying assignment for the formula φ. This is the analytic crux of the reduction; it does NOT touch the garbage triples (their only role is to absorb the unused tips, which a perfect matching handles for free).

THE PROOF IDEA (pure combinatorics): Let T : Finset (TripleIdx n m) be the matching selection. * Define σ i j := decide (posT i j ∈ T) — for each variable i, the wheel state read off from which positive triples were selected. * Each b-node (i,j) is covered exactly once (hY); the only triples touching it are posT i j and negT i j (incidence ycoord_inl). So EXACTLY ONE of the two is in T: posT i j ∈ T ↔ ¬ negT i j ∈ T (the helper card_filter_pair_eq_one). * Each a-node (i,j) is covered exactly once (hX); the only triples touching it are posT i j and negT i (j-1) (incidence xcoord_inl, the CYCLIC spoke shift). So posT i j ∈ T ↔ ¬ negT i (j-1) ∈ T. * Chaining the two facts forces σ i j = σ i (j-1) for every spoke ⟹ σ i is a ValidCover ⟹ by validCover_iff_const, σ i is CONSTANT (the wheel admits only the all-true / all-false covers — the two truth values). Take the assignment a i := !(σ i 0). * Each s1-node k is covered exactly once (hX), and the only triples touching it are the clause-k slot triples (xcoord_s1). Hence some clauseT k slotStar ∈ T; its W-tip τ = (iS, k, sgn) (with (iS, sgn) = φ k slotStar) is then covered by that clause triple, so the matching wheel triple over τ (posT iS k if sgn, else negT iS k) is NOT in T (hW: the W-fibre over τ has card 1). Reading this back through σ shows the literal φ k slotStar evaluates to true, hence clause k is satisfied.

STANDING LIMIT: this module proves ONLY the reverse direction. The forward direction (Satisfiable φ → threeDMI (tripleFn φ) — a matching from an assignment) is milestone 8.

NOTE on the synthInstance.maxSize bump: DecidableEq (TripleIdx n m) (a 4-way nested Sum of products) does not synthesize at the default maxSize; the filter_congr rewrites whose target predicate is idx = posT i j ∨ idx = negT i j push the threshold higher still. A scoped set_option synthInstance.maxSize 512 in on reverse clears it (the generic helper needs none).

Axiom-clean (no native_decide; the only decide is the data-level Prop-membership read). Expect [propext, Classical.choice, Quot.sound] on both reverse and the helper.

Helper lemma

theorem Sundog.SATReductionReverse.card_filter_pair_eq_one {α : Type u_1} [DecidableEq α] {T : Finset α} {a b : α} (hab : a ≠ b) (h : {x ∈ T | x = a ∨ x = b}.card = 1) : a ∈ T ↔ b ∉ T

In a Finset T, if exactly one of two DISTINCT elements a, b is present (the {a,b} fibre of T has card 1), then membership of a is the negation of membership of b.

The reverse theorem

theorem Sundog.SATReductionReverse.reverse {n m : ℕ} [NeZero m] (φ : SATNPHard.Formula n m) (h : ThreeDMReindex.threeDMI (SATReduction.tripleFn φ)) : SATNPHard.Satisfiable φ

Reverse correctness. A perfect 3-dimensional matching of the gadget triple map yields a satisfying assignment: the wheel triples force each variable's selection constant (a truth value), and each clause's selected slot triple frees its literal's wheel triple, making the literal true. (One direction only; the forward direction is milestone 8.)

Axiom audit.

Expect `[propext, Classical.choice, Quot.sound]` — NO `sorryAx`, NO `Lean.ofReduceBool`.