landscape_linear
plain-language theorem explainer
For any SAT instance the sum of variables and clauses is at least the number of variables. Researchers assembling certificates for the Recognition Science to Turing complexity bridge cite this linear size relation. The proof is a direct one-line application of the standard natural-number addition inequality.
Claim. For every SAT instance with $n$ variables and $m$ clauses, $n + m$ is at least $n$.
background
In the TuringBridge module a SATInstance is a structure carrying a positive natural number of variables and a positive natural number of clauses; the module encodes such an instance as a J-cost landscape whose minimum cost is zero precisely when the clauses are satisfied. The surrounding context is the open bridge from R-hat minimization on the full Z^3 ledger to classical Turing-machine complexity classes, with encoding faithfulness and non-naturality of the R-hat certificate already in place. Upstream results supply the J-cost definition and the ledger factorization that make the landscape encoding possible.
proof idea
The proof is a one-line term that applies the Nat.le_add_right lemma to the two natural numbers n_vars and n_clauses.
why it matters
The declaration supplies the landscape_linear field inside the TuringBridgeCert structure that collects the minimal facts needed for the P versus NP bridge. It fills the basic size relation required by the module's strategy while the superpolynomial simulation overhead from R-hat to Turing tape remains the open gap identified in the module documentation and the referenced paper section on Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.