demoRecognitionScenario
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish any unconditional separation between P and NP.
- Does not belong to the verified certificate chain.
- Does not apply outside the hypothetical ledger-model assumptions.
- Does not supply a general construction for arbitrary cost functions.
formal statement (Lean)
113noncomputable def demoRecognitionScenario : RecognitionScenario :=
proof body
Definition body.
114 let rc : RecognitionComplete := {
115 Tc := fun _ => 0
116 Tr := fun n => n
117 Tc_subpoly := by
118 use 1, (1 / 3 : ℝ)
119 constructor <;> norm_num
120 intro n hn
121 have hlog : 0 ≤ Real.log (n : ℝ) := by
122 cases n with
123 | zero => simp
124 | succ n' =>
125 have : (1 : ℝ) ≤ (Nat.succ n' : ℝ) := by exact_mod_cast Nat.succ_le_succ (Nat.zero_le _)
126 simpa using Real.log_nonneg_iff.mpr this
127 have hrpow : 0 ≤ (n : ℝ)^(1/3 : ℝ) :=
128 Real.rpow_nonneg_of_nonneg (show 0 ≤ (n : ℝ) by exact_mod_cast Nat.zero_le _) _
129 simpa [mul_comm, mul_left_comm, mul_assoc] using mul_nonneg (by norm_num) (mul_nonneg hrpow hlog)
130 Tr_linear := by
131 use (1 : ℝ)
132 constructor <;> norm_num
133 intro n _; simp }
134 {
135 rc
136 sat_bound := by
137 intro inst
138 constructor
139 · have : 0 ≤ (inst.n : ℝ)^(1/3 : ℝ) * Real.log (inst.n : ℝ) := by
140 have hlog : 0 ≤ Real.log (inst.n : ℝ) := by
141 cases inst.n with
142 | zero => simp
143 | succ n' =>
144 have : (1 : ℝ) ≤ (inst.n : ℝ) := by exact_mod_cast Nat.succ_le_succ (Nat.zero_le _)
145 simpa using Real.log_nonneg_iff.mpr this
146 have hrpow : 0 ≤ (inst.n : ℝ)^(1/3 : ℝ) :=
147 Real.rpow_nonneg_of_nonneg (show 0 ≤ (inst.n : ℝ) by exact_mod_cast Nat.zero_le _) _
148 simpa [mul_comm, mul_left_comm, mul_assoc] using mul_nonneg hrpow hlog
149 simpa using this
150 · have : inst.n / 2 ≤ inst.n := Nat.div_le_self _ _
151 simpa using this
152 eventual_gap := by
153 intro n hn
154 constructor
155 · have hn0 : 0 < n := lt_of_le_of_lt (by decide : (0 : ℕ) < 100) hn
156 simpa using hn0
157 · exact le_of_lt (lt_of_le_of_lt hn (by decide : (100 : ℕ) < 200))
158 }
159
160/-- Turing incompleteness: the model ignores recognition cost -/