RankTestExact
plain-language theorem explainer
RankTestExact defines the existence of a Boolean oracle true exactly when the linear system of a BWD-3 model admits an admissible solution. Complexity researchers studying exact SAT reductions via linear encodings in Recognition Science would cite this interface. The definition is a direct existential statement equating the flag to the LinearFeasible predicate with no added computational content.
Claim. Let $n,N$ be natural numbers and let $M$ be a linear encoding model for a CNF formula in $n$ variables with dimension $N$. The exact rank test property holds when there exists a Boolean value $d$ such that $d$ equals true if and only if there exists an admissible vector $u$ satisfying the linear equation $L u = b$.
background
The BWD3Model structure encodes a 3SAT instance as a linear system $L u = b$ over the rationals together with an admissibility predicate on solutions. The model supplies soundness and completeness axioms relating CNF satisfiability to admissible linear witnesses, plus a Schur-pinch condition that excludes fractional solutions. LinearFeasible is the proposition asserting existence of such an admissible witness for the given model. The module works in the setting of Boolean phase states in the linearized log-domain model, where admissible solutions must project to discrete Boolean assignments with no fractional witnesses.
proof idea
The definition is realized by existentially quantifying a Boolean flag and stating its logical equivalence to the LinearFeasible predicate for the model. No lemmas or tactics are invoked beyond the direct statement of the existential.
why it matters
This definition supplies the abstract interface consumed by the classical rank test theorem, which constructs the decider via the decide tactic, and by the SAT decider theorem that derives an exact satisfiability predicate from it. It fills the scaffold stage for an optional algorithmic interface allowing a rank or null-space test to be plugged in as a Boolean oracle. The construction supports exact decision procedures within the complexity analysis of SAT encodings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.