ResolutionTime
plain-language theorem explainer
The resolution-time record packages a SAT instance with an octave count and a proposition that R-hat reaches minimum defect on the encoded J-cost landscape. Complexity theorists bridging Recognition Science to P versus NP cite this packaging when quantifying global recognition time against Turing locality. The definition assembles the three fields directly with no computation or proof obligation.
Claim. A resolution time for a SAT instance consists of the instance (with positive numbers of variables and clauses), a natural number of octaves, and a proposition asserting that the minimum J-cost defect is attained.
background
The module constructs a bridge from Recognition Science to classical complexity classes. SATInstance is the structure carrying positive counts of variables and clauses whose J-cost landscape encoding has total cost zero precisely when the instance is satisfiable. J-cost itself is the functional obeying the Recognition Composition Law, with R-hat acting as the contractive operator that drives defect to zero on the full Z^3 lattice. The module document states that the encoding step and the non-naturality of the R-hat certificate (operation on the entire lattice rather than polynomial truth tables) are already established, while convergence rate depends on the spectral gap.
proof idea
This is a direct structure definition that packages the SAT instance, the octave count, and the reaches-minimum proposition. No lemmas are applied; the declaration simply declares the three fields.
why it matters
The record supplies the time parameter inside the SeparationClaim structure, which concludes that superpolynomial simulation overhead from global J-cost minimization to local Turing steps implies P ≠ NP. It occupies the convergence-rate slot in the four-step strategy of the module document, linking R-hat's action on the phi-ladder to the open Turing-simulation question. The parent claim remains conditional on faithful encoding and on the octave count growing faster than any polynomial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.