[jesusvilela]

Research-only continuation — draft, not ready to merge

This PR preserves the negative ETH/Kakeya/λSAT incidence experiments while extracting a classical, constructive GF(2) graph-boundary theorem and reproducible external CDCL controls. No production SAT/UNSAT verdict, certification, or ACAF dispatch path changes.

Exact finite mathematics (P, classical proof plus tested construction; NOT Lean-formalized)

For the graph boundary partial: GF(2)^E -> GF(2)^V, the image consists exactly of vertex charge vectors whose XOR sum is even on each connected component. Rank(partial) = |V| - #components. A spanning-forest algorithm constructs an edge assignment in the consistent case or returns an odd-charge component as an explicit linear obstruction otherwise. The recognition layer requires full CNF XOR coverage and exactly two XOR incidences per variable, otherwise refuses the specialization. Crucially, this GF(2) cokernel differs from the real signed clause-variable connection Laplacian; no characteristic-two spectral theorem is assumed.

Read: docs/ladder/VIOLATION_TSEITIN_BOUNDARY_THEOREM.md and backend/violation_tseitin_boundary.py.

Measured finite external CDCL experiment (M, NOT an ETH/Kakeya theorem)

• PySAT Glucose4 bounded by conflicts, SAT models independently replayed, UNKNOWN calls counted as censored.
• Six generator families: random, local, community and hub 3-CNFs, plus cubic prism and rewired Tseitin. Non-isomorphism checks on seeded rewired cubic graphs. Sign- and degree-margin-preserving topology rewiring nulls.
• Pre-registered original hypothesis and explicitly post-pilot GF(2) comparator addendum.
• Initial 36 CNFs: structural LOFO log2-capped-conflict MAE 2.054; signed 1.986; rewired null 1.939 — the null did better.
• Disjoint seed IDs 100–105: 108 labeled CNFs, 324 Glucose4 calls, 2.16% censored. Classical baseline 2.230; signed alone 2.250; baseline + existing GF(2) rank/consistency 1.312; GF(2) + signed 1.262; GF(2) + matched rewired topology null 1.305.
• At largest-size n=96 held-out fold, signed vs null difference reverses (1.16224 vs 1.16152). Potential incremental signed signal remains exploratory and unconfirmed; feature computation is still slower than median CDCL solving on this corpus.
• Existing GF(2) frame resolved all 36 generated pure-parity Tseitin CNFs (18 SAT, 18 UNSAT); 72 non-parity cases were inconclusive.

Review gates before any promotion

Verify the constructive proof and its exact relation to code, repeat on genuinely new nonisomorphic graph topologies and additional CDCL engines, use stronger matched controls and censoring-aware analysis, account for all feature time, and formalize the graph-boundary proposition in Lean before calling it Lean-verified.

DO NOT MERGE as a solver improvement. The production trust base is unchanged, no complexity-class result is implied, and no continuous Kakeya or local-smoothing transport theorem has been proved.

Reports: docs/ladder/ETH_KAKEYA_VIOLATION_GEOMETRY.md; VIOLATION_CROSS_INSTANCE_REPORT.md; VIOLATION_SIGNED_CONNECTION_ORBIT_REPORT.md; VIOLATION_CDCL_TOPOLOGY_PREREG.md; VIOLATION_CDCL_PARITY_ADDENDUM.md; VIOLATION_TSEITIN_BOUNDARY_THEOREM.md. The isolated .github/workflows/violation-geometry-lab.yml uploads raw JSON for successful and unsuccessful outcomes.