Documentation

LeanPool.Sundogcert.ThreeDMReindex

Sundogcert/ThreeDMReindex.lean — MILESTONE 5 of the 3SAT ≤ 3DM marathon: the GENERIC REINDEXING BRIDGE. (Lean 4 / mathlib v4.30.0.)

WHAT THIS FILE PROVIDES (pure index bookkeeping — NOT reduction correctness): * threeDMI t — perfect 3-dimensional matching stated over an ARBITRARY Fintype index I (a selection T : Finset I covering each W-, X-, and Y-element exactly once). This mirrors MatchingNPHard.ThreeDM verbatim, except the index is a clean Fintype rather than Fin s. * threeDM_reindex (THE BRIDGE) — threeDMI t ↔ ThreeDM (fun i => t (e.symm i)) with e := Fintype.equivFin I : I ≃ Fin (card I). This connects the natural-index matching to the real Fin s-indexed MatchingNPHard.ThreeDM (with s = Fintype.card I). The RHS triple-function is EXACTLY the shape SATReduction.reduce produces. * threeDM_reindex_comp — the point-free restatement threeDMI t ↔ ThreeDM (t ∘ e.symm), which reads cleanly when t = SATReduction.tripleFn φ in m8 (defeq to the above). * map_filter_card_eq — the load-bearing helper: pushing a Finset through an equiv-embedding and re-filtering by a transported predicate preserves the filtered cardinality. Generic over an ARBITRARY equiv e : J ≃ K and an arbitrary projection — one helper serves BOTH the forward direction (e := equivFin I) and the reverse (e := (equivFin I).symm).

WHY THIS EXISTS: the heavy forward/reverse gadget counting (milestones 6/7) is far cleaner over a structured Fintype index I = SATReduction.TripleIdx n m (a 4-way Sum) than over the opaque Fin (card I). This bridge lets that counting be done over I and then transported, for free, onto the Fin s-indexed MatchingNPHard.ThreeDM that the formalized hardness chain consumes.

THE STANDING LIMIT (named): this module is INDEX BOOKKEEPING ONLY. It proves that re-indexing a triple map along a finite equivalence does not change whether a perfect matching exists — a relabeling fact, nothing about the gadgets. The REDUCTION CORRECTNESS (Satisfiable φ ↔ threeDMI (tripleFn φ)) — that the wheel + clause + garbage triples actually enforce satisfiability — is milestones 6/7, and is NOT touched here.

Axiom-clean (decide/native_decide never used). Expect the standard classical trio.

The matching predicate over an arbitrary Fintype index. #

source
def Sundog.ThreeDMReindex.threeDMI {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {I : Type u_4} (t : I → W × X × Y) :
Prop

Perfect 3-dimensional matching over an arbitrary Fintype index I — a selection T : Finset I covering each W-element, each X-element, and each Y-element exactly once. Mirrors MatchingNPHard.ThreeDM exactly, but indexed by I rather than Fin s.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The load-bearing card-preservation helper (generic over an arbitrary equiv). #

    source
    theorem Sundog.ThreeDMReindex.map_filter_card_eq {W : Type u_1} {X : Type u_2} {Y : Type u_3} {J : Type u_5} {K : Type u_6} (e : J ≃ K) (T : Finset J) {Z : Type u_7} [DecidableEq Z] (proj : W × X × Y → Z) (t : J → W × X × Y) (z : Z) :
    {i ∈ Finset.map e.toEmbedding T | proj (t (e.symm i)) = z}.card = {a ∈ T | proj (t a) = z}.card

    Pushing a Finset through an equiv-embedding and re-filtering by the transported predicate preserves the filtered cardinality. Generic over an arbitrary equiv e : J ≃ K and an arbitrary projection proj — this one helper serves both the forward (e := equivFin I) and reverse (e := (equivFin I).symm) directions of threeDM_reindex.

    The reindexing bridge. #

    source
    theorem Sundog.ThreeDMReindex.threeDM_reindex {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {I : Type u_4} [Fintype I] (t : I → W × X × Y) :
    threeDMI t ↔ MatchingNPHard.ThreeDM fun (i : Fin (Fintype.card I)) => t ((Fintype.equivFin I).symm i)

    The reindexing bridge. A perfect matching over the arbitrary Fintype index I exists iff one exists for the Fin (card I)-reindexed triple map (along e := Fintype.equivFin I). This is the bridge from threeDMI to the real Fin s-indexed MatchingNPHard.ThreeDM.

    source
    theorem Sundog.ThreeDMReindex.threeDM_reindex_comp {W : Type u_1} {X : Type u_2} {Y : Type u_3} [DecidableEq W] [DecidableEq X] [DecidableEq Y] {I : Type u_4} [Fintype I] (t : I → W × X × Y) :
    threeDMI t ↔ MatchingNPHard.ThreeDM (t ∘ ⇑(Fintype.equivFin I).symm)

    Point-free restatement of the bridge: threeDMI t ↔ ThreeDM (t ∘ (equivFin I).symm). Defeq to threeDM_reindex; reads cleanly when t = SATReduction.tripleFn φ in m8.