SATLedger
SATLedger encodes a SAT instance inside the ledger model by bundling variable count n, clause count m, a list-of-lists clause representation, and a balanced-parity result map over the n indices. Researchers modeling hypothetical computation-recognition separations in Recognition Science would reference this structure when stating bounds on SAT instances. The declaration is a plain structure definition with no proof obligations or lemmas.
claimA SAT instance in ledger representation is a tuple $(n, m, C, r)$ where $n, m$ are natural numbers, $C$ is a list of lists of signed variable indices, and $r$ is a map from the finite set of $n$ indices to booleans that records the result via balanced-parity encoding.
background
In the ledger framework, events are recorded as balanced double-entry lists whose parity outcomes become observable only after recognition. The structure imports the Clause type from RSatEncoding (at most three literals per clause) and the balanced predicate from LedgerForcing, which asserts that every ledger event list satisfies the double-entry condition. The module is explicitly labeled exploratory scaffolding outside the verified certificate chain and uses these fields to package demonstration data for complexity separation arguments.
proof idea
This is a structure definition that directly assembles the four fields n, m, clauses, and result_encoding. No lemmas or tactics are invoked; the declaration serves only as a data carrier for downstream use in RecognitionScenario and P_vs_NP_resolved.
why it matters in Recognition Science
SATLedger supplies the instance type required by the downstream RecognitionScenario structure, which states the hypothetical bounds Tc = O(n^{1/3} log n) and Tr = Omega(n), and by the P_vs_NP_resolved theorem that contrasts polynomial computation with linear recognition under ledger assumptions. It therefore occupies the role of concrete data carrier inside the scaffold exploration of how balanced-parity encoding creates an information barrier between computation and observation scales. The module doc-comment explicitly disclaims any claim to unconditional resolution.
scope and limits
- Does not claim an unconditional proof of P versus NP separation.
- Does not verify any concrete time bounds for SAT solvers.
- Does not connect to the verified certificate chain such as UltimateClosure.
- Does not define the actual computation or recognition functions.
formal statement (Lean)
92structure SATLedger where
93 /-- Number of variables -/
94 n : ℕ
95 /-- Number of clauses -/
96 m : ℕ
97 /-- Clause structure encoded in ledger -/
98 clauses : List (List (Bool × ℕ))
99 /-- Result encoded using balanced-parity across n cells -/
100 result_encoding : Fin n → Bool
101
102/-- A recognition scenario packages the demonstration data for the separation story. -/