{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"8f16eed340160696283203b335995c6351fa22b4e4eb1c5903d48fa9c4e1a8f5","problem":{"id":18,"title":"3-SAT: prove monotonicity when clauses are removed","description":"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.\n\nScope: 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.","statement":"(fun sat : Nat → (Nat → Bool) → Prop =>\n ∀ n : Nat, ∀ mask1 mask2 : Nat → Bool,\n (∀ t : Nat, t < (2 * n) ^ 3 → mask1 t = true → mask2 t = true) →\n sat n mask2 → sat n mask1)\n(fun n mask => ∃ assignment : Nat → Bool,\n   ∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →\n     mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →\n       (if i < n then assignment i else !(assignment (i - n))) = true ∨\n       (if j < n then assignment j else !(assignment (j - n))) = true ∨\n       (if k < n then assignment k else !(assignment (k - n))) = true)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := ((fun sat : Nat → (Nat → Bool) → Prop =>\n ∀ n : Nat, ∀ mask1 mask2 : Nat → Bool,\n (∀ t : Nat, t < (2 * n) ^ 3 → mask1 t = true → mask2 t = true) →\n sat n mask2 → sat n mask1)\n(fun n mask => ∃ assignment : Nat → Bool,\n   ∀ i j k : Nat, i < 2 * n → j < 2 * n → k < 2 * n →\n     mask (i * (2 * n) ^ 2 + j * (2 * n) + k) = true →\n       (if i < n then assignment i else !(assignment (i - n))) = true ∨\n       (if j < n then assignment j else !(assignment (j - n))) = true ∨\n       (if k < n then assignment k else !(assignment (k - n))) = true))\n\n#check OA_statement\n","proof":null}