SATLedger
plain-language theorem explainer
SATLedger packages a SAT instance as a ledger-encoded structure with fields for variable count, clause count, clause lists, and a boolean result map over the variables. Researchers examining hypothetical ledger-based distinctions between computation and recognition scales would reference this encoding when modeling information hiding. The declaration is a direct structure definition introducing four fields with no attached proof obligations.
Claim. A SAT instance in ledger representation consists of natural numbers $n$ (variables) and $m$ (clauses), a list of clauses each given as a list of pairs (sign, index), and a function from the finite set of $n$ indices to booleans that encodes the result via balanced parity.
background
This structure appears inside a scaffold module whose documentation states it is exploratory and not part of any verified certificate chain. The module examines hypothetical ledger implications for complexity, including possible divergence between computation and recognition costs under balanced-parity encoding. It imports ledger concepts such as the balanced predicate on event lists and clause encodings from RSatEncoding and SAT.CNF that represent 3-SAT literals as signed indices.
proof idea
The declaration is a structure definition that directly introduces the four fields n, m, clauses, and result_encoding with no lemmas, tactics, or computational content.
why it matters
SATLedger supplies the instance type used by the hypothetical P_vs_NP_resolved theorem and the RecognitionScenario structure in the same module. It illustrates how the ledger double-entry mechanism can create an information-theoretic barrier between computation and observation scales, though the module documentation explicitly labels all such separation claims as unproven hypotheses. The construction touches the open question of whether recognition costs remain linear while computation costs become sub-polynomial inside the RS ledger model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.