JCostLandscape
plain-language theorem explainer
JCostLandscape encodes a SAT instance as a J-cost landscape on which each clause contributes a local defect term. Researchers bridging Recognition Science recognition dynamics to classical complexity classes cite this structure when analyzing R-hat minimization. The declaration is a structure definition that assembles the underlying SATInstance, sets landscape size to the sum of variables and clauses, and includes the zero-cost equivalence proposition.
Claim. Let $S$ be a SAT instance with $n$ variables and $m$ clauses. A J-cost landscape for $S$ is the structure consisting of $S$, the landscape size $n+m$, and the proposition that minimum J-cost equals zero if and only if $S$ is satisfiable.
background
The module develops the bridge from Recognition Science to Turing complexity by encoding SAT instances as J-cost landscapes on which R-hat acts. A SATInstance is the structure carrying positive numbers of variables and clauses. The defect functional equals J for positive arguments and supplies the local cost contribution per clause.
proof idea
This is a structure definition that packages an SATInstance with its derived landscape size equal to the sum of variables and clauses together with a field of type Prop for the min-cost equivalence.
why it matters
The structure supplies the encoding step in the P versus NP bridge. It is referenced by the encoding_faithful theorem, which asserts zero J-cost exactly on satisfiable instances, and by the TuringBridgeCert structure that assembles the remaining open pieces including non-naturality of the R-hat certificate. The construction rests on the Recognition Composition Law and contractivity properties but leaves the superpolynomial Turing simulation overhead unresolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.