Bilateral Deficiency: Residual SAT Optimisation and Independent Domination in Regular-DIM Graphs

Abstract

Unrefereed candidate. No journal submission, external specialist review, unaffiliated independent reproduction, or full proof-assistant formalisation of the universal theory has been undertaken. This release defines bilateral deficiency as the minimum deficiency of a bipolar residual restriction. It proves a size-preserving bijection with independent dominating sets of clause-literal formula graphs, a generating-polynomial identity, algebraic operations, MaxSAT recovery, and a fixed-width complexity boundary. For regular graphs equipped with a dominating induced matching, bilateral deficiency is exactly the gap i(G) - μ*(G). Within the cubic-DIM class, the manuscript proves a constructive 7/6 upper bound, constructs connected linear-gap families, and proves that order 50 is the minimum possible order of a violation. This minimum-order statement is explicitly restricted to cubic graphs admitting a dominating induced matching; minimum order outside that class remains open. The core artifact includes source, witnesses, semantic and structural checks, three finite threshold encodings, four native LRAT derivations, three Lean-checked LRAT paths, a parser-independent Lean proof of the eight-variable terminal signature, and a clean-room producer-side encoding audit. These finite checks do not formalise every universal theorem. The optional 5.79 GB LRAT proof object is deposited as a lossless 1.17 GB Zstandard transport with hashes for both layers; it is not part of the minimum replay burden. This is an immutable child of the TxGraffiti conjecture 3 resolution (DOI 10.5281/zenodo.21852504). The scholarly author is Anonymous. Ian Pitchford acts only as package maintainer and publisher. Original prose, data, and figures are licensed CC BY 4.0; original code is MIT licensed; third-party material retains its upstream terms. See LICENSE.md and the checksum inventories inside the package.