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

WHAT THIS FILE PROVIDES (the variable "wheel" / truth-setting gadget + its LOCAL CORRECTNESS): The Garey–Johnson truth-setting ring for a 3-CNF formula with m clauses. For each j : Fin m the gadget owns two INTERNAL nodes a j, b j (covered exactly once, living only here) and two TIP nodes posTip j, negTip j (shared later with the clause gadgets). The two cover triples are positive t_j = (posTip j, a j, b j) negative t⁻_j = (negTip j, a (j+1), b j) [index j+1 CYCLIC in Fin m]. Because b j lies ONLY in {t_j, t⁻_j}, any valid internal cover selects exactly one triple per j — i.e. is a Selection σ : Fin m → Bool (σ j = true picks t_j, false picks t⁻_j). Node a j is touched by t_j (iff σ j = true) and by t⁻_(j-1) (iff σ (j-1) = false); "a j covered exactly once" is the EXCLUSIVE-OR of those two facts.

THE ENGINE (`validCover_iff_const`): the ring has EXACTLY TWO valid internal covers — the
all-true and all-false selections — the two truth values of the variable.  We also expose,
per constant state, which tips are left FREE (raw, label-deferred): the true-state frees every
`negTip` and the false-state frees every `posTip`.

THE GADGET PICTURE (a ring; arrows are the two triples per spoke j, indices cyclic):

    a 0 ──t_0── b 0 ──t⁻_0── a 1 ──t_1── b 1 ──t⁻_1── a 2 ── … ── (wraps to a 0)
      posTip j attaches to t_j;  negTip j attaches to t⁻_j .

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 wheel's LOCAL correctness only. The clause gadget, the garbage-collection triples, and the global assembly onto Sundog.MatchingNPHard.ThreeDM (including the obligation that b j truly lies only in {t_j, t⁻_j}, which makes σ well-defined) are milestones 3–8.

Decidability of ValidCover is registered explicitly (it is a ∀ over Fin m of a decidable Prop, but does not auto-resolve through the def). This locks the two-cover claim at m = 3 by kernel decide — AXIOM-CLEAN (no Lean.ofReduceBool; we use decide, never native_decide).

@[reducible, inline]

abbrev Sundog.VarWheel.Selection (m : ℕ) : Type

A selection of one triple per spoke: σ j = true picks the positive triple t_j, σ j = false picks the negative triple t⁻_j.

Equations

• Sundog.VarWheel.Selection m = (Fin m → Bool)

def Sundog.VarWheel.aCoveredOnce {m : ℕ} [NeZero m] (σ : Selection m) (j : Fin m) : Prop

The internal node a j is covered EXACTLY ONCE: exactly one of σ j = true (the positive triple t_j touches a j) and σ (j-1) = false (the negative triple t⁻_(j-1) touches a j) holds.

Equations

• Sundog.VarWheel.aCoveredOnce σ j = Xor (σ j = true) (σ (j - 1) = false)

theorem Sundog.VarWheel.aCoveredOnce_iff {m : ℕ} [NeZero m] (σ : Selection m) (j : Fin m) : aCoveredOnce σ j ↔ σ j = σ (j - 1)

The covered-once exclusive-or collapses to the local agreement σ j = σ (j-1): xor a (¬b) = (a == b).

def Sundog.VarWheel.ValidCover {m : ℕ} [NeZero m] (σ : Selection m) : Prop

A valid internal cover: every internal node a j is covered exactly once.

Equations

• Sundog.VarWheel.ValidCover σ = ∀ (j : Fin m), Sundog.VarWheel.aCoveredOnce σ j

Decidability.

`aCoveredOnce` is decidable (it is an `Xor` of two decidable `Prop`s), but the `∀`-wrapper
`ValidCover` does not auto-resolve through the `def`; we register both instances explicitly so
`decide` fires at `m = 3` below. 

@[implicit_reducible]

instance Sundog.VarWheel.instDecidableACoveredOnce {m : ℕ} [NeZero m] (σ : Selection m) (j : Fin m) : Decidable (aCoveredOnce σ j)

Equations

• Sundog.VarWheel.instDecidableACoveredOnce σ j = Sundog.VarWheel.instDecidableACoveredOnce._aux_1 σ j

@[implicit_reducible]

instance Sundog.VarWheel.instDecidableValidCover {m : ℕ} [NeZero m] (σ : Selection m) : Decidable (ValidCover σ)

Equations

• Sundog.VarWheel.instDecidableValidCover σ = Sundog.VarWheel.instDecidableValidCover._aux_1 σ

The engine: local correctness.

The wheel has EXACTLY TWO valid internal covers, the all-true and all-false selections. 

theorem Sundog.VarWheel.validCover_iff_const {m : ℕ} [NeZero m] (_hm : 0 < m) (σ : Selection m) : ValidCover σ ↔ (σ = fun (x : Fin m) => true) ∨ σ = fun (x : Fin m) => false

The two-cover engine. A selection is a valid internal cover iff it is constant — the all-true or the all-false truth value. (The hm : 0 < m hypothesis is kept in the signature for the downstream assembly; the wheel itself runs on the [NeZero m] instance.)

Free-tip characterization (raw, per constant state).

Truth-value LABELING is deferred to milestone 3; here we record, per constant state, which
family of tips is left uncovered ("free") and thus available to the clause gadgets. 

def Sundog.VarWheel.posTipFree {m : ℕ} (σ : Selection m) (j : Fin m) : Prop

The positive tip posTip j is free in state σ iff its triple t_j was NOT selected.

Equations

• Sundog.VarWheel.posTipFree σ j = (σ j = false)

def Sundog.VarWheel.negTipFree {m : ℕ} (σ : Selection m) (j : Fin m) : Prop

The negative tip negTip j is free in state σ iff its triple t⁻_j was NOT selected.

Equations

• Sundog.VarWheel.negTipFree σ j = (σ j = true)

theorem Sundog.VarWheel.trueState_frees_neg {m : ℕ} (σ : Selection m) (h : σ = fun (x : Fin m) => true) : (∀ (j : Fin m), ¬posTipFree σ j) ∧ ∀ (j : Fin m), negTipFree σ j

The all-true (one truth value) state frees every negative tip and no positive tip.

theorem Sundog.VarWheel.falseState_frees_pos {m : ℕ} (σ : Selection m) (h : σ = fun (x : Fin m) => false) : (∀ (j : Fin m), posTipFree σ j) ∧ ∀ (j : Fin m), ¬negTipFree σ j

The all-false (other truth value) state frees every positive tip and no negative tip.

Concrete decide-lock at m = 3 (kernel decide, axiom-clean — NOT native_decide).

Mirrors `validCover_iff_const` at `m = 3`: the only two valid covers are the constants
`![true,true,true]` and `![false,false,false]`. 

Axiom audit.

Expect `[propext, Classical.choice, Quot.sound]` (or a subset) — NO `sorryAx`, and NO
`Lean.ofReduceBool` (the latter would signal a `native_decide`, which we deliberately avoid).