gbrain: sync converted org-mode brain files

projects/passepartout/architecture/_index.org

@@ -13,14 +13,14 @@ Architecture overview — narrative introduction, staged build-out, systemic eff
 
 | Stage | Delivers | Key cost | Timeline |
 |-------+----------+----------+----------|
-| [[id:4a1f23b0-abc1-4def-9876-543210abcdef][0 — Now]] | Baseline: conventional computing | Patching treadmill, no deductive guarantees | Today |
-| [[id:4a1f23b0-abc2-4def-9876-543210abcdef][1 — Social Protocol]] | Communication integrity, provable DAG | Crypto overhead, key management | Today |
-| [[id:4a1f23b0-abc3-4def-9876-543210abcdef][2 — Verification]] | Verified gate, capability auth | Policy formalization burden | Today (limited) |
-| [[id:4a1f23b0-abc4-4def-9876-543210abcdef][3 — Lisp Machine]] | Lisp image, Merkle memory, no kernel | Lisp tax, no backward compat, single address space | 2-5yr (soft) / 5-10yr (ASIC) |
-| [[id:4a1f23b0-abc5-4def-9876-543210abcdef][4 — Inference]] | In-process LLM, token interception | ~10x compute/RAM/storage | Server now; consumer 3-5yr |
-| [[id:4a1f23b0-abc6-4def-9876-543210abcdef][5 — Weights]] | Plist-native weights, weight-level provenance | ~100x GPU / ~2-5x ASIC | GPU hybrid now; ASIC 5-10yr |
-| [[id:4a1f23b0-abc7-4def-9876-543210abcdef][6 — Training]] | Verified fine-tuning, neural world model | ~100x fine-tuning only | 3-5yr fine-tuning |
-| [[id:4a1f23b0-abc8-4def-9876-543210abcdef][7 — Remaining]] | Physical threats, oracles, speculation, bootstrap axiom | Mitigations are non-computational | Forever |
+|| [[id:4a1f23b0-abc1-4def-9876-543210abcdef][0 — Now]] | Baseline: conventional computing | Patching treadmill, no deductive guarantees | Today |
+|| [[id:4a1f23b0-abc2-4def-9876-543210abcdef][1 — Social Protocol]] | Communication integrity, provable DAG + **Truth Layer (contradiction detection, verification economy)** | Crypto overhead, DAG storage growth, stake model attack surface | Today |
+|| [[id:4a1f23b0-abc3-4def-9876-543210abcdef][2 — Verification]] | Verified gate, capability auth + **Symbolic Reasoner (CL HOL engine, knowledge-dependent auth)** | Reasoner dev cost, policy formalization burden | Today (limited) |
+|| [[id:4a1f23b0-abc4-4def-9876-543210abcdef][3 — Lisp Machine]] | Lisp image, Merkle memory, no kernel | Lisp tax, no backward compat, single address space | 2-5yr (soft) / 5-10yr (ASIC) |
+|| [[id:4a1f23b0-abc5-4def-9876-543210abcdef][4 — Inference]] | In-process LLM, token interception | ~10x compute/RAM/storage | Server now; consumer 3-5yr |
+|| [[id:4a1f23b0-abc6-4def-9876-543210abcdef][5 — Weights]] | Plist-native weights, weight-level provenance | ~100x GPU / ~2-5x ASIC | GPU hybrid now; ASIC 5-10yr |
+|| [[id:4a1f23b0-abc7-4def-9876-543210abcdef][6 — Training]] | Verified fine-tuning, neural world model | ~100x fine-tuning only | 3-5yr fine-tuning |
+|| [[id:4a1f23b0-abc8-4def-9876-543210abcdef][7 — Remaining]] | Physical threats, oracles, speculation, bootstrap axiom | Mitigations are non-computational | Forever |
 
 **Systemic analysis:**
 - [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic effects over time]] — how verification cascades across society, economics, and geopolitics

projects/passepartout/architecture/stage-1-social-protocol.org

@@ -78,6 +78,39 @@ those machines - malware that compromises an endpoint can sign messages using
 the endpoint's keys. The messages are authentic; the sender wasn't. The social protocol
 carries the authorization; it doesn't evaluate it.
 
+### Truth Layer — Contradiction Detection and Verification Economy
+
+The provenance store seeds (signed empirical parameters) generalize to a
+full **truth-accumulation layer** over the social protocol DAG. Every
+knowledge assertion — not just parameters but any formal claim extracted
+from Org prose by the LLM — is a signed, DAG-tracked message.
+
+| Component | What it does | Depends on |
+|-----------|-------------|------------|
+| Signed knowledge assertions | Any instance asserts P (a formal claim) signed with its DID, Merkle-linked to source evidence | DID identities, DAG |
+| Contradiction detection | The DAG flags when instance A asserts P and instance B asserts ¬P. Conflicts are protocol events, not bugs | Signed assertions, DAG query |
+| Verification staking | Instances vouch for assertions with reputation or compute stake. Surviving challenges accumulate confidence; false assertions degrade the issuer's weight | Contradiction detection |
+| Truth scoring | Every assertion carries a confidence tier: (1) extracted/LLM-guess → (2) locally consistent → (3) corroborated by N independent instances → (4) gate-enforced | Staking, corroboration count |
+| Reasoner code exchange | The same protocol distributes CL reasoner prototypes. Users collaborate on the symbolic reasoner (Stage 2) before it enters the gate | Signed code, DAG versioning |
+
+**The verification economy emerges naturally.** Instances that contribute
+verified assertions gain reputation. Instances that propagate falsehoods
+lose it. Over time, the protocol converges toward truths the same way
+markets converge toward prices — without a central authority, through
+incentive alignment.
+
+**Cost:** Assertion storage grows with the DAG. Contradiction detection
+requires O(log n) DAG traversal per new assertion — feasible at social-
+protocol scale (thousands of instances, not millions). Verification
+staking introduces economic attack surface (Sybil, collusion) that must be
+modeled in the stake function.
+
+**Bootstrap path:** The first assertions are LLM-extracted from Org prose
+(confidence tier 1). Contradictions are initially rare (few instances,
+sparse knowledge). As the instance count grows, contradiction frequency
+increases and quality converges. This is Cyc's pump-priming problem solved
+through network effects instead of hand-curation.
+
 ← [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Stage 0 — Now]]  → [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]]
 
 :PROPERTIES:

projects/passepartout/architecture/stage-2-verification.org

@@ -78,6 +78,70 @@ use, the friction may lead users to bypass the gate.
 *Full gate guarantees arrive when Passepartout runs on its own Lisp machine
 (Stage 3). Before that, it's a correctness proof running on an untrusted substrate.*
 
+### Symbolic Reasoner — CL-Native Higher-Order Logic Engine
+
+The gate needs to evaluate not just *security policy* but *epistemic
+validity*: is this action consistent with what the system knows about the
+world? The provenance store (Stage 1) provides quality-scored assertions,
+but there is no engine to **reason over them** — to combine assertions,
+prove entailments, detect contradictions, or generate causal explanations.
+
+**A CL-native symbolic reasoner** fills this gap. It operates over the
+symbolic index of the Knowledge subsystem (predicates, relations,
+constraints extracted from Org prose) and returns (entailed | contradicted
+| undetermined) for any query.
+
+### Architecture
+
+| Layer | What it does | Implementation |
+|-------|-------------|----------------|
+| Assertion store | Quality-scored formal claims from Stage 1's truth layer | Provenance store hash table (Stage 2) |
+| Constraint solver | SAT/SMT-style search over bounded problem spaces | Screamer (CL, existing) |
+| Deduction engine | Forward/backward chaining over first-order subset of assertions | CL-native, starts as Screamer extension |
+| Higher-order layer | Nested modalities — belief, intention, causation, temporal |
+> Screamer cannot express these natively | CL macros + custom proof search |
+| Gate interface | (action, context) → (permit \| deny \| needs-evidence) | ACL2 FFI across the Lisp boundary |
+
+### Why not Lean directly
+
+Lean 4 is C++ at its core — a separate trust domain that breaks the single
+address space. The reasoner must be CL-native for the Stage 3 Lisp machine
+model. Lean is the *reference* design: its tactics, elaboration, and type
+theory inspire the CL implementation, but the engine itself is written in
+Common Lisp and lives in the same memory graph as the evaluator and gate.
+
+### Development path across stages
+
+The reasoner is *born at Stage 1* and *hardens through Stage 2*:
+
+| Stage | Reasoner state | How it gets there |
+|-------|---------------|-------------------|
+| 1 | CL prototype (Screamer-based, first-order) | Shared via social protocol's Reasoner Code Exchange. Users test against local symbolic indices, share patches |
+| 1 | Higher-order extensions sketched | CL macros for modal logic, causal chains — tested on small assertion sets |
+| 2 | Reasoner feeds gate decisions | Gate delegates knowledge-dependent checks: "is this action valid given what we know?" Works on quality-scored assertions from Stage 1's truth layer |
+| 3 | Reasoner absorbed into address space | Same memory graph as evaluator, gate, LLM. No FFI, no IPC |
+| 4 | Reasoner enters self-improvement loop | In-process LLM reads reasoner code, proposes improvements, gate checks policy |
+
+### Cost
+
+- **Screamer-level reasoning:** O(n) over the relevant subtree — the same
+  sparse tree retrieval the Knowledge subsystem already uses. A 4K-assertion
+  context resolves in milliseconds
+- **Higher-order deduction:** O(exp) in the general case. Scoped by the
+  LLM narrowing the reasoning window first — the user never waits for a
+  global proof
+- **Proof quality vs speed:** The reasoner can return (entailed with
+  confidence 0.83) rather than a binary yes/no. The gate chooses the
+  threshold per domain
+
+### What this enables
+
+The gate graduates from checking *who* is authorized to checking *what is
+true*. A policy can say "deny actions based on false premises" — and the
+reasoner determines which premises are false. This is the connection
+between security verification and knowledge verification that the original
+Cyc architecture required but could not enforce.
+
 ← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]]  → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]
 
 :PROPERTIES: