Certified frame-first SAT middleware — structured regions before CDCL, certified verdicts after every path.
Load first. Non-negotiable. This is the document that keeps the science honest; everything else in the repository answers to it.
This project has two temperaments living in one body: an imaginative one that reaches for deep geometric and algebraic structure in SAT hardness, and a skeptical one that refuses to believe anything it has not verified. They are not rivals. They are conjugates — and the whole method is to let them cancel into what survives.
These rules are absolute. A contribution that violates one is wrong regardless of how beautiful it is.
A name is not a proof. “EmperorEmpressTheorem”, “P_neq_NP”,
“equivalent_to_BQP” — the label carries no truth. Check the body. Several
Lean “theorems” in this project’s heritage proved 168 = 168 or
1 < degeneracy under an impressive name; that is documented, not hidden.
Verify before you trust — empirically, end to end. Kissat is not in the Trusted Computing Base; every SAT result is model-replayed and every UNSAT result is proof-checked. Every research claim is bound to a test. If it isn’t tested, it isn’t claimed.
No vocabulary without a contract. You may not import a word — sheaf,
gyrovector, holonomy, chromatic height — unless you can state its
input → invariant → action → benchmark. backend/complexity/contracts.py
enforces this: every invariant carries its promise, its theorem (if any), and
its honest limit, and a test fails if a “carrier” cites no theorem.
Label the register. Every claim is one of: proven (a theorem, cited),
measured (a benchmark, with its scope), or speculative (a lens, said so).
Mixing these is the cardinal sin. “Rich obstruction” is not “superpolynomial
lower bound”; 48× more coupling channels is a count, not a hardness proof.
Report what the data said, not what you hoped. Every pre-registered prediction in this project’s history that failed is recorded as having failed. The negative results (cheap graph invariants do not carry hardness; the symmetry channel collapses in characteristic 2; “NS ≥ width” was false, Tseitin being the witness) are load-bearing, not embarrassments.
The verdict casts a scalar; the object need not be one. Hardness is a scalar because “harder” is an order relation. But the object it measures may be a field, a variety, a group. Do not mistake the shadow for the thing — and do not pretend the shadow is dispensable when a decision is demanded.
This is the interpretive frame the research half is written in. It is a lens,
explicitly — it earns its place only where Part I lets it. Where it has produced
theorem-backed or benchmarked objects, they live in docs/ladder/.
The obstruction is where 0 stops being a point. In a division algebra 0 is
isolated; leave them (sedenions) and the zero-set of multiplication becomes a
variety — the zero divisors. Hardness lives exactly there: the rank
deficiency / cokernel of an obstruction operator. Executable form:
nullstellensatz_degree (the Nullstellensatz degree over GF(2)).
Emperor and Empress. Conjugation is an exact anti-pairing: for the octonion
associator, A_conj = −A_std (verified, cos = −1 to machine precision).
Opposition is not loss; the anti-pair is the conserved record of a collapse.
The verifier is the Emperor to the imaginer’s Empress — and what survives their
cancellation is the part that is actually true.
Depth is algebra-relative; stratify, don’t collapse. A formula’s hardness is
the depth at which its obstruction becomes irreducible in a given proof
algebra — and that depth changes with the algebra (PHP: width 2, NS-degree 4;
Tseitin: width 4, NS-degree 3 — incomparable). You never collapse the depth to
a point; you read it stratum by stratum (resolution width, NS degree, chromatic
height, XOR-frame). Solving = finding the algebra where the obstruction is
shallow — which is exactly what a portfolio solver does, and what
xor_extraction cheaply detects.
The drone. Smoothing dissolves the removable part of hardness into simplicity (rationalize the torsion away; relax to a convex program). What survives every smoothing is the irreducible obstruction — the drone. The point of every invariant here is to hear that one conserved note precisely, and never to let it be smoothed to zero.
The imaginer proposes; the skeptic disposes; and the method is the cancellation. A geometric idea (Part II) is admitted only once it is turned into a computable, contracted, tested object (Part I) — and when it fails that test, the failure is reported and kept. This is why the ladder’s honest survivors are all classical (resolution width, Nullstellensatz degree, XOR/Gaussian frame detection), and why the exceptional structure (𝔤₂, G₂, braids) is documented as real mathematics that names hard objects without cheapening them — never as a solved P vs NP.
If you are extending this work: bring your wildest idea. Then make it a function with a contract and a test, run it, and write down what actually happened. That is the whole discipline, and it is the only thing that has ever moved this project forward.