Turing_incomplete
plain-language theorem explainer
The theorem exhibits a ledger computation model whose measurement fails to recover a balanced-parity bit under a strict size bound, while any TuringModel is forced to assign zero recognition cost. Researchers studying ledger dual-complexity separations would cite the explicit witness construction. The proof supplies a concrete LedgerComputation instance whose measurement_bound axiom directly negates the universal recovery claim, then applies recognition_free to set the Turing function to zero.
Claim. For any Turing model $TM$, there exist a problem type and a ledger computation $LC$ such that there is $n$, a finset $M$ of cardinality less than $n$, and it is not true that $LC$ measures the encoded balanced-parity instance to recover bit $b$ for every mask, while the recognition complexity of $TM$ is the constant-zero function.
background
The ComputationBridge module is explicitly marked scaffold and outside the verified certificate chain; it explores hypothetical ledger-based complexity implications. TuringModel is the structure whose recognition_complexity field is identically zero by the recognition_free axiom. LedgerComputation augments this with an explicit measure operation on states together with the measurement_bound axiom that encodes flux conservation and observation cost. The upstream BalancedParityHidden.enc supplies the hidden-mask encoder that forces the information barrier between evolution and measurement.
proof idea
The tactic proof lets LC be the LedgerComputation with Unit states, identity evolve, trivial encode, and constant-false measure. It discharges measurement_bound by classical instantiation of the universal claim at b=true, yielding an immediate contradiction. The existential is witnessed by refining to the size-1 empty-mask case and applying the bound; recognition_complexity is then set to zero by funext on TM.recognition_free.
why it matters
The declaration populates the hypothetical P-vs-NP framework inside the scaffold module by separating computation from recognition cost via the ledger structure. It directly uses the TuringModel and LedgerComputation definitions together with the balanced-parity encoder. The module documentation states that such results remain exploratory and are not part of the verified RS chain (UltimateClosure, CPMClosureCert). No downstream citations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.