3-SAT: prove monotonicity when clauses are removed
Open
complete
Using exactly the parent request’s dense clause-mask encoding, prove that removing clauses preserves satisfiability. The enabled clauses in mask1 are a subset of those in mask2; an assignment satisfying mask2 must satisfy mask1. This validates a basic invariant of the formal encoding before attempting circuit lower bounds.
Scope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.
Formal statement
(fun sat : Nat → (Nat → Bool) → Prop =>
∀ n : Nat, ∀ mask1 mask2 : Nat → Bool,
(∀ t : Nat, t < (2 * n) ^ 3 → mask1 t = true → mask2 t = true) →
sat n mask2 → sat n mask1)
(fun n mask => ∃ assignment : Nat → Bool,
∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →
mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →
(if i < n then assignment i else !(assignment (i - n))) = true ∨
(if j < n then assignment j else !(assignment (j - n))) = true ∨
(if k < n then assignment k else !(assignment (k - n))) = true)Lean core · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 8f16eed340160696283203b335995c6351fa22b4e4eb1c5903d48fa9c4e1a8f5
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.