RecognitionComplete
plain-language theorem explainer
RecognitionComplete packages dual complexity functions Tc (internal evolution steps) and Tr (observation operations) with Tc subpolynomial and Tr at least linear. Researchers examining ledger-based separations between computation and recognition would reference the structure to frame hypothetical distinctions in P versus NP. The declaration is a plain structure definition that introduces the fields and bounds without further derivation.
Claim. A structure consisting of maps $T_c, T_r : ℕ → ℕ$ such that there exist $c, k ∈ ℝ$ with $0 < k < 1$ and $T_c(n) ≤ c n^k log n$ for all $n > 0$, together with $c' > 0$ such that $T_r(n) ≥ c' n$ for all $n > 0$.
background
The module is explicitly marked scaffold and exploratory; it examines ledger-style dual complexity but lies outside the verified certificate chain. Tc records internal evolution steps while Tr records observation operations. The local setting treats the ledger's double-entry structure as forcing an information-theoretic barrier between computation and observation.
proof idea
Structure definition that directly declares the four fields: the two maps and the two existential bounds on their growth rates.
why it matters
The structure supplies the complexity data consumed by ClayBridge, clay_bridge_theorem, CompleteModel, and main_resolution inside the same module. It operationalizes the hypothetical separation story in which the Turing model sees only Tc while the ledger model retains Tr. The declaration sits inside an explicitly non-certificate exploration of P versus NP implications and does not close any verified chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.