Sundogcert/ClauseGadget.lean — MILESTONE 3 of the 3SAT ≤ 3DM marathon.

WHAT THIS FILE PROVIDES (the Garey–Johnson CLAUSE gadget + the POLARITY BRIDGE): For each clause c_k the gadget owns two INTERNAL nodes s1_k, s2_k (covered exactly once, local to this clause) and THREE cover triples, one per literal-slot k' ∈ {0,1,2}: slot-k' triple = (tip(c_k, k'), s1_k, s2_k) The slot-k' triple is USABLE iff that literal's TIP is FREE — i.e. NOT consumed by its variable wheel (milestone 2). Hence s1_k, s2_k are coverable iff AT LEAST ONE of the three slots' tips is free. The global matching uses exactly one such triple; garbage collection mops up the remaining free tips (milestone 4).

THE GADGET PICTURE (one clause c_k; the three slot-triples fan into the shared internal pair):

    tip(c_k,0) ─┐
    tip(c_k,1) ─+──▶  s1_k , s2_k   (each slot-triple = (tip, s1_k, s2_k))
    tip(c_k,2) ─┘
    `s1_k, s2_k` coverable  ↔  ∃ slot k' with tip(c_k,k') FREE.

THE POLARITY CONVENTION (this DISCHARGES milestone 2's deferred truth-value labeling — the classic bug locus, so stated with care and validated end-to-end by kernel decide below): Variable xᵢ takes the Boolean value ai IFF its wheel runs the CONSTANT selection σᵢ = fun _ => !ai. Then: ai = true ⟹ σᵢ = const false ⟹ (VarWheel.falseState_frees_pos) POSITIVE tips free; ai = false ⟹ σᵢ = const true ⟹ (VarWheel.trueState_frees_neg) NEGATIVE tips free. With VarWheel.posTipFree σ j := (σ j = false) and negTipFree σ j := (σ j = true), and σᵢ = fun _ => !ai: posTipFree ↔ (!ai = false) ↔ ai = true; negTipFree ↔ (!ai = true) ↔ ai = false . A literal l = (i, sign): a POSITIVE literal (sign = true) uses the positive tip, free iff ai = true, i.e. iff evalLiteral = ai; a NEGATIVE literal (sign = false) uses the negative tip, free iff ai = false, i.e. iff evalLiteral = !ai. In every case the tip is free exactly when the literal evaluates to true — litTipFree ↔ evalLiteral = true. THIS is the bridge.

THE IMPORTED WALL (named, NOT proved — mathlib has no complexity framework): * the NP complexity class and poly-time-ness of the 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 proves the clause gadget's LOCAL correctness (a clause is coverable iff it is satisfied, via the polarity bridge). The garbage-collection triples and the GLOBAL assembly onto Sundog.MatchingNPHard.ThreeDM are milestones 4–8.

Decidability of clauseCoverable is registered explicitly (it is an ∃ over Fin 3 of a decidable Prop). This locks the polarity convention end-to-end by kernel decide — AXIOM-CLEAN (no Lean.ofReduceBool; we use decide, never native_decide).

def Sundog.ClauseGadget.clauseCoverable (free : Fin 3 → Bool) : Prop

The clause gadget's internal pair s1_k, s2_k is coverable iff AT LEAST ONE of the three slots' tips is free. free k records whether the slot-k tip is free.

Equations

• Sundog.ClauseGadget.clauseCoverable free = ∃ (k : Fin 3), free k = true

@[implicit_reducible]

instance Sundog.ClauseGadget.instDecidableClauseCoverable (free : Fin 3 → Bool) : Decidable (clauseCoverable free)

clauseCoverable is an ∃ over Fin 3 of a decidable Prop; register the instance explicitly so decide fires at the def level (and for the downstream milestones 5–8).

Equations

• Sundog.ClauseGadget.instDecidableClauseCoverable free = Sundog.ClauseGadget.instDecidableClauseCoverable._aux_1 free

The polarity bridge (substantive — USES the VarWheel free-tip predicates).

`posTipFree`/`negTipFree` live under `variable {m : ℕ} [NeZero m]` in `VarWheel`, so the bridge
defs/theorems carry the same `{m} [NeZero m]` binders. 

theorem Sundog.ClauseGadget.posTipFree_const_iff (ai : Bool) {m : ℕ} [NeZero m] (j : Fin m) : VarWheel.posTipFree (fun (x : Fin m) => !ai) j ↔ ai = true

A positive tip under the constant wheel σ = fun _ => !ai is free iff ai = true.

theorem Sundog.ClauseGadget.negTipFree_const_iff (ai : Bool) {m : ℕ} [NeZero m] (j : Fin m) : VarWheel.negTipFree (fun (x : Fin m) => !ai) j ↔ ai = false

A negative tip under the constant wheel σ = fun _ => !ai is free iff ai = false.

def Sundog.ClauseGadget.litTipFree {n : ℕ} (a : SATNPHard.Assignment n) (l : SATNPHard.Literal n) {m : ℕ} (j : Fin m) : Prop

Whether the tip of literal l (under assignment a, on the variable's wheel j) is FREE: a positive literal looks at the positive tip, a negative literal at the negative tip — each under the constant state fun _ => !(a l.1) carrying xₗ.₁'s truth value.

Equations

• Sundog.ClauseGadget.litTipFree a l j = if l.2 = true then Sundog.VarWheel.posTipFree (fun (x : Fin m) => !a l.1) j else Sundog.VarWheel.negTipFree (fun (x : Fin m) => !a l.1) j

theorem Sundog.ClauseGadget.litTipFree_iff_eval {n : ℕ} (a : SATNPHard.Assignment n) (l : SATNPHard.Literal n) {m : ℕ} [NeZero m] (j : Fin m) : litTipFree a l j ↔ SATNPHard.evalLiteral a l = true

THE BRIDGE (discharges milestone 2's deferred labeling): the tip of literal l is free exactly when l evaluates to true. Case on the sign l.2; both sides split in lockstep on the same if l.2, the positive/negative tip branch matching the evalLiteral branch.

Clause local correctness (clean composition — near-definitional once the bridge is set).

theorem Sundog.ClauseGadget.clauseCoverable_iff_clauseSat {n : ℕ} (a : SATNPHard.Assignment n) (c : SATNPHard.Clause n) : (clauseCoverable fun (k : Fin 3) => SATNPHard.evalLiteral a (c k)) ↔ SATNPHard.clauseSat a c

A clause's internal pair is coverable (some slot-tip free) iff the clause is SATISFIED — both sides unfold to ∃ k, evalLiteral a (c k) = true.

Concrete decide-locks at the clause x₀ ∨ x₁ ∨ x₀ (SATNPHard.cSat).

These exercise `evalLiteral` + `clauseCoverable` together, validating the POLARITY convention
end-to-end by kernel `decide` — AXIOM-CLEAN (no `Lean.ofReduceBool`, no `native_decide`).
`![false, true]` makes `a 1 = true` ⟹ slot-1 literal `(1, true)` evaluates true ⟹ coverable;
`![false, false]` makes every literal false ⟹ NOT coverable. 

theorem Sundog.ClauseGadget.lockSat : clauseCoverable fun (k : Fin 3) => SATNPHard.evalLiteral ![false, true] (SATNPHard.cSat k)

SAT lock: a = ![false, true] covers the clause via the x₁ slot.

theorem Sundog.ClauseGadget.lockUnsat : ¬clauseCoverable fun (k : Fin 3) => SATNPHard.evalLiteral ![false, false] (SATNPHard.cSat k)

UNSAT lock: a = ![false, false] leaves every slot-tip consumed — not coverable.

Axiom audit.

Bridge iffs: `[propext]`.  `clauseCoverable_iff_clauseSat`: NO axioms (purely definitional).
Decide-locks: `[propext, Quot.sound]` — NO `sorryAx`, NO `Lean.ofReduceBool` (genuine kernel
`decide`, NOT `native_decide`).