ResolutionTime
plain-language theorem explainer
ResolutionTime records the octave count at which R-hat drives J-cost defect to its global minimum on a SAT-encoded landscape. Complexity theorists examining the P versus NP question through recognition operators would cite the record when measuring global lattice minimization against local Turing steps. The declaration is a bare structure definition with three fields and no computational content.
Claim. For a SAT instance $S$ with $n$ variables and $m$ clauses, a resolution time consists of the instance $S$, a natural number $k$ of octaves, and the proposition that the recognition operator reaches its minimum J-cost defect on the landscape of $S$ after $k$ octaves.
background
The module sets up a bridge from Recognition Science to classical complexity: R-hat operates on the full Z³ ledger while Turing machines use local tape rules. SATInstance encodes an instance with $n$ variables and $m$ clauses; each clause contributes a local term to total J-cost, which reaches zero precisely when the instance is satisfiable. Upstream imports supply JcostCore for the landscape definition and the active-edge count A from IntegrationGap.
proof idea
The declaration is a structure definition; it introduces the type with no proof body or reduction steps.
why it matters
ResolutionTime supplies the time parameter inside SeparationClaim, which states that if R-hat resolves SAT instances in time no polynomial Turing machine can match then P ≠ NP. It occupies the convergence-rate slot in the four-step strategy of the module documentation, connecting R-hat's global J-cost minimization to the classical separation. The remaining open piece is the Turing simulation overhead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.