IndisputableMonolith.Complexity.SAT.Completeness

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3import IndisputableMonolith.Complexity.SAT.XOR
   4import IndisputableMonolith.Complexity.SAT.Backprop
   5import IndisputableMonolith.Complexity.SAT.Isolation
   6import IndisputableMonolith.Complexity.SAT.SmallBias
   7import IndisputableMonolith.Complexity.SAT.PC
   8
   9namespace IndisputableMonolith
  10namespace Complexity
  11namespace SAT
  12
  13/-- Build a fully-determined backpropagation state from a total assignment. -/
  14def completeStateFrom {n} (x : Assignment n) : BPState n :=
  15  { assign := fun v => some (x v) }
  16
  17/-- The state built from a total assignment is complete. -/
  18lemma complete_completeStateFrom {n} (x : Assignment n) :
  19    complete (completeStateFrom x) := by
  20  intro v
  21  rfl
  22
  23/-- The state built from a satisfying assignment is consistent. -/
  24lemma consistent_completeStateFrom {n} (x : Assignment n) (φ : CNF n) (H : XORSystem n)
  25    (hxφ : evalCNF x φ = true) (hxH : satisfiesSystem x H) :
  26    consistent (completeStateFrom x) φ H := by
  27  refine ⟨x, ?eqall, hxφ, hxH⟩
  28  intro v; rfl
  29
  30/-!
  31# Propagation Completeness for Geometrically Isolated SAT Instances
  32
  33This module defines the key theorems connecting geometric isolation to backward
  34propagation completeness. The main claim (Theorem 5 in the paper) is that for
  35every satisfiable 3-CNF φ, the isolating H ∈ 𝓗_geo(n) produces an instance
  36φ ∧ H where XOR-augmented propagation determines all variables.
  37
  38## Structure
  39
  401. `IsolationInvariant`: Structural conditions promised by geometric isolation
  412. `PropagationReachability`: Every variable is reachable by propagation chains
  423. `BackpropCompleteUnderInvariant`: Main implication
  434. `ProgramTarget`: Full end-to-end specification
  44
  45## Critical Claim Status
  46
  47The propagation-enablement theorem (Theorem 5) is the key claim requiring
  48verification. The proof strategy relies on:
  49- Linear masks target every variable via single-variable constraints H_{a,n,j}
  50- XOR cascade: determined variables unlock others via parity relations
  51- Clause cascade: known values simplify clauses, forcing more variables
  52- Termination: geometric structure ensures no stalls
  53
  54Formal verification is in progress via Tracks A and B.
  55-/
  56
  57/-- Propagation graph: variable v₁ → v₂ if determining v₁ can force v₂. -/
  58structure PropagationGraph (n : Nat) where
  59  edges : Var n → Var n → Prop
  60
  61/-- A variable is reachable from initial units in the propagation graph.
  62    Defined inductively to ensure termination. -/
  63inductive Reachable {n} (G : PropagationGraph n) (init : Set (Var n)) : Var n → Prop
  64  | base : ∀ v, v ∈ init → Reachable G init v
  65  | step : ∀ u v, Reachable G init u → G.edges u v → Reachable G init v
  66
  67/-- All variables are reachable from initial units. -/
  68def AllReachable {n} (G : PropagationGraph n) (init : Set (Var n)) : Prop :=
  69  ∀ v, Reachable G init v
  70
  71/-- Structural invariant promised by the isolation construction (Track A).
  72
  73This captures the combinatorial conditions that geometric isolation guarantees:
  741. `hasUnits`: Some variables have unit constraints from H (direct determination)
  752. `connected`: The propagation graph reaches all variables from units
  763. `noStalls`: No stall configurations exist (propagation always has progress)
  77
  78**WARNING (2026-04-07)**: The `noStalls` field is UNSATISFIABLE for Tseitin formulas
  79on expander graphs (and many other hard formula families). At the initial empty
  80state, no clause is unit and no XOR constraint has a single unknown, so BPStep
  81cannot fire. This makes `IsolationInvariant` uninhabitable for such formulas. -/
  82structure IsolationInvariant (n : Nat) (φ : CNF n) (H : XORSystem n) : Prop where
  83  /-- At least one variable has a unit (single-variable) XOR constraint. -/
  84  hasUnits : ∃ v : Var n, ∃ p : Bool, [{ vars := [v], parity := p }] ⊆ H
  85  /-- The propagation graph constructed from φ ∧ H is connected. -/
  86  connected : ∃ G : PropagationGraph n, ∃ init : Set (Var n), AllReachable G init
  87  /-- No stall configurations: if unknowns remain, some rule applies. -/
  88  noStalls : ∀ s : BPState n, ¬complete s → ∃ s', BPStep φ H s s' ∧ s ≠ s'
  89
  90/-- Backprop completeness under the isolation invariant (Track B target). -/
  91def BackpropCompleteUnderInvariant {n} (φ : CNF n) (H : XORSystem n) : Prop :=
  92  IsolationInvariant n φ H → BackpropSucceeds φ H
  93
  94/-- **PROVED**: Determined values match the unique solution.
  95
  96**Proof**: Pick x to be the unique solution (from `huniq`).
  97Then if all determined values in s match x, the premise `s.assign v = some (x v)`
  98combined with `hdetermined : s.assign v = some b` gives `b = x v`.
  99
 100**Status**: PROVED (formerly axiom) -/
 101theorem determined_values_correct {n} (φ : CNF n) (H : XORSystem n)
 102    (huniq : UniqueSolutionXOR { φ := φ, H := H })
 103    (s : BPState n) (v : Var n) (b : Bool)
 104    (hdetermined : s.assign v = some b) :
 105    ∃ x : Assignment n, (∀ v', s.assign v' = some (x v')) →
 106      evalCNF x φ = true ∧ satisfiesSystem x H ∧ x v = b := by
 107  -- UniqueSolutionXOR means ∃! a, evalCNF a φ = true ∧ satisfiesSystem a H
 108  unfold UniqueSolutionXOR at huniq
 109  -- Get the unique solution
 110  obtain ⟨x, ⟨hx_sat_φ, hx_sat_H⟩, _⟩ := huniq
 111  -- Use x as our witness
 112  use x
 113  intro h_all_match
 114  -- From h_all_match at v: s.assign v = some (x v)
 115  -- Combined with hdetermined: s.assign v = some b
 116  -- We get: b = x v
 117  have hv_match := h_all_match v
 118  rw [hdetermined] at hv_match
 119  simp only [Option.some.injEq] at hv_match
 120  exact ⟨hx_sat_φ, hx_sat_H, hv_match.symm⟩
 121
 122/-- **FALSIFIED HYPOTHESIS**: Geometric propagation theorem.
 123
 124    Original claim: geometric isolation enables propagation completeness.
 125
 126    **FALSIFICATION (2026-04-07):**
 127    The `IsolationInvariant.noStalls` condition requires that BPStep (unit
 128    propagation + XOR inference) never stalls on any incomplete state.
 129    This is provably false:
 130
 131    Counterexample — Tseitin formulas on expander graphs:
 132    • At the initial empty state, every 3-clause has 3 unknown literals → no unit clause.
 133    • XOR constraints span many variables → no single-unknown XOR constraint.
 134    • BPStep cannot fire, yet the state is incomplete → noStalls is violated.
 135    • Ben-Sasson & Wigderson (2001) proved expander-Tseitin formulas require
 136      exponential-length resolution proofs; no local propagation suffices.
 137
 138    Additionally, SAT has no intrinsic geometric structure — variables can be
 139    permuted arbitrarily — so Morton ordering provides zero structural advantage.
 140
 141    **STATUS**: FALSIFIED — `IsolationInvariant.noStalls` is unsatisfiable for
 142    expander-based formulas regardless of XOR system choice. -/
 143def geometric_isolation_enables_propagation_hypothesis {n} (φ : CNF n) (H : XORSystem n) : Prop :=
 144  Satisfiable φ → isolates φ H → H ∈ linearFamily n → IsolationInvariant n φ H
 145
 146theorem geometric_isolation_enables_propagation_thm {n} (φ : CNF n) (hsat : Satisfiable φ)
 147    (H : XORSystem n) (hiso : isolates φ H) (hgeo : H ∈ linearFamily n)
 148    (h : geometric_isolation_enables_propagation_hypothesis (n:=n) φ H) :
 149    IsolationInvariant n φ H :=
 150  h hsat hiso hgeo
 151
 152/-- **FALSIFIED HYPOTHESIS**: Polynomial-time 3-SAT algorithm.
 153
 154    Original claim: a polynomial-time algorithm for 3-SAT exists, combining
 155    geometric isolation, propagation enablement, and polynomial-size family
 156    construction to solve 3-SAT in O(n^{11/3} log n) time.
 157
 158    **FALSIFICATION (2026-04-07):**
 159    This hypothesis depends on three links, all of which fail:
 160
 161    1. **Deterministic isolation fails**: Derandomizing Valiant-Vazirani to a
 162       polynomial-size deterministic family would itself be a major complexity
 163       breakthrough (implying NP ⊆ P/poly). The `geoFamily` provides no
 164       advantage because SAT has no intrinsic geometric structure.
 165
 166    2. **Propagation completeness is provably false**: See the falsification
 167       of `geometric_isolation_enables_propagation_hypothesis` above.
 168       Expander-Tseitin formulas stall BPStep at the initial empty state.
 169
 170    3. **The BWD3 alternative route is circular**: `complete_forces_all_sat`
 171       in `BWD3LogEncoding.lean` proves that the base admissibility filter
 172       makes every formula appear satisfiable (including unsatisfiable ones).
 173
 174    4. **Oracle separation barrier**: This claim relativizes (works identically
 175       with any oracle). Baker-Gill-Solovay (1975) proved P ≠ NP relative to
 176       some oracles. Therefore no relativizing argument can prove P = NP.
 177
 178    **STATUS**: FALSIFIED — depends on at least three independently falsified premises. -/
 179def polynomial_time_3sat_algorithm_hypothesis (n : Nat) : Prop :=
 180  ProgramTarget n →
 181  ∃ (alg : CNF n → Option (Assignment n)),
 182    (∀ φ, Satisfiable φ → ∃ x, alg φ = some x ∧ evalCNF x φ = true) ∧
 183    (∀ φ, ¬Satisfiable φ → alg φ = none)
 184
 185theorem polynomial_time_3sat_algorithm (n : Nat)
 186    (h : polynomial_time_3sat_algorithm_hypothesis n) :
 187    ProgramTarget n →
 188    ∃ (alg : CNF n → Option (Assignment n)),
 189      (∀ φ, Satisfiable φ → ∃ x, alg φ = some x ∧ evalCNF x φ = true) ∧
 190      (∀ φ, ¬Satisfiable φ → alg φ = none) :=
 191  h
 192
 193/-- Backpropagation succeeds when there is a unique solution under XOR constraints.
 194This is a semantic existence result that does not rely on a specific step system. -/
 195theorem backprop_succeeds_of_unique {n} (φ : CNF n) (H : XORSystem n)
 196    (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
 197    BackpropSucceeds φ H := by
 198  intro s0
 199  rcases huniq with ⟨x, hx, _uniq⟩
 200  refine ⟨completeStateFrom x, ?hcomp, ?hcons⟩
 201  · exact complete_completeStateFrom x
 202  · rcases hx with ⟨hxφ, hxH⟩
 203    exact consistent_completeStateFrom x φ H hxφ hxH
 204
 205/-- PC ⇒ backpropagation succeeds (via uniqueness).
 206Note: with the current abstract step semantics, uniqueness alone suffices for success.
 207PC becomes relevant once a concrete BPStep is connected to semantic forcing. -/
 208theorem backprop_succeeds_from_PC {n}
 209    (inputs : Finset (Var n)) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n)
 210    (_hpc : PC inputs aRef φ H)
 211    (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
 212    BackpropSucceeds φ H :=
 213  backprop_succeeds_of_unique φ H huniq
 214
 215end SAT
 216end Complexity
 217end IndisputableMonolith
 218