P_vs_NP_resolved
plain-language theorem explainer
The declaration asserts that in the ledger model a constant-true function satisfies the computational condition of returning true in sublinear time on every positive-size SAT instance while any observer function from instances and query sets to booleans can be forced to disagree on a two-variable empty instance with the empty query set. Researchers examining dual-scale complexity separations induced by balanced parity would cite the result when testing ledger-based hypotheses. The term proof splits the conjunction, supplies the constant solver,
Claim. There exists a function from ledger-encoded SAT instances to booleans such that for every instance with $n>0$ there is $t<n$ where the function returns true. For every observer mapping ledger instances and subsets of variables to booleans there exist an instance and a subset $M$ with $|M|<n/2$ such that the observer output differs from some boolean value.
background
SATLedger is the structure with fields n (number of variables), m (number of clauses), clauses (list of lists of Bool-Nat pairs), and result_encoding (Fin n to Bool). The module is explicitly labeled a scaffold exploring hypothetical ledger implications for complexity and states that its separation results rely on model assumptions rather than unconditional theorems. Upstream material includes the definition of nontrivial kinship systems and the scale function phi^k from cosmology, though neither is invoked in the argument.
proof idea
The term proof applies constructor to the conjunction. The first conjunct is discharged by refining to the constant-true function and using simpa plus decide to witness t=0. The second conjunct proceeds classically, introduces the concrete instance with n=2, m=0 and empty clauses, refines to the empty Finset, then performs by_cases on the observer output to exhibit the differing boolean.
why it matters
The declaration supplies the P versus NP hypothesis inside the ComputationBridge scaffold, illustrating how the ledger's double-entry structure can separate computation from recognition scales. It touches the open question of whether balanced-parity encoding creates an information-theoretic barrier, but the module doc states the file is not part of the verified certificate chain and should not be cited as a resolution of P versus NP.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.