Sundogcert/SATReduction.lean — MILESTONE 4 of the 3SAT ≤ 3DM marathon: the GLOBAL ASSEMBLY
SCAFFOLDING (the DATA LAYER). This module fixes the three coordinate types, the triple-index
type, the reduction function, the cardinality lemmas, and the theorem that reduce φ PLUGS INTO
the already-formalized hardness chain 3DM ≤ X3C ≤ Decodes. (Lean 4 / mathlib v4.30.0.)
THE THREE COORDINATE TYPES (each of cardinality 2·m·n — the chain weight q):
* Tip = Fin n × Fin m × Bool (the W-part: tip = variable·spoke·sign).
* XNode = (Fin n × Fin m) ⊕ Fin m ⊕ Fin (m*(n-1)) (a-nodes ⊕ s1-nodes ⊕ garbage g1).
* YNode = (Fin n × Fin m) ⊕ Fin m ⊕ Fin (m*(n-1)) (b-nodes ⊕ s2-nodes ⊕ garbage g2).
CARDINALITIES. |Tip| = n·m·2 = 2mn. |XNode| = |YNode| = n·m + m + m·(n-1); with n ≥ 1
([NeZero n]) one has m·(n-1) + m = m·n in ℕ, so each is n·m + m·n = 2mn. The [NeZero n]
is exactly what makes the garbage count close the books to 2mn.
THE TRIPLE-INDEX TYPE (a clean 4-way Sum — avoids any Fin-arithmetic decode):
TripleIdx = (Fin n × Fin m) ⊕ (Fin n × Fin m) ⊕ (Fin m × Fin 3) ⊕ (Fin (m*(n-1)) × Tip)
indexing, in order: the wheel POSITIVE triples, the wheel NEGATIVE triples, the CLAUSE
slot-triples (clause k, slot), and the GARBAGE triples (garbage g, any free tip w).
THE TRIPLE FUNCTION tripleFn φ : TripleIdx → Tip × XNode × YNode (faithful to m2/m3 gadgets):
* wheel POS (i,j): ((i, j, true), inl (i, j), inl (i, j))
— posTip(i,j); a-node (i,j); b-node (i,j). Matches VarWheel t_j=(posTip,a j,b j).
* wheel NEG (i,j): ((i, j, false), inl (i, j+1), inl (i, j))
— negTip(i,j); a-node (i,j+1) (j+1 CYCLIC in Fin m); b-node (i,j). Matches
t⁻_j=(negTip, a(j+1), b j).
* CLAUSE (k,slot): let l := φ k slot; ((l.1, k, l.2), inr (inl k), inr (inl k))
— tip of literal l at spoke k; s1_k; s2_k. Matches the ClauseGadget slot-triple
(tip(c_k,slot), s1_k, s2_k); tip polarity = l.2 (the literal sign).
* GARBAGE (g,w): (w, inr (inr g), inr (inr g))
— any free tip w; g1_g; g2_g. Garbage absorbs any leftover free tip.
THE REDUCTION (Fin s → Tip × XNode × YNode, s = card TripleIdx, via the canonical equiv):
reduce φ := fun i => tripleFn φ ((Fintype.equivFin _).symm i), where
Fintype.equivFin T : T ≃ Fin (card T) (so .symm : Fin (card T) → T). equivFin is
noncomputable, so reduce is noncomputable — fine; nothing here is meant to run.
THE CHAIN-CONNECTION PAYOFF (this milestone's deliverable):
reduce_chain_connects φ : ThreeDM (reduce φ) ↔ Decodes (reduce3DM (reduce φ)) (2*m*n),
obtained by feeding card_tip/card_xnode/card_ynode to the already-proved
MatchingNPHard.threeDM_iff_Decodes. So the SAT-side reduce function is now wired onto the
formalized 3DM ≤ X3C ≤ Decodes chain.
THE IMPORTED WALL (named, NOT proved — mathlib has no complexity framework):
* the NP complexity class itself, and poly-time-ness of any reduction;
* 3SAT's OWN NP-hardness — Cook–Levin, the deep terminal wall sourcing every Karp-reduction
hardness claim in this 3SAT ≤ 3DM ≤ X3C ≤ Decodes chain.
STANDING LIMIT: this module is the DATA LAYER only. It builds the reduction's TYPES, INDEX, and
TRIPLE MAP and connects them to the chain by cardinality. The GADGET CORRECTNESS
(Satisfiable φ ↔ ThreeDM (reduce φ)) — that the wheel + clause + garbage triples actually
enforce satisfiability — is milestones 5–7.
Axiom-clean throughout (decide is never used here; no native_decide). Expect
[propext, Classical.choice, Quot.sound] on the four audited results.
The three coordinate types (each of cardinality 2·m·n). #
The triple-index type (a clean 4-way Sum). #
The reduction's triple index: wheel-positive ⊕ wheel-negative ⊕ clause-slot ⊕ garbage.
Equations
Instances For
Decidable equality on the 4-way nested Sum index type, assembled layer by layer so that
instance synthesis stays within the default synthInstance.maxSize (a blind search over the
full nesting otherwise overflows it).
The triple function — faithful to the milestone-2/3 gadgets. #
The triple map TripleIdx → Tip × XNode × YNode: each index slot emits its gadget triple.
Equations
- Sundog.SATReduction.tripleFn φ (Sum.inl (i, j)) = ((i, j, true), Sum.inl (i, j), Sum.inl (i, j))
- Sundog.SATReduction.tripleFn φ (Sum.inr (Sum.inl (i, j))) = ((i, j, false), Sum.inl (i, j + 1), Sum.inl (i, j))
- Sundog.SATReduction.tripleFn φ (Sum.inr (Sum.inr (Sum.inl (k, slot)))) = (((φ k slot).1, k, (φ k slot).2), Sum.inr (Sum.inl k), Sum.inr (Sum.inl k))
- Sundog.SATReduction.tripleFn φ (Sum.inr (Sum.inr (Sum.inr (g, w)))) = (w, Sum.inr (Sum.inr g), Sum.inr (Sum.inr g))
Instances For
The reduction. Re-index the gadget triple map along the canonical finite equiv, giving the
Fin s → Tip × XNode × YNode shape the matching problem wants (s = card TripleIdx).
noncomputable because Fintype.equivFin is.
Equations
Instances For
Cardinality lemmas — the hypotheses threeDM_iff_Decodes needs (q := 2*m*n). #
|XNode| = n·m + m + m·(n-1) = 2mn (the m·(n-1)+m = m·n step uses n ≥ 1).
|YNode| = n·m + m + m·(n-1) = 2mn (same shape as XNode).
The chain-connection theorem — the milestone-4 payoff. #
THE CHAIN CONNECTION (the m4 deliverable). reduce φ plugs into the formalized hardness
chain: ThreeDM (reduce φ) ↔ Decodes (reduce3DM (reduce φ)) (2mn), by feeding the three card
lemmas to the already-proved MatchingNPHard.threeDM_iff_Decodes. The GADGET correctness
(Satisfiable φ ↔ ThreeDM (reduce φ)) is milestones 5–7.
Axiom audit. #
Expect `[propext, Classical.choice, Quot.sound]` (or a subset) — NO `sorryAx`, and NO
`Lean.ofReduceBool` (we never use `decide`/`native_decide` in this module).