RecognitionScenario
plain-language theorem explainer
RecognitionScenario packages a RecognitionComplete pair of complexity functions with explicit bounds showing sub-polynomial computation cost and at least linear recognition cost for SAT instances. Researchers examining ledger dualities in complexity would cite it when illustrating potential scale-dependent separations. The declaration is a direct structure definition that assembles the rc component and the two forall properties with no lemmas or tactics.
Claim. Let $(T_c, T_r)$ be a recognition-complete complexity pair satisfying $T_c$ sub-polynomial and $T_r$ at least linear. A RecognitionScenario consists of such a pair together with the properties that for every SAT ledger instance with $n$ variables, $T_c(n) ≤ n^{1/3} log n$ and $T_r(n) ≥ n/2$, and that for all $n ≥ 100$, $T_c(n) < n$ while $T_r(n) ≥ n$.
background
The ComputationBridge module is marked as a scaffold exploring hypothetical ledger-based complexity separations and lies outside the verified RS certificate chain. RecognitionComplete is the structure supplying dual functions $T_c : ℕ → ℕ$ for internal evolution steps and $T_r$ for observation operations, constrained by sub-polynomial growth on $T_c$ and linear lower bound on $T_r$. SATLedger encodes an SAT instance through its variable count $n$, clause list, and balanced-parity result encoding across $n$ cells.
proof idea
The declaration is a structure definition. It directly includes the rc field of type RecognitionComplete and states the sat_bound and eventual_gap properties as fields. No lemmas are applied and no tactics are used; the form serves as a packaging construct for downstream instantiation.
why it matters
This definition supplies the data type instantiated by demoRecognitionScenario with the concrete choice $T_c = 0$ and $T_r = id$. It supports the hypothetical SAT separation hypothesis inside the Computation Bridge exploration. The module records that such constructions rely on model assumptions rather than unconditional results and remain outside the core RS forcing chain (T0-T8) and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.