From 79c01d191209ff32be11625c64c47bcd18de25d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:39:00 +0100 Subject: [PATCH 01/48] research: add bounded violation parity and Kakeya-style incidence diagnostics --- backend/violation_geometry.py | 312 ++++++++++++++++++++++++++++++++++ 1 file changed, 312 insertions(+) create mode 100644 backend/violation_geometry.py diff --git a/backend/violation_geometry.py b/backend/violation_geometry.py new file mode 100644 index 0000000..d866458 --- /dev/null +++ b/backend/violation_geometry.py @@ -0,0 +1,312 @@ +"""Finite, experimental ETH x Kakeya incidence probe for CNF formulas. + +The clauses define a violation map v : {0,1}^n -> {0,1}^m. +Every CNF model has v=0 and therefore passes every homogeneous parity +check =0 over GF(2). A set of parity rows is an *over-approximation* +of the original model set unless its kernel has no realizable nonzero +violation vector. In particular, passing the checks is NEVER a SAT proof. + +The Kakeya-inspired incidence sets below are *finite subsets of Boolean +assignments*, not Euclidean tubes. Their Gram spectrum is a diagnostic, +not a transfer of a Kakeya maximal inequality, complexity bound or proof. +All audits enumerate assignments and are bounded by MAX_ENUM_VARS. +""" +from __future__ import annotations + +from collections import Counter +from dataclasses import dataclass +from itertools import chain, combinations +from math import sqrt +from random import Random +from typing import Sequence + +from .cnf_utils import CNFFormula + +MAX_ENUM_VARS = 12 +MAX_CLAUSES = 128 + + +def _check_formula(formula: CNFFormula, max_vars: int) -> None: + if not 0 <= max_vars <= MAX_ENUM_VARS: + raise ValueError(f"max_vars must be between 0 and {MAX_ENUM_VARS}") + if not isinstance(formula.num_vars, int) or not 0 <= formula.num_vars <= max_vars: + raise ValueError("formula exceeds explicit assignment-enumeration budget") + if len(formula.clauses) > MAX_CLAUSES: + raise ValueError("formula exceeds clause budget") + for clause in formula.clauses: + for literal in clause: + if (not isinstance(literal, int) or isinstance(literal, bool) + or literal == 0 or abs(literal) > formula.num_vars): + raise ValueError(f"invalid literal in CNF: {literal!r}") + + +def violation_masks(formula: CNFFormula, *, max_vars: int = 10) -> tuple[int, ...]: + """Enumerate v_F(x), with assignment bit i encoding variable i+1. + + Bit j of the returned mask is 1 iff clause j is violated. A zero mask + identifies a model. Declared but unused variables are still enumerated. + """ + _check_formula(formula, max_vars) + masks = [] + for assignment in range(1 << formula.num_vars): + v = 0 + for i, clause in enumerate(formula.clauses): + if not any(bool(assignment & (1 << (abs(lit) - 1))) == (lit > 0) + for lit in clause): + v |= 1 << i + masks.append(v) + return tuple(masks) + + +def _check_rows(rows: Sequence[int], clause_count: int) -> None: + if not 0 <= clause_count <= MAX_CLAUSES: + raise ValueError("invalid clause count") + for row in rows: + if not isinstance(row, int) or isinstance(row, bool) or not 0 < row < (1 << clause_count): + raise ValueError(f"invalid parity row: {row!r}") + + +def parity_accepts(violation: int, row: int) -> bool: + """Does the homogeneous GF(2) check = 0 hold?""" + if violation < 0 or row < 0: + raise ValueError("bitmasks must be nonnegative") + return ((violation & row).bit_count() & 1) == 0 + + +@dataclass(frozen=True) +class HashAudit: + models: int + spurious: int + + @property + def survivors(self) -> int: + return self.models + self.spurious + + @property + def equivalent_on_enumerated_domain(self) -> bool: + return self.spurious == 0 + + +def audit_hash(masks: Sequence[int], rows: Sequence[int], clause_count: int) -> HashAudit: + """Exact finite audit, not a scalable verifier or a SAT certificate.""" + _check_rows(rows, clause_count) + if any(mask < 0 or mask >= (1 << clause_count) for mask in masks): + raise ValueError("violation mask out of clause domain") + models = sum(v == 0 for v in masks) + spurious = sum(v != 0 and all(parity_accepts(v, row) for row in rows) + for v in masks) + return HashAudit(models, spurious) + + +def _candidate_rows(clause_count: int, max_weight: int, + budget: int, seed: int) -> tuple[int, ...]: + """Include every singleton then reservoir-sample pairs/triples. + + This is a deliberately finite candidate search, NOT the expander-code / + deterministic exact-counting construction of the ETH manuscript. + """ + if not 0 <= clause_count <= MAX_CLAUSES: + raise ValueError("invalid clause count") + if budget < clause_count or budget > 8192: + raise ValueError("candidate budget must be within [clause_count, 8192]") + if max_weight < 1 or max_weight > 3: + raise ValueError("max_weight must be in [1, 3]") + singles = [1 << j for j in range(clause_count)] + capacity = budget - len(singles) + rng = Random(seed) + sampled: list[int] = [] + if capacity > 0: + combos = chain.from_iterable(combinations(range(clause_count), weight) + for weight in range(2, min(max_weight, clause_count) + 1)) + for index, combo in enumerate(combos): + row = sum(1 << j for j in combo) + if index < capacity: + sampled.append(row) + else: + slot = rng.randrange(index + 1) + if slot < capacity: + sampled[slot] = row + return tuple(sorted(singles + sampled, key=lambda row: (row.bit_count(), row))) + + +def greedy_violation_rows(training_masks: Sequence[int], clause_count: int, *, + max_rows: int = 8, max_weight: int = 3, + candidate_budget: int = 512, + candidate_seed: int = 0) -> tuple[int, ...]: + """Greedily reject observed nonzero violation masks, weighted by frequency. + + This is a supervised small-n *diagnostic*. Since it sees training assignments, + it must not be presented as a cheap dispatch feature or proof of an asymptotic + improvement. Rows are a relaxation on out-of-sample assignments. + """ + if not 0 <= clause_count <= MAX_CLAUSES: + raise ValueError("invalid clause count") + if not 0 <= max_rows <= 32: + raise ValueError("max_rows must be in [0, 32]") + if any(mask < 0 or mask >= (1 << clause_count) for mask in training_masks): + raise ValueError("violation mask out of clause domain") + candidates = _candidate_rows(clause_count, max_weight, candidate_budget, + candidate_seed) + remaining = Counter(v for v in training_masks if v) + selected: list[int] = [] + for _ in range(max_rows): + if not remaining: + break + winner = 0 + best_gain = 0 + for row in candidates: + if row in selected: + continue + gain = sum(count for v, count in remaining.items() + if not parity_accepts(v, row)) + if gain > best_gain: + winner, best_gain = row, gain + if not winner: + break + selected.append(winner) + remaining = Counter({v: count for v, count in remaining.items() + if parity_accepts(v, winner)}) + return tuple(selected) + + +def matched_random_rows(rows: Sequence[int], clause_count: int, seed: int) -> tuple[int, ...]: + """Null control: same number of checks and identical row-weight sequence.""" + _check_rows(rows, clause_count) + rng = Random(seed) + return tuple(sum(1 << j for j in rng.sample(range(clause_count), row.bit_count())) + for row in rows) + + +@dataclass(frozen=True) +class IncidenceOverlap: + active_rows: int + top_gram_eigenvalue: float + mean_pairwise_cosine: float + maximum_multiplicity: int + + +def _top_eigenvalue(gram: list[list[float]]) -> float: + """Power iteration for a symmetric, entrywise nonnegative Gram matrix.""" + n = len(gram) + if n == 0: + return 0.0 + v = [1.0 / sqrt(n)] * n + last = 0.0 + for _ in range(300): + w = [sum(gram[i][j] * v[j] for j in range(n)) for i in range(n)] + norm = sqrt(sum(x * x for x in w)) + if norm == 0: + return 0.0 + v = [x / norm for x in w] + eig = sum(v[i] * sum(gram[i][j] * v[j] for j in range(n)) + for i in range(n)) + if abs(eig - last) < 1e-12: + return eig + last = eig + return last + + +def incidence_overlap(masks: Sequence[int], rows: Sequence[int], + clause_count: int) -> IncidenceOverlap: + """Normalized Gram spectrum of parity-check pass sets on NON-models only. + + T_row = {x: v_F(x) != 0 and = 0}. Columns are finite + assignment states, not Euclidean tubes. G[i,j] = |Ti intersect Tj| / + sqrt(|Ti| |Tj|). This does not inherit any Kakeya inequality. + """ + _check_rows(rows, clause_count) + if len(rows) > 64: + raise ValueError("incidence overlap supports at most 64 rows") + if any(v < 0 or v >= (1 << clause_count) for v in masks): + raise ValueError("violation mask out of clause domain") + sets = [frozenset(i for i, v in enumerate(masks) + if v and parity_accepts(v, row)) for row in rows] + active = [s for s in sets if s] + k = len(active) + if k == 0: + return IncidenceOverlap(0, 0.0, 0.0, 0) + gram = [[len(active[i] & active[j]) / sqrt(len(active[i]) * len(active[j])) + for j in range(k)] for i in range(k)] + cosines = [gram[i][j] for i in range(k) for j in range(i + 1, k)] + nonmodels = [i for i, v in enumerate(masks) if v] + maximum = max((sum(i in s for s in active) for i in nonmodels), default=0) + return IncidenceOverlap(k, _top_eigenvalue(gram), + sum(cosines) / len(cosines) if cosines else 0.0, + maximum) + + +@dataclass(frozen=True) +class MatchedControl: + seed: int + rows: tuple[int, ...] + heldout_spurious: int + overlap: IncidenceOverlap + + +@dataclass(frozen=True) +class BridgeReport: + variables: int + clauses: int + states: int + models: int + training_states: int + heldout_states: int + chosen_rows: tuple[int, ...] + singleton_baseline_rows: tuple[int, ...] + singleton_heldout_spurious: int + singleton_overlap: IncidenceOverlap + training_spurious: int + heldout_spurious: int + exact_audit: HashAudit + overlap: IncidenceOverlap + controls: tuple[MatchedControl, ...] + + +def run_bridge_experiment(formula: CNFFormula, *, max_vars: int = 10, + split_seed: int = 41, candidate_seed: int = 19, + max_rows: int = 8, max_weight: int = 3, + candidate_budget: int = 512, + control_seeds: Sequence[int] = (13, 29, 47, 71)) -> BridgeReport: + """Train/holdout pilot with matched check-weight nulls; no solver verdicts. + + The full audit is only a finite-n consistency oracle; the heldout count + measures generalization of a row set fitted on a different assignment set. + """ + if len(control_seeds) > 64: + raise ValueError("too many matched controls") + masks = violation_masks(formula, max_vars=max_vars) + indices = list(range(len(masks))) + Random(split_seed).shuffle(indices) + train_n = min(len(indices), max(1, (2 * len(indices)) // 3)) + if len(indices) > 1: + train_n = min(train_n, len(indices) - 1) + training = tuple(masks[i] for i in indices[:train_n]) + heldout = tuple(masks[i] for i in indices[train_n:]) + chosen = greedy_violation_rows(training, len(formula.clauses), + max_rows=max_rows, max_weight=max_weight, + candidate_budget=candidate_budget, + candidate_seed=candidate_seed) + singleton = greedy_violation_rows(training, len(formula.clauses), + max_rows=len(chosen), max_weight=1, + candidate_budget=max(1, len(formula.clauses))) + controls = [] + for seed in control_seeds: + random_rows = matched_random_rows(chosen, len(formula.clauses), seed) + controls.append(MatchedControl(seed, random_rows, + audit_hash(heldout, random_rows, len(formula.clauses)).spurious, + incidence_overlap(masks, random_rows, len(formula.clauses)))) + whole = audit_hash(masks, chosen, len(formula.clauses)) + return BridgeReport( + variables=formula.num_vars, clauses=len(formula.clauses), + states=len(masks), models=whole.models, + training_states=len(training), heldout_states=len(heldout), + chosen_rows=chosen, + singleton_baseline_rows=singleton, + singleton_heldout_spurious=audit_hash(heldout, singleton, len(formula.clauses)).spurious, + singleton_overlap=incidence_overlap(masks, singleton, len(formula.clauses)), + training_spurious=audit_hash(training, chosen, len(formula.clauses)).spurious, + heldout_spurious=audit_hash(heldout, chosen, len(formula.clauses)).spurious, + exact_audit=whole, + overlap=incidence_overlap(masks, chosen, len(formula.clauses)), + controls=tuple(controls), + ) From 7dba4da644a37e072359dba184206cffacb41235 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:39:12 +0100 Subject: [PATCH 02/48] test: verify finite violation, overlap and matched control contracts --- backend/tests/test_violation_geometry.py | 111 +++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 backend/tests/test_violation_geometry.py diff --git a/backend/tests/test_violation_geometry.py b/backend/tests/test_violation_geometry.py new file mode 100644 index 0000000..5030f0f --- /dev/null +++ b/backend/tests/test_violation_geometry.py @@ -0,0 +1,111 @@ +"""Finite ETH x Kakeya probe invariants (no SAT verdicts).""" +import math +import random +import pytest +from backend.cnf_utils import CNFFormula +from backend.violation_geometry import ( + audit_hash, greedy_violation_rows, incidence_overlap, matched_random_rows, + parity_accepts, run_bridge_experiment, violation_masks) + + +def direct_satisfies(formula, assignment): + return all(any(bool(assignment & (1 << (abs(lit)-1))) == (lit > 0) + for lit in clause) for clause in formula.clauses) + + +def test_violation_masks_match_direct_cnf_semantics(): + for formula in [CNFFormula(0, []), CNFFormula(0, [[]]), + CNFFormula(2, []), CNFFormula(2, [[1,2],[-1,-2]]), + CNFFormula(3, [[1,-2], [2,3], [-1], [1,-1], []])]: + masks = violation_masks(formula) + assert len(masks) == 2**formula.num_vars + assert [v == 0 for v in masks] == [ + direct_satisfies(formula, x) for x in range(2**formula.num_vars)] + + +def test_parity_relaxation_never_eliminates_a_real_model(): + rng = random.Random(20261029) + for _ in range(70): + n, m = rng.randrange(1,6), rng.randrange(1,12) + clauses = [[rng.choice((-1,1))*rng.randint(1,n) + for _ in range(rng.randint(0,4))] for _ in range(m)] + f = CNFFormula(n, clauses) + masks = violation_masks(f) + rows = tuple(rng.randint(1,(1<= a.models + assert all(all(parity_accepts(v,r) for r in rows) for v in masks if v==0) + + +def test_relaxation_is_not_a_sat_certificate(): + masks = violation_masks(CNFFormula(1, [[1],[-1]])) + weak = audit_hash(masks, [1], 2) + assert (weak.models,weak.spurious) == (0,1) + assert not weak.equivalent_on_enumerated_domain + strong = audit_hash(masks, [3], 2) + assert (strong.models,strong.spurious)==(0,0) + + +def test_greedy_searches_clause_violation_space(): + masks = violation_masks(CNFFormula(1, [[1],[-1]])) + rows = greedy_violation_rows(masks,2,max_rows=1,max_weight=2) + assert rows==(3,) + assert audit_hash(masks, rows, 2).spurious==0 + + +def test_holdout_and_controls_accounted(): + f=CNFFormula(3, [[1,2],[-1,3],[-2,-3],[1,-3]]) + r=run_bridge_experiment(f,max_rows=2) + assert r.states==8 + assert r.training_states+r.heldout_states==8 + assert r.models==sum(v==0 for v in violation_masks(f)) + assert r.training_spurious+r.heldout_spurious==r.exact_audit.spurious + assert len(r.controls)==4 + assert len(r.singleton_baseline_rows)<=len(r.chosen_rows) + for c in r.controls: + assert sorted(row.bit_count() for row in c.rows)==sorted(row.bit_count() for row in r.chosen_rows) + + +def test_incidence_has_known_spectra(): + masks=violation_masks(CNFFormula(1, [[1],[-1]])) + identical=incidence_overlap(masks,(1,1),2) + assert identical.active_rows==2 + assert math.isclose(identical.top_gram_eigenvalue,2) + assert math.isclose(identical.mean_pairwise_cosine,1) + assert identical.maximum_multiplicity==2 + disjoint=incidence_overlap(masks,(1,2),2) + assert math.isclose(disjoint.top_gram_eigenvalue,1) + assert math.isclose(disjoint.mean_pairwise_cosine,0) + assert disjoint.maximum_multiplicity==1 + empty=incidence_overlap(violation_masks(CNFFormula(2,[])),(),0) + assert empty.top_gram_eigenvalue==0 + + +def test_spurious_nonincreasing_with_more_rows(): + f=CNFFormula(4,[[1,-2],[-1,2],[3,4],[-3,-4],[1,3]]) + masks=violation_masks(f) + counts=[audit_hash(masks,greedy_violation_rows(masks,5,max_rows=k),5).spurious for k in range(5)] + assert counts==sorted(counts,reverse=True) + + +def test_declared_unused_variables_remain_counted(): + f=CNFFormula(3,[[1]]) + assert sum(v==0 for v in violation_masks(f))==4 + assert run_bridge_experiment(f).models==4 + + +def test_matched_null_deterministic(): + rows=(0b11,0b111,0b101) + r=matched_random_rows(rows,8,77) + assert r==matched_random_rows(rows,8,77) + assert [v.bit_count() for v in r]==[v.bit_count() for v in rows] + + +def test_resource_limits_and_invalid_inputs(): + with pytest.raises(ValueError): violation_masks(CNFFormula(13,[]),max_vars=12) + with pytest.raises(ValueError): violation_masks(CNFFormula(1,[[0]])) + with pytest.raises(ValueError): violation_masks(CNFFormula(1,[[2]])) + with pytest.raises(ValueError): greedy_violation_rows((1,),3,candidate_budget=2) + with pytest.raises(ValueError): audit_hash((1,),(8,),3) + with pytest.raises(ValueError): incidence_overlap((8,),(1,),3) From 8ae7e6b0ff50e562f6149b5e9e0ffe10dac63a48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:39:21 +0100 Subject: [PATCH 03/48] experiment: add reproducible five-family parity incidence probe --- .../scripts/violation_geometry_probe.py | 88 +++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 docs/ladder/scripts/violation_geometry_probe.py diff --git a/docs/ladder/scripts/violation_geometry_probe.py b/docs/ladder/scripts/violation_geometry_probe.py new file mode 100644 index 0000000..6ea8849 --- /dev/null +++ b/docs/ladder/scripts/violation_geometry_probe.py @@ -0,0 +1,88 @@ +"""Reproducible bounded ETH x Kakeya violation-geometry pilot. + +Run: python docs/ladder/scripts/violation_geometry_probe.py [--json] +""" +from __future__ import annotations +import argparse +import json +import random +import sys +from dataclasses import asdict +from itertools import combinations, product +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parents[3])) +from backend.cnf_utils import CNFFormula +from backend.violation_geometry import run_bridge_experiment + + +def xor_cnf(variables, rhs): + return [[-v if bit else v for v,bit in zip(variables,bits)] + for bits in product((0,1), repeat=len(variables)) + if sum(bits)%2 != rhs] + + +def corpus(): + edges=list(combinations(range(4),2)) + ids={edge:j+1 for j,edge in enumerate(edges)} + k4=[] + for vertex in range(4): + inc=tuple(ids[e] for e in edges if vertex in e) + k4+=xor_cnf(inc,1 if vertex==0 else 0) + pigeons,holes=4,3 + var=lambda p,h:p*holes+h+1 + php=[[var(p,h) for h in range(holes)] for p in range(pigeons)] + for p,q in combinations(range(pigeons),2): + for h in range(holes): + php.append([-var(p,h),-var(q,h)]) + def rand3(planted): + rng=random.Random(92) + clauses=[] + for _ in range(34): + vs=rng.sample(range(1,9),3) + ss=[rng.choice((-1,1)) for _ in vs] + if planted and all(s==-1 for s in ss): + ss[0]=1 + clauses.append([s*v for s,v in zip(ss,vs)]) + return CNFFormula(8,clauses) + return { + "tseitin-K4-odd": CNFFormula(6,k4), + "pigeonhole-4to3": CNFFormula(12,php), + "xor-two-triples": CNFFormula(6,xor_cnf((1,2,3),1)+xor_cnf((4,5,6),0)), + "random-3SAT": rand3(False), + "planted-3SAT": rand3(True), + } + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json",action="store_true") + parser.add_argument("--split-seed",type=int,default=41) + parser.add_argument("--candidate-seed",type=int,default=19) + parser.add_argument("--rows",type=int,default=8) + parser.add_argument("--weight",type=int,default=3) + parser.add_argument("--budget",type=int,default=512) + args=parser.parse_args() + out={} + for name,formula in corpus().items(): + out[name]=asdict(run_bridge_experiment( + formula,max_vars=12,split_seed=args.split_seed, + candidate_seed=args.candidate_seed,max_rows=args.rows, + max_weight=args.weight,candidate_budget=args.budget)) + if args.json: + print(json.dumps({"warning":"finite exploratory pilot, not a Kakeya or SAT complexity theorem", + "args":vars(args),"corpus":out},indent=2)) + return + print("Finite ETH x Kakeya pilot (non-certifying, small-n only)") + for name,r in out.items(): + nulls=[c["heldout_spurious"] for c in r["controls"]] + print(f"{name:20} n={r['variables']:2} m={r['clauses']:2} " + f"#SAT={r['models']:4} rows={len(r['chosen_rows']):2} " + f"held-out={r['heldout_spurious']:3} " + f"singleton={r['singleton_heldout_spurious']:3} " + f"matched-null-mean={sum(nulls)/len(nulls):5.2f} " + f"GramEig={r['overlap']['top_gram_eigenvalue']:.3f}") + print("No solver verdicts; parity checks are relaxations unless independently certified.") + + +if __name__=="__main__": + main() From 3ca1b49aba87240320b5287c160c5ac1de080d88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:39:33 +0100 Subject: [PATCH 04/48] docs: evidence floor, null controls and falsification contract for ETH-Kakeya bridge --- docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md | 50 ++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md diff --git a/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md b/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md new file mode 100644 index 0000000..a487658 --- /dev/null +++ b/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md @@ -0,0 +1,50 @@ +# Violation-space geometry: ETH x Kakeya (experimental) + +**2026-10-29 | development branch only | H: hypothesis, S: geometric translation, M: bounded pilot.** This is a research probe, not a new certified solver frame. + +Sources: OpenAI, [ETH manuscript](https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf), especially clause-violation parity tests and sparse common-zero systems; [local smoothing manuscript](https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf), especially spherical extension and Kakeya tube overlap. See [Lean ETH scope](https://github.com/openai/math/blob/main/lean/docs/378.md) and [Lean local smoothing scope](https://github.com/openai/math/blob/main/lean/docs/079.md). External verification of research claims is separate from released formal statements. + +## Finite mathematical object + +For a CNF F with n **declared** Boolean variables and m clauses, let the violation signature v_F(x) in GF(2)^m have j-th bit 1 iff x violates clause j. A binary matrix A of check rows defines H_A(F) = {x : A v_F(x) = 0}. All models of F lie in H_A(F), but the converse is false in general. Equivalence on the complete assignment domain holds exactly if + + ker(A) intersect (im(v_F) minus {0}) = empty. + +A retained nonsatisfying assignment is a **spurious survivor**, not evidence of satisfiability. This experimental code enumerates up to 2^12 assignments and never returns a solver verdict. It is not OpenAI's deterministic parity construction, expander coding, interpolation counter or claimed subexponential algorithm. + +For each check row a, define a finite *nonmodel survivor set* T_a = {x : v_F(x) != 0 and = 0 mod 2}. Exclude genuine models, which would otherwise occur in every pass set. Define the incidence operator I[a,x] = 1[x in T_a] / sqrt(|T_a|) for nonempty T_a, otherwise 0; and Gram G = I I^T. Thus G[a,b] = |T_a intersect T_b| / sqrt(|T_a||T_b|), whenever both sets are nonempty. Record the top eigenvalue, mean pairwise overlap cosine and maximum multiplicity. **These sets are not Euclidean tubes; no Kakeya maximal inequality, wave equation estimate, or Hausdorff-dimension theorem applies without an entirely new bridge.** + +## Pre-registered discriminating pilot + +- **Object:** finite clause-violation signatures, with n<=12 and m<=128; count all declared variables, including unused ones. +- **Candidate action:** seeded greedy selection of up to 8 rows from singleton checks and bounded samples of weight-2 and weight-3 checks. Train only on two-thirds of assignment states. +- **Controls:** a trained singleton-only greedy baseline and four seeded row-weight-matched random check matrices. Evaluate all on identical held-out states and report the full truth-table equivalence audit separately. +- **Prediction H:** learned sparse checks may decrease spurious held-out survivors relative to weight-matched random rows; Gram spectral features might independently predict difficulty beyond classical density, XOR rank and frame count. +- **Kill conditions:** withdraw the empirical generalization claim if repeated held-out instance and split seeds erase the effect. Retire the *Kakeya-inspired predictive lift* if Gram statistics offer no incremental out-of-sample predictive signal over ordinary structural features. A low survivor count alone is NOT such a prediction. +- **Promotion:** all observations remain M on specified small instances. A theorem needs its exact statement and proof. A solver win needs controlled runtime including feature computation; a general complexity result is not implied. +- **Safety:** no production router, scout, certified SAT/UNSAT branch, DRAT or trusted-base changes. + +## Reproduction + + python -m pytest backend/tests/test_violation_geometry.py -q + python docs/ladder/scripts/violation_geometry_probe.py + python docs/ladder/scripts/violation_geometry_probe.py --json + python docs/ladder/scripts/violation_geometry_probe.py --split-seed 5 + +This requires neither Kissat nor drat-trim. All random sources are local and seeded. Included families: odd-charge K4 Tseitin, pigeonhole 4-to-3, two XOR triples, random 3-SAT, planted 3-SAT. + +**One split exploratory local run** (split seed 41, candidate seed 19, four random controls): + +| Family | #SAT | Learned held-out spurious | Greedy singleton held-out spurious | Matched random mean | +|---|---:|---:|---:|---:| +| Odd-charge K4 | 0 | 5 | 15 | 5.00 | +| Pigeonhole 4-to-3 | 0 | 4 | 126 | 35.00 | +| Two XOR triples | 16 | 1 | 13 | 5.00 | +| Random 3-SAT | 4 | 1 | 20 | 10.75 | +| Planted 3-SAT | 6 | 4 | 22 | 9.00 | + +These are toy cases. One family **ties** the random null. Twelve additional local assignment-split seeds show K4 beats the four-null mean on 6 splits and loses on 6, so there is no stable K4 advantage yet. Learned checks use labelled training assignments—unavailable to a scalable solver without equivalent work—so better hold-out rejection than random checks does not establish useful solver performance. + +## Next bridge, not yet built + +Explore whether a pre-solve cheaply sampled violation proxy and normalized incidence spectrum improves ACAF's independent routing decisions. Evaluate on **new formulas** rather than merely new assignments of training formulas; hold out entire generators, match structural controls and CPU time, and record failure. Only after that investigate typed connection-Laplacian/curvature or Fourier-analytic transport. Do not promote conceptual correspondence to a theorem. From a0f53cec58cc25dcce5ed9c0cc919679bfa5f400 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:46:45 +0100 Subject: [PATCH 05/48] research: center parity incidence and measure gauge-invariant signed cycles --- backend/violation_spectral_null.py | 96 ++++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 backend/violation_spectral_null.py diff --git a/backend/violation_spectral_null.py b/backend/violation_spectral_null.py new file mode 100644 index 0000000..a65ecf9 --- /dev/null +++ b/backend/violation_spectral_null.py @@ -0,0 +1,96 @@ +"""Centered finite parity incidence and signed-triangle diagnostics. + +Not Kakeya geometry, not a SAT hardness invariant, and never a verdict. +Drop constant-on-sample check rows before computing Pearson correlations. +This removes the trivial shared ~1/2 acceptance background of random checks. +""" +from __future__ import annotations + +from dataclasses import dataclass +from itertools import combinations +from typing import Sequence + +import numpy as np + +from .violation_geometry import _check_rows, parity_accepts + + +@dataclass(frozen=True) +class CenteredOverlap: + sampled_nonmodels: int + variable_checks: int + largest_eigenvalue_per_check: float + mean_absolute_correlation: float + signed_triangle_frustration: float + triangle_mass: float + + +def _correlations(bit_vectors: Sequence[Sequence[int]]) -> np.ndarray: + """Pearson matrix of rows; constant rows must be removed by caller. + + Gauge action b_i -> 1-b_i flips c_ij for every j!=i, so the sign + of c_ij*c_jk*c_ki is invariant under all independent row flips. + """ + b = np.asarray(bit_vectors, dtype=np.float64) + if b.ndim != 2 or b.shape[1] < 1: + raise ValueError("expected a rectangular matrix with at least one column") + means = b.mean(axis=1, keepdims=True) + std = b.std(axis=1, keepdims=True) + if np.any(std < 1e-12): + raise ValueError("constant observation rows cannot be centered") + x = (b - means) / std + cov = (x @ x.T) / b.shape[1] + return np.clip((cov + cov.T) / 2.0, -1.0, 1.0) + + +def _triangle_stats(corr: np.ndarray, *, threshold: float = 0.10) -> tuple[float, float]: + """Weighted negative signed triangles / all substantial triangle mass. + + This is a *signed cycle statistic*, not the minimum frustrated-edge + deletion number and not automatically a CNF contradiction certificate. + """ + k = len(corr) + negative = 0.0 + total = 0.0 + for i, j, k3 in combinations(range(k), 3): + a, b, c = float(corr[i, j]), float(corr[j, k3]), float(corr[k3, i]) + if min(abs(a), abs(b), abs(c)) < threshold: + continue + product = a * b * c + total += abs(product) + if product < 0: + negative += abs(product) + return (negative / total if total else 0.0, total) + + +def centered_incidence(masks: Sequence[int], rows: Sequence[int], + clause_count: int, *, threshold: float = 0.10) -> CenteredOverlap: + """Standardized row covariance on finite NON-model sampled signatures. + + For N nonmodels, b_{ix} = 1 if row i accepts signature x, and + C_ij = E[(b_i-p_i)(b_j-p_j)]/sqrt(p_i(1-p_i)p_j(1-p_j)). + Constant rows are excluded; |rows|<=64, N<=4096. + """ + _check_rows(rows, clause_count) + if len(rows) > 64 or len(masks) > 4096: + raise ValueError("bounded experimental incidence budget exceeded") + if not 0 <= threshold < 1: + raise ValueError("threshold must lie in [0,1)") + if any(not isinstance(v, int) or v < 0 or v >= (1 << clause_count) + for v in masks): + raise ValueError("invalid violation masks") + nonmodels = [v for v in masks if v] + n = len(nonmodels) + observations = [] + for row in rows: + bits = [int(parity_accepts(v, row)) for v in nonmodels] + if 0 < sum(bits) < n: + observations.append(bits) + k = len(observations) + if k == 0: + return CenteredOverlap(n, 0, 0.0, 0.0, 0.0, 0.0) + corr = _correlations(observations) + top = float(np.linalg.eigvalsh(corr)[-1]) / k + pairs = [abs(float(corr[i, j])) for i in range(k) for j in range(i+1, k)] + f, mass = _triangle_stats(corr, threshold=threshold) + return CenteredOverlap(n, k, top, sum(pairs) / len(pairs) if pairs else 0.0, f, mass) From a21515aecf4356318ca4d486b150d4f904a3405a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:46:53 +0100 Subject: [PATCH 06/48] test: independent and anti-correlated parity overlap and orientation-gauge invariance --- backend/tests/test_violation_spectral_null.py | 62 +++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 backend/tests/test_violation_spectral_null.py diff --git a/backend/tests/test_violation_spectral_null.py b/backend/tests/test_violation_spectral_null.py new file mode 100644 index 0000000..2fe74be --- /dev/null +++ b/backend/tests/test_violation_spectral_null.py @@ -0,0 +1,62 @@ +"""Centered finite overlap has gauge-invariant cycle signs and null controls.""" +import math +import numpy as np +import pytest +from backend.violation_spectral_null import ( + centered_incidence, _correlations, _triangle_stats) + + +def test_centered_constant_rows_drop(): + assert centered_incidence((0, 0), (1,), 1).variable_checks == 0 + assert centered_incidence((1, 1), (1,), 1).variable_checks == 0 + + +def test_independent_binary_checks_decorrelated(): + # Both checks are balanced and independent over all four possible patterns. + cor = _correlations(((0, 0, 1, 1), (0, 1, 0, 1))) + assert np.allclose(cor, np.eye(2)) + assert math.isclose(float(np.linalg.eigvalsh(cor)[-1]), 1.0) + + +def test_complementary_rows_negative_correlation_gram_psd(): + cor = _correlations(((0, 1, 0, 1), (1, 0, 1, 0))) + assert np.allclose(cor, np.array([[1, -1], [-1, 1]])) + # Nonnegative power iteration starting at all-ones would incorrectly get zero. + assert math.isclose(float(np.linalg.eigvalsh(cor)[-1]), 2.0) + + +def test_triangle_product_is_invariant_under_row_orientation(): + bits = np.array([[0, 0, 0, 1, 1, 1, 1, 0], + [0, 0, 1, 1, 1, 0, 0, 1], + [1, 1, 0, 1, 0, 0, 1, 0]], dtype=int) + cor = _correlations(bits) + flipped = bits.copy() + flipped[0] = 1 - flipped[0] + flipped[2] = 1 - flipped[2] + cor2 = _correlations(flipped) + assert np.allclose(cor2, cor * np.outer(np.array([-1, 1, -1]), + np.array([-1, 1, -1]))) + f, m = _triangle_stats(cor, threshold=0) + f2, m2 = _triangle_stats(cor2, threshold=0) + assert math.isclose(f, f2) + assert math.isclose(m, m2) + + +def test_explicit_negative_cycle_has_frustration_one(): + c = np.array([[1, .5, -.5], [.5, 1, .5], [-.5, .5, 1]]) + f, m = _triangle_stats(c) + assert f == 1.0 and math.isclose(m, .125) + assert min(np.linalg.eigvalsh(c)) >= -1e-9 + + +def test_centered_one_clause_and_bounded_errors(): + result = centered_incidence((1, 2, 3), (1, 2), 2) + assert result.variable_checks == 2 + assert 0 <= result.mean_absolute_correlation <= 1 + assert 0 <= result.largest_eigenvalue_per_check <= 1 + with pytest.raises(ValueError): + centered_incidence((4,), (1,), 2) + with pytest.raises(ValueError): + centered_incidence((1,), tuple([1] * 65), 2) + with pytest.raises(ValueError): + _correlations(((1, 1, 1),)) From 231660032130ca24ea757b4e8e40c07ac7579f2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:47:26 +0100 Subject: [PATCH 07/48] research: family-held-out DPLL effort probe with sampled parity and centered incidence ablations --- backend/violation_cross_instance.py | 452 ++++++++++++++++++++++++++++ 1 file changed, 452 insertions(+) create mode 100644 backend/violation_cross_instance.py diff --git a/backend/violation_cross_instance.py b/backend/violation_cross_instance.py new file mode 100644 index 0000000..bc14a2f --- /dev/null +++ b/backend/violation_cross_instance.py @@ -0,0 +1,452 @@ +"""Instance-held-out pilot: does finite violation incidence predict DPLL effort? + +This module never returns SAT/UNSAT decisions. The geometry is a diagnostic, +not Euclidean Kakeya geometry and not a consequence of either OpenAI theorem. +Unlike violation_geometry.violation_masks, its extraction samples bounded +assignments; the exact DPLL cost is calculated independently as an *outcome*. +""" +from __future__ import annotations + +from dataclasses import dataclass +from itertools import combinations, product +from math import log2, sqrt +from random import Random +from time import perf_counter_ns +from typing import Sequence + +import numpy as np + +from .cnf_utils import CNFFormula +from .violation_spectral_null import centered_incidence +from .violation_geometry import ( + MAX_ENUM_VARS, _check_formula, greedy_violation_rows, + incidence_overlap, matched_random_rows, parity_accepts, +) + +FAMILIES = ("random-2SAT", "random-3SAT", "planted-3SAT", + "random-3XOR", "tseitin", "pigeonhole") +STRUCTURAL = ("n", "m_over_n", "mean_width", "binary_fraction", "unit_fraction", + "max_occurrence_over_n", "occurrence_cv", "polarity_imbalance", + "xor_pattern_fraction") +SAMPLED = ("mean_violated_fraction", "std_violated_fraction", "sampled_model_fraction", + "unique_violation_fraction") +LEARNED = ("learned_rejection_fraction", "learned_gram_top", "learned_gram_cosine", + "learned_max_multiplicity_fraction") +NULL = ("null_rejection_fraction", "null_gram_top", "null_gram_cosine", + "null_max_multiplicity_fraction") +CENTERED = ("centered_gram_top", "centered_mean_abs_correlation", + "centered_triangle_frustration", "centered_triangle_mass") +CENTERED_NULL = ("null_centered_gram_top", "null_centered_mean_abs_correlation", + "null_centered_triangle_frustration", "null_centered_triangle_mass") +RIDGE_ALPHA = 10.0 + + +def _xor_clauses(variables: Sequence[int], rhs: int) -> list[list[int]]: + return [[-v if bit else v for v, bit in zip(variables, bits)] + for bits in product((0, 1), repeat=len(variables)) + if sum(bits) % 2 != rhs] + + +def _shuffle_vars(formula: CNFFormula, rng: Random) -> CNFFormula: + """Preserve satisfiability with signed variable relabelings and clause order.""" + names = list(range(1, formula.num_vars + 1)) + rng.shuffle(names) + flips = [rng.choice((-1, 1)) for _ in names] + clauses = [[(1 if lit > 0 else -1) * names[abs(lit) - 1] * flips[abs(lit) - 1] + for lit in c] for c in formula.clauses] + for c in clauses: + rng.shuffle(c) + rng.shuffle(clauses) + return CNFFormula(formula.num_vars, clauses) + + +def generate_formula(family: str, seed: int) -> CNFFormula: + """Small, fixed families; seeded; no truth labels enter the generator choice.""" + if family not in FAMILIES: + raise ValueError(f"unknown generator family: {family}") + rng = Random(seed + 10_007 * (FAMILIES.index(family) + 1)) + if family in ("random-2SAT", "random-3SAT", "planted-3SAT"): + n = rng.randint(8, 11) + k = 2 if family == "random-2SAT" else 3 + ratio = rng.uniform(1.4, 3.4) if k == 2 else rng.uniform(2.8, 5.8) + m = round(n * ratio) + planted = rng.randrange(1 << n) if family == "planted-3SAT" else None + clauses = [] + for _ in range(m): + variables = rng.sample(range(1, n + 1), k) + signs = [rng.choice((-1, 1)) for _ in variables] + clause = [a * v for a, v in zip(signs, variables)] + if planted is not None and not any( + (bool(planted & (1 << (abs(lit) - 1))) == (lit > 0)) + for lit in clause): + j = rng.randrange(k) + clause[j] = -clause[j] + clauses.append(clause) + return CNFFormula(n, clauses) + if family == "random-3XOR": + n = rng.randint(8, 11) + q = rng.randint(n - 2, n + 3) + plant = rng.randrange(1 << n) if rng.randrange(2) else None + clauses = [] + for _ in range(q): + variables = sorted(rng.sample(range(1, n + 1), 3)) + rhs = (sum(bool(plant & (1 << (v - 1))) for v in variables) % 2 + if plant is not None else rng.randrange(2)) + clauses += _xor_clauses(variables, rhs) + return CNFFormula(n, clauses) + if family == "tseitin": + # K4, triangular prism, cube; edge variables, degree-three vertices. + shape = seed % 3 + if shape == 0: + edges = list(combinations(range(4), 2)) + vertices = 4 + elif shape == 1: + edges = [(0, 1), (1, 2), (2, 0), (3, 4), (4, 5), (5, 3), + (0, 3), (1, 4), (2, 5)] + vertices = 6 + else: + edges = [(i, i ^ (1 << j)) for i in range(8) for j in range(3) + if i < (i ^ (1 << j))] + vertices = 8 + charges = [rng.randrange(2) for _ in range(vertices)] + charges[-1] = (sum(charges[:-1]) + (seed % 2)) % 2 + clauses = [] + for v in range(vertices): + incident = [j + 1 for j, (a, b) in enumerate(edges) if a == v or b == v] + clauses += _xor_clauses(incident, charges[v]) + return _shuffle_vars(CNFFormula(len(edges), clauses), rng) + # PHP p -> h int: + mask = 0 + for i, clause in enumerate(clauses): + if not any(bool(assignment & (1 << (abs(lit) - 1))) == (lit > 0) + for lit in clause): + mask |= (1 << i) + return mask + + +def sampled_signatures(formula: CNFFormula, *, budget: int, seed: int, + max_vars: int = MAX_ENUM_VARS) -> tuple[int, ...]: + """Sample unique assignments, strictly less than the total state space.""" + _check_formula(formula, max_vars) + if not isinstance(budget, int) or budget < 1 or budget >= (1 << formula.num_vars): + raise ValueError("sample budget must be positive and strictly below 2^n") + indices = Random(seed).sample(range(1 << formula.num_vars), budget) + return tuple(_violation_at(formula.clauses, x) for x in indices) + + +def _split_sampled_signatures(formula: CNFFormula, budget: int, + seed: int) -> tuple[tuple[int, ...], tuple[int, ...]]: + _check_formula(formula, MAX_ENUM_VARS) + if not isinstance(budget, int) or budget < 2 or budget >= (1 << formula.num_vars): + raise ValueError("sample total must fit strictly below 2^n") + indices = Random(seed).sample(range(1 << formula.num_vars), budget) + half = budget // 2 + return (tuple(_violation_at(formula.clauses, x) for x in indices[:half]), + tuple(_violation_at(formula.clauses, x) for x in indices[half:])) + + +def _xor_pattern_fraction(formula: CNFFormula) -> float: + """Conventional literal sign-pattern detector, not an XOR SAT solver.""" + buckets: dict[tuple[int, ...], set[int]] = {} + for clause in formula.clauses: + vv = [abs(lit) for lit in clause] + if len(vv) not in (2, 3) or len(set(vv)) != len(vv): + continue + variables = tuple(sorted(vv)) + sign_by_var = {abs(lit): lit < 0 for lit in clause} + mask = sum(1 << j for j, v in enumerate(variables) if sign_by_var[v]) + buckets.setdefault(variables, set()).add(mask) + accounted = 0 + for vv, masks in buckets.items(): + if len(masks) == (1 << (len(vv) - 1)): + if len({m.bit_count() % 2 for m in masks}) == 1: + accounted += len(masks) + return accounted / max(1, len(formula.clauses)) + + +def structural_features(formula: CNFFormula) -> tuple[float, ...]: + _check_formula(formula, MAX_ENUM_VARS) + n = formula.num_vars + if n == 0: + raise ValueError("cross-instance probe needs at least one variable") + m = len(formula.clauses) + widths = [len(c) for c in formula.clauses] + pos, neg = [0] * n, [0] * n + for clause in formula.clauses: + for literal in clause: + (pos if literal > 0 else neg)[abs(literal) - 1] += 1 + degrees = [p + q for p, q in zip(pos, neg)] + mean_deg = sum(degrees) / n + sd_deg = sqrt(sum((d - mean_deg) ** 2 for d in degrees) / n) + return (float(n), m / n, sum(widths) / max(m, 1), + sum(w == 2 for w in widths) / max(m, 1), + sum(w == 1 for w in widths) / max(m, 1), + max(degrees, default=0) / n, + sd_deg / max(mean_deg, 1.0), + sum(abs(p - q) for p, q in zip(pos, neg)) / max(sum(degrees), 1), + _xor_pattern_fraction(formula)) + + +def _aggregate_violation_features(train: Sequence[int], probe: Sequence[int], + m: int) -> tuple[float, ...]: + masks = tuple(train) + tuple(probe) + values = [v.bit_count() / max(m, 1) for v in masks] + mean = sum(values) / len(values) + dev = sqrt(sum((v - mean) ** 2 for v in values) / len(values)) + return (mean, dev, sum(v == 0 for v in masks) / len(masks), + len(set(masks)) / len(masks)) + + +def _geometry_features(probe: Sequence[int], rows: Sequence[int], m: int) -> tuple[float, ...]: + inc = incidence_overlap(probe, rows, m) + num_nonmodel = sum(v != 0 for v in probe) + survived = sum(v != 0 and all(parity_accepts(v, row) for row in rows) + for v in probe) + return ((num_nonmodel - survived) / max(num_nonmodel, 1), + inc.top_gram_eigenvalue / max(inc.active_rows, 1), + inc.mean_pairwise_cosine, + inc.maximum_multiplicity / max(inc.active_rows, 1)) + + +def _dpll_search_nodes(formula: CNFFormula) -> int: + """Deterministic unit-propagating DPLL reference effort, NOT CDCL time.""" + clauses = formula.clauses + calls = 0 + + def dfs(assign: dict[int, bool]) -> bool: + nonlocal calls + calls += 1 + values = assign.copy() + while True: + changed = False + all_satisfied = True + for clause in clauses: + unassigned = [] + satisfied = False + for literal in clause: + var = abs(literal) + if var in values: + if values[var] == (literal > 0): + satisfied = True + break + else: + unassigned.append(literal) + if satisfied: + continue + all_satisfied = False + if not unassigned: + return False + if len(unassigned) == 1: + lit = unassigned[0] + var = abs(lit) + implied = lit > 0 + if var in values and values[var] != implied: + return False + if var not in values: + values[var] = implied + changed = True + if all_satisfied: + return True + if not changed: + break + var = next((v for v in range(1, formula.num_vars + 1) if v not in values), None) + if var is None: + return False + for bit in (False, True): + extended = values.copy() + extended[var] = bit + if dfs(extended): + return True + return False + + dfs({}) + return calls + + +@dataclass(frozen=True) +class FormulaRecord: + family: str + seed: int + n: int + m: int + dpll_nodes: int + target_log2_nodes: float + features: tuple[float, ...] + structural_ns: int + sampling_ns: int + row_selection_ns: int + geometry_ns: int + null_geometry_ns: int + centered_ns: int + null_centered_ns: int + dpll_ns: int + + @property + def measured_feature_ns(self) -> int: + return (self.structural_ns + self.sampling_ns + + self.row_selection_ns + self.geometry_ns + self.centered_ns) + + +def record_formula(formula: CNFFormula, family: str, seed: int, *, + budget: int = 48, rows: int = 6, candidate_budget: int = 96, + seed_offset: int = 0) -> FormulaRecord: + """Compute pre-solving predictors and separate held-out effort target.""" + if rows < 0 or rows > 32: + raise ValueError("rows outside [0,32]") + if not 2 <= budget < (1 << formula.num_vars): + raise ValueError("sample budget exhausted assignment space") + m = len(formula.clauses) + if candidate_budget < m: + raise ValueError("candidate budget below number of clauses") + ts = perf_counter_ns() + s = structural_features(formula) + struct_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + train, probe = _split_sampled_signatures(formula, budget, seed + seed_offset * 100003 + 1081) + sampled = _aggregate_violation_features(train, probe, m) + sampling_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + learned_rows = greedy_violation_rows(train, m, max_rows=rows, + max_weight=3, candidate_budget=candidate_budget, + candidate_seed=seed + seed_offset * 37 + 1057) + selection_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + learned = _geometry_features(probe, learned_rows, m) + geom_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + null_rows = matched_random_rows(learned_rows, m, seed + seed_offset * 73 + 23) + null = _geometry_features(probe, null_rows, m) + null_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + center = centered_incidence(probe, learned_rows, m) + center_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + center_null = centered_incidence(probe, null_rows, m) + center_null_ns = perf_counter_ns() - ts + ts = perf_counter_ns() + dpll_nodes = _dpll_search_nodes(formula) + dpll_ns = perf_counter_ns() - ts + return FormulaRecord( + family, seed, formula.num_vars, m, dpll_nodes, + log2(1 + dpll_nodes), + s + sampled + learned + null + + (center.largest_eigenvalue_per_check, + center.mean_absolute_correlation, + center.signed_triangle_frustration, center.triangle_mass) + + (center_null.largest_eigenvalue_per_check, + center_null.mean_absolute_correlation, + center_null.signed_triangle_frustration, center_null.triangle_mass), + struct_ns, sampling_ns, selection_ns, geom_ns, null_ns, + center_ns, center_null_ns, dpll_ns) + + +FEATURE_INDEX = {name: i for i, name in enumerate(STRUCTURAL + SAMPLED + LEARNED + NULL + CENTERED + CENTERED_NULL)} +PREDICTORS = { + "constant": (), + "structure": STRUCTURAL, + "structure+sample": STRUCTURAL + SAMPLED, + "structure+sample+null": STRUCTURAL + SAMPLED + NULL, + "structure+sample+learned-pass": STRUCTURAL + SAMPLED + LEARNED[:1], + "structure+sample+learned-gram": STRUCTURAL + SAMPLED + LEARNED, + "structure+sample+centered": STRUCTURAL + SAMPLED + CENTERED, + "structure+sample+null-centered": STRUCTURAL + SAMPLED + CENTERED_NULL, + "structure+sample+all-geometry": STRUCTURAL + SAMPLED + LEARNED + CENTERED, +} + + +def _predict_ridge(train: Sequence[FormulaRecord], + test: Sequence[FormulaRecord], names: Sequence[str], + alpha: float = RIDGE_ALPHA) -> np.ndarray: + y = np.array([v.target_log2_nodes for v in train], dtype=float) + if not names: + return np.full(len(test), y.mean()) + indices = [FEATURE_INDEX[name] for name in names] + X = np.array([[v.features[i] for i in indices] for v in train], dtype=float) + Z = np.array([[v.features[i] for i in indices] for v in test], dtype=float) + mu = X.mean(axis=0) + sd = X.std(axis=0) + sd[sd < 1e-12] = 1.0 + X = (X - mu) / sd + Z = (Z - mu) / sd + design = np.column_stack((np.ones(len(X)), X)) + penalty = np.diag([0.0] + [float(alpha)] * X.shape[1]) + coefficients = np.linalg.solve(design.T @ design + penalty, design.T @ y) + return np.column_stack((np.ones(len(Z)), Z)) @ coefficients + + +@dataclass(frozen=True) +class FoldResult: + heldout_family: str + instances: int + min_nodes: int + median_nodes: float + max_nodes: int + mae_log2_by_predictor: dict[str, float] + + +@dataclass(frozen=True) +class CrossInstanceReport: + seed_count: int + instances: int + sample_budget: int + row_budget: int + candidate_budget: int + folds: tuple[FoldResult, ...] + overall_mae_log2: dict[str, float] + median_feature_ms: float + median_structural_ms: float + median_null_ms: float + median_dpll_ms: float + median_centered_ms: float + max_enum_vars: int + evidence_level: str = "M: finite measured DPLL-reference effort only" + + +def cross_instance_benchmark(*, seed_count: int = 12, sample_budget: int = 48, + rows: int = 6, candidate_budget: int = 96, + seed_offset: int = 0) -> CrossInstanceReport: + """Leave one generator FAMILY out per fold; report every fold and null.""" + if not 2 <= seed_count <= 32: + raise ValueError("seed_count must be in [2,32]") + dataset = [] + for family in FAMILIES: + for seed in range(seed_count): + formula = generate_formula(family, seed) + dataset.append(record_formula(formula, family, seed, + budget=sample_budget, rows=rows, + candidate_budget=candidate_budget, + seed_offset=seed_offset)) + folds = [] + accum = {name: 0.0 for name in PREDICTORS} + for heldout in FAMILIES: + train = [r for r in dataset if r.family != heldout] + test = [r for r in dataset if r.family == heldout] + actual = np.array([r.target_log2_nodes for r in test]) + losses = {} + for name, features in PREDICTORS.items(): + predicted = _predict_ridge(train, test, features) + losses[name] = float(np.mean(np.abs(predicted - actual))) + accum[name] += losses[name] * len(test) + nodes = sorted(v.dpll_nodes for v in test) + folds.append(FoldResult(heldout, len(test), nodes[0], + (nodes[(len(nodes)-1)//2] + nodes[len(nodes)//2]) / 2, + nodes[-1], losses)) + full = {name: error / len(dataset) for name, error in accum.items()} + return CrossInstanceReport( + seed_count, len(dataset), sample_budget, rows, candidate_budget, + tuple(folds), full, + float(np.median([r.measured_feature_ns / 1e6 for r in dataset])), + float(np.median([r.structural_ns / 1e6 for r in dataset])), + float(np.median([r.null_geometry_ns / 1e6 for r in dataset])), + float(np.median([r.dpll_ns / 1e6 for r in dataset])), + float(np.median([r.centered_ns / 1e6 for r in dataset])), + MAX_ENUM_VARS) From e4e92a4578f135cd29ce846592172ae4755b6713 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:47:38 +0100 Subject: [PATCH 08/48] test: bound sampled features and independently verify family-held-out evaluation --- .../tests/test_violation_cross_instance.py | 80 +++++++++++++++++++ 1 file changed, 80 insertions(+) create mode 100644 backend/tests/test_violation_cross_instance.py diff --git a/backend/tests/test_violation_cross_instance.py b/backend/tests/test_violation_cross_instance.py new file mode 100644 index 0000000..f2a557c --- /dev/null +++ b/backend/tests/test_violation_cross_instance.py @@ -0,0 +1,80 @@ +"""Test oracle separation, held-out-family folds and deterministic controls.""" +import math +import pytest +from backend.cnf_utils import CNFFormula +from backend.violation_cross_instance import ( + FAMILIES, PREDICTORS, _dpll_search_nodes, _xor_clauses, + cross_instance_benchmark, generate_formula, record_formula, + sampled_signatures, structural_features) +from backend.violation_geometry import violation_masks + + +def test_sample_is_bounded_and_does_not_enumerate_all_assignments(): + f = CNFFormula(4, [[1], [-2], [1, -3]]) + sample = sampled_signatures(f, budget=7, seed=42) + full = violation_masks(f) + assert len(sample) == 7 and all(v in full for v in sample) + assert sample == sampled_signatures(f, budget=7, seed=42) + with pytest.raises(ValueError): + sampled_signatures(f, budget=16, seed=42) + with pytest.raises(ValueError): + sampled_signatures(f, budget=0, seed=42) + + +def test_dpll_baselines_count_nodes_not_sat_verdicts(): + assert _dpll_search_nodes(CNFFormula(3, [])) == 1 + assert _dpll_search_nodes(CNFFormula(1, [[1], [-1]])) == 1 + assert _dpll_search_nodes(CNFFormula(1, [[1]])) == 1 + assert _dpll_search_nodes(CNFFormula(2, [[1, 2]])) > 1 + + +def test_all_generators_fit_budget_and_valid_semantics(): + for family in FAMILIES: + for seed in range(5): + f = generate_formula(family, seed) + assert 1 <= f.num_vars <= 12 + assert 0 < len(f.clauses) <= 128 + assert all(1 <= abs(x) <= f.num_vars for c in f.clauses for x in c) + assert generate_formula(family, seed) == f + assert len(structural_features(f)) == 9 + r = record_formula(f, family, seed, budget=24, candidate_budget=96) + assert len(r.features) == 29 + assert r.dpll_nodes >= 1 + assert math.isfinite(r.target_log2_nodes) + assert r.measured_feature_ns >= r.structural_ns + + +def test_tseitin_charge_parity_sets_sat_status(): + for seed in range(6): + f = generate_formula("tseitin", seed) + masks = violation_masks(f, max_vars=12) + assert (any(v == 0 for v in masks)) == (seed % 2 == 0) + + +def test_xor_convention(): + f = CNFFormula(3, _xor_clauses((1, 2, 3), 1)) + masks = violation_masks(f) + assert [i for i, v in enumerate(masks) if v == 0] == [1, 2, 4, 7] + + +def test_cross_instance_folds_and_null_comparator(): + r = cross_instance_benchmark(seed_count=2, sample_budget=24, + rows=4, candidate_budget=96) + assert r.instances == 2 * len(FAMILIES) + assert {f.heldout_family for f in r.folds} == set(FAMILIES) + assert set(r.overall_mae_log2) == set(PREDICTORS) + assert all(math.isfinite(v) and v >= 0 for v in r.overall_mae_log2.values()) + assert all(f.instances == 2 for f in r.folds) + assert r.seed_count == 2 + assert r.median_dpll_ms >= 0 and r.median_centered_ms >= 0 + + +def test_no_formula_labels_are_used_in_feature_extraction(monkeypatch): + # Predictor work happens BEFORE and separately from the reference DPLL call. + from backend import violation_cross_instance as mod + f = generate_formula("random-3SAT", 0) + def no_oracle(_): + raise RuntimeError("target requested") + monkeypatch.setattr(mod, "_dpll_search_nodes", no_oracle) + with pytest.raises(RuntimeError, match="target requested"): + mod.record_formula(f, "random-3SAT", 0, budget=24, candidate_budget=96) From da9d296642480d563a4be594665858722eddc77f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:48:05 +0100 Subject: [PATCH 09/48] benchmark: deterministic cross-generator holdouts and multi-seed geometry ablations --- .../scripts/violation_cross_instance_probe.py | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 docs/ladder/scripts/violation_cross_instance_probe.py diff --git a/docs/ladder/scripts/violation_cross_instance_probe.py b/docs/ladder/scripts/violation_cross_instance_probe.py new file mode 100644 index 0000000..826ff41 --- /dev/null +++ b/docs/ladder/scripts/violation_cross_instance_probe.py @@ -0,0 +1,85 @@ +"""Leave-one-family-out ETH x Kakeya *diagnostic* experiment. + +Run: + python docs/ladder/scripts/violation_cross_instance_probe.py --seed-count 24 --replicates 10 + python docs/ladder/scripts/violation_cross_instance_probe.py --json +No SAT/UNSAT certificate or general complexity claim is produced. +""" +from __future__ import annotations + +import argparse +import json +import math +import sys +from dataclasses import asdict +from pathlib import Path +from statistics import mean, median + +sys.path.insert(0, str(Path(__file__).resolve().parents[3])) +from backend.violation_cross_instance import cross_instance_benchmark, PREDICTORS + + +def main() -> None: + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("--seed-count", type=int, default=12, + help="2..32 distinct formula seeds for each of six generator families") + p.add_argument("--replicates", type=int, default=1, + help="independent assignment-sampling offsets, 1..30") + p.add_argument("--sample-budget", type=int, default=48) + p.add_argument("--rows", type=int, default=6) + p.add_argument("--candidate-budget", type=int, default=96) + p.add_argument("--json", action="store_true") + args = p.parse_args() + if not 1 <= args.replicates <= 30: + p.error("replicates must be within 1..30") + runs = [ + cross_instance_benchmark(seed_count=args.seed_count, sample_budget=args.sample_budget, + rows=args.rows, candidate_budget=args.candidate_budget, + seed_offset=i) + for i in range(args.replicates) + ] + aggregate = { + name: { + "mean_mae_log2_nodes": mean(run.overall_mae_log2[name] for run in runs), + "min_mae_log2_nodes": min(run.overall_mae_log2[name] for run in runs), + "max_mae_log2_nodes": max(run.overall_mae_log2[name] for run in runs), + "replicates_better_than_structural": sum( + run.overall_mae_log2[name] < run.overall_mae_log2["structure"] + for run in runs), + } + for name in PREDICTORS + } + feature_cost_ms = median(run.median_feature_ms for run in runs) + structure_cost_ms = median(run.median_structural_ms for run in runs) + dpll_cost_ms = median(run.median_dpll_ms for run in runs) + payload = { + "evidence": "M: finite held-out-family predictions of fixed DPLL nodes, not CDCL or Kakeya", + "canary_provenance": "family stratification and raw degree dispersion; no A4/Z2 group assertions", + "parameters": vars(args), + "instances_per_replicate": runs[0].instances, + "families": [fold.heldout_family for fold in runs[0].folds], + "aggregate": aggregate, + "median_feature_cost_ms": feature_cost_ms, + "median_structural_cost_ms": structure_cost_ms, + "median_reference_dpll_ms": dpll_cost_ms, + "runs": [asdict(run) for run in runs], + } + if args.json: + print(json.dumps(payload, indent=2)) + return + print(f"Instance-held-out probe: {runs[0].instances} toy CNFs per replicate; " + f"{args.replicates} feature-sampling offsets") + print(f"{'predictor':37} {'mean MAE':>10} {'vs structure':>13}") + base = aggregate["structure"]["mean_mae_log2_nodes"] + for name, row in aggregate.items(): + value = row["mean_mae_log2_nodes"] + print(f"{name:37} {value:10.4f} {value-base:+13.4f}") + print(f"Median feature cost {feature_cost_ms:.4f} ms; " + f"structure {structure_cost_ms:.4f} ms; " + f"reference DPLL {dpll_cost_ms:.4f} ms") + print("Null controls, all folds, and seed-level results: use --json.") + print("These are finite diagnostic statistics; no solver claims follow.") + + +if __name__ == "__main__": + main() From 1e22bc16f8869552dff4aacae01a94cde1967de1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:48:18 +0100 Subject: [PATCH 10/48] ci: isolated finite bridge tests and leave-family-out null control runner --- .github/workflows/violation-geometry-lab.yml | 45 ++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 .github/workflows/violation-geometry-lab.yml diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml new file mode 100644 index 0000000..24d1517 --- /dev/null +++ b/.github/workflows/violation-geometry-lab.yml @@ -0,0 +1,45 @@ +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" + +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: Run mathematical, sampling and isolation tests + 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 + - name: Reproduce leave-one-family-out results and null controls + run: | + python docs/ladder/scripts/violation_cross_instance_probe.py --seed-count 12 --replicates 2 --json > /tmp/violation_geometry_report.json + python - <<'PY' + import json, math + with open("/tmp/violation_geometry_report.json", encoding="utf-8") as fh: + report = json.load(fh) + assert report["instances_per_replicate"] == 72 + assert len(report["families"]) == 6 + assert len(report["runs"]) == 2 + for name, stats in report["aggregate"].items(): + assert math.isfinite(stats["mean_mae_log2_nodes"]), name + assert stats["mean_mae_log2_nodes"] >= 0, name + print("Bounded hold-out report and controls are well formed; no solver speed claim.") + PY From 7c241088290057f3e7c3015006a89c27c6aa8f23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:48:53 +0100 Subject: [PATCH 11/48] docs: retain negative LOFO evidence, Canary provenance and gauge-invariant signed cycles --- .../ladder/VIOLATION_CROSS_INSTANCE_REPORT.md | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md diff --git a/docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md b/docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md new file mode 100644 index 0000000..1c00f74 --- /dev/null +++ b/docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md @@ -0,0 +1,66 @@ +# ETH x Kakeya: cross-instance falsification and centered signed cycles + +**2026-10-29. Development branch: dev/kakeya-violation-frame. Status M/R for the predictive hypothesis, P for elementary finite identities, S for Kakeya vocabulary.** The production SAT path remains untouched. + +## Why this round exists + +The original [finite pilot](ETH_KAKEYA_VIOLATION_GEOMETRY.md) trained sparse parity checks on a fraction of *assignments from the same formula*, then evaluated other assignments of that formula. That cannot establish generalization to unseen formulas; moreover, its Gram spectrum required complete enumeration. + +This round adds **bounded assignment sampling as a feature extractor**; an independent unit-propagating **DPLL search-node counter as a reference target**; and **leave-one-entire-generator-family-out** (LOFO) prediction. The model is deterministic fixed-penalty ridge regression with all standardization fit only on training families. No proof, UNSAT verdict, CDCL solver, or Lean theorem is invoked by the predictor. + +## Canary provenance, with corrections + +Source: private [jesusvilela/-SAT_Research_Canary](https://github.com/jesusvilela/-SAT_Research_Canary), especially [flavor_analyzer.hpp](https://github.com/jesusvilela/-SAT_Research_Canary/blob/main/backend/cpp/flavor_analyzer.hpp) and [evolve_heuristics.py](https://github.com/jesusvilela/-SAT_Research_Canary/blob/main/studies/evolve_heuristics.py). + +We borrow the **actual low-cost measurements** (degree dispersion) and the idea of **family-stratified sampling and ablation**. We do **not** import the C++ thresholds calling low-variance 3CNF "Z2_x_Z2" or high-variance CNF "A4": those thresholds are classifiers, not group identification proofs. We do **not** import sample selection based on known solve times; that would leak the target. The Canary studies' simulated/mocked benchmarking results and cloned synthetic instances are not evidence here. + +## Bounded representation + +For F, evaluate its violation vector v_F(x) only on 48 distinct uniformly selected Boolean assignments (24 for choosing sparse checks, 24 held out for computing features). Sampling is strictly less than 2^n, n<=12; enumerated truth tables are not used to construct *cross-instance predictors*. + +The original incidence matrix uses row check-pass indicators restricted to nonsatisfying sampled assignments. The new **centered covariance** removes the large random-check overlap background. Write b_i(x) = 1 when check i passes and v_F(x) != 0, p_i=E[b_i] over sampled nonmodels, and remove rows with p_i in {0,1}. Set + + Z_i(x) = (b_i(x)-p_i)/sqrt(p_i*(1-p_i)) + C_ij = E[Z_i(x)*Z_j(x)]. + +C is a positive-semidefinite correlation Gram matrix. We record its largest eigenvalue divided by its number of nonconstant rows, mean absolute off-diagonal correlation, and signed triangle statistic. + + f_triangle = sum_{i=0.10 participate and a zero denominator gives f=0. This is a signed **triangle** statistic, *not* the frustration index of an arbitrary signed graph or a CNF contradiction certificate. + +**Exact finite invariance (P).** Flipping the orientation of any row's binary indicator maps Z_i to -Z_i. For a diagonal sign matrix D, C' = D C D. Consequently the entire eigenvalue multiset and the sign of each triangle product C_ij C_jk C_ki are invariant. This finite gauge identity is tested. It says nothing by itself about NP hardness, holonomy of a nontrivial connection, or a Kakeya bound. + +## Held-out family evaluation (M) + +Six seeded families: random 2-SAT, random 3-SAT, planted 3-SAT, random 3-XOR, charged cubic Tseitin graph CNFs (K4, triangular prism, cube), and pigeonhole CNFs. PHP has only three base sizes and Tseitin only three base graphs, each repeatedly relabeled; **these are not independent graph topologies**, so statistical generality is still limited. + +Targets: log2(1 + deterministic lexicographic DPLL recursive calls) with unit propagation, **not modern CDCL runtime**. Nine baseline structural features include degree dispersion inspired by Canary, plus n, m/n, clause width, polarity and XOR-pattern indicators. Additional feature groups include sampled violation histograms, learned sparse-check pass/uncentered overlap, random-check matched-null overlap, and centered signed-cycle features. + +All errors below are LOFO **mean absolute errors**, averaged over ten independently seeded *assignment-sampling* offsets on the same fixed formula corpus per size. Lower is better. + +| CNFs | Structural only | + sampled violations | + learned uncentered overlap | + centered overlap / triangles | +|---:|---:|---:|---:|---:| +| 72 (12 per family) | **0.67735** | 0.72411 | 0.72411 | 0.71460 | +| 144 (24 per family) | **0.64016** | 0.67691 | 0.68232 | 0.68559 | +| 192 (32 per family) | **0.61441** | 0.70232 | 0.70679 | 0.70472 | + +Across ten repeats, the centered variant improves on structure-only in **3/10**, **0/10**, and **0/10** cases respectively; the uncentered learned variant improves in **1/10**, **0/10**, and **0/10** cases. Random weight-matched check features are tracked separately by the script and do not rescue the predictor. The modest improvement of centered features on one initial 72-formula split was not replicated. + +Illustrative local Python run (72 CNFs): median complete geometry feature extraction ~4.4 ms, structural-only extraction ~0.08 ms, reference DPLL itself ~0.09 ms. These timing readings are noisy, environment-specific and *not* throughput benchmarks. The feature extraction is already materially more expensive than the toy reference solver. + +**Correction / R (bounded scope).** Retire the claim that this specific learned incidence/signed-triangle representation predicts held-out toy DPLL effort better than classical structure, on the tested generators and evaluation regime. Do NOT retire the elementary algebra or assert it cannot work with other observables. This negative result was measured after exploring feature variations; centered-feature additions were exploratory, not pre-registered confirmatory tests. + +## Reproduction and exact scope + + python -m pytest -q backend/tests/test_violation_geometry.py backend/tests/test_violation_spectral_null.py backend/tests/test_violation_cross_instance.py + python docs/ladder/scripts/violation_cross_instance_probe.py --seed-count 12 --replicates 1 + python docs/ladder/scripts/violation_cross_instance_probe.py --seed-count 24 --replicates 10 --json + python docs/ladder/scripts/violation_cross_instance_probe.py --seed-count 32 --replicates 10 --json + +The CLI outputs *every* predictor and each held-out family in JSON, plus feature extraction costs. A branch-only [GitHub Actions lane](../../.github/workflows/violation-geometry-lab.yml) runs the tests and a small reproducibility probe without installing Kissat/drat-trim. A green lane proves only bounded contracts and successful execution. + +## Next admissible bridge (H) + +First seek a much cheaper **unlabeled** structural projection, under matched size/width/degree controls, and test on genuinely new graph families. Next evaluate whether incremental predictive information survives **CDCL** effort, with time/memory cost charged to the predictor; no routing integration until it does. A continuous Kakeya maximal estimate or connection-Laplacian smoothing bound would require a separately constructed, typed finite-to-continuous transport theorem. No such theorem is claimed here. From 4f4d4dbe9b231ce04998bb400ebc0961763231f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:49:12 +0100 Subject: [PATCH 12/48] docs: supersede five-instance optimism with family-held-out negative result --- docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md b/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md index a487658..05d6cbe 100644 --- a/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md +++ b/docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md @@ -45,6 +45,6 @@ This requires neither Kissat nor drat-trim. All random sources are local and see These are toy cases. One family **ties** the random null. Twelve additional local assignment-split seeds show K4 beats the four-null mean on 6 splits and loses on 6, so there is no stable K4 advantage yet. Learned checks use labelled training assignments—unavailable to a scalable solver without equivalent work—so better hold-out rejection than random checks does not establish useful solver performance. -## Next bridge, not yet built +## Cross-instance continuation and correction (2026-10-29) -Explore whether a pre-solve cheaply sampled violation proxy and normalized incidence spectrum improves ACAF's independent routing decisions. Evaluate on **new formulas** rather than merely new assignments of training formulas; hold out entire generators, match structural controls and CPU time, and record failure. Only after that investigate typed connection-Laplacian/curvature or Fourier-analytic transport. Do not promote conceptual correspondence to a theorem. +The above proposed bridge has now been implemented and tested, including sampling, leave-one-generator-family-out ridge prediction, centered incidence, a signed triangle statistic and matched random controls. The result is **negative for the proposed hardness predictor in this bounded regime**: see [VIOLATION_CROSS_INSTANCE_REPORT.md](VIOLATION_CROSS_INSTANCE_REPORT.md) for full numbers, seed repetitions and Canary provenance. The finite parity and gauge identities survive; predictive advantage and scalability have not been established. Do not promote the earlier five-instance pilot into a solver result. From 36826e3cf4c414446e5f81e94617aed619431211 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:49:14 +0100 Subject: [PATCH 13/48] docs: link experimental falsification from development README --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 2bfb5de..0fac1ac 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,8 @@ Headless. No web UI. No *trust-me*. +> **Experimental development branch — ETH × Kakeya incidence:** the [finite cross-instance report](docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md) keeps a **negative** result visible: after holding out entire small CNF families, learned overlap and signed-cycle statistics do not outperform classical structural predictors of a reference DPLL's search nodes. Mathematical invariants are not algorithmic speedups. The [initial bridge](docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md) is preserved, not rewritten to hide its limitations. No production solver decisions are changed. + 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 From 952b826a1d44d2c113d9e901a94c03529f8222d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 17:49:21 +0100 Subject: [PATCH 14/48] test: refute symmetry inference from Canary degree-regularity threshold --- backend/tests/test_violation_cross_instance.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/backend/tests/test_violation_cross_instance.py b/backend/tests/test_violation_cross_instance.py index f2a557c..17bc3b9 100644 --- a/backend/tests/test_violation_cross_instance.py +++ b/backend/tests/test_violation_cross_instance.py @@ -78,3 +78,13 @@ def no_oracle(_): monkeypatch.setattr(mod, "_dpll_search_nodes", no_oracle) with pytest.raises(RuntimeError, match="target requested"): mod.record_formula(f, "random-3SAT", 0, budget=24, candidate_budget=96) + + +def test_canary_low_degree_variance_is_not_a_symmetry_proof(): + # Every variable has degree 3 and each clause has length 3. + # The canary's flavor threshold would call this Z2_x_Z2, but it has + # no complete XOR sign-pattern group at all. + f = CNFFormula(4, [[1, 2, 3], [1, 2, 4], [1, 3, 4], [2, 3, 4]]) + features = structural_features(f) + assert features[6] == 0.0 # degree coefficient of variation + assert features[8] == 0.0 # fraction of complete XOR clause patterns From 1a0e6e31c56e7d6facb75fcd30c4711aa78e754f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:01:40 +0100 Subject: [PATCH 15/48] research: exact Z2 signed-incidence cycle obstruction and polarity-margin null --- backend/violation_connection.py | 160 ++++++++++++++++++++++++++++++++ 1 file changed, 160 insertions(+) create mode 100644 backend/violation_connection.py diff --git a/backend/violation_connection.py b/backend/violation_connection.py new file mode 100644 index 0000000..023adf3 --- /dev/null +++ b/backend/violation_connection.py @@ -0,0 +1,160 @@ +"""Finite signed clause-variable connection, independent of assignment sampling. + +This is a *diagnostic* on the signed bipartite incidence graph, not a +SAT/UNSAT certificate, a connection-Laplacian theorem, or a Kakeya estimate. +Literal duplication is normalized; tautological clauses have no edges. +""" +from __future__ import annotations + +from collections import defaultdict +from dataclasses import dataclass +from itertools import combinations +from random import Random + +from .cnf_utils import CNFFormula + + +@dataclass(frozen=True) +class SignedConnection: + edges: int + components: int + cycle_rank: int + globally_balanced: bool + four_cycles: int + negative_four_cycles: int + negative_square_fraction: float + square_density: float + tautological_clauses: int + + +def _rows(formula: CNFFormula) -> list[dict[int, int]]: + """Each row: variable index (0-based) -> signed literal (+1/-1).""" + if not isinstance(formula.num_vars, int) or isinstance(formula.num_vars, bool) or formula.num_vars < 0: + raise ValueError('invalid declared variable count') + result = [] + for clause in formula.clauses: + signs: dict[int, int] = {} + tautology = False + for lit in clause: + if (not isinstance(lit, int) or isinstance(lit, bool) or + lit == 0 or abs(lit) > formula.num_vars): + raise ValueError('invalid literal') + var, sign = abs(lit) - 1, (1 if lit > 0 else -1) + if var in signs and signs[var] != sign: + tautology = True + signs[var] = sign + result.append({} if tautology else signs) + return result + + +def signed_connection(formula: CNFFormula, *, max_wedges: int = 250000) -> SignedConnection: + """Exact BFS Z2 switching obstruction and all signed four-cycles. + + A negative cycle obstructs a factorization s(c,v)=g(c)g(v) for all + incidences. This factorization is NOT equivalent to satisfiability. + Cost O(n+m+L+sum_v degree(v)^2), bounded by max_wedges. + """ + if max_wedges < 0: + raise ValueError('negative wedge budget') + rows = _rows(formula) + n, m = formula.num_vars, len(rows) + by_var: list[list[tuple[int,int]]] = [[] for _ in range(n)] + adj: list[list[tuple[int,int]]] = [[] for _ in range(n+m)] + edge_count = 0 + for ci, row in enumerate(rows): + for v, s in row.items(): + by_var[v].append((ci, s)) + adj[ci].append((m+v, s)) + adj[m+v].append((ci, s)) + edge_count += 1 + components = 0 + balanced = True + spins = [0] * (n + m) + for root in range(n + m): + if spins[root]: + continue + components += 1 + spins[root] = 1 + stack = [root] + while stack: + node = stack.pop() + for neighbor, sign in adj[node]: + expected = spins[node] * sign + if spins[neighbor] == 0: + spins[neighbor] = expected + stack.append(neighbor) + elif spins[neighbor] != expected: + balanced = False + wedges = sum(len(v)*(len(v)-1)//2 for v in by_var) + if wedges > max_wedges: + raise ValueError('signed square wedge budget exceeded') + # Clause-pair shared-variable wedge signs: a positive/negative pair + # creates a negative C4, regardless of variable or clause gauge flips. + wedge_signs: dict[tuple[int,int], list[int]] = defaultdict(lambda:[0,0]) + for entries in by_var: + for (c1,s1),(c2,s2) in combinations(entries,2): + counts = wedge_signs[(c1,c2)] + counts[0 if s1*s2 > 0 else 1] += 1 + four = sum((pos+neg)*(pos+neg-1)//2 for pos,neg in wedge_signs.values()) + neg_four = sum(pos*neg for pos,neg in wedge_signs.values()) + possible = (m*(m-1)//2) * (n*(n-1)//2) + taut_count = 0 + for original in formula.clauses: + literals = set(original) + taut_count += int(any(-lit in literals for lit in literals)) + return SignedConnection(edge_count, components, + edge_count - (m+n) + components, + balanced, four, neg_four, + neg_four / four if four else 0.0, + four / possible if possible else 0.0, + taut_count) + + +def connection_features(sig: SignedConnection) -> tuple[float, ...]: + """Five finite structural features; low-dimensional baseline augmentation.""" + return (sig.cycle_rank/max(sig.edges,1), + float(not sig.globally_balanced), + sig.negative_square_fraction, + sig.square_density, + sig.four_cycles/max(sig.edges,1)) + + +def margin_matched_sign_null(formula: CNFFormula, *, seed: int, + target_swaps: int = 32) -> tuple[CNFFormula, int]: + """Swap checkerboards; preserve clause support and BOTH sign margins. + + A 2x2 swap flips [[+,-],[-,+]] -> [[-,+],[+,-]] on edges of a + clause-variable square. Row and column positive counts remain fixed. + Unlike variable gauge flips this null need NOT preserve the SAT solution + set. It tests signed-incidence structure alone. Zero swaps = null failure. + """ + if not 0 <= target_swaps <= 1024: + raise ValueError('invalid swap budget') + # Restrict the null to simple clauses. Otherwise duplicate literals + # or tautologies would change the syntax or meaning on serialization. + for clause in formula.clauses: + if len({abs(lit) for lit in clause}) != len(clause): + raise ValueError('margin null requires distinct variables per clause') + rows = _rows(formula) + m = len(rows) + rng = Random(seed) + done = 0 + for _ in range(target_swaps*80): + if done >= target_swaps or m < 2: + break + c1,c2 = rng.sample(range(m),2) + one, two = rows[c1], rows[c2] + plus = [v for v,s in one.items() if s == 1 and two.get(v) == -1] + minus = [v for v,s in one.items() if s == -1 and two.get(v) == 1] + if not plus or not minus: + continue + u,v = rng.choice(plus), rng.choice(minus) + for c in (c1,c2): + rows[c][u] *= -1 + rows[c][v] *= -1 + done += 1 + # Preserve *clause and literal order* of the original as much as possible. + output = [] + for old, signs in zip(formula.clauses, rows): + output.append([signs[abs(lit)-1]*abs(lit) for lit in old]) + return CNFFormula(formula.num_vars,output),done From b7faca199e883229d5c30319f889de6fda0fdf82 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:01:51 +0100 Subject: [PATCH 16/48] experiment: train-family-held-out sign connection with relabeling-median DPLL oracle --- backend/violation_orbit.py | 171 +++++++++++++++++++++++++++++++++++++ 1 file changed, 171 insertions(+) create mode 100644 backend/violation_orbit.py diff --git a/backend/violation_orbit.py b/backend/violation_orbit.py new file mode 100644 index 0000000..e5c74d0 --- /dev/null +++ b/backend/violation_orbit.py @@ -0,0 +1,171 @@ +"""Hold-out family probe with relabeling-robust DPLL effort and signed incidence. + +The signed connection is computed BEFORE any DPLL calls. DPLL nodes are +research outcomes, never SAT verdicts or proof certificates. The checkerboard +null preserves support plus both clause and variable sign margins; it does +NOT preserve satisfiability in general, so it is ONLY a feature null. +""" +from __future__ import annotations + +from dataclasses import dataclass +from math import log2 +from random import Random +from statistics import mean, median +from time import perf_counter_ns + +import numpy as np + +from .cnf_utils import CNFFormula +from .violation_connection import (signed_connection, connection_features, + margin_matched_sign_null) +from .violation_cross_instance import (FAMILIES, STRUCTURAL, + generate_formula, structural_features, _dpll_search_nodes, _shuffle_vars) + +SIGNED = ('cycle_rank_per_edge', 'negative_cycle_obstruction', + 'negative_square_fraction', 'square_density', 'squares_per_edge') +NULL = tuple('null_' + x for x in SIGNED) +FEATURES = STRUCTURAL + SIGNED + NULL +INDICES = {name: i for i, name in enumerate(FEATURES)} +PREDICTORS = { + 'constant': (), + 'structure': STRUCTURAL, + 'structure+signed-connection': STRUCTURAL + SIGNED, + 'structure+margin-null': STRUCTURAL + NULL, + 'signed-only': SIGNED, +} + + +@dataclass(frozen=True) +class OrbitSample: + family: str + seed: int + features: tuple[float, ...] + raw_log_nodes: float + orbit_median_log_nodes: float + orbit_log_node_range: float + distinct_orbit_counts: int + successful_null_switches: int + structural_ns: int + signed_ns: int + null_ns: int + reference_ns: int + + +def orbit_effort(formula: CNFFormula, *, seed: int, + repeats: int = 8) -> tuple[float, float, int, float]: + """Median log2(1+search nodes) over reproducible signed relabelings. + + Finite Monte Carlo averaging is NOT exactly gauge invariant; its purpose + is to reduce lexicographic branch/phase artifacts in the measured target. + """ + if not 2 <= repeats <= 24: + raise ValueError('orbit repeats must be 2..24') + nodes = [_dpll_search_nodes(_shuffle_vars(formula, Random( + seed * 1000003 + 2009 * i + 17011))) for i in range(repeats)] + logs = [log2(1+x) for x in nodes] + return median(logs), max(logs)-min(logs), len(set(nodes)), mean(nodes) + + +def measure_orbit_record(formula: CNFFormula, family: str, seed: int, *, + repeats: int = 8, null_swaps: int = 32, + offset: int = 0) -> OrbitSample: + if family not in FAMILIES: + raise ValueError('unknown family') + start = perf_counter_ns() + base = structural_features(formula) + structural_ns = perf_counter_ns() - start + start = perf_counter_ns() + sign = connection_features(signed_connection(formula)) + signed_ns = perf_counter_ns() - start + start = perf_counter_ns() + null_formula, successful = margin_matched_sign_null( + formula, seed=seed + 331*offset + 173, target_swaps=null_swaps) + null_sign = connection_features(signed_connection(null_formula)) + null_ns = perf_counter_ns() - start + start = perf_counter_ns() + raw_nodes = _dpll_search_nodes(formula) + robust, spread, distinct, _ = orbit_effort( + formula, seed=seed + 10007 * (FAMILIES.index(family)+1) + offset*313, + repeats=repeats) + reference_ns = perf_counter_ns() - start + return OrbitSample(family,seed,base+sign+null_sign,log2(1+raw_nodes), + robust,spread,distinct,successful, + structural_ns,signed_ns,null_ns,reference_ns) + + +def _ridge_predict(train, test, columns, outcome): + y = np.array([getattr(v, outcome) for v in train], dtype=float) + if not columns: + return np.full(len(test), float(y.mean())) + positions = [INDICES[name] for name in columns] + a = np.array([[v.features[i] for i in positions] for v in train]) + b = np.array([[v.features[i] for i in positions] for v in test]) + mu,sd = a.mean(axis=0),a.std(axis=0) + sd[sd<1e-12] = 1.0 + a,b=(a-mu)/sd,(b-mu)/sd + a=np.column_stack((np.ones(len(a)),a)) + b=np.column_stack((np.ones(len(b)),b)) + penalty=np.diag([0.0]+[10.0]*len(positions)) + return b @ np.linalg.solve(a.T @ a + penalty,a.T @ y) + + +@dataclass(frozen=True) +class OrbitFold: + heldout_family: str + size: int + raw_mae: dict[str,float] + orbit_mae: dict[str,float] + median_orbit_spread: float + fraction_orbits_varying: float + null_switches_success: int + + +@dataclass(frozen=True) +class OrbitReport: + formulas: int + seed_count: int + orbit_repeats: int + folds: tuple[OrbitFold,...] + overall_raw_mae: dict[str,float] + overall_orbit_mae: dict[str,float] + median_feature_ms: float + median_structure_ms: float + median_reference_ms: float + fraction_nulls_with_switches: float + median_orbit_range: float + evidence: str = 'M: finite relabeling-averaged reference DPLL, no solver speed claim' + + +def orbit_holdout_benchmark(*,seed_count: int = 12, repeats: int = 8, + null_swaps: int = 32, offset: int = 0) -> OrbitReport: + if not 2 <= seed_count <= 32 or not 0 <= offset <= 100000: + raise ValueError('seed or offset budget exceeded') + dataset = [measure_orbit_record(generate_formula(fam,seed),fam,seed, + repeats=repeats,null_swaps=null_swaps,offset=offset) + for fam in FAMILIES for seed in range(seed_count)] + folds=[] + raw,orbit=({name:0.0 for name in PREDICTORS} for _ in range(2)) + for heldout in FAMILIES: + train=[v for v in dataset if v.family!=heldout] + test=[v for v in dataset if v.family==heldout] + by_target=[] + for target,acc in [('raw_log_nodes',raw),('orbit_median_log_nodes',orbit)]: + true=np.array([getattr(v,target) for v in test]) + loss={} + for name,cols in PREDICTORS.items(): + guess=_ridge_predict(train,test,cols,target) + loss[name]=float(np.mean(abs(guess-true))) + acc[name]+=len(test)*loss[name] + by_target.append(loss) + folds.append(OrbitFold(heldout,len(test),by_target[0],by_target[1], + median(v.orbit_log_node_range for v in test), + sum(v.distinct_orbit_counts>1 for v in test)/len(test), + sum(v.successful_null_switches>0 for v in test))) + return OrbitReport(len(dataset),seed_count,repeats,tuple(folds), + {key:value/len(dataset) for key,value in raw.items()}, + {key:value/len(dataset) for key,value in orbit.items()}, + median((v.structural_ns+v.signed_ns)/1e6 for v in dataset), + median(v.structural_ns/1e6 for v in dataset), + median(v.reference_ns/1e6 for v in dataset), + sum(v.successful_null_switches>0 for v in dataset)/len(dataset), + median(v.orbit_log_node_range for v in dataset)) From 22681e1e5995635195125bca456b0039e3f3c7c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:02:00 +0100 Subject: [PATCH 17/48] test: exact signed cycle calculus, gauge invariance and checkerboard sign margins --- backend/tests/test_violation_connection.py | 105 +++++++++++++++++++++ 1 file changed, 105 insertions(+) create mode 100644 backend/tests/test_violation_connection.py diff --git a/backend/tests/test_violation_connection.py b/backend/tests/test_violation_connection.py new file mode 100644 index 0000000..542314d --- /dev/null +++ b/backend/tests/test_violation_connection.py @@ -0,0 +1,105 @@ +"""Validate signed square transport and matched-null invariants.""" +from collections import Counter +from itertools import combinations +from random import Random + +import pytest + +from backend.cnf_utils import CNFFormula +from backend.violation_connection import ( + signed_connection, connection_features, margin_matched_sign_null) +from backend.violation_cross_instance import _shuffle_vars + + +def test_negative_and_positive_single_square(): + positive = signed_connection(CNFFormula(2,[[1,2],[1,2]])) + negative = signed_connection(CNFFormula(2,[[1,2],[1,-2]])) + assert (positive.four_cycles,positive.negative_four_cycles) == (1,0) + assert (negative.four_cycles,negative.negative_four_cycles) == (1,1) + assert positive.globally_balanced + assert not negative.globally_balanced + assert positive.cycle_rank == negative.cycle_rank == 1 + + +def test_negative_six_cycle_without_squares(): + # Three binary clauses sharing variables in a simple 6-cycle. + result = signed_connection(CNFFormula(3,[[1,2],[2,3],[3,-1]])) + assert result.four_cycles == 0 + assert not result.globally_balanced + assert result.cycle_rank == 1 + + +def test_sign_switch_relabel_and_clause_shuffle_gauge(): + f = CNFFormula(4,[[1,2,-3],[1,-2,4],[-1,-3,4],[2,3,-4]]) + orig = signed_connection(f) + for seed in range(15): + image = _shuffle_vars(f,Random(seed)) + new = signed_connection(image) + assert orig == new + assert len(connection_features(orig)) == 5 + + +def test_tautological_clauses_are_not_obstructions(): + f = CNFFormula(2,[[1,-1,2],[1,2]]) + r = signed_connection(f) + assert r.tautological_clauses == 1 + assert r.four_cycles == 0 + assert r.globally_balanced + + +def _margins(f): + return (tuple(Counter(abs(lit) for lit in c) for c in f.clauses), + tuple(sum(lit>0 for lit in c) for c in f.clauses), + tuple(sum(lit>0 for c in f.clauses for lit in c if abs(lit)==v) + for v in range(1,f.num_vars+1))) + + +def test_checkerboard_null_preserves_both_sign_margins(): + f=CNFFormula(3,[[1,-2,3],[-1,2,-3],[1,-2,-3],[-1,2,3]]) + p=_margins(f) + out,done = margin_matched_sign_null(f,seed=4,target_swaps=20) + assert done > 0 + assert _margins(out) == p + assert signed_connection(out).edges == signed_connection(f).edges + assert margin_matched_sign_null(f,seed=4,target_swaps=20) == (out,done) + + +def test_null_noop_and_bounds(): + f=CNFFormula(2,[[1],[2]]) + same,done = margin_matched_sign_null(f,seed=1,target_swaps=10) + assert done == 0 and same==f + with pytest.raises(ValueError): + margin_matched_sign_null(CNFFormula(1,[[1,-1]]),seed=1) + with pytest.raises(ValueError): + signed_connection(CNFFormula(1,[[2]])) + with pytest.raises(ValueError): + signed_connection(CNFFormula(2,[[1,2],[1,-2]]),max_wedges=0) + + +def test_signed_square_count_against_literal_four_cycle_enumeration(): + rng=Random(20261029) + for _ in range(120): + n,m=rng.randint(1,5),rng.randint(1,6) + clauses=[] + for _ in range(m): + vs=rng.sample(range(1,n+1),rng.randint(0,n)) + clauses.append([v*rng.choice((-1,1)) for v in vs]) + f=CNFFormula(n,clauses) + s=signed_connection(f) + total=negative=0 + for c1,c2 in combinations(f.clauses,2): + one={abs(l):1 if l>0 else -1 for l in c1} + two={abs(l):1 if l>0 else -1 for l in c2} + for v,w in combinations(one.keys()&two.keys(),2): + total+=1 + negative+=int(one[v]*one[w]*two[v]*two[w]==-1) + assert (s.four_cycles,s.negative_four_cycles)==(total,negative) + + +def test_balanced_connection_has_no_semantic_sat_implication(): + # UNSAT conjunction of unit clauses: acyclic and thus balanced. + unsat=signed_connection(CNFFormula(1,[[1],[-1]])) + assert unsat.globally_balanced + # SAT CNF with an unbalanced square: set x=True. + sat=signed_connection(CNFFormula(2,[[1,2],[1,-2]])) + assert not sat.globally_balanced From df797c6d7be8c76b43162b12ecffcbad4abff96c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:02:08 +0100 Subject: [PATCH 18/48] test: signed relabeling changes DPLL nodes but preserves connection; hold-out nulls --- backend/tests/test_violation_orbit.py | 64 +++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 backend/tests/test_violation_orbit.py diff --git a/backend/tests/test_violation_orbit.py b/backend/tests/test_violation_orbit.py new file mode 100644 index 0000000..ac17b29 --- /dev/null +++ b/backend/tests/test_violation_orbit.py @@ -0,0 +1,64 @@ +"""Orbit target is separately sampled; structural features precede oracle calls.""" +from math import isfinite +from random import Random + +import pytest + +from backend.violation_cross_instance import generate_formula, _dpll_search_nodes, _shuffle_vars +from backend.violation_connection import signed_connection, connection_features +from backend.violation_orbit import ( + orbit_effort, orbit_holdout_benchmark, measure_orbit_record, PREDICTORS) + + +def test_same_cnf_changed_dpll_cost_by_signed_renaming(): + f=generate_formula('random-3SAT',0) + original=_dpll_search_nodes(f) + image=[_dpll_search_nodes(_shuffle_vars(f,Random(1000+j))) for j in range(40)] + assert original == 7 + assert min(image) == 7 + assert max(image) == 21 + assert len(set(image)) > 1 + assert all(signed_connection(f)==signed_connection(_shuffle_vars(f,Random(j))) + for j in range(10)) + + +def test_relabeling_orbit_is_finite_and_repeatable(): + f=generate_formula('random-3SAT',0) + a=orbit_effort(f,seed=9,repeats=6) + assert a==orbit_effort(f,seed=9,repeats=6) + assert a[1]>=0 and 1<=a[2]<=6 + assert a[3]>=1 + with pytest.raises(ValueError): orbit_effort(f,seed=9,repeats=1) + + +def test_feature_production_precedes_reference_oracle(monkeypatch): + from backend import violation_orbit as mod + f=generate_formula('random-3SAT',0) + expected = (mod.structural_features(f) + + connection_features(signed_connection(f))) + def stop_oracle(_): + assert expected[:9]==mod.structural_features(f) + raise RuntimeError('target called') + monkeypatch.setattr(mod,'_dpll_search_nodes',stop_oracle) + with pytest.raises(RuntimeError,match='target called'): + mod.measure_orbit_record(f,'random-3SAT',0,repeats=2,null_swaps=0) + + +def test_small_cross_family_holdout_runs_with_matched_controls(): + report=orbit_holdout_benchmark(seed_count=2,repeats=3,null_swaps=4) + assert report.formulas==12 + assert len(report.folds)==6 + assert set(report.overall_raw_mae)==set(PREDICTORS) + assert set(report.overall_orbit_mae)==set(PREDICTORS) + assert all(isfinite(x) and x>=0 for x in report.overall_orbit_mae.values()) + assert 0 <= report.fraction_nulls_with_switches <= 1 + assert report.median_feature_ms>=0 + assert report.median_reference_ms>=0 + + +def test_orbit_features_are_baseline_compatible(): + f=generate_formula('random-3XOR',2) + r=measure_orbit_record(f,'random-3XOR',2,repeats=3,null_swaps=4) + assert len(r.features)==19 + assert r.raw_log_nodes>=1.0 + assert 0 <= r.successful_null_switches <= 4 From cb7d378465036852907d5a7473d7c589274f4ec0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:02:31 +0100 Subject: [PATCH 19/48] benchmark: reproducible six-family signed connection and orbit-normalized DPLL probe --- docs/ladder/scripts/violation_orbit_probe.py | 70 ++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 docs/ladder/scripts/violation_orbit_probe.py diff --git a/docs/ladder/scripts/violation_orbit_probe.py b/docs/ladder/scripts/violation_orbit_probe.py new file mode 100644 index 0000000..fabb602 --- /dev/null +++ b/docs/ladder/scripts/violation_orbit_probe.py @@ -0,0 +1,70 @@ +"""Reproducible Z2 signed-connection pilot with orbit-averaged DPLL targets. + +Run: python docs/ladder/scripts/violation_orbit_probe.py --seeds 12 --offsets 3 +The experiment is diagnostic, not a SAT solver or continuous Kakeya theorem. +""" +from __future__ import annotations + +import argparse +import json +import sys +from dataclasses import asdict +from pathlib import Path +from statistics import mean, median + +sys.path.insert(0,str(Path(__file__).resolve().parents[3])) +from backend.violation_orbit import PREDICTORS, orbit_holdout_benchmark + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--seeds',type=int,default=12,help='formula seeds per family, 2..32') + parser.add_argument('--orbits',type=int,default=8,help='signed relabelings, 2..24') + parser.add_argument('--null-swaps',type=int,default=32,help='margin-preserving attempted swaps') + parser.add_argument('--offsets',type=int,default=3,help='independent relabeling and null seeds, 1..16') + parser.add_argument('--json',action='store_true') + args=parser.parse_args() + if not 1 <= args.offsets <= 16: + parser.error('offsets must be in 1..16') + reports=[orbit_holdout_benchmark(seed_count=args.seeds,repeats=args.orbits, + null_swaps=args.null_swaps,offset=i) for i in range(args.offsets)] + summaries={} + for target in ('overall_raw_mae','overall_orbit_mae'): + base=[getattr(r,target)['structure'] for r in reports] + summaries[target]={ + key:{'mean_mae':mean(getattr(r,target)[key] for r in reports), + 'wins_vs_structural':sum(getattr(r,target)[key] < getattr(r,target)['structure'] + for r in reports), + 'mean_delta_vs_structural':mean(getattr(r,target)[key]-base[i] + for i,r in enumerate(reports))} + for key in PREDICTORS} + payload={'claim':'M: finite exploratory DPLL node prediction, not SAT speed or Kakeya bound', + 'parameters':vars(args),'total_formulas':reports[0].formulas, + 'mean_median_orbit_range':mean(r.median_orbit_range for r in reports), + 'mean_fraction_nulls_with_switches':mean(r.fraction_nulls_with_switches for r in reports), + 'median_structural_ms':median(r.median_structure_ms for r in reports), + 'median_feature_ms':median(r.median_feature_ms for r in reports), + 'median_orbit_reference_ms':median(r.median_reference_ms for r in reports), + 'averages':summaries, + 'replicates':[asdict(r) for r in reports]} + if args.json: + print(json.dumps(payload,indent=2)) + return + print('Z2 factor-graph connection; held-out generator families, relabeling-median DPLL nodes') + print('formulas per offset:',payload['total_formulas'],'; offsets:',args.offsets) + for target,rows in summaries.items(): + print(target) + for name,v in rows.items(): + print(' %-35s MAE %.4f ; delta %+0.4f ; wins %d/%d' % ( + name,v['mean_mae'],v['mean_delta_vs_structural'], + v['wins_vs_structural'],args.offsets)) + print('median log-node orbit range: %.3f ; fraction with mobile sign null: %.3f' % ( + payload['mean_median_orbit_range'],payload['mean_fraction_nulls_with_switches'])) + print('median feature: %.3f ms; baseline: %.3f ms; orbit reference: %.3f ms' % ( + payload['median_feature_ms'],payload['median_structural_ms'], + payload['median_orbit_reference_ms'])) + print('Note: finite orbit samples are not exactly coordinate invariant; --json has all folds.') + + +if __name__=='__main__': + main() From b713bc31a01a01b0a95b3c1b4f6b2d7df2f8490a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:02:44 +0100 Subject: [PATCH 20/48] ci: test signed cycle and orbit holdouts, upload reproducible negative evidence --- .github/workflows/violation-geometry-lab.yml | 53 ++++++++++++++------ 1 file changed, 39 insertions(+), 14 deletions(-) diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml index 24d1517..be62034 100644 --- a/.github/workflows/violation-geometry-lab.yml +++ b/.github/workflows/violation-geometry-lab.yml @@ -12,6 +12,9 @@ on: - "docs/ladder/*VIOLATION*" - ".github/workflows/violation-geometry-lab.yml" +permissions: + contents: read + jobs: finite-evidence: runs-on: ubuntu-latest @@ -22,24 +25,46 @@ jobs: python-version: "3.12" - name: Install bounded probe dependencies run: python -m pip install "numpy>=1.24" "pytest>=7.4" - - name: Run mathematical, sampling and isolation tests + - 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 - - name: Reproduce leave-one-family-out results and null controls + backend/tests/test_violation_cross_instance.py \ + backend/tests/test_violation_connection.py \ + backend/tests/test_violation_orbit.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_cross_instance_probe.py --seed-count 12 --replicates 2 --json > /tmp/violation_geometry_report.json + python docs/ladder/scripts/violation_orbit_probe.py \ + --seeds 12 --orbits 8 --null-swaps 32 --offsets 3 \ + --json > evidence/orbit_connection.json python - <<'PY' - import json, math - with open("/tmp/violation_geometry_report.json", encoding="utf-8") as fh: - report = json.load(fh) - assert report["instances_per_replicate"] == 72 - assert len(report["families"]) == 6 - assert len(report["runs"]) == 2 - for name, stats in report["aggregate"].items(): - assert math.isfinite(stats["mean_mae_log2_nodes"]), name - assert stats["mean_mae_log2_nodes"] >= 0, name - print("Bounded hold-out report and controls are well formed; no solver speed claim.") + 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 + 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 From 998379af9f0ee70542ff471bb37604ee97a62a92 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:03:50 +0100 Subject: [PATCH 21/48] research: count balanced components for exact Z2 Laplacian nullity identity --- backend/violation_connection.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/backend/violation_connection.py b/backend/violation_connection.py index 023adf3..32d272b 100644 --- a/backend/violation_connection.py +++ b/backend/violation_connection.py @@ -25,6 +25,7 @@ class SignedConnection: negative_square_fraction: float square_density: float tautological_clauses: int + balanced_components: int def _rows(formula: CNFFormula) -> list[dict[int, int]]: @@ -69,6 +70,7 @@ def signed_connection(formula: CNFFormula, *, max_wedges: int = 250000) -> Signe edge_count += 1 components = 0 balanced = True + balanced_components = 0 spins = [0] * (n + m) for root in range(n + m): if spins[root]: @@ -76,6 +78,7 @@ def signed_connection(formula: CNFFormula, *, max_wedges: int = 250000) -> Signe components += 1 spins[root] = 1 stack = [root] + component_balanced = True while stack: node = stack.pop() for neighbor, sign in adj[node]: @@ -85,6 +88,8 @@ def signed_connection(formula: CNFFormula, *, max_wedges: int = 250000) -> Signe stack.append(neighbor) elif spins[neighbor] != expected: balanced = False + component_balanced = False + balanced_components += int(component_balanced) wedges = sum(len(v)*(len(v)-1)//2 for v in by_var) if wedges > max_wedges: raise ValueError('signed square wedge budget exceeded') @@ -107,7 +112,7 @@ def signed_connection(formula: CNFFormula, *, max_wedges: int = 250000) -> Signe balanced, four, neg_four, neg_four / four if four else 0.0, four / possible if possible else 0.0, - taut_count) + taut_count, balanced_components) def connection_features(sig: SignedConnection) -> tuple[float, ...]: From 7359ccc39570b51203a05aad1ad7a1dc8f807056 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:03:56 +0100 Subject: [PATCH 22/48] math: explicit finite Z2 signed graph Laplacian and nonnegative edge energy --- backend/violation_laplacian.py | 46 ++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 backend/violation_laplacian.py diff --git a/backend/violation_laplacian.py b/backend/violation_laplacian.py new file mode 100644 index 0000000..db3e45a --- /dev/null +++ b/backend/violation_laplacian.py @@ -0,0 +1,46 @@ +"""Exact finite Z2 signed graph connection Laplacian for clause-variable frames. + +This is NOT the continuous Euclidean wave-equation operator and is not +an extension of OpenAI's Kakeya theorem. It is a separate finite matrix +whose nullity is controlled by signed graph cycle balance. Not a SAT solver. +""" +from __future__ import annotations + +from typing import Sequence +import numpy as np + +from .cnf_utils import CNFFormula +from .violation_connection import _rows + + +def signed_laplacian(formula: CNFFormula, *, max_vertices: int=64) -> np.ndarray: + """L = D - A_s for the signed clause-variable bipartite graph. + + For real z, z.T L z = sum_edges (z_clause-sign*z_variable)^2 >=0. + The kernel has one dimension for each balanced connected component, + including isolated nodes; unbalanced components contribute zero. + This is a finite graph identity, not a solver certificate. + """ + rows=_rows(formula) + m,n=len(rows),formula.num_vars + if not isinstance(max_vertices,int) or max_vertices<0 or n+m>max_vertices: + raise ValueError('laplacian vertex budget exceeded') + L=np.zeros((n+m,n+m),dtype=np.float64) + for ci,row in enumerate(rows): + for v,sign in row.items(): + j=m+v + L[ci,ci]+=1 + L[j,j]+=1 + L[ci,j]-=sign + L[j,ci]-=sign + return L + + +def signed_energy(formula: CNFFormula, vector: Sequence[float]) -> float: + """Return the exact edge-energy expression for a real node vector.""" + rows=_rows(formula) + m,n=len(rows),formula.num_vars + if len(vector)!=m+n: + raise ValueError('expected one real coordinate per clause/variable node') + return sum((vector[ci]-sign*vector[m+v])**2 + for ci,row in enumerate(rows) for v,sign in row.items()) From 8afbfcf1681e1284c6a1a8e83a77c2572ce110f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:04:04 +0100 Subject: [PATCH 23/48] test: energy identity, PSD, nullity equals balanced components, gauge spectrum --- backend/tests/test_violation_laplacian.py | 54 +++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 backend/tests/test_violation_laplacian.py diff --git a/backend/tests/test_violation_laplacian.py b/backend/tests/test_violation_laplacian.py new file mode 100644 index 0000000..d1c357e --- /dev/null +++ b/backend/tests/test_violation_laplacian.py @@ -0,0 +1,54 @@ +"""Numerical differential checks of the elementary Z2 graph Laplacian theorem.""" +from random import Random +import numpy as np +import pytest +from backend.cnf_utils import CNFFormula +from backend.violation_connection import signed_connection +from backend.violation_laplacian import signed_laplacian, signed_energy +from backend.violation_cross_instance import _shuffle_vars + + +def test_laplacian_quadratic_energy_and_psd(): + rng=Random(14) + for _ in range(100): + n,m=rng.randrange(0,5),rng.randrange(0,5) + clauses=[] + for j in range(m): + vv=rng.sample(range(1,n+1),rng.randrange(n+1)) + clauses.append([v*rng.choice((-1,1)) for v in vv]) + f=CNFFormula(n,clauses) + L=signed_laplacian(f) + z=np.array([rng.uniform(-2,2) for j in range(n+m)]) + assert np.allclose(L,L.T) + assert np.isclose(z @ L @ z,signed_energy(f,z),atol=1e-10) + ev=np.linalg.eigvalsh(L) + assert all(x>=-1e-9 for x in ev) + expected=signed_connection(f).balanced_components + assert sum(abs(x)<1e-8 for x in ev)==expected + + +def test_balanced_vs_unbalanced_nullity(): + good=CNFFormula(2,[[1,2],[1,2]]) + bad=CNFFormula(2,[[1,2],[1,-2]]) + assert signed_connection(good).balanced_components==1 + assert signed_connection(bad).balanced_components==0 + assert sum(abs(x)<1e-9 for x in np.linalg.eigvalsh(signed_laplacian(good)))==1 + assert sum(abs(x)<1e-9 for x in np.linalg.eigvalsh(signed_laplacian(bad)))==0 + # A satisfiability contradiction need not create graph holonomy. + unsat=CNFFormula(1,[[1],[-1]]) + assert signed_connection(unsat).balanced_components==1 + + +def test_gauge_relabelings_preserve_eigenvalues(): + f=CNFFormula(4,[[1,2,-3],[1,-2,4],[-1,-3,4],[2,3,-4]]) + original=np.linalg.eigvalsh(signed_laplacian(f)) + for seed in range(20): + relabeled=_shuffle_vars(f,Random(seed)) + current=np.linalg.eigvalsh(signed_laplacian(relabeled)) + assert np.allclose(original,current,atol=1e-10) + + +def test_safe_laplacian_bounds(): + with pytest.raises(ValueError):signed_laplacian(CNFFormula(80,[])) + with pytest.raises(ValueError):signed_laplacian(CNFFormula(1,[[0]])) + with pytest.raises(ValueError):signed_energy(CNFFormula(1,[[1]]),[1]) From 4cfae991ba295095398f246d3f9457af05323198 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:04:40 +0100 Subject: [PATCH 24/48] research report: finite Z2 connection theorem, observer-invariant DPLL audit, matched null failure --- ...IOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md diff --git a/docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md b/docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md new file mode 100644 index 0000000..c646fcf --- /dev/null +++ b/docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md @@ -0,0 +1,81 @@ +# The signed incidence connection and the relabeling orbit: an ETH/Kakeya bridge audit + +**29 October 2026 | development branch: dev/kakeya-violation-frame | source: [lambda-sat-solver](../../README.md).** + +Evidence typing: **P** = elementary finite signed-graph identities, with an explicit proof below and numerical verification, **M** = small synthetic measurements, **R** = failed predictive lift *within the tested scope*, **S/H** = prospective analogy/bridge to wave smoothing, Kakeya, n-manifold geometry, SAT complexity or solver runtime. None of these is a formal Lean proof or an asymptotic SAT result. + +## Why relabel the observer, not only the formula? + +The previous cross-instance target was log2(1+DPLL recursive calls) for a fixed lexicographic variable order and False-first phase. Its cost changes under Boolean-variable permutation and complement, although satisfiability and the abstract formula are unchanged. + +Witness: one generated random-3SAT instance (generator seed 0) takes 7 recursive calls in its original presentation; on 40 seeded logically equivalent signed relabelings, it takes 7 to 21 calls. The original target was thus partly a property of the *coordinate/branching convention*. This does not invalidate its earlier negative result; it narrows its meaning. + +The new target samples 8 reproducible signed variable relabelings and takes the median of log2(1+DPLL nodes). **A finite sampled orbit median is not an exactly gauge-invariant functional.** It reduces dependence on the arbitrary representation; no claim of continuous Hamiltonian, holonomy flow, or quantum computation is implied. + +## A genuinely typed finite connection + +Normalize repeated literals and ignore tautological clauses. Define a bipartite factor graph with clause vertices C, variable vertices V and signed edge sigma(c,v) in {+1,-1} recording literal polarity. For any closed factor-graph walk gamma, set + + H(gamma) = product_{e in gamma} sigma(e) in {+1,-1}. + +A negative cycle H=-1 is an obstruction to finding vertex spins g(node) in {+1,-1} satisfying sigma(c,v)=g(c)g(v) on every edge. Conversely, if all cycle products equal +1, a spanning-forest propagation constructs those spins. This equivalence follows directly from path multiplication; it is not a SAT contradiction theorem. + +For a clause pair c=6 even when no 4-cycles exist. + +The actual finite connection Laplacian is L_sigma = D - A_sigma, where A_sigma is the symmetric signed adjacency matrix of that bipartite graph. For any real node vector z, + + z^T L_sigma z = sum_{(c,v) edge} (z_c - sigma(c,v) z_v)^2 >= 0. + +Hence L_sigma is positive semidefinite. On a connected component, the energy is zero exactly when all edge relations z_c=sigma(c,v)z_v hold. If the component is balanced this leaves one free real scalar (kernel dimension 1); if it has a negative cycle all coordinates must vanish (kernel dimension 0). **Therefore nullity(L_sigma) equals the number of balanced connected components**, isolated vertices included. + +Gauge switching sigma'_{uv}=g_u sigma_{uv}g_v yields L_sigma'=G L_sigma G, preserving the eigenvalue multiset. Variable complementation and permutations give particular such transformations plus vertex permutations. Note that switching *clause* signs is a valid graph gauge transformation but is not generally a semantics-preserving Boolean formula transformation. + +Tests include 100 seeded small matrices comparing the edge-sum energy with z^T L z, PSD/eigenvalue nullity, 120 randomly generated CNFs checking four-cycle counts against independent enumeration, and signed-relabeling invariance. + +**Boundary:** a balanced factor graph may encode an UNSAT CNF (x AND not-x), and an unbalanced graph may encode a SAT CNF ((x OR y) AND (x OR not-y)). Nullity and negative holonomy cannot be used for certified SAT/UNSAT decisions. + +## Matched controls borrowed from the Canary direction, not its unverifiable claims + +Control 1: the nine classical structural predictors already include clause width, density, literal polarity imbalance, variable degree dispersion and XOR pattern recognition. The variance feature is inspired by the private Canary flavor analyzer; the claimed Z2xZ2/A4 symmetry tags are not imported. + +Control 2: seeded **checkerboard sign switches** on two clauses sharing two variables, changing [[+,-],[-,+]] into [[-,+],[+,-]]. These preserve every clause's positive literal count, every variable's positive occurrence count, the entire unsigned clause-variable incidence, clause widths and degrees. They are a matched *feature null*, not a semantics-preserving SAT transformation. A null with **zero successful switches is not a useful randomization control**. In the toy corpus, only about 72%-74% of formulas admit at least one switch with the chosen budget; the pigeonhole family has zero. The report explicitly tracks this failure. + +All six generator families are held out in turn; model fitting and standardization occur only on the other five. We compare a constant, the classical structural baseline, structure+signed connection, structure+margin-matched null, and signed connection alone. Fixed ridge penalty alpha=10. No solver result influences feature extraction. + +## Exploratory local measurements (M) + +Across 10 **orientation/null-seed offsets** of the *same generated formula set*, 8 signed-relabeling DPLL runs per formula, and 32 target checkerboard switches. Entries are LOFO mean absolute prediction error on log2(1+DPLL recursive calls); **lower is better**. + +| Formulas (6 families) | Raw target: structural / signed / null | Orbit-median target: structural / signed / null | Signed wins vs structural (10 offsets) | +|---|---|---|---| +| 72 | 0.67735 / 0.71387 / 0.70533 | **0.57845** / 0.64165 / 0.63634 | 0/10 | +| 144 | 0.64016 / 0.65144 / 0.64089 | **0.53892** / 0.60951 / 0.60693 | 0/10 | +| 192 | 0.61441 / 0.67751 / 0.67863 | **0.55051** / 0.64702 / 0.64601 | 0/10 | + +At 192 formulas the raw reference median varies by about 0.94 log2 units across relabelings for a typical instance (median range across the 10 offsets). Across all 3 corpus sizes, the signed connection underperforms the classical structure-only predictor on the orbit target, and the margin-matched sign null performs similarly to the measured signed connection. Some individual held-out families show minor gains, but the losses on other families dominate; family templates are small and repeated. + +Illustrative local Python 3.13 timing for 192 formulas: median classical feature extraction about **0.068 ms**, signed+classical feature extraction about **0.268 ms**, and 8-run orbit reference computation about **1.04 ms**. These are not comparable production solver timings. The null randomization cost is *not* included in the signed feature's stated cost, because it is a diagnostic control rather than a proposed routing feature. + +The 72-formula results are reproduced in dedicated branch CI with raw machine-readable JSON retained as an artifact; larger 144/192 runs are available from the same code and commands. Ten offsets on the same base formula set do **not** constitute ten independent held-out datasets. The small PHP corpus cycles through three base sizes, and the Tseitin corpus cycles through three graph topologies. We cannot infer population confidence intervals from the repeated offsets alone. + +**R, bounded:** retire the claim that this specific signed-incidence/4-cycle connection predicts held-out toy DPLL effort better than conventional structural features. This supersedes the attempt to rescue the earlier centered parity-pass spectrum with another scalar. Keep the finite spectral and gauge identities as P. + +## Commands + + python -m pytest -q backend/tests/test_violation_connection.py backend/tests/test_violation_laplacian.py backend/tests/test_violation_orbit.py + python docs/ladder/scripts/violation_orbit_probe.py --seeds 12 --offsets 3 --json + python docs/ladder/scripts/violation_orbit_probe.py --seeds 24 --offsets 10 --json + python docs/ladder/scripts/violation_orbit_probe.py --seeds 32 --offsets 10 --json + +All runs are deterministic modulo elapsed-time measurements and standard numerical tolerances. + +## What remains open (H) + +The next useful test is not another feature expansion on these six families. Build genuinely unseen graph topology generators (multiple cubic expanders, distinct community graphs, nonisomorphic PHP generalizations), preserve a large-n view, and use external certified CDCL runtime with all feature costs charged. Pre-register which feature predicts what, against degree/width/sign-matched nulls that actually mix. If the goal is a Kakeya or local smoothing lift, specify a valid finite-to-continuous oscillatory extension operator and an estimate; the finite Z2 connection Laplacian alone does not supply it. + +References: [ETH paper](https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf), [local smoothing/Kakeya paper](https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf), [prior negative report](VIOLATION_CROSS_INSTANCE_REPORT.md). From 3d4daf76eacdd8987f0cd60296b0b7e4016d347f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:04:49 +0100 Subject: [PATCH 25/48] ci: verify Z2 Laplacian identity and archive 192-formula 10-seed orbit evidence --- .github/workflows/violation-geometry-lab.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml index be62034..206da77 100644 --- a/.github/workflows/violation-geometry-lab.yml +++ b/.github/workflows/violation-geometry-lab.yml @@ -32,7 +32,8 @@ jobs: 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_orbit.py \ + backend/tests/test_violation_laplacian.py - name: Reproduce assignment-held-out controls run: | mkdir -p evidence @@ -43,6 +44,9 @@ jobs: 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 @@ -54,6 +58,10 @@ jobs: 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") From 0ff606cf21d0cb458b43ae51f0b2e698fe17e467 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 18:05:15 +0100 Subject: [PATCH 26/48] docs: expose Z2 connection theorem and orbit audit without erasing negative results --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0fac1ac..04b2381 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ Headless. No web UI. No *trust-me*. -> **Experimental development branch — ETH × Kakeya incidence:** the [finite cross-instance report](docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md) keeps a **negative** result visible: after holding out entire small CNF families, learned overlap and signed-cycle statistics do not outperform classical structural predictors of a reference DPLL's search nodes. Mathematical invariants are not algorithmic speedups. The [initial bridge](docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md) is preserved, not rewritten to hide its limitations. No production solver decisions are changed. +> **Experimental development branch — ETH × Kakeya incidence:** the [initial bridge](docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md) and its [cross-instance negative result](docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md) remain in the record. Our latest [signed-connection and observer-orbit audit](docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md) distinguishes two things: a finite, gauge-invariant graph Laplacian identity that can be proved, and a proposed SAT-hardness predictor that still loses to classical structure on held-out small formulas. A moving frame should not mistake the observer's variable ordering for the formula's intrinsic difficulty. These are research instruments, **not** new solver certificates or asymptotic hardness results; no production decision path is changed. 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 From 0099bb9ed439079cfc1d2ba1349dd4bfeb1aefb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:42:32 +0100 Subject: [PATCH 27/48] research: preregister held-out topology CDCL benchmark and falsification gates --- docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md diff --git a/docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md b/docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md new file mode 100644 index 0000000..b5071ea --- /dev/null +++ b/docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md @@ -0,0 +1,21 @@ +# CDCL topology-transfer experiment: pre-registered design + +Date: 2026-10-29. Branch: `dev/kakeya-violation-frame`. Previous, superseding evidence: [signed-orbit report](VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md). Status **H** until an external CDCL runner produces machine-readable **M**. The prior learned incidence and signed-connection predictors lost to classical structure in small DPLL tests; do not erase that conclusion. + +**Research question.** On *independently generated and non-identical* CNFs larger than the 12-variable truth-table pilots, does signed clause-variable holonomy improve out-of-generator and out-of-size prediction of CDCL work, beyond unsigned topology, variable degree and polarity structure? The object is the finite signed incidence graph. This is neither the Kakeya maximal theorem nor a SAT complexity theorem. + +**Frozen data/target.** Generators: uniform random 3-CNF, local ring 3-CNF, four-community 3-CNF, hub-biased 3-CNF, degree-three prism Tseitin, and reconnected degree-three Tseitin. Declared Boolean variables per formula 48, 72, 96; formula seeds independent and documented. The Tseitin generators use cubic graphs with 32, 48 or 64 vertices, respectively; charges are deliberately even/odd by seed to test SAT and UNSAT conditions without using solver labels for features. We shall also inspect non-isomorphism of distinct seeded cubic graph instances, not just their raw labeled edge lists. + +Run PySAT Glucose4 (`g4`) as an *external experimental CDCL instrument*, with fixed per-call conflict budget (default 2,000), three signed relabelings (same formula, independent solver start per orientation) and no previously learnt clauses shared across runs. Record reported conflicts, decisions, propagations, result (SAT/UNSAT/UNKNOWN), per-call wall time and total feature time. SAT model, when present, must replay on that **input** CNF; UNSAT from the external solver is a benchmark observation, not a λSAT certified result. UNKNOWN is **right censored**, never mislabeled as easy or as a decision. The primary target is log2(1+min(reported conflicts, budget)) and the censoring fraction is reported beside every error. Do not treat this budgeted statistic as an uncensored latent true conflict count. + +**Predictors and fair controls.** Frozen ridge regression penalty alpha=10 and train-only feature scaling. Baseline: declared n, m/n, clause width, variable occurrence CV/maximum, polarity imbalance, XOR-clause-pattern fraction, plus **unsigned** connected component count, cycle rank and four-cycle density. Experimental extras: signed negative 4-cycle fraction, unbalanced-component fraction and normalized negative-square count. Null: deterministic same-sign, degree- and polarity-margin-preserving support edge swaps. This null changes the formula semantics and graph topology, so is a **feature-null only**, not a SAT matching pair. Report successful switches; a zero-switch null is invalid and must not be counted as meaningful control. Solver outputs must never be used in feature extraction. + +**Splits.** Leave-one-generator-family-out (LOFO) and train on smaller n, test on the largest n. No re-training after inspection of held-out errors. Include both SAT and UNSAT where possible, but do not claim a balanced outcome distribution unless measured. Report per-family errors, unique graph topology checks, missing/UNKNOWN counts and feature-to-CDCL work overhead. + +**Primary prediction.** At least 0.03 reduction in mean absolute **log2-capped-conflicts** error over the full LOFO sample against baseline, and outperform the nontrivially mixing support-swapped null, with >=80% completed calls. Secondary prediction: incremental gain on the held-out largest n and extraction cost less than 10% of solver wall time at median. These are conservative *promotion gates*, not something CI should assert as a mandatory success. + +**Kill conditions.** If the signed features lose to the baseline or to the matched null, retire this specific prediction in the tested regime. If too many calls are censored, or null switches systematically fail, report **inconclusive**, not success or null equivalence. If the solver label, feature extraction or isomorphism gate leaks across splits, invalidate that run. If geometric features cost more than solving, no production routing promotion even if predictive accuracy improves. + +**Provenance and scope.** Canary contributes cheap degree statistics and family-stratified ablation, not inferred `A4` or `Z2×Z2` group identities; OpenAI ETH and Kakeya papers motivate questions but imply none of these CDCL predictions. No certified solver path, clause preprocessing, or `main` is changed. All evidence remains finite **M**, and algorithmic/general asymptotic claims remain **H**. + +Reproduction contract: small deterministic CI smoke suite plus raw JSON artifacts, with explicit versions for Python/PySAT and exact family, seed, n, solver, budgets, outcome coverage and feature time. The CI outcome is *validity* rather than a guaranteed geometry win. From b73e5e10f66c1b6083fb504fbed3e5c7496965d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:43:22 +0100 Subject: [PATCH 28/48] research: independent cubic topologies and capped external Glucose4 CDCL transfer benchmark --- backend/violation_cdcl_topology.py | 476 +++++++++++++++++++++++++++++ 1 file changed, 476 insertions(+) create mode 100644 backend/violation_cdcl_topology.py diff --git a/backend/violation_cdcl_topology.py b/backend/violation_cdcl_topology.py new file mode 100644 index 0000000..cd7edbe --- /dev/null +++ b/backend/violation_cdcl_topology.py @@ -0,0 +1,476 @@ +"""Held-out topology benchmark: finite signed graph features vs external CDCL effort. + +Fully independent of λSAT production routing and certification. PySAT Glucose4 +is an experimental CDCL oracle, not part of the trusted base. A conflict cap +produces censored UNKNOWN outcomes; all prediction targets are explicitly +budget-capped. No Kakeya, smoothing, NP-hardness or asymptotic claim follows. + +The source contract is docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md. +""" +from __future__ import annotations + +from dataclasses import asdict, dataclass +from hashlib import sha256 +from itertools import combinations, product +from math import log2, sqrt +from random import Random +from statistics import median +from time import perf_counter_ns +from typing import Callable, Sequence + +import numpy as np + +from .cnf_utils import CNFFormula +from .violation_connection import signed_connection +from .violation_cross_instance import _shuffle_vars, _xor_clauses + +FAMILIES = ("uniform3", "ring3", "community3", "hub3", + "tseitin-prism", "tseitin-rewired") +BASE = ("n", "clauses_per_variable", "mean_width", "binary_fraction", + "unit_fraction", "maximum_occurrence_per_variable", "degree_cv", + "literal_polarity_imbalance", "xor_pattern_fraction", + "components_per_variable", "unsigned_cycle_rank_per_edge", + "unsigned_squares_per_edge", "unsigned_square_density") +SIGN = ("negative_square_fraction", "negative_squares_per_edge", + "fraction_unbalanced_components", "unbalanced_any") +NULL = tuple("rewired_" + name for name in SIGN) +FEATURES = BASE + SIGN + NULL +COLS = {name: i for i, name in enumerate(FEATURES)} +PREDICTORS = { + "constant": (), + "classical": BASE, + "classical+signed": BASE + SIGN, + "classical+rewired-null": BASE + NULL, + "signed-only": SIGN, +} +RIDGE_ALPHA = 10.0 + + +def _connected(edges: set[tuple[int, int]], vertices: int) -> bool: + adj = [[] for _ in range(vertices)] + for a, b in edges: + adj[a].append(b) + adj[b].append(a) + seen, stack = {0}, [0] + while stack: + for v in adj[stack.pop()]: + if v not in seen: + seen.add(v) + stack.append(v) + return len(seen) == vertices + + +def cubic_graph(vertices: int, topology: str, seed: int) -> tuple[tuple[int, int], ...]: + """Connected, simple cubic prism, optionally degree-preserving rewired. + + The random-rewired family starts from a prism but its edge switches change + graph topology, not just variable labels or clause signs. + """ + if vertices < 8 or vertices % 2 or topology not in ("prism", "rewired"): + raise ValueError("cubic graph needs an even vertex count >=8 and a known topology") + half = vertices // 2 + edges: set[tuple[int, int]] = set() + def edge(a: int, b: int) -> tuple[int, int]: + return (min(a, b), max(a, b)) + for i in range(half): + edges.add(edge(i, (i + 1) % half)) + edges.add(edge(half + i, half + (i + 1) % half)) + edges.add(edge(i, half + i)) + if topology == "rewired": + rng = Random(seed + 90101) + accepted = 0 + for _ in range(vertices * 400): + if accepted >= vertices * 8: + break + first, second = rng.sample(sorted(edges), 2) + a, b = first + c, d = second + if len({a, b, c, d}) != 4: + continue + if rng.randrange(2): + new = {edge(a, c), edge(b, d)} + else: + new = {edge(a, d), edge(b, c)} + if len(new) < 2 or any(e in edges for e in new): + continue + trial = (edges - {first, second}) | new + if not _connected(trial, vertices): + continue + edges = trial + accepted += 1 + if accepted < vertices: + raise RuntimeError("cubic rewiring failed its nontriviality budget") + degree = [0] * vertices + for a, b in edges: + degree[a] += 1 + degree[b] += 1 + if len(edges) != 3 * vertices // 2 or any(d != 3 for d in degree) or not _connected(edges, vertices): + raise AssertionError("cubic graph contract violated") + return tuple(sorted(edges)) + + +def _weighted_sample3(rng: Random, n: int) -> list[int]: + weights = [1.0 / (v + 3) ** 0.7 for v in range(n)] + available = list(range(1, n + 1)) + output = [] + for _ in range(3): + k = rng.choices(range(len(available)), + weights=[weights[v - 1] for v in available], k=1)[0] + output.append(available.pop(k)) + return output + + +def generate_formula(family: str, size: int, seed: int) -> CNFFormula: + """Distinct seeded graphs at n=48/72/96 and small n=12 for theorem tests. + + Tseitin formulas have variable count 3*vertices/2 == size; clause count + 4*vertices. Their signed charges are consistent iff seed is even. + """ + if family not in FAMILIES or size < 12 or size % 3: + raise ValueError("unknown family or invalid variable size") + rng = Random(seed * 10007 + size * 421 + FAMILIES.index(family) * 1000003) + if family.startswith("tseitin-"): + vertices = 2 * size // 3 + edges = cubic_graph(vertices, "prism" if family.endswith("prism") else "rewired", seed) + charges = [rng.randrange(2) for _ in range(vertices)] + charges[-1] = (sum(charges[:-1]) + seed % 2) % 2 + clauses: list[list[int]] = [] + for vertex in range(vertices): + inc = [i+1 for i,(a,b) in enumerate(edges) if a == vertex or b == vertex] + if len(inc) != 3: + raise AssertionError("invalid cubic incidence") + clauses.extend(_xor_clauses(inc, charges[vertex])) + return CNFFormula(size, clauses) + + n = size + m = round(4.26 * n) + clauses = [] + seen = set() + radius = max(4, n // 12) + block_size = n // 4 + attempts = 0 + while len(clauses) < m: + attempts += 1 + if attempts > 200 * m: + raise RuntimeError("cannot generate enough distinct signed clauses") + if family == "uniform3": + variables = rng.sample(range(1,n+1), 3) + elif family == "ring3": + if rng.random() < 0.20: + variables = rng.sample(range(1,n+1), 3) + else: + center = rng.randrange(n) + pool = [((center + offset) % n) + 1 + for offset in range(-radius, radius+1)] + variables = rng.sample(pool, 3) + elif family == "community3": + if rng.random() < 0.15: + variables = rng.sample(range(1,n+1), 3) + else: + block = rng.randrange(4) + start = block * block_size + stop = n if block == 3 else start + block_size + variables = rng.sample(range(start+1, stop+1), 3) + else: + variables = _weighted_sample3(rng,n) + clause = [v*rng.choice((-1,1)) for v in variables] + key = tuple(sorted(clause)) + if key not in seen: + seen.add(key) + clauses.append(clause) + return CNFFormula(n,clauses) + + +def support_degree_sign_null(formula: CNFFormula, *, seed: int, + swaps: int = 160) -> tuple[CNFFormula,int]: + """Rewire two same-sign literal incidences; preserve exact sign margins. + + Keeps n, m, every clause width and +/- count, variable total degrees + and variable positive/negative occurrence counts. Unlike relabeling, it + can change SAT, signed topology and conflict work. Feature-null only. + """ + if not 0 <= swaps <= 2048: + raise ValueError("invalid swap budget") + clauses = [list(c) for c in formula.clauses] + if any(len({abs(l) for l in c}) != len(c) for c in clauses): + raise ValueError("null needs non-tautological simple clauses") + rng = Random(seed) + done = 0 + for _ in range(swaps*30): + if done >= swaps or len(clauses) < 2: + break + a,b = rng.sample(range(len(clauses)), 2) + if not clauses[a] or not clauses[b]: + continue + i,j = rng.randrange(len(clauses[a])),rng.randrange(len(clauses[b])) + la,lb = clauses[a][i],clauses[b][j] + if ((la > 0) != (lb > 0) or abs(la) == abs(lb) or + abs(la) in [abs(v) for v in clauses[b]] or + abs(lb) in [abs(v) for v in clauses[a]]): + continue + clauses[a][i], clauses[b][j] = lb,la + done += 1 + return CNFFormula(formula.num_vars,clauses),done + + +def _xor_pattern_fraction(formula: CNFFormula) -> float: + groups: dict[tuple[int,...],set[int]] = {} + for clause in formula.clauses: + vv = [abs(lit) for lit in clause] + if len(vv) not in (2,3) or len(set(vv)) != len(vv): + continue + vs = tuple(sorted(vv)) + signs = {abs(lit):lit<0 for lit in clause} + mask = sum(1< tuple[float,...]: + n,m = formula.num_vars,len(formula.clauses) + if n < 1: + raise ValueError("zero declared variables") + widths = [len(c) for c in formula.clauses] + pos,neg=[0]*n,[0]*n + for c in formula.clauses: + for lit in c: + if not 1<=abs(lit)<=n: + raise ValueError("literal outside declared variables") + (pos if lit>0 else neg)[abs(lit)-1] += 1 + deg = [a+b for a,b in zip(pos,neg)] + avg = sum(deg)/n + cv = sqrt(sum((x-avg)**2 for x in deg)/n)/max(avg,1.) + return (float(n),m/n, + sum(widths)/max(m,1),sum(w==2 for w in widths)/max(m,1), + sum(w==1 for w in widths)/max(m,1), + max(deg,default=0)/n,cv, + sum(abs(a-b) for a,b in zip(pos,neg))/max(sum(deg),1), + _xor_pattern_fraction(formula)) + + +def _signed_features(sig) -> tuple[float,...]: + return (sig.negative_square_fraction, + sig.negative_four_cycles/max(sig.edges,1), + (sig.components-sig.balanced_components)/max(sig.components,1), + float(not sig.globally_balanced)) + + +def extract_features(formula: CNFFormula, *, null_seed: int, swaps: int = 160 + ) -> tuple[tuple[float,...],int,int,int]: + """Return (features, baseline_ns, extra_signed_ns, null_ns). No solver calls.""" + start=perf_counter_ns() + struct = _structural(formula) + sig = signed_connection(formula,max_wedges=500000) + baseline = struct + (sig.components/max(formula.num_vars,1), + sig.cycle_rank/max(sig.edges,1), + sig.four_cycles/max(sig.edges,1),sig.square_density) + baseline_ns=perf_counter_ns()-start + start=perf_counter_ns() + signed = _signed_features(sig) + signed_ns=perf_counter_ns()-start + start=perf_counter_ns() + rewired,count=support_degree_sign_null(formula,seed=null_seed,swaps=swaps) + null_signed=_signed_features(signed_connection(rewired,max_wedges=500000)) + null_ns=perf_counter_ns()-start + if len(baseline+signed+null_signed)!=len(FEATURES): + raise AssertionError("feature contract") + return baseline+signed+null_signed,count,baseline_ns,signed_ns+null_ns + + +def canonical_labeled_digest(formula: CNFFormula) -> str: + """Labels are kept. This detects duplicate CNFs, not graph isomorphism.""" + data = repr((formula.num_vars,sorted(tuple(sorted(c)) for c in formula.clauses))) + return sha256(data.encode("utf-8")).hexdigest() + + +@dataclass(frozen=True) +class CDCLCall: + status: str + conflicts: int + decisions: int + propagations: int + wall_ms: float + valid_sat_model: bool | None + + +def _model_replay(formula: CNFFormula, model: Sequence[int] | None) -> bool: + if model is None: + return False + values = {abs(v):v>0 for v in model if 00) for lit in clause) + for clause in formula.clauses) + + +def cdcl_call(formula: CNFFormula, *, budget: int = 2000, engine: str="g4", + solver_factory: Callable | None = None) -> CDCLCall: + """External CDCL observation with a conflict cap, model replay and no TCB change.""" + if not 1 <= budget <= 100000: + raise ValueError("conflict budget out of bounds") + if solver_factory is None: + try: + from pysat.solvers import Solver + except ImportError as exc: + raise RuntimeError("external CDCL experiment requires pip install python-sat") from exc + solver_factory=Solver + start=perf_counter_ns() + with solver_factory(name=engine,bootstrap_with=formula.clauses,use_timer=False) as solver: + solver.conf_budget(budget) + answer=solver.solve_limited() + stats=solver.accum_stats() + valid=None + if answer is True: + valid=_model_replay(formula,solver.get_model()) + if not valid: + raise AssertionError("external solver SAT model failed independent clause replay") + status={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[answer] + ms=(perf_counter_ns()-start)/1e6 + return CDCLCall(status,int(stats.get("conflicts",0)),int(stats.get("decisions",0)), + int(stats.get("propagations",0)),ms,valid) + + +@dataclass(frozen=True) +class TopologyRecord: + family: str + size: int + seed: int + digest: str + features: tuple[float,...] + null_switches: int + baseline_ms: float + signed_plus_null_ms: float + calls: tuple[CDCLCall,...] + capped_log_conflicts: float + capped_log_decisions: float + censored_calls: int + median_cdcl_wall_ms: float + + +def measure_formula(formula: CNFFormula, family: str, size: int, seed: int, + *, orbits: int=3, budget: int=2000, swaps: int=160, + solver_factory: Callable | None=None) -> TopologyRecord: + if not 1<=orbits<=8 or family not in FAMILIES: + raise ValueError("orbit or family budget exceeded") + features,count,baseline_ns,extra_ns=extract_features(formula, + null_seed=seed*199+size*11+921,swaps=swaps) + calls=[] + for i in range(orbits): + image=(formula if i==0 else _shuffle_vars(formula, + Random(seed*100003+size*917+FAMILIES.index(family)*1009+i*37))) + calls.append(cdcl_call(image,budget=budget,solver_factory=solver_factory)) + resolved={call.status for call in calls if call.status!="UNKNOWN"} + if len(resolved)>1: + raise AssertionError("external CDCL disagreeing under equivalent relabelings") + return TopologyRecord(family,size,seed,canonical_labeled_digest(formula), + features,count,baseline_ns/1e6,extra_ns/1e6,tuple(calls), + median(log2(1+min(budget,c.conflicts)) for c in calls), + median(log2(1+min(budget,c.decisions)) for c in calls), + sum(c.status=="UNKNOWN" for c in calls), + median(c.wall_ms for c in calls)) + + +def _predict_ridge(train: Sequence[TopologyRecord],test: Sequence[TopologyRecord], + columns: Sequence[str], target: str) -> np.ndarray: + y=np.array([getattr(x,target) for x in train],dtype=float) + if not columns: + return np.full(len(test),float(y.mean())) + col=[COLS[name] for name in columns] + X=np.array([[r.features[i] for i in col] for r in train]) + Z=np.array([[r.features[i] for i in col] for r in test]) + mu,sd=X.mean(axis=0),X.std(axis=0) + sd[sd<1e-12]=1. + X,Z=(X-mu)/sd,(Z-mu)/sd + X=np.column_stack((np.ones(len(X)),X)) + Z=np.column_stack((np.ones(len(Z)),Z)) + penalty=np.diag([0.]+[RIDGE_ALPHA]*len(col)) + return Z@np.linalg.solve(X.T@X+penalty,X.T@y) + + +def _eval_fold(train: Sequence[TopologyRecord],test: Sequence[TopologyRecord], + target: str) -> dict[str,float]: + observed=np.array([getattr(x,target) for x in test],dtype=float) + return {name:float(np.mean(np.abs(_predict_ridge(train,test,features,target)-observed))) + for name,features in PREDICTORS.items()} + + +@dataclass(frozen=True) +class Fold: + label: str + count: int + censored_call_fraction: float + failed_null_fraction: float + capped_conflict_mae: dict[str,float] + capped_decision_mae: dict[str,float] + + +@dataclass(frozen=True) +class TopologyReport: + seed_count: int + sizes: tuple[int,...] + budget: int + orbits: int + records: tuple[TopologyRecord,...] + family_holdouts: tuple[Fold,...] + size_holdout: Fold | None + aggregate_family_mae: dict[str,float] + total_formulas: int + unique_labeled_formulas: int + censored_call_fraction: float + null_nontrivial_fraction: float + median_baseline_ms: float + median_signed_increment_ms: float + median_cdcl_ms: float + evidence: str="M: budget-capped external CDCL stats; not a SAT certificate" + + +def _fold(label: str,train: Sequence[TopologyRecord], + test: Sequence[TopologyRecord]) -> Fold: + if not train or not test: + raise ValueError("empty holdout") + return Fold(label,len(test), + sum(r.censored_calls for r in test)/sum(len(r.calls) for r in test), + sum(r.null_switches==0 for r in test)/len(test), + _eval_fold(train,test,"capped_log_conflicts"), + _eval_fold(train,test,"capped_log_decisions")) + + +def topology_benchmark(*,seeds: int=4,sizes: Sequence[int]=(48,72), + orbits: int=3,budget: int=2000,swaps: int=160, + solver_factory: Callable | None=None) -> TopologyReport: + if not 2<=seeds<=16 or not sizes or len(set(sizes))!=len(sizes): + raise ValueError("invalid seed count or size list") + if any(n<12 or n>144 or n%3 for n in sizes): + raise ValueError("size must be multiple of 3 between 12 and 144") + dataset=[] + for family in FAMILIES: + for n in sizes: + for seed in range(seeds): + formula=generate_formula(family,n,seed) + dataset.append(measure_formula(formula,family,n,seed, + orbits=orbits,budget=budget,swaps=swaps, + solver_factory=solver_factory)) + digest_count=len({r.digest for r in dataset}) + if digest_count!=len(dataset): + raise AssertionError("duplicate labeled CNF: invalid formula split") + folds=[] + for heldout in FAMILIES: + train=[r for r in dataset if r.family!=heldout] + test=[r for r in dataset if r.family==heldout] + folds.append(_fold(heldout,train,test)) + size_fold=None + if len(sizes)>=2: + largest=max(sizes) + size_fold=_fold("largest_size="+str(largest), + [r for r in dataset if r.size!=largest], + [r for r in dataset if r.size==largest]) + full={name:sum(f.count*f.capped_conflict_mae[name] for f in folds)/len(dataset) + for name in PREDICTORS} + return TopologyReport(seeds,tuple(sizes),budget,orbits,tuple(dataset), + tuple(folds),size_fold,full,len(dataset),digest_count, + sum(r.censored_calls for r in dataset)/sum(len(r.calls) for r in dataset), + sum(r.null_switches>0 for r in dataset)/len(dataset), + median(r.baseline_ms for r in dataset), + median(r.signed_plus_null_ms for r in dataset), + median(r.median_cdcl_wall_ms for r in dataset)) From 22b09568f83baf63f5997ce0865c63d486b01686 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:43:47 +0100 Subject: [PATCH 29/48] test: distinct cubic topology, polarity-preserving null and censored CDCL contracts --- backend/tests/test_violation_cdcl_topology.py | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 backend/tests/test_violation_cdcl_topology.py diff --git a/backend/tests/test_violation_cdcl_topology.py b/backend/tests/test_violation_cdcl_topology.py new file mode 100644 index 0000000..e76cfa5 --- /dev/null +++ b/backend/tests/test_violation_cdcl_topology.py @@ -0,0 +1,165 @@ +"""Topology-holdout contracts, with external PySAT test only when installed.""" +from collections import Counter +from itertools import combinations +from random import Random + +import numpy as np +import pytest + +from backend.cnf_utils import CNFFormula +from backend.violation_connection import signed_connection +from backend.violation_cross_instance import _shuffle_vars +from backend.violation_cdcl_topology import ( + BASE, SIGN, NULL, PREDICTORS, FAMILIES, cubic_graph, generate_formula, + support_degree_sign_null, extract_features, cdcl_call, + canonical_labeled_digest, topology_benchmark) + + +def _sign_margins(f): + return (tuple((len(c),sum(v>0 for v in c)) for c in f.clauses), + Counter((abs(v), v>0) for c in f.clauses for v in c)) + + +def _is_model(f, state): + return all(any(bool(state & (1 << (abs(v)-1))) == (v>0) + for v in c) for c in f.clauses) + + +@pytest.mark.parametrize("vertices", [8, 16, 32, 48]) +def test_cubic_nontrivial_topologies(vertices): + for topology in ("prism", "rewired"): + edges = cubic_graph(vertices, topology, seed=33) + assert edges == cubic_graph(vertices, topology, seed=33) + assert len(edges) == vertices*3//2 + degrees=Counter(v for a,b in edges for v in (a,b)) + assert set(degrees.values()) == {3} + assert len(edges) == len(set(edges)) + assert cubic_graph(vertices, "prism", 33) != cubic_graph(vertices, "rewired", 33) + + +def test_graph_isomorphism_checks_of_rewired_seeded_graphs(): + nx = pytest.importorskip("networkx") + graphs=[] + for seed in range(4): + G=nx.Graph() + G.add_edges_from(cubic_graph(32, "rewired", seed)) + graphs.append(G) + assert all(not nx.is_isomorphic(a,b) for a,b in combinations(graphs,2)) + prism=nx.Graph() + prism.add_edges_from(cubic_graph(32,"prism",0)) + assert all(not nx.is_isomorphic(prism,g) for g in graphs) + + +def test_generators_have_unique_signed_clauses_and_fixed_budget(): + hashes=set() + for family in FAMILIES: + for n in (48, 72): + for seed in (0,1,2): + f=generate_formula(family,n,seed) + assert f.num_vars==n + assert all(len(c)==3 and len({abs(v) for v in c})==3 + for c in f.clauses) + assert all(1<=abs(v)<=n for c in f.clauses for v in c) + assert len({tuple(sorted(c)) for c in f.clauses})==len(f.clauses) + if family.startswith("tseitin"): + assert len(f.clauses)==4*(2*n//3) + else: + assert len(f.clauses)==round(4.26*n) + h=canonical_labeled_digest(f) + assert h not in hashes + hashes.add(h) + + +def test_tseitin_charge_parity_in_small_explicit_truth_table(): + # Recheck generator truth without using the CDCL instrument. + for family in ("tseitin-prism","tseitin-rewired"): + for seed in range(4): + f=generate_formula(family,12,seed) + satisfiable=any(_is_model(f,x) for x in range(1<0, family + assert _sign_margins(f)==_sign_margins(randomised) + assert canonical_labeled_digest(f)!=canonical_labeled_digest(randomised) + assert support_degree_sign_null(f,seed=77,swaps=80)==(randomised,count) + + +def test_signed_connection_and_structural_features_are_gauge_invariant(): + for family in FAMILIES: + f=generate_formula(family,48,3) + features,null_count,base_ns,extra_ns=extract_features(f,null_seed=11,swaps=32) + assert len(features)==len(BASE)+len(SIGN)+len(NULL) + assert 0<=features[len(BASE)+2]<=1 + assert null_count>0 and base_ns>=0 and extra_ns>=0 + original=signed_connection(f) + assert original==signed_connection(_shuffle_vars(f,Random(39))) + + +class FakeCDCL: + def __init__(self, answer, clauses, model=None): + self.answer=answer + self.clauses=clauses + self.model=model + self.budget=None + def __enter__(self): return self + def __exit__(self,*args): return False + def conf_budget(self,b): self.budget=b + def solve_limited(self): + assert self.budget is not None + return self.answer + def accum_stats(self): + return {"conflicts": min(17,self.budget), + "decisions": 23, "propagations": 109} + def get_model(self): return self.model + + +def fake_factory(answer,model=None): + return lambda **kw: FakeCDCL(answer,kw["bootstrap_with"],model=model) + + +def test_external_observation_truths_and_censoring_are_distinct(): + f=CNFFormula(2,[[1],[2]]) + sat=cdcl_call(f,budget=20,solver_factory=fake_factory(True,[1,2])) + assert sat.status=="SAT" and sat.valid_sat_model is True + bad=fake_factory(True,[-1,-2]) + with pytest.raises(AssertionError,match="replay"): + cdcl_call(f,budget=20,solver_factory=bad) + unsat=cdcl_call(f,budget=10,solver_factory=fake_factory(False)) + unknown=cdcl_call(f,budget=10,solver_factory=fake_factory(None)) + assert unsat.status=="UNSAT" and unsat.valid_sat_model is None + assert unknown.status=="UNKNOWN" and unknown.valid_sat_model is None + + +def test_external_pysat_glucose4_smoke_if_installed(): + pytest.importorskip("pysat.solvers") + sat=cdcl_call(CNFFormula(2,[[1],[2]]),budget=100) + unsat=cdcl_call(CNFFormula(1,[[1],[-1]]),budget=100) + assert sat.status=="SAT" and sat.valid_sat_model + assert unsat.status=="UNSAT" + assert sat.conflicts>=0 and unsat.conflicts>=0 + + +def test_fake_oracle_family_and_size_holdouts_do_not_require_verdicts(): + # Fake UNSAT stats are test data only; never publish them as measured SAT results. + report=topology_benchmark(seeds=2,sizes=(12,15),orbits=2, + budget=50,swaps=8,solver_factory=fake_factory(False)) + assert report.total_formulas==24 + assert report.unique_labeled_formulas==24 + assert len(report.family_holdouts)==len(FAMILIES) + assert report.size_holdout is not None + assert report.size_holdout.count==12 + assert set(report.aggregate_family_mae)==set(PREDICTORS) + assert report.censored_call_fraction==0 + assert all(np.isfinite(v) and v>=0 for v in report.aggregate_family_mae.values()) + + +def test_invalid_instrument_budgets(): + with pytest.raises(ValueError): cubic_graph(7,"rewired",1) + with pytest.raises(ValueError): generate_formula("uniform3",47,2) + with pytest.raises(ValueError): support_degree_sign_null(CNFFormula(1,[[1,-1]]),seed=1) + with pytest.raises(ValueError): cdcl_call(CNFFormula(1,[[1]]),budget=0,solver_factory=fake_factory(None)) From 8db6d2c4e56f50cb2054e02a8c2b9c530af22b43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:44:00 +0100 Subject: [PATCH 30/48] benchmark: export reproducible Glucose4 topology-heldout conflicts with censoring --- .../scripts/violation_cdcl_topology_probe.py | 72 +++++++++++++++++++ 1 file changed, 72 insertions(+) create mode 100644 docs/ladder/scripts/violation_cdcl_topology_probe.py diff --git a/docs/ladder/scripts/violation_cdcl_topology_probe.py b/docs/ladder/scripts/violation_cdcl_topology_probe.py new file mode 100644 index 0000000..2c524e0 --- /dev/null +++ b/docs/ladder/scripts/violation_cdcl_topology_probe.py @@ -0,0 +1,72 @@ +"""PySAT Glucose4 topology experiment: reproducible held-out CDCL work. + +This CLI is separate from lambda-sat's certified solve path. It emits raw +sample/seed, model replay, conflict counts, UNKNOWN censoring, selected +regression features, null-swaps and feature overhead. + +Usage: + python docs/ladder/scripts/violation_cdcl_topology_probe.py \ + --seeds 3 --sizes 48 72 --orbits 2 --budget 2000 --json +""" +from __future__ import annotations + +import argparse +import json +import os +import platform +import sys +from dataclasses import asdict +from importlib.metadata import PackageNotFoundError, version +from pathlib import Path + +sys.path.insert(0,str(Path(__file__).resolve().parents[3])) +from backend.violation_cdcl_topology import PREDICTORS, topology_benchmark + + +def main() -> None: + p=argparse.ArgumentParser(description=__doc__) + p.add_argument("--seeds",type=int,default=4,help="2..16 independent formula seeds") + p.add_argument("--sizes",type=int,nargs="+",default=[48,72,96], + help="declared variable counts, each divisible by 3") + p.add_argument("--orbits",type=int,default=3,help="1..8 signed relabelings per CNF") + p.add_argument("--budget",type=int,default=2000,help="per-call CDCL conflict budget") + p.add_argument("--swaps",type=int,default=160,help="support-rewiring null attempts") + p.add_argument("--json",action="store_true") + args=p.parse_args() + report=topology_benchmark(seeds=args.seeds,sizes=args.sizes,orbits=args.orbits, + budget=args.budget,swaps=args.swaps) + try: + pysat_version=version("python-sat") + except PackageNotFoundError: + pysat_version="unknown" + payload={"design":"docs/ladder/VIOLATION_CDCL_TOPOLOGY_PREREG.md", + "kind":"experimental Glucose4 CDCL statistics, NOT certified λSAT results", + "instrument":{"python":sys.version.split()[0], + "platform":platform.platform(), + "python_sat":pysat_version, + "solver":"g4", + "github_sha":os.environ.get("GITHUB_SHA","unrecorded local")}, + "parameters":vars(args), + "report":asdict(report)} + if args.json: + print(json.dumps(payload,indent=2,sort_keys=True)) + return + print("Glucose4, fixed conflict budget and independent signed relabelings") + print("CNFs:",report.total_formulas,"unique labeled:",report.unique_labeled_formulas, + "unknown calls: %.1f%%"%(100*report.censored_call_fraction)) + print("Unsigned graph, degree and polarity features are included in 'classical'.") + for k,v in report.aggregate_family_mae.items(): + print(f" {k:30} log2 capped-conflicts LOFO MAE {v:.4f}") + if report.size_holdout: + print("Largest n holdout:", report.size_holdout.label, + report.size_holdout.capped_conflict_mae) + print("Nontrivial null coverage: %.1f%%"%(100*report.null_nontrivial_fraction)) + print("Feature cost baseline / +signed+control / CDCL median: " + f"{report.median_baseline_ms:.3f} / {report.median_signed_increment_ms:.3f} / " + f"{report.median_cdcl_ms:.3f} ms") + print("Raw outcomes, missingness and family folds are available with --json.") + print("No geometry win is required for valid evidence; claims remain bounded.") + + +if __name__=="__main__": + main() From ec169542256137682c48c7bddb62dc761b9d73d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:44:11 +0100 Subject: [PATCH 31/48] ci: isolated PySAT Glucose4 topology transfer job with raw censored evidence --- .github/workflows/violation-geometry-lab.yml | 53 ++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml index 206da77..6c5d8a9 100644 --- a/.github/workflows/violation-geometry-lab.yml +++ b/.github/workflows/violation-geometry-lab.yml @@ -76,3 +76,56 @@ jobs: 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 + - 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: Preserve CDCL evidence, including unsuccessful hypotheses + uses: actions/upload-artifact@v4 + with: + name: violation-cdcl-topology-evidence + path: evidence/cdcl_topology.json + retention-days: 30 From fb9d5c97d7d61313cec774e4e4df0914492ec5a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:45:55 +0100 Subject: [PATCH 32/48] research: timestamp post-pilot GF2 positive-control design and unseen seed replication --- docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md diff --git a/docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md b/docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md new file mode 100644 index 0000000..75b5944 --- /dev/null +++ b/docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md @@ -0,0 +1,15 @@ +# Post-pilot GF(2) control and disjoint-seed replication (exploratory addendum) + +**29 October 2026.** This addendum was written AFTER inspecting the 36-formula Glucose4 pilot. It must not be represented as part of the original [pre-registration](VIOLATION_CDCL_TOPOLOGY_PREREG.md), nor as a confirmatory test of hypotheses chosen before that pilot. Source: [λSAT existing parity frame](../../backend/xor_extraction.py). + +The pilot's measured LOFO log2 capped-conflicts MAE was classical=2.054, classical+signed=1.986, classical+margin/degree-preserving topology null=1.939. Signed improved over structure but **lost to its null control**. Two of 72 solver runs were censored (2.8%). Median baseline feature time ~3.92 ms; full signed + support-rewired control time adds ~3.97 ms; median Glucose4 solve time was ~0.315 ms. Thus no solver routing advantage exists on these measured instances. + +**Identified missing classical comparator.** The previous "classical" vector included the share of complete XOR clause patterns but did not explicitly compute their *global GF(2) rank and inconsistency*. Our Tseitin generators purposely alternate even/odd charges; recovered parity equations can be contradictory even when clause incidence degree, width and local signs look very similar. In λSAT, `extract_xors`, `_rref_gf2`, and `gf2_xor_solve` already implement this algebraic gate. Include its rank deficiency, exact coverage, consistency, number of recovered constraints and verified SAT or sound UNSAT state as **formula-only predictors / positive controls**. This may act as a partial solver: charge its wall cost, do not hide its algebraic advantage. + +**Disjoint new corpus, fixed before running the follow-up.** Seed IDs 100–105 inclusive, variable sizes 48, 72, 96, the same six families, three fresh signed-relabeling CDCL calls per formula, Glucose4 with 5,000 conflicts per call, support-rewiring null with 160 successful switches sought. This is *additional exploratory replication* after seeing an earlier pilot; no formal statistical inference or general hardness claim. The explicit size holdout trains n=48,72 and tests n=96. + +**Comparators.** Fixed ridge penalty 10 with train-only standardized features: classical unsigned topology; classical+signed; classical+support-rewired-null; classical+GF(2); classical+GF(2)+signed; classical+GF(2)+rewired-null. Inspect per-family and per-size errors, censoring, SAT/UNSAT counts, distinct generator topologies, feature costs and GF(2) frame validity. Report the exact sign of every delta; do NOT tune ridge after observing results. + +**Falsification gate.** If signed loses to classical+GF(2), or if null performs equally well, retain the failed distinctiveness conclusion. If the parity frame solves an instance directly, that is an *algebraic* result, not evidence for Kakeya smoothing or a hypercomplex speedup. An apparent error reduction cannot become a production-routing claim if extractor cost is above CDCL time. UNKNOWN is not counted as solved. + +**Evidence boundary.** Retain earlier negative DPLL rounds and the first CDCL pilot, with their exact artifacts. Raw JSON from GitHub Actions is the authority for these observations, not this prose. From b5e70d42483291630931288794f030eb564424e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:46:05 +0100 Subject: [PATCH 33/48] experiment: add disjoint seed-start control for unseen graph replication --- backend/violation_cdcl_topology.py | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/backend/violation_cdcl_topology.py b/backend/violation_cdcl_topology.py index cd7edbe..7d6e3ed 100644 --- a/backend/violation_cdcl_topology.py +++ b/backend/violation_cdcl_topology.py @@ -423,6 +423,7 @@ class TopologyReport: median_signed_increment_ms: float median_cdcl_ms: float evidence: str="M: budget-capped external CDCL stats; not a SAT certificate" + seed_start: int=0 def _fold(label: str,train: Sequence[TopologyRecord], @@ -436,17 +437,18 @@ def _fold(label: str,train: Sequence[TopologyRecord], _eval_fold(train,test,"capped_log_decisions")) -def topology_benchmark(*,seeds: int=4,sizes: Sequence[int]=(48,72), - orbits: int=3,budget: int=2000,swaps: int=160, +def topology_benchmark(*,seeds: int=4,seed_start: int=0, + sizes: Sequence[int]=(48,72),orbits: int=3, + budget: int=2000,swaps: int=160, solver_factory: Callable | None=None) -> TopologyReport: - if not 2<=seeds<=16 or not sizes or len(set(sizes))!=len(sizes): + if not 2<=seeds<=16 or not 0<=seed_start<=1000000 or not sizes or len(set(sizes))!=len(sizes): raise ValueError("invalid seed count or size list") if any(n<12 or n>144 or n%3 for n in sizes): raise ValueError("size must be multiple of 3 between 12 and 144") dataset=[] for family in FAMILIES: for n in sizes: - for seed in range(seeds): + for seed in range(seed_start,seed_start+seeds): formula=generate_formula(family,n,seed) dataset.append(measure_formula(formula,family,n,seed, orbits=orbits,budget=budget,swaps=swaps, @@ -473,4 +475,4 @@ def topology_benchmark(*,seeds: int=4,sizes: Sequence[int]=(48,72), sum(r.null_switches>0 for r in dataset)/len(dataset), median(r.baseline_ms for r in dataset), median(r.signed_plus_null_ms for r in dataset), - median(r.median_cdcl_wall_ms for r in dataset)) + median(r.median_cdcl_wall_ms for r in dataset),seed_start=seed_start) From 1a9bf16e4fa81ce9109ce536c16d8c6e0d521212 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:46:14 +0100 Subject: [PATCH 34/48] cli: enable disjoint future CDCL seed ranges --- docs/ladder/scripts/violation_cdcl_topology_probe.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/ladder/scripts/violation_cdcl_topology_probe.py b/docs/ladder/scripts/violation_cdcl_topology_probe.py index 2c524e0..d250479 100644 --- a/docs/ladder/scripts/violation_cdcl_topology_probe.py +++ b/docs/ladder/scripts/violation_cdcl_topology_probe.py @@ -26,6 +26,7 @@ def main() -> None: p=argparse.ArgumentParser(description=__doc__) p.add_argument("--seeds",type=int,default=4,help="2..16 independent formula seeds") + p.add_argument("--seed-start",type=int,default=0,help="first formula seed; use disjoint starts for new corpora") p.add_argument("--sizes",type=int,nargs="+",default=[48,72,96], help="declared variable counts, each divisible by 3") p.add_argument("--orbits",type=int,default=3,help="1..8 signed relabelings per CNF") @@ -33,7 +34,8 @@ def main() -> None: p.add_argument("--swaps",type=int,default=160,help="support-rewiring null attempts") p.add_argument("--json",action="store_true") args=p.parse_args() - report=topology_benchmark(seeds=args.seeds,sizes=args.sizes,orbits=args.orbits, + report=topology_benchmark(seeds=args.seeds,seed_start=args.seed_start, + sizes=args.sizes,orbits=args.orbits, budget=args.budget,swaps=args.swaps) try: pysat_version=version("python-sat") From c817c0c833e3d9b8fe4368b74f74bcb0f9deb5bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:46:45 +0100 Subject: [PATCH 35/48] research: add audited existing GF2 rank and certified-frame comparator to external CDCL topology pilot --- backend/violation_cdcl_parity.py | 186 +++++++++++++++++++++++++++++++ 1 file changed, 186 insertions(+) create mode 100644 backend/violation_cdcl_parity.py diff --git a/backend/violation_cdcl_parity.py b/backend/violation_cdcl_parity.py new file mode 100644 index 0000000..8f98ed3 --- /dev/null +++ b/backend/violation_cdcl_parity.py @@ -0,0 +1,186 @@ +"""Formula-only GF(2) positive control for the external CDCL topology study. + +Runs the existing λSAT XOR extractor and frame without modifying its +certification path. This addendum was planned *after* seeing the first +36-formula CDCL pilot: exploratory, not retroactive preregistration. +""" +from __future__ import annotations + +from dataclasses import dataclass +from math import sqrt +from statistics import median +from time import perf_counter_ns + +import numpy as np + +from .cnf_utils import CNFFormula +from .xor_extraction import extract_xors, _rref_gf2, gf2_xor_solve +from .violation_cdcl_topology import ( + BASE, SIGN, NULL, FAMILIES, RIDGE_ALPHA, + TopologyRecord, generate_formula, topology_benchmark, +) + +GF2 = ("recovered_xor_fraction", "xor_constraint_density", + "xor_rank_per_variable", "xor_rank_deficiency", + "xor_inconsistent") +ALL_FEATURES = BASE + SIGN + NULL + GF2 +COLUMNS = {name: i for i,name in enumerate(ALL_FEATURES)} +PREDICTORS = { + "classical": BASE, + "classical+signed": BASE + SIGN, + "classical+topology-null": BASE + NULL, + "classical+GF2": BASE + GF2, + "classical+GF2+signed": BASE + GF2 + SIGN, + "classical+GF2+topology-null": BASE + GF2 + NULL, + "GF2-only": GF2, +} + + +@dataclass(frozen=True) +class GF2Control: + features: tuple[float,...] + frame_status: str + extracted_constraints: int + rank: int + elapsed_ms: float + + +def gf2_control(formula: CNFFormula) -> GF2Control: + """Time actual algebraic extraction/solve; no CDCL calls or labels.""" + start=perf_counter_ns() + parsed=extract_xors(formula) + n=formula.num_vars + augmented=[] + spanned=set() + for xor in parsed.xors: + row=0 + for var in xor.variables: + if not 1<=var<=n: + raise AssertionError("malformed extracted XOR") + row|=1<<(var-1) + spanned.add(var) + if xor.rhs: + row|=1< np.ndarray: + target=np.asarray([r.capped_log_conflicts for r in train],dtype=float) + if not names: + return np.full(len(test),float(target.mean())) + ix=[COLUMNS[s] for s in names] + X=np.asarray([[r.features[i] for i in ix] for r in train],dtype=float) + Z=np.asarray([[r.features[i] for i in ix] for r in test],dtype=float) + mean,std=X.mean(axis=0),X.std(axis=0) + std[std<1e-12]=1. + X,Z=(X-mean)/std,(Z-mean)/std + X=np.column_stack((np.ones(len(X)),X)) + Z=np.column_stack((np.ones(len(Z)),Z)) + penalty=np.diag([0.]+[RIDGE_ALPHA]*len(ix)) + return Z@np.linalg.solve(X.T@X+penalty,X.T@target) + + +def _loss(train: list[AugmentedRecord], + test: list[AugmentedRecord]) -> dict[str,float]: + truth=np.asarray([r.capped_log_conflicts for r in test]) + return {name:float(np.mean(np.abs(_predict(train,test,columns)-truth))) + for name,columns in PREDICTORS.items()} + + +@dataclass(frozen=True) +class GF2Fold: + heldout: str + count: int + mae_log2_capped_conflicts: dict[str,float] + + +@dataclass(frozen=True) +class GF2Report: + formulas: int + seed_start: int + seed_count: int + sizes: tuple[int,...] + status_counts: dict[str,int] + pure_xor_checked: int + family_holdouts: tuple[GF2Fold,...] + largest_size_holdout: GF2Fold | None + aggregate_mae: dict[str,float] + median_gf2_ms: float + median_cdcl_ms: float + censored_call_fraction: float + match_error_count: int + provenance: str="post-pilot exploratory control; existing sound λSAT GF2 gate" + + +def parity_holdout(*,seeds: int=6,seed_start: int=100, + sizes: tuple[int,...]=(48,72,96), + orbits: int=3,budget: int=5000,swaps: int=160 + ) -> GF2Report: + """Independent seed range, same CDCL calls, existing XOR frame comparison.""" + original=topology_benchmark(seeds=seeds,seed_start=seed_start, + sizes=sizes,orbits=orbits,budget=budget,swaps=swaps) + dataset=[] + for rec in original.records: + f=generate_formula(rec.family,rec.size,rec.seed) + ctrl=gf2_control(f) + # A resolved CDCL result must not disagree with a sound GF(2) gate. + for call in rec.calls: + if (ctrl.frame_status!="INCONCLUSIVE" and call.status!="UNKNOWN" + and call.status!=ctrl.frame_status): + raise AssertionError("CDCL result contradicts independent GF(2) frame") + dataset.append(AugmentedRecord(rec,ctrl)) + groups=[] + totals={name:0. for name in PREDICTORS} + for heldout in FAMILIES: + train=[r for r in dataset if r.base.family!=heldout] + test=[r for r in dataset if r.base.family==heldout] + errors=_loss(train,test) + groups.append(GF2Fold(heldout,len(test),errors)) + for name,value in errors.items(): + totals[name]+=len(test)*value + largest=max(sizes) + test=[r for r in dataset if r.base.size==largest] + train=[r for r in dataset if r.base.size!=largest] + sizefold=GF2Fold("n="+str(largest),len(test),_loss(train,test)) if train else None + counts={name:sum(r.gf2.frame_status==name for r in dataset) + for name in ("SAT","UNSAT","INCONCLUSIVE")} + pure=sum(r.gf2.frame_status in ("SAT","UNSAT") for r in dataset) + return GF2Report(len(dataset),seed_start,seeds,tuple(sizes), + counts,pure,tuple(groups),sizefold, + {name:value/len(dataset) for name,value in totals.items()}, + median(r.gf2.elapsed_ms for r in dataset), + original.median_cdcl_ms,original.censored_call_fraction,0) From c2ff9f6f161d884585ce6243bdb62fcdab24c716 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:46:57 +0100 Subject: [PATCH 36/48] research: retain seed-level GF2/CDCL parity gate audit alongside aggregate regressions --- backend/violation_cdcl_parity.py | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/backend/violation_cdcl_parity.py b/backend/violation_cdcl_parity.py index 8f98ed3..c11de83 100644 --- a/backend/violation_cdcl_parity.py +++ b/backend/violation_cdcl_parity.py @@ -121,6 +121,22 @@ def _loss(train: list[AugmentedRecord], for name,columns in PREDICTORS.items()} +@dataclass(frozen=True) +class GF2Case: + family: str + size: int + seed: int + digest: str + frame_status: str + extracted_constraints: int + rank: int + features: tuple[float,...] + gf2_ms: float + capped_log_conflicts: float + call_statuses: tuple[str,...] + censored_calls: int + + @dataclass(frozen=True) class GF2Fold: heldout: str @@ -139,6 +155,7 @@ class GF2Report: family_holdouts: tuple[GF2Fold,...] largest_size_holdout: GF2Fold | None aggregate_mae: dict[str,float] + cases: tuple[GF2Case,...] median_gf2_ms: float median_cdcl_ms: float censored_call_fraction: float @@ -179,8 +196,13 @@ def parity_holdout(*,seeds: int=6,seed_start: int=100, counts={name:sum(r.gf2.frame_status==name for r in dataset) for name in ("SAT","UNSAT","INCONCLUSIVE")} pure=sum(r.gf2.frame_status in ("SAT","UNSAT") for r in dataset) + cases=tuple(GF2Case(r.base.family,r.base.size,r.base.seed,r.base.digest, + r.gf2.frame_status,r.gf2.extracted_constraints,r.gf2.rank, + r.gf2.features,r.gf2.elapsed_ms,r.base.capped_log_conflicts, + tuple(call.status for call in r.base.calls),r.base.censored_calls) + for r in dataset) return GF2Report(len(dataset),seed_start,seeds,tuple(sizes), counts,pure,tuple(groups),sizefold, - {name:value/len(dataset) for name,value in totals.items()}, + {name:value/len(dataset) for name,value in totals.items()},cases, median(r.gf2.elapsed_ms for r in dataset), original.median_cdcl_ms,original.censored_call_fraction,0) From 7de55b3564d5d0f6ad5329d496343e0f250f21ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:47:09 +0100 Subject: [PATCH 37/48] test: existing GF2 frame detects global Tseitin charge and crosschecks external CDCL --- backend/tests/test_violation_cdcl_parity.py | 60 +++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 backend/tests/test_violation_cdcl_parity.py diff --git a/backend/tests/test_violation_cdcl_parity.py b/backend/tests/test_violation_cdcl_parity.py new file mode 100644 index 0000000..966c3c3 --- /dev/null +++ b/backend/tests/test_violation_cdcl_parity.py @@ -0,0 +1,60 @@ +"""GF(2) parity gate as a known sound positive comparator, not invented geometry.""" +import pytest + +from backend.cnf_utils import CNFFormula +from backend.violation_cdcl_parity import GF2,PREDICTORS,gf2_control,parity_holdout +from backend.violation_cdcl_topology import generate_formula +from backend.xor_extraction import gf2_xor_solve + + +@pytest.mark.parametrize("family",["tseitin-prism","tseitin-rewired"]) +def test_global_charge_obstruction_is_recovered_in_each_graph(family): + for size in (12,48,72): + for seed in range(4): + f=generate_formula(family,size,seed) + check=gf2_control(f) + assert check.extracted_constraints==2*size//3 + assert check.features[0]==1.0 + assert check.rank==2*size//3-1 + assert check.frame_status==("UNSAT" if seed%2 else "SAT") + # Existing verified frame and new feature extractor agree. + assert check.frame_status==gf2_xor_solve(f).status + assert check.elapsed_ms>=0 + + +def test_incomplete_nonxor_must_never_claim_full_frame(): + for family in ("uniform3","ring3","community3","hub3"): + f=generate_formula(family,48,100) + report=gf2_control(f) + assert report.frame_status=="INCONCLUSIVE" + assert report.extracted_constraints>=0 + assert 0<=report.features[0]<=1 + assert len(report.features)==len(GF2) + + +def test_real_glucose4_independent_positive_control_if_installed(): + pytest.importorskip("pysat.solvers") + report=parity_holdout(seeds=2,seed_start=100,sizes=(12,15), + orbits=1,budget=200,swaps=8) + assert report.formulas==24 + assert report.seed_start==100 + assert len(report.cases)==24 + assert set(report.aggregate_mae)==set(PREDICTORS) + assert report.status_counts["SAT"]>=4 + assert report.status_counts["UNSAT"]>=4 + assert report.status_counts["SAT"]+report.status_counts["UNSAT"]==report.pure_xor_checked + assert report.match_error_count==0 + assert len(report.family_holdouts)==6 + assert report.largest_size_holdout is not None + for r in report.cases: + assert r.frame_status in ("SAT","UNSAT","INCONCLUSIVE") + assert all(s in ("SAT","UNSAT","UNKNOWN") for s in r.call_statuses) + + +def test_pure_xor_and_partial_nonxor_compare_not_equate(): + xor=CNFFormula(3,[[1,2,3],[1,-2,-3],[-1,2,-3],[-1,-2,3]]) + assert gf2_control(xor).frame_status=="SAT" + # Extra clause makes the full formula potentially different: + # an entailed XOR cannot decide this partial fragment alone. + augmented=CNFFormula(4,xor.clauses+[[4]]) + assert gf2_control(augmented).frame_status=="INCONCLUSIVE" From fc3c41e293f3d6670ac5657af19990e6cdd264b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:47:19 +0100 Subject: [PATCH 38/48] benchmark: disjoint-seed GF2 gate positive-control and signed geometry ablation --- .../scripts/violation_cdcl_parity_probe.py | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 docs/ladder/scripts/violation_cdcl_parity_probe.py diff --git a/docs/ladder/scripts/violation_cdcl_parity_probe.py b/docs/ladder/scripts/violation_cdcl_parity_probe.py new file mode 100644 index 0000000..b71d327 --- /dev/null +++ b/docs/ladder/scripts/violation_cdcl_parity_probe.py @@ -0,0 +1,63 @@ +"""Post-pilot parity-vs-signed-geometry control on disjoint CDCL seeds. + +Run: + python docs/ladder/scripts/violation_cdcl_parity_probe.py \ + --seeds 6 --seed-start 100 --sizes 48 72 96 --orbits 3 --budget 5000 --json +""" +from __future__ import annotations + +import argparse +import json +import os +import platform +import sys +from dataclasses import asdict +from importlib.metadata import version, PackageNotFoundError +from pathlib import Path + +sys.path.insert(0,str(Path(__file__).resolve().parents[3])) +from backend.violation_cdcl_parity import PREDICTORS,parity_holdout + + +def main(): + p=argparse.ArgumentParser(description=__doc__) + p.add_argument("--seeds",type=int,default=6) + p.add_argument("--seed-start",type=int,default=100) + p.add_argument("--sizes",type=int,nargs="+",default=[48,72,96]) + p.add_argument("--orbits",type=int,default=3) + p.add_argument("--budget",type=int,default=5000) + p.add_argument("--swaps",type=int,default=160) + p.add_argument("--json",action="store_true") + args=p.parse_args() + result=parity_holdout(seeds=args.seeds,seed_start=args.seed_start, + sizes=tuple(args.sizes),orbits=args.orbits, + budget=args.budget,swaps=args.swaps) + try: + pysat_version=version("python-sat") + except PackageNotFoundError: + pysat_version="unavailable" + output={"design":"docs/ladder/VIOLATION_CDCL_PARITY_ADDENDUM.md", + "kind":"post-pilot exploratory GF(2) positive control vs Glucose4", + "instrument":{"python":sys.version.split()[0],"pysat":pysat_version, + "platform":platform.platform(),"github_sha":os.environ.get("GITHUB_SHA","local")}, + "parameters":vars(args), + "report":asdict(result)} + if args.json: + print(json.dumps(output,indent=2,sort_keys=True)) + return + print("Disjoint-seed GF(2) frame vs signed-topology CDCL prediction") + print(f"{result.formulas} formulae; seeds {result.seed_start}..{result.seed_start+result.seed_count-1}") + print("Actual independent algebraic frame:",result.status_counts) + print(f"Glucose4 censored fraction: {result.censored_call_fraction:.3f}") + for name,error in result.aggregate_mae.items(): + print(f" {name:36} LOFO MAE {error:.4f}") + if result.largest_size_holdout: + print("Largest n held out:",result.largest_size_holdout.mae_log2_capped_conflicts) + print(f"Median independent GF2 feature time: {result.median_gf2_ms:.3f} ms; " + f"Glucose4 call: {result.median_cdcl_ms:.3f} ms") + print("Machine-readable per-formula gate states and conflicts: use --json.") + print("No asymptotic SAT, Kakeya or prod-router claims.") + + +if __name__=="__main__": + main() From 585b85aaf7667b68268878caee3102a285cc3856 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:47:34 +0100 Subject: [PATCH 39/48] ci: reproduce disjoint CDCL topology corpus and audited existing GF2 frame comparator --- .github/workflows/violation-geometry-lab.yml | 41 +++++++++++++++++++- 1 file changed, 39 insertions(+), 2 deletions(-) diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml index 6c5d8a9..5574500 100644 --- a/.github/workflows/violation-geometry-lab.yml +++ b/.github/workflows/violation-geometry-lab.yml @@ -91,7 +91,7 @@ jobs: 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 + 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 @@ -123,9 +123,46 @@ jobs: 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/cdcl_topology.json + path: evidence/*.json retention-days: 30 From e43dbb8c3a2b87df0da42f37850edf166c412add Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:49:02 +0100 Subject: [PATCH 40/48] math: constructive GF2 boundary-cokernel obstruction and Tseitin forest witness --- backend/violation_tseitin_boundary.py | 179 ++++++++++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 backend/violation_tseitin_boundary.py diff --git a/backend/violation_tseitin_boundary.py b/backend/violation_tseitin_boundary.py new file mode 100644 index 0000000..aedbae7 --- /dev/null +++ b/backend/violation_tseitin_boundary.py @@ -0,0 +1,179 @@ +"""Constructive GF(2) graph-boundary theorem for fully recovered Tseitin CNFs. + +Let partial: F_2^E -> F_2^V map an edge bit to its two endpoints. +Then im(partial) is exactly the set of charge vectors with even XOR sum +on every connected component. This classical incidence fact is constructive, +and different from the real signed clause-variable graph Laplacian. + +Only *fully covered* recovered XOR encodings with each variable in exactly +two XOR equations are admitted. This experimental module neither changes +the λSAT trusted base nor claims a new complexity theorem. +""" +from __future__ import annotations + +from dataclasses import dataclass +from typing import Sequence + +from .cnf_utils import CNFFormula, verify_model +from .xor_extraction import extract_xors + + +@dataclass(frozen=True) +class BoundaryWitness: + vertices: int + edges: int + components: tuple[tuple[int,...],...] + rank: int + charges_per_component: tuple[int,...] + consistent: bool + odd_component_indices: tuple[int,...] + edge_bits: tuple[int,...] | None + + +def edge_boundary(vertices: int, edges: Sequence[tuple[int,int]], + values: Sequence[int]) -> tuple[int,...]: + """Compute GF(2) incidence boundary; each edge toggles BOTH endpoints.""" + if not isinstance(vertices,int) or isinstance(vertices,bool) or vertices<0: + raise ValueError("invalid vertex count") + if len(edges)!=len(values): + raise ValueError("edge/value count mismatch") + result=[0]*vertices + for (a,b),value in zip(edges,values): + if (not isinstance(a,int) or not isinstance(b,int) or + isinstance(a,bool) or isinstance(b,bool) or + a==b or not (0<=a BoundaryWitness: + """O(V+E) constructive component-parity test with a forest witness. + + Parallel edges are allowed, indexed separately, as in a multigraph. + Odd charge on a connected component is a left-kernel obstruction. + Otherwise choose non-tree edge bits zero and solve leaf-to-root along a + spanning forest. The proof uses no Gaussian inversion or solver oracle. + """ + if not isinstance(vertices,int) or isinstance(vertices,bool) or vertices<0: + raise ValueError("invalid vertex count") + if len(charges)!=vertices or any(c not in (0,1) for c in charges): + raise ValueError("charges must be one GF(2) bit per vertex") + adj=[[] for _ in range(vertices)] + for i,(a,b) in enumerate(edges): + if (not isinstance(a,int) or not isinstance(b,int) or + isinstance(a,bool) or isinstance(b,bool) or + not (0<=a RecoveredTseitin | None: + """Recover a GF(2) boundary system from *complete* short-XOR CNF. + + Admit only XOR fragments in which each variable belongs to exactly two + recovered constraints, so the XOR matrix is an unoriented graph boundary. + If coverage is partial or a variable has other incidence, refuse rather + than pretending general parity constraints are a graph. + """ + extracted=extract_xors(formula) + if not extracted.xors or extracted.num_xor_clauses!=len(formula.clauses): + return None + membership=[[] for _ in range(formula.num_vars)] + for ci,xor in enumerate(extracted.xors): + for var in xor.variables: + if not 1<=var<=formula.num_vars: + raise AssertionError("malformed recovered XOR variable") + membership[var-1].append(ci) + if any(len(groups)!=2 or groups[0]==groups[1] for groups in membership): + return None + edges=tuple((groups[0],groups[1]) for groups in membership) + charges=tuple(x.rhs for x in extracted.xors) + return RecoveredTseitin(len(extracted.xors),edges,charges,formula.num_vars) + + +@dataclass(frozen=True) +class TseitinDecision: + status: str # SAT | UNSAT | NOT_TSEITIN + rank: int | None + component_charges: tuple[int,...] | None + odd_component: tuple[int,...] | None + model: dict[int,bool] | None + + +def decide_tseitin_boundary(formula: CNFFormula) -> TseitinDecision: + """Constructively decide the recognized pure graph-boundary XOR subclass. + + UNSAT: the listed odd-charge XOR equation component sums to 0=1. + SAT: edge assignment from spanning tree is replayed on ORIGINAL CNF. + Other CNFs: NOT_TSEITIN. No production routing or certificate change. + """ + graph=recover_tseitin_graph(formula) + if graph is None: + return TseitinDecision("NOT_TSEITIN",None,None,None,None) + cert=solve_boundary(graph.vertices,graph.edges,graph.charges) + if cert.odd_component_indices: + k=cert.odd_component_indices[0] + return TseitinDecision("UNSAT",cert.rank,cert.charges_per_component, + cert.components[k],None) + model={v+1:bool(bit) for v,bit in enumerate(cert.edge_bits or ())} + if not verify_model(formula,model): + raise AssertionError("Tseitin spanning-forest witness failed CNF replay") + return TseitinDecision("SAT",cert.rank,cert.charges_per_component,None,model) From b514a6b973c64f7ceca193c3a9c9323a68769d28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:49:20 +0100 Subject: [PATCH 41/48] test: brute-force GF2 image/cokernel theorem and recovered Tseitin witnesses --- .../tests/test_violation_tseitin_boundary.py | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 backend/tests/test_violation_tseitin_boundary.py diff --git a/backend/tests/test_violation_tseitin_boundary.py b/backend/tests/test_violation_tseitin_boundary.py new file mode 100644 index 0000000..81b7bcd --- /dev/null +++ b/backend/tests/test_violation_tseitin_boundary.py @@ -0,0 +1,109 @@ +"""Independent finite checks of graph-boundary image = even component charges.""" +from itertools import product +from random import Random +import pytest + +from backend.cnf_utils import CNFFormula,verify_model +from backend.violation_cdcl_topology import generate_formula +from backend.violation_tseitin_boundary import ( + solve_boundary,edge_boundary,recover_tseitin_graph, + decide_tseitin_boundary) +from backend.xor_extraction import gf2_xor_solve + + +def test_path_and_explicit_odd_charge_witness(): + edges=((0,1),(1,2)) + yes=solve_boundary(3,edges,(1,0,1)) + assert yes.consistent and yes.rank==2 + assert yes.edge_bits==(1,1) + assert edge_boundary(3,edges,yes.edge_bits)==(1,0,1) + no=solve_boundary(3,edges,(1,0,0)) + assert not no.consistent + assert no.odd_component_indices==(0,) + assert no.components==((0,1,2),) + assert no.charges_per_component==(1,) + assert no.edge_bits is None + + +def test_disconnected_and_isolated_obstruction(): + edges=((0,1),(2,3)) + yes=solve_boundary(5,edges,(1,1,0,0,0)) + assert yes.consistent and yes.rank==2 + assert len(yes.components)==3 + no=solve_boundary(5,edges,(1,1,0,0,1)) + assert not no.consistent + assert no.odd_component_indices==(2,) + assert no.components[2]==(4,) + assert no.charges_per_component==(0,0,1) + + +def test_parallel_edges_and_empty_graph_are_handled(): + edges=((0,1),(0,1)) + for charges in ((0,0),(1,1)): + result=solve_boundary(2,edges,charges) + assert result.consistent + assert edge_boundary(2,edges,result.edge_bits)==charges + assert not solve_boundary(2,edges,(1,0)).consistent + assert solve_boundary(0,(),()).rank==0 + + +def test_random_graphs_match_bruteforce_gf2_image_and_rank(): + rng=Random(20261029) + for _ in range(120): + vertices=rng.randrange(1,7) + possible=[(a,b) for a in range(vertices) for b in range(a+1,vertices)] + edges=tuple(rng.sample(possible,rng.randrange(min(8,len(possible))+1))) + if edges and rng.randrange(3)==0: + edges=edges+(rng.choice(edges),) # allow multigraph boundary + reachable={edge_boundary(vertices,edges,x) for x in product((0,1),repeat=len(edges))} + for charges in product((0,1),repeat=vertices): + cert=solve_boundary(vertices,edges,charges) + assert cert.consistent==(charges in reachable) + assert cert.rank==vertices-len(cert.components) + assert 2**cert.rank==len(reachable) + if cert.consistent: + assert edge_boundary(vertices,edges,cert.edge_bits)==charges + else: + assert all(cert.charges_per_component[k]==1 for k in cert.odd_component_indices) + + +def test_fully_recovered_tseitin_has_exact_graph_obstruction(): + for family in ("tseitin-prism","tseitin-rewired"): + for n in (12,48,72,96): + for seed in range(4): + f=generate_formula(family,n,seed) + graph=recover_tseitin_graph(f) + assert graph is not None + assert graph.vertices==2*n//3 + assert len(graph.edges)==n + decision=decide_tseitin_boundary(f) + linear=gf2_xor_solve(f) + assert decision.status==linear.status + assert decision.status==("SAT" if seed%2==0 else "UNSAT") + assert decision.rank==graph.vertices-1 + if decision.status=="SAT": + assert decision.model is not None + assert verify_model(f,decision.model) + else: + assert decision.odd_component is not None + assert sum(graph.charges[v] for v in decision.odd_component)%2==1 + + +def test_non_graph_and_partial_xor_must_be_rejected(): + random3=generate_formula("uniform3",48,99) + assert recover_tseitin_graph(random3) is None + assert decide_tseitin_boundary(random3).status=="NOT_TSEITIN" + # One XOR variable belongs to exactly one parity equation: not a boundary. + xor=CNFFormula(3,[[1,2,3],[1,-2,-3],[-1,2,-3],[-1,-2,3]]) + assert recover_tseitin_graph(xor) is None + assert decide_tseitin_boundary(xor).status=="NOT_TSEITIN" + with_extra=CNFFormula(3,xor.clauses+[[1]]) + assert recover_tseitin_graph(with_extra) is None + + +def test_invalid_boundary_inputs(): + with pytest.raises(ValueError):solve_boundary(2,((0,2),),(0,0)) + with pytest.raises(ValueError):solve_boundary(2,((0,0),),(0,0)) + with pytest.raises(ValueError):solve_boundary(2,(),(0,)) + with pytest.raises(ValueError):solve_boundary(2,(),(2,0)) + with pytest.raises(ValueError):edge_boundary(2,((0,1),),(2,)) From 1bc05e137445e6a544161230d46a79741609f05e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:49:32 +0100 Subject: [PATCH 42/48] ci: brute-force check image-cokernel theorem and constructive Tseitin witnesses --- .github/workflows/violation-geometry-lab.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/violation-geometry-lab.yml b/.github/workflows/violation-geometry-lab.yml index 5574500..c2ab5f4 100644 --- a/.github/workflows/violation-geometry-lab.yml +++ b/.github/workflows/violation-geometry-lab.yml @@ -33,7 +33,8 @@ jobs: 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_laplacian.py \ + backend/tests/test_violation_tseitin_boundary.py - name: Reproduce assignment-held-out controls run: | mkdir -p evidence From 90cdcf2ffebe862b04e95a3496142b4e9de522df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:50:03 +0100 Subject: [PATCH 43/48] docs: rigorous finite graph boundary proof and measured GF2 CDCL evidence --- .../VIOLATION_TSEITIN_BOUNDARY_THEOREM.md | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md diff --git a/docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md b/docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md new file mode 100644 index 0000000..c628b43 --- /dev/null +++ b/docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md @@ -0,0 +1,60 @@ +# Tseitin's exact graph-boundary obstruction + +**29 October 2026 | dev/kakeya-violation-frame.** P = elementary classical finite graph theorem with proof below; M = bounded tests and external CDCL results; H/S = any proposed bridge to Kakeya, local smoothing, n-manifolds, or a new asymptotic SAT advantage. This is NOT a new theorem in the mathematical literature. + +## Typed GF(2) boundary (not the real signed Laplacian) + +Let G=(V,E) be a finite undirected multigraph without self-loops. Treat each edge as a Boolean variable and each vertex as an XOR parity equation with charge b_v. The linear boundary is + + partial: GF(2)^E -> GF(2)^V, + (partial x)_v = XOR_{e incident to v} x_e. + +For each connected component C define q_C(b)=XOR_{v in C} b_v. + +**Classical proposition (P):** + + im(partial) = {b : q_C(b)=0 for every connected component C} + rank(partial) = |V| - number_of_components(G) + dim coker(partial) = number_of_components(G). + +**Proof (necessity).** XOR all vertex equations over C. Each internal edge occurs exactly twice, hence cancels mod 2. Thus q_C(b)=0. + +**Proof (sufficiency).** Choose a rooted spanning forest, set non-tree edge bits to zero, and traverse each tree from leaves to root. At a non-root vertex v, set its parent edge bit equal to the residual charge at v and XOR that value into its parent's charge. All non-root equations hold by construction, and each root residual equals q_C(b), which is zero by hypothesis. This constructs x in O(|V|+|E|) from adjacency lists. Since these component conditions are independent and sufficient, rank(partial)=|V|-#components, while the cokernel has one GF(2) degree per component. Equivalently, component indicator vectors span the left kernel of partial. + +The implementation in [violation_tseitin_boundary.py](../../backend/violation_tseitin_boundary.py) returns either verified edge bits (SAT) or an odd-charge connected-component witness of the XOR contradiction (UNSAT). Its tests check all charge vectors against an independent brute-force image on seeded small graphs, including multiedges, disconnected components and isolated vertices. + +### CNF recovery contract + +Use the existing λSAT complete XOR-group extractor. Admit the graph-boundary specialization only if every original clause belongs to a recovered XOR encoding and every declared variable appears in **exactly two distinct XOR equations**, determining that edge's two endpoint vertices. Reconstructed SAT assignments are independently replayed on the original CNF. Partial-XOR, non-graph-XOR and unmatched-clause inputs return NOT_TSEITIN. The module leaves the existing XOR extractor, certified solver decisions, ACAF, and main untouched. + +This finite boundary map is DIFFERENT from the real signed clause-variable graph Laplacian developed in the earlier round. The latter has energy sum_(c,v) (z_c - sigma_cv z_v)^2 and a kernel indexed by balanced signed components; its variables are real-valued at clause and variable vertices. The characteristic-two boundary map acts between edge and vertex GF(2) chains. In particular, DO NOT transfer real-Laplacian rank, spectral positivity or Kakeya smoothing claims to partial*partial^T over GF(2): the characteristic-two calculation requires its own proof. The obstruction used here is the left cokernel of partial. + +## External CDCL and GF(2) positive control (M) + +[Disjoint-seed exploratory protocol, written after the first pilot](VIOLATION_CDCL_PARITY_ADDENDUM.md): generator seeds 100–105, declared variables 48/72/96, six generator families, 3 independent signed-relabeling Glucose4 runs per formula, conflict budget 5,000. There were **108 distinct labeled CNFs and 324 solver calls; 2.16% UNKNOWN/censored**. + +The existing λSAT GF(2) frame independently resolved **36/36 generated fully parity-encoded Tseitin CNFs**: 18 SAT with a verified algebraic model and 18 UNSAT by inconsistency of global charges. It returned INCONCLUSIVE for all 72 random 3-CNF examples. + +Leave-one-generator-family-out MAE for log2(1+budget-capped CDCL conflicts), lower is better: + +| Formula-only predictors | MAE | +|---|---:| +| Classical (degree, unsigned cycles, density, polarity, XOR coverage) | 2.2298 | +| Classical + signed connection | 2.2501 | +| Classical + GF(2) rank / consistency | 1.3121 | +| Classical + GF(2) + support-rewired null | 1.3051 | +| Classical + GF(2) + signed connection | **1.2623** | + +The main improvement is from the existing GF(2) algebraic frame, not an inferred Kakeya inequality. The signed connection offers a modest *post-hoc, exploratory* incremental improvement after conditioning on rank, but on the held-out largest n=96, signed and null errors were 1.16224 and 1.16152 respectively (null fractionally better). This does not establish a robust distinctive signal. + +GitHub Actions median feature times: ~3.69 ms for baseline feature preparation; an additional ~4.42 ms for signed/null preparation; ~0.85 ms for the GF(2) gate audit; versus ~0.32 ms for a Glucose4 solve. These stages have overlapping work, so they are not additive production timing predictions, but their scale defeats a current **routing speedup** claim. + +The raw per-instance solver results, oracle statuses and exact GF(2) gate controls are preserved as JSON workflow artifacts. The prism family shares one graph topology per size; its differently charged examples are not independent nonisomorphic graphs. The rewired cubic family uses independently switched graphs, and tests check seeded nonisomorphism. The experiment retains the earlier null-negative DPLL results and the first 36-formula CDCL pilot. + +## Reproduction and next formal step + + python -m pytest -q backend/tests/test_violation_tseitin_boundary.py + python -m pytest -q backend/tests/test_violation_cdcl_topology.py backend/tests/test_violation_cdcl_parity.py + python docs/ladder/scripts/violation_cdcl_parity_probe.py --seeds 6 --seed-start 100 --sizes 48 72 96 --orbits 3 --budget 5000 --json + +A meaningful Lean target is the image/cokernel equivalence for a finite graph's GF(2) boundary together with its constructive spanning-forest witness. That would be a formalized classical result. A geometric or analytic lift would need an additional typed transport theorem, not yet demonstrated. From 6710ab93316b990c93159a867835dee728cc4d30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Thu, 29 Oct 2026 19:50:35 +0100 Subject: [PATCH 44/48] docs: reconcile ETH-Kakeya failures with constructive GF2 boundary and CDCL evidence --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 04b2381..ec7e062 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ Headless. No web UI. No *trust-me*. -> **Experimental development branch — ETH × Kakeya incidence:** the [initial bridge](docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md) and its [cross-instance negative result](docs/ladder/VIOLATION_CROSS_INSTANCE_REPORT.md) remain in the record. Our latest [signed-connection and observer-orbit audit](docs/ladder/VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md) distinguishes two things: a finite, gauge-invariant graph Laplacian identity that can be proved, and a proposed SAT-hardness predictor that still loses to classical structure on held-out small formulas. A moving frame should not mistake the observer's variable ordering for the formula's intrinsic difficulty. These are research instruments, **not** new solver certificates or asymptotic hardness results; no production decision path is changed. +> **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 From 0096e7cd4c8d79ef3db1e4f2fc4b746fd4417807 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 30 Oct 2026 22:15:19 +0000 Subject: [PATCH 45/48] Skip Kissat-dependent tests when unavailable Co-authored-by: jesusvilela <19171959+jesusvilela@users.noreply.github.com> --- backend/tests/test_acaf.py | 10 ++++++++++ backend/tests/test_metametasolver.py | 9 +++++++++ backend/tests/test_metasolver.py | 8 ++++++++ 3 files changed, 27 insertions(+) diff --git a/backend/tests/test_acaf.py b/backend/tests/test_acaf.py index c138b80..21591bb 100644 --- a/backend/tests/test_acaf.py +++ b/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_kissat = pytest.mark.skipif( + shutil.which("kissat") is None, + reason="Kissat binary not available", +) + 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_kissat 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_kissat 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) diff --git a/backend/tests/test_metametasolver.py b/backend/tests/test_metametasolver.py index 8cd9c0e..5fe290e 100644 --- a/backend/tests/test_metametasolver.py +++ b/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_kissat = pytest.mark.skipif( + shutil.which("kissat") is None, + reason="Kissat binary not available", +) + 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_kissat 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_kissat 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_kissat def test_portfolio_agrees_with_ground_truth(self): # cross-check the portfolio verdict against a single certified solve from backend.metasolver import metasolve diff --git a/backend/tests/test_metasolver.py b/backend/tests/test_metasolver.py index 60ec65c..59cbec2 100644 --- a/backend/tests/test_metasolver.py +++ b/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_kissat = pytest.mark.skipif( + shutil.which("kissat") is None, + reason="Kissat binary not available", +) + 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_kissat 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_kissat 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: From 32b0ab1ba1d2ae2d7a6734fa2b66029f51dab192 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 30 Oct 2026 22:17:03 +0000 Subject: [PATCH 46/48] Gate CDCL tests and fix CI install commands Co-authored-by: jesusvilela <19171959+jesusvilela@users.noreply.github.com> --- .github/workflows/tests.yml | 7 ++++--- backend/tests/test_acaf.py | 10 +++++----- backend/tests/test_metametasolver.py | 12 ++++++------ backend/tests/test_metasolver.py | 10 +++++----- 4 files changed, 20 insertions(+), 19 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 10904be..cd998d8 100644 --- a/.github/workflows/tests.yml +++ b/.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,6 +60,7 @@ 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. @@ -75,7 +77,6 @@ jobs: - 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 run: | diff --git a/backend/tests/test_acaf.py b/backend/tests/test_acaf.py index 21591bb..c0e0552 100644 --- a/backend/tests/test_acaf.py +++ b/backend/tests/test_acaf.py @@ -22,9 +22,9 @@ from backend.cnf_utils import CNFFormula # noqa: E402 from backend.eval.generators import pigeonhole # noqa: E402 -requires_kissat = pytest.mark.skipif( - shutil.which("kissat") is None, - reason="Kissat binary not available", +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", ) @@ -124,13 +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_kissat + @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_kissat + @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) diff --git a/backend/tests/test_metametasolver.py b/backend/tests/test_metametasolver.py index 5fe290e..9630a85 100644 --- a/backend/tests/test_metametasolver.py +++ b/backend/tests/test_metametasolver.py @@ -22,9 +22,9 @@ default_arms, metametasolve, ) -requires_kissat = pytest.mark.skipif( - shutil.which("kissat") is None, - reason="Kissat binary not available", +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", ) @@ -51,7 +51,7 @@ def test_structured_islands_decided_instantly_by_one_arm(self): class TestTunnelPortfolio: - @requires_kissat + @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) @@ -60,14 +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_kissat + @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_kissat + @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 diff --git a/backend/tests/test_metasolver.py b/backend/tests/test_metasolver.py index 59cbec2..8fa371b 100644 --- a/backend/tests/test_metasolver.py +++ b/backend/tests/test_metasolver.py @@ -24,9 +24,9 @@ from backend.eval.generators import pigeonhole # noqa: E402 from backend.metasolver import metasolve # noqa: E402 -requires_kissat = pytest.mark.skipif( - shutil.which("kissat") is None, - reason="Kissat binary not available", +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", ) @@ -97,14 +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_kissat + @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_kissat + @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: From 1bd1b9051d0f4b94e9df1f84af02d22c25e69345 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 30 Oct 2026 22:18:10 +0000 Subject: [PATCH 47/48] Fix certification workflow solver setup Co-authored-by: jesusvilela <19171959+jesusvilela@users.noreply.github.com> --- .github/workflows/tests.yml | 32 ++++++++++++++------------------ 1 file changed, 14 insertions(+), 18 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index cd998d8..2ee0a9d 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -62,26 +62,12 @@ jobs: 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 - - - 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 @@ -90,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: | From bdf306799b971f29272e502b7c1253dc4ba2e0c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jes=C3=BAs=20Vilela=20Jato?= Date: Tue, 10 Nov 2026 11:07:39 +0100 Subject: [PATCH 48/48] test: exhaustively verify GF2 graph-boundary image for every simple graph up to four vertices --- .../tests/test_violation_tseitin_boundary.py | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/backend/tests/test_violation_tseitin_boundary.py b/backend/tests/test_violation_tseitin_boundary.py index 81b7bcd..46351dc 100644 --- a/backend/tests/test_violation_tseitin_boundary.py +++ b/backend/tests/test_violation_tseitin_boundary.py @@ -107,3 +107,29 @@ def test_invalid_boundary_inputs(): with pytest.raises(ValueError):solve_boundary(2,(),(0,)) with pytest.raises(ValueError):solve_boundary(2,(),(2,0)) with pytest.raises(ValueError):edge_boundary(2,((0,1),),(2,)) + +def test_exhaustive_all_simple_graphs_through_four_vertices(): + """Independent exact image/rank check for every simple graph on <=4 nodes.""" + from itertools import combinations + + for vertices in range(5): + possible = tuple(combinations(range(vertices), 2)) + for mask in range(1 << len(possible)): + edges = tuple(edge for bit, edge in enumerate(possible) if (mask >> bit) & 1) + reachable = { + edge_boundary(vertices, edges, bits) + for bits in product((0, 1), repeat=len(edges)) + } + # Connected components are read from the returned certificate; + # enumerate every possible charge vector independently. + for charges in product((0, 1), repeat=vertices): + result = solve_boundary(vertices, edges, charges) + assert result.consistent == (charges in reachable) + assert result.rank == vertices - len(result.components) + assert len(reachable) == (1 << result.rank) + if result.consistent: + assert edge_boundary(vertices, edges, result.edge_bits) == charges + else: + assert all(result.charges_per_component[i] == 1 + for i in result.odd_component_indices) +