Sundogcert/SATReductionForward.lean — MILESTONE 8 of the 3SAT ≤ 3DM marathon: the FORWARD
DIRECTION of the reduction's correctness, and the analytic crux of the whole reduction.
WHAT THIS FILE PROVES (forward):
Satisfiable φ → threeDMI (tripleFn φ)
— a satisfying assignment for the formula φ yields a perfect 3-dimensional matching of the
gadget triple map. This is the hard direction: it must EXHIBIT the matching explicitly and then
verify all three cover conditions (each W-, X-, and Y-element hit exactly once).
THE CONSTRUCTION (pure combinatorics, all inside the proof). From a satisfying assignment a and
a per-clause witness slot slotStar k (choose from sat), build three triple families:
* WHEEL triples — one per (i, j): wheelTriple ij = negT i j if a i, else posT i j. The
tip it consumes is (i, j, !(a i)); so a tip (i, j, s) is FREE (unconsumed) iff s = a i.
* CLAUSE triples — one per clause k: clauseT k (slotStar k), whose W-tip
((φ k (slotStar k)).1, k, (φ k (slotStar k)).2) is a free tip (the witness literal is true,
so its sign matches a at its variable — hlitfree). These m tips are the CLAIMED tips.
* GARBAGE triples — one per g : Fin (m·(n-1)): garbageT g (β g), where β bijects
Fin (m·(n-1)) onto the UNCLAIMED free tips (freeTips \ claimedTips; the count
n·m − m = m·(n−1) uses n ≥ 1, and the bijection comes from Fintype.equivFinOfCardEq).
The matching T is the union of the three image families.
THE THREE COVER CONDITIONS. Because the three families live in DISJOINT Sum summands of
TripleIdx, any predicate's filtered count over T splits as wheel + clause + garbage
(hsplit), and each part — an image of an injective map over univ — reduces to a univ-filter
count (hredWheel/hredClause/hredGarbage). Then:
* W-condition: each tip (i, j, s) is hit once — CONSUMED → (1,0,0); free & CLAIMED → (0,1,0);
free & UNCLAIMED → (0,0,1).
* X-condition: an a-node is hit by exactly one wheel triple (the CYCLIC spoke shift, via
xcoord_inl); an s1/g1-node by exactly the matching clause/garbage triple (xcoord_s1/g1).
* Y-condition: a b-node by exactly the single wheel triple at (i, j) (NO cyclic shift,
ycoord_inl); an s2/g2-node by the matching clause/garbage triple (ycoord_s2/g2).
STANDING LIMIT: this module proves ONLY the forward direction. The reverse direction
(threeDMI (tripleFn φ) → Satisfiable φ) is milestone 7 (Sundogcert/SATReductionReverse.lean),
and the index-bridge to the Fin s-indexed MatchingNPHard.ThreeDM is milestone 5
(Sundogcert/ThreeDMReindex.lean). Nothing here is claimed about NP-hardness itself.
NOTE on synthInstance.maxSize: DecidableEq (TripleIdx n m) (a 4-way nested Sum of products)
does not synthesize at the default maxSize inside this large proof context; a scoped
set_option synthInstance.maxSize 512 in on forward clears it (as in m7).
Axiom-clean (no native_decide, no decide). Expect [propext, Classical.choice, Quot.sound].
The W-fibre (tip) cover condition of the forward matching, factored out of forward.
Given the disjoint-split reduction hsplit, the per-family univ-filter reductions hred*,
and the per-family tip characterizations h*tip, every tip w is covered exactly once by the
matching: consumed → wheel hits it once; free & claimed → the clause triple; free & unclaimed →
the garbage triple.
The X-node cover condition of the forward matching, factored out of forward.
Each a-node inl (i,j) is hit by exactly one wheel triple (the cyclic spoke shift); each
s1-node by exactly its clause triple; each g1-node by exactly its garbage triple.
The Y-node cover condition of the forward matching, factored out of forward.
Each b-node inl (i,j) is hit by exactly one wheel triple (no cyclic shift on the Y side); each
s2-node by exactly its clause triple; each g2-node by exactly its garbage triple.