demoRecognitionScenario
plain-language theorem explainer
This definition supplies a concrete recognition scenario in which computation cost is constantly zero while recognition cost equals the input size. Researchers examining ledger-based dual-complexity models would reference it for demonstration purposes within exploratory complexity arguments. The body directly instantiates the dual-cost record with the constant-zero and identity maps, then discharges the required sub-polynomial and linear growth conditions by norm_num together with case analysis on natural numbers and non-negativity lemmas for r
Claim. Let $T_c(n)=0$ and $T_r(n)=n$. The resulting structure satisfies $T_c(n)leq n^{1/3}log n$ and $T_r(n)geq n/2$ for every SAT instance, together with the eventual-gap condition that $T_c(n)<n$ and $T_r(n)geq n$ for all sufficiently large $n$.
background
A recognition scenario packages a dual-cost record together with explicit bounds that witness a computation-versus-recognition split on SAT instances and an eventual growth gap. The dual-cost record itself consists of two functions (internal evolution steps and observation operations) plus proofs that the first is sub-polynomial and the second is linear. This definition appears inside a scaffold module whose documentation states that the file explores hypothetical ledger implications for complexity theory and is not part of any verified certificate chain. Upstream dependencies include the CPM2D model construction and the successor and zero lemmas from ArithmeticFromLogic that support the case analysis on natural numbers.
proof idea
The definition first builds a dual-cost record by setting the computation function to the constant zero and the recognition function to the identity. It then proves the sub-polynomial property via norm_num, Real.log_nonneg_iff, rpow_nonneg_of_nonneg, and case analysis on zero versus successor. The linear property is discharged by a trivial norm_num witness. The outer structure is assembled by proving the SAT bound from non-negativity of the cubic-log term and the trivial inequality n/2 leq n, and the eventual gap by direct comparison for n between 100 and 200.
why it matters
The definition supplies a ready-made example for the separation story inside the ComputationBridge module. It illustrates the hypothetical Turing-incompleteness and SAT-separation claims listed in the module documentation, showing how dual complexity parameters can diverge under ledger assumptions. The construction is consistent with the information-hiding barrier created by balanced-parity encoding. It touches the open question whether the ledger model produces a genuine distinction between P and NP at the recognition scale, while remaining outside the verified certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.