RecognitionComplete
plain-language theorem explainer
RecognitionComplete defines a structure for dual complexity in the ledger model, pairing a sub-polynomial computation function Tc with a linear recognition function Tr. Complexity theorists examining information barriers from balanced parity would cite this to illustrate separation between internal steps and observation costs. The declaration encodes the bounds directly as structure fields without invoking additional lemmas.
Claim. Let $Tc, Tr : ℕ → ℕ$. The structure requires existence of $c, k ∈ ℝ$ with $0 < k < 1$ such that $∀ n > 0$, $Tc(n) ≤ c ⋅ n^k ⋅ log n$, and existence of $c > 0$ such that $∀ n > 0$, $Tr(n) ≥ c ⋅ n$.
background
The module provides a scaffold for exploring P versus NP implications of the ledger framework, where double-entry structures enforce information hiding through balanced-parity encoding. RecognitionComplete introduces the dual parameters Tc for internal evolution steps and Tr for observation operations, with the sub-polynomial and linear bounds respectively. Upstream constructions like the CPM2D model and simplicial ledger bridges supply the physical and combinatorial foundations for these complexity measures.
proof idea
The declaration is a bare structure definition that directly asserts the two functions and their bounding properties. No tactics or lemmas are required; the fields themselves constitute the claim.
why it matters
It serves as the core data structure for downstream objects including ClayBridge, which projects to the Turing model by ignoring Tr, and the main_resolution theorem that posits unconditional separation. This aligns with the module's hypothetical framework for resolving P versus NP at different scales, though the module itself flags the exploration as unproven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.