Draft research: GF(2) boundary obstruction and controlled CDCL topology probes

.github/workflows/tests.yml

@@ -27,13 +27,14 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+          pip install -e ".[dev]"
 
       # Best-effort: install the external solvers so the @requires_kissat
       # integration tests run too. If a package is unavailable the tests skip
       # gracefully (shutil.which -> None), so this lane stays green either way.
       - name: Install SAT solvers (best effort)
-        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim cadical || true
-          pip install -e .[dev]
+        run: |
+          sudo apt-get update && sudo apt-get install -y kissat drat-trim cadical || true
 
       - name: Run test suite
         run: python -m pytest backend/tests/ -q
@@ -59,28 +60,14 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+          pip install -e ".[dev]"
 
-      # Mandatory, NOT best-effort: no "|| true". If these are unavailable the lane
-      # must fail rather than silently skip the certification it is guarding.
-      - name: Install Kissat + drat-trim (mandatory)
-        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim
-
-      - name: Assert the external tools are present
-        run: |
-          command -v kissat
-          command -v drat-trim
-
-      - name: Certification smoke (real DRAT UNSAT + model-replay SAT)
-        run: python .github/scripts/certification_smoke.py
-
-      - name: Certification-relevant tests must run (not skip)
-        run: python -m pytest backend/tests/test_integration.py backend/tests/test_kissat_wrapper.py -q
-          pip install -e .[dev]
-
-      - name: Build SAT/proof tools
+      # Mandatory, NOT best-effort: build from source because Ubuntu 24.04 does not
+      # provide Kissat or drat-trim packages.
+      - name: Install CaDiCaL and build Kissat + drat-trim (mandatory)
         run: |
           sudo apt-get update
-          sudo apt-get install -y build-essential git
+          sudo apt-get install -y build-essential git cadical
           git clone --depth 1 https://github.com/arminbiere/kissat.git /tmp/kissat
           cd /tmp/kissat
           ./configure
@@ -89,8 +76,18 @@ jobs:
           git clone --depth 1 https://github.com/marijnheule/drat-trim.git /tmp/drat-trim
           make -C /tmp/drat-trim -j2
           sudo cp /tmp/drat-trim/drat-trim /usr/local/bin/drat-trim
+
+      - name: Assert the external tools are present
+        run: |
           command -v kissat
           command -v drat-trim
+          command -v cadical
+
+      - name: Certification smoke (real DRAT UNSAT + model-replay SAT)
+        run: python .github/scripts/certification_smoke.py
+
+      - name: Certification-relevant tests must run (not skip)
+        run: python -m pytest backend/tests/test_integration.py backend/tests/test_kissat_wrapper.py -q
 
       - name: Run strict certification smoke tests
         run: |

.github/workflows/violation-geometry-lab.yml

@@ -0,0 +1,169 @@
+name: violation-geometry-lab
+
+on:
+  push:
+    branches: ["dev/kakeya-violation-frame"]
+  workflow_dispatch:
+  pull_request:
+    paths:
+      - "backend/violation_*.py"
+      - "backend/tests/test_violation_*.py"
+      - "docs/ladder/scripts/violation_*"
+      - "docs/ladder/*VIOLATION*"
+      - ".github/workflows/violation-geometry-lab.yml"
+
+permissions:
+  contents: read
+
+jobs:
+  finite-evidence:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Install bounded probe dependencies
+        run: python -m pip install "numpy>=1.24" "pytest>=7.4"
+      - name: Test mathematical invariants and observer isolation
+        run: |
+          python -m pytest -q \
+            backend/tests/test_violation_geometry.py \
+            backend/tests/test_violation_spectral_null.py \
+            backend/tests/test_violation_cross_instance.py \
+            backend/tests/test_violation_connection.py \
+            backend/tests/test_violation_orbit.py \
+            backend/tests/test_violation_laplacian.py \
+            backend/tests/test_violation_tseitin_boundary.py
+      - name: Reproduce assignment-held-out controls
+        run: |
+          mkdir -p evidence
+          python docs/ladder/scripts/violation_cross_instance_probe.py \
+            --seed-count 12 --replicates 2 --json > evidence/assignment_heldout.json
+      - name: Reproduce family-held-out signed-connection and orbit controls
+        run: |
+          python docs/ladder/scripts/violation_orbit_probe.py \
+            --seeds 12 --orbits 8 --null-swaps 32 --offsets 3 \
+            --json > evidence/orbit_connection.json
+          python docs/ladder/scripts/violation_orbit_probe.py \
+            --seeds 32 --orbits 8 --null-swaps 32 --offsets 10 \
+            --json > evidence/orbit_connection_192.json
+          python - <<'PY'
+          import json
+          import math
+          with open("evidence/assignment_heldout.json", encoding="utf-8") as f:
+              old = json.load(f)
+          assert old["instances_per_replicate"] == 72
+          assert len(old["families"]) == 6
+          with open("evidence/orbit_connection.json", encoding="utf-8") as f:
+              report = json.load(f)
+          assert report["total_formulas"] == 72
+          assert len(report["replicates"]) == 3
+          with open("evidence/orbit_connection_192.json", encoding="utf-8") as f:
+              large = json.load(f)
+          assert large["total_formulas"] == 192
+          assert len(large["replicates"]) == 10
+          assert 0 <= report["mean_fraction_nulls_with_switches"] <= 1
+          for target, predictors in report["averages"].items():
+              assert target in ("overall_raw_mae", "overall_orbit_mae")
+              for name, stats in predictors.items():
+                  assert math.isfinite(stats["mean_mae"]), name
+                  assert stats["mean_mae"] >= 0, name
+          print("Finite evidence and controls valid; no predictive-win condition imposed.")
+          PY
+      - name: Retain raw evidence including negative results
+        uses: actions/upload-artifact@v4
+        with:
+          name: violation-geometry-evidence
+          path: evidence/*.json
+          retention-days: 30
+
+
+  cdcl-topology:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Install bounded research-only CDCL instrument
+        run: |
+          python -m pip install "numpy>=1.24" "pytest>=7.4" "networkx>=3.1" "python-sat>=1.8.dev10"
+      - name: Verify genuinely distinct graphs and margin-preserving nulls
+        run: |
+          python -m pytest -q backend/tests/test_violation_cdcl_topology.py backend/tests/test_violation_cdcl_parity.py
+      - name: Run conflict-capped Glucose4 topology transfer pilot
+        run: |
+          mkdir -p evidence
+          python docs/ladder/scripts/violation_cdcl_topology_probe.py \
+            --seeds 3 --sizes 48 72 --orbits 2 --budget 2000 --swaps 64 --json \
+            > evidence/cdcl_topology.json
+          python - <<'PY'
+          import json, math
+          with open("evidence/cdcl_topology.json",encoding="utf-8") as fp:
+              payload=json.load(fp)
+          x=payload["report"]
+          assert x["total_formulas"] == 36
+          assert x["unique_labeled_formulas"] == 36
+          assert len(x["family_holdouts"]) == 6
+          assert 0 <= x["censored_call_fraction"] <= 1
+          assert 0 <= x["null_nontrivial_fraction"] <= 1
+          for rec in x["records"]:
+              assert len(rec["calls"]) == 2
+              assert rec["null_switches"] >= 0
+              for call in rec["calls"]:
+                  assert call["status"] in ("SAT","UNSAT","UNKNOWN")
+                  if call["status"]=="SAT":
+                      assert call["valid_sat_model"] is True
+                  else:
+                      assert call["valid_sat_model"] is None
+          for name,value in x["aggregate_family_mae"].items():
+              assert math.isfinite(value) and value >= 0,name
+          print("External CDCL pilot complete, all models independently replayed.")
+          print("Censored fraction:",x["censored_call_fraction"])
+          print("LOFO MAE:",x["aggregate_family_mae"])
+          PY
+      - name: Disjoint-seed confirmation instrument and post-pilot GF2 control
+        run: |
+          python docs/ladder/scripts/violation_cdcl_topology_probe.py \
+            --seeds 6 --seed-start 100 --sizes 48 72 96 \
+            --orbits 3 --budget 5000 --swaps 160 --json \
+            > evidence/cdcl_disjoint.json
+          python docs/ladder/scripts/violation_cdcl_parity_probe.py \
+            --seeds 6 --seed-start 100 --sizes 48 72 96 \
+            --orbits 3 --budget 5000 --swaps 160 --json \
+            > evidence/cdcl_parity_disjoint.json
+          python - <<'PY'
+          import json, math
+          with open("evidence/cdcl_disjoint.json",encoding="utf-8") as fp:
+              original=json.load(fp)["report"]
+          with open("evidence/cdcl_parity_disjoint.json",encoding="utf-8") as fp:
+              parity=json.load(fp)["report"]
+          assert original["total_formulas"]==108
+          assert original["unique_labeled_formulas"]==108
+          assert parity["formulas"]==108
+          assert parity["status_counts"]["SAT"]==18
+          assert parity["status_counts"]["UNSAT"]==18
+          assert parity["status_counts"]["INCONCLUSIVE"]==72
+          assert parity["match_error_count"]==0
+          ref={(r["family"],r["size"],r["seed"]):r for r in original["records"]}
+          for case in parity["cases"]:
+              key=case["family"],case["size"],case["seed"]
+              assert case["digest"]==ref[key]["digest"]
+              assert case["capped_log_conflicts"]==ref[key]["capped_log_conflicts"]
+              assert case["call_statuses"]==[c["status"] for c in ref[key]["calls"]]
+          for name,value in parity["aggregate_mae"].items():
+              assert math.isfinite(value) and value>=0,name
+          print("Disjoint-seed CDCL and GF2 gate samples independently cross-checked.")
+          print("disjoint coverage:",original["censored_call_fraction"])
+          print("disjoint baseline:",original["aggregate_family_mae"])
+          print("post-pilot GF2 controls:",parity["aggregate_mae"])
+          print("median GF2 ms:",parity["median_gf2_ms"])
+          PY
+      - name: Preserve CDCL evidence, including unsuccessful hypotheses
+        uses: actions/upload-artifact@v4
+        with:
+          name: violation-cdcl-topology-evidence
+          path: evidence/*.json
+          retention-days: 30

README.md

@@ -6,6 +6,8 @@
 
 Headless. No web UI. No *trust-me*.
 
+> **Experimental λSAT/ETH × Kakeya research branch:** the [initial violation-space hypothesis](docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md), [negative DPLL cross-family results](docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md), and [signed-orbit audit](docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md) remain visible. Our [Glucose4/GF(2) follow-up](docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md) holds out 108 new formulas: classical structural MAE 2.230, existing GF(2) rank/consistency MAE 1.312, and GF(2) plus signed connection MAE 1.262 (post-hoc exploratory; no routing speedup). The [constructive graph-boundary theorem and witness](docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md) explain the actual global XOR obstruction, distinct from the real signed Laplacian or Euclidean Kakeya. All experiments are isolated from certified solver decisions; the [CI evidence](.github/workflows/violation-geometry-lab.yml) retains raw JSON and negative controls. No production paths or asymptotic complexity claims change.
+
 A λ-logic middleware for Boolean satisfiability that **verifies every verdict it emits** —
 SAT by model replay, UNSAT by an independent DRAT proof or a sound algebraic frame. On top
 of the solver sits a research program on the *intrinsic shape of SAT hardness*: three sound

backend/tests/test_acaf.py

@@ -5,10 +5,13 @@
 to a cores-sized diversified portfolio. Every verdict certified and agreeing with truth.
 """
 
+import shutil
 import sys
 from itertools import combinations, product
 from pathlib import Path
 
+import pytest
+
 sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "docs/ladder/scripts"))
 
 from frame_benchmark import random_3sat, random_xorsat  # noqa: E402
@@ -19,6 +22,11 @@
 from backend.cnf_utils import CNFFormula  # noqa: E402
 from backend.eval.generators import pigeonhole  # noqa: E402
 
+requires_cdcl = pytest.mark.skipif(
+    not all(shutil.which(binary) for binary in ("kissat", "cadical", "drat-trim")),
+    reason="Kissat, CaDiCaL, and drat-trim are required for CDCL tests",
+)
+
 
 def _tseitin_k4():
     edges = list(combinations(range(4), 2))
@@ -116,11 +124,13 @@ def test_structured_goes_to_frame_stage(self):
             assert r.status == "UNSAT" and r.certified
             assert r.stage == "frame" and r.winner == frame and r.breadth == 0
 
+    @requires_cdcl
     def test_easy_tunnel_uses_a_single_arm_not_a_swarm(self):
         r = acaf_solve(random_3sat(140, round(4.26 * 140), 0), timeout_s=20)
         assert r.status in ("SAT", "UNSAT") and r.certified
         assert r.stage == "single" and r.breadth == 1        # no swarm overhead
 
+    @requires_cdcl
     def test_hard_tunnel_escalates_to_cores_sized_portfolio(self):
         import os
         r = acaf_solve(random_3sat(280, round(4.26 * 280), 0), timeout_s=30)

backend/tests/test_metametasolver.py

@@ -5,6 +5,7 @@
 matches ground truth; never leak losing processes; and never trust an unchecked arm.
 """
 
+import shutil
 import sys
 from itertools import combinations, product
 from pathlib import Path
@@ -21,6 +22,11 @@
     default_arms, metametasolve,
 )
 
+requires_cdcl = pytest.mark.skipif(
+    not all(shutil.which(binary) for binary in ("kissat", "cadical", "drat-trim")),
+    reason="Kissat, CaDiCaL, and drat-trim are required for CDCL tests",
+)
+
 
 def _tseitin_k4():
     edges = list(combinations(range(4), 2))
@@ -45,6 +51,7 @@ def test_structured_islands_decided_instantly_by_one_arm(self):
 
 
 class TestTunnelPortfolio:
+    @requires_cdcl
     def test_tunnel_decided_by_certified_cdcl_arm(self):
         f = random_3sat(120, round(4.26 * 120), 0)
         r = metametasolve(f, breadth=4, timeout_s=25)
@@ -53,12 +60,14 @@ def test_tunnel_decided_by_certified_cdcl_arm(self):
         assert r.winner.startswith(("kissat", "cadical"))
         assert r.arms >= 4                                  # the portfolio actually raced
 
+    @requires_cdcl
     def test_sat_winner_carries_a_verified_model(self):
         f = random_3sat(90, 300, 5)
         r = metametasolve(f, breadth=4, timeout_s=25)
         if r.status == "SAT":
             assert r.model is not None and verify_model(f, r.model)
 
+    @requires_cdcl
     def test_portfolio_agrees_with_ground_truth(self):
         # cross-check the portfolio verdict against a single certified solve
         from backend.metasolver import metasolve

backend/tests/test_metasolver.py

@@ -7,6 +7,7 @@
 CMS is exponential (the axis on which the metasolver beats it).
 """
 
+import shutil
 import sys
 from itertools import combinations, product
 from pathlib import Path
@@ -23,6 +24,11 @@
 from backend.eval.generators import pigeonhole  # noqa: E402
 from backend.metasolver import metasolve  # noqa: E402
 
+requires_cdcl = pytest.mark.skipif(
+    not all(shutil.which(binary) for binary in ("kissat", "drat-trim")),
+    reason="Kissat and drat-trim are required for CDCL tests",
+)
+
 
 def _tseitin_k4():
     edges = list(combinations(range(4), 2))
@@ -91,12 +97,14 @@ def test_counting_beats_cms_instantly(self):
         assert r.status == "UNSAT" and r.strategy == "counting" and r.certified
         assert r.seconds < 1.0
 
+    @requires_cdcl
     def test_tunnel_falls_to_certified_cdcl(self):
         r = metasolve(random_3sat(120, round(4.26 * 120), 0))
         assert r.status in ("SAT", "UNSAT")
         assert r.strategy in ("kissat", "cadical")
         assert r.certified                  # DRAT (UNSAT) or model replay (SAT)
 
+    @requires_cdcl
     def test_sat_verdicts_carry_verified_models(self):
         r = metasolve(random_3sat(40, 120, 3))
         if r.status == "SAT" and r.model is not None: