rewrite ideas/_index.org with full page listing

- architecture.org becomes a narrative: problem → three-subsystem solution
  → staged approach → what it means
- Moved TAM, revenue paths, analytical frames, strategy/IP links to _index.org
- _index.org is now the navigation hub with roadmap table and all catalog links

.org-ids.json

@@ -5,7 +5,6 @@
   "0a4e0b8f-25e0-4b78-9633-fc37d03cefe9": "projects/flags/asset-protection-structures.org",
   "5ac2f037-fc3c-45ac-a6e8-acc20e005cb0": "projects/flags/legal-structure-alternatives.org",
   "1e5f6a7b-8c9d-0e1f-2a3b-4c5d6e7f8a9b": "projects/flags/_index.org",
-  "2afd9a3c-e96a-54c7-ac77-a05a28065b4b": "projects/passepartout/biology-parallels.org",
   "7a1b2c3d-4e5f-6a7b-8c9d-0e1f2a3b4c5d": "projects/passepartout/_index.org",
   "04c2f221-c54f-51e5-b40a-48822cd16d45": "projects/passepartout/common-logic-iso-24707.org",
   "4a1f23b0-abc1-4def-9876-543210abcdef": "projects/passepartout/architecture/stage-0-now.org",
@@ -109,6 +108,17 @@
   "c34940cc-090e-57c4-8020-e78b1d32b96c": "projects/passepartout/strategy/compliance/domain-gate-packages.org",
   "bafdaa23-de0b-444c-9151-c87ac65add32": "projects/passepartout/strategy/compliance/lfp-dppp.org",
   "717ef2df-2a80-4362-b23a-5e7e12554251": "projects/passepartout/strategy/compliance/dora.org",
+  "1e2f3a4b-5c6d-7e8f-9a0b-1c2d3e4f5a6b": "ideas/world-models-plain-language.org",
+  "3a4b5c6d-7e8f-9a0b-1c2d-3e4f5a6b7c8d": "ideas/architectural-integration-three-pronged.org",
   "2cdca4b0-6b41-44b4-acb0-af21d0e27b00": "ideas/orders-of-magnitude-time.org",
-  "329a30cd-55fb-496d-a60b-91388c211bba": "ideas/_index.org"
+  "9c0d1e2f-3a4b-5c6d-7e8f-9a0b1c2d3e4f": "ideas/knowledge-tree-middle.org",
+  "f4e5d6c7-b8a9-0c1d-2e3f-4a5b6c7d8e9f": "ideas/schafmeister-clasp-nanotechnology.org",
+  "2afd9a3c-e96a-54c7-ac77-a05a28065b4b": "ideas/biology-parallels.org",
+  "4b5c6d7e-8f9a-0b1c-2d3e-4f5a6b7c8d9e": "ideas/neurological-software-empirical-middle.org",
+  "0d1e2f3a-4b5c-6d7e-8f9a-0b1c2d3e4f5a": "ideas/world-models-middle-domain.org",
+  "7a8b9c0d-1e2f-3a4b-5c6d-7e8f9a0b1c2d": "ideas/open-source-wolfram-lisp.org",
+  "329a30cd-55fb-496d-a60b-91388c211bba": "ideas/_index.org",
+  "5c6d7e8f-9a0b-1c2d-3e4f-5a6b7c8d9e0f": "ideas/wider-implications-three-pronged.org",
+  "8b9c0d1e-2f3a-4b5c-6d7e-8f9a0b1c2d3e": "ideas/passepartout-bootstrap-mathematica.org",
+  "2f3a4b5c-6d7e-8f9a-0b1c-2d3e4f5a6b7c": "ideas/practical-powers-three-pronged.org"
 }

ideas/_index.org

@@ -6,4 +6,22 @@
 #+title: Ideas
 #+filetags: :index:
 
-Section index for ideas. Browse by file.
+Cross-domain concepts, speculative analysis, and architectural thinking for the Passepartout project.
+
+**The three-pronged system series** — new tonight:
+
+- [[id:f4e5d6c7-b8a9-0c1d-2e3f-4a5b6c7d8e9f][Schafmeister and Clasp]] — Lisp in computational nanotechnology, existence proof for the architecture
+- [[id:7a8b9c0d-1e2f-3a4b-5c6d-7e8f9a0b1c2d][Open-source Wolfram Language in Lisp]] — viability of bootstrapping a Mathematica equivalent
+- [[id:8b9c0d1e-2f3a-4b5c-6d7e-8f9a0b1c2d3e][Passepartout bootstrapping Mathematica]] — what the neurosymbolic engine could generate autonomously
+- [[id:9c0d1e2f-3a4b-5c6d-7e8f-9a0b1c2d3e4f][Middle of the Knowledge Tree]] — the gap between logic and nanotechnology
+- [[id:0d1e2f3a-4b5c-6d7e-8f9a-0b1c2d3e4f5a][The Middle Domain as World Models]] — mapping empirical science onto world model architecture
+- [[id:1e2f3a4b-5c6d-7e8f-9a0b-1c2d3e4f5a6b][World Models — Plain Language]] — explanation without jargon
+- [[id:2f3a4b5c-6d7e-8f9a-0b1c-2d3e4f5a6b7c][Practical Powers of the Three-Pronged System]] — 10 concrete capabilities
+- [[id:3a4b5c6d-7e8f-9a0b-1c2d-3e4f5a6b7c8d][Architectural Integration]] — how the three prongs fit into Passepartout's subsystems and stages
+- [[id:4b5c6d7e-8f9a-0b1c-2d3e-4f5a6b7c8d9e][Neurological Software in the Empirical Middle]] — neural networks in the provenance framework
+- [[id:5c6d7e8f-9a0b-1c2d-3e4f-5a6b7c8d9e0f][Wider Implications]] — what the three-pronged system means for science, safety, regulation, and trust
+
+**Earlier ideas:**
+
+- [[id:2afd9a3c-e96a-54c7-ac77-a05a28065b4b][Biology as Proof of the Lisp Model]] — biological systems as evidence for Lisp architecture
+- [[id:2cdca4b0-6b41-44b4-acb0-af21d0e27b00][Orders of Magnitude — Time]] — a time-scale framework for the Passepartout roadmap

ideas/architectural-integration-three-pronged.org

@@ -0,0 +1,106 @@
+:PROPERTIES:
+:CREATED:  [2026-05-25 Mon]
+:ID:       3a4b5c6d-7e8f-9a0b-1c2d-3e4f5a6b7c8d
+:END:
+#+title: Architectural Integration of the Three-Pronged System
+#+filetags: :ideas:passepartout:architecture:
+
+An analysis of how the deductive / provenance-tracked empirical / probabilistic oracle model fits into Passepartout's architecture, at what stage it becomes operational, and what it means for the existing subsystems.
+
+**The three prongs are not three engines.**
+
+The initial framing (deductive + provenance + probabilistic) implies three parallel reasoning systems. It is more accurate to say: two reasoning engines and one data layer.
+
+- **The symbolic engine** handles everything that can be formalized: deductive proofs, empirical equations, validity predicates, pipeline composition, uncertainty propagation. This is one engine — it reasons about symbols using rules that are either proven (ACL2) or well-defined (force field equations).
+
+- **The probabilistic oracle** (LLM) handles everything that cannot be formalized: parameter selection, model choice, interpretation of results in natural language, failure diagnosis, creative hypothesis generation. It proposes; the symbolic engine checks.
+
+- **The provenance store** is not an engine. It is a structured database that stores empirical parameter sets, validity envelopes, experimental benchmarks, and comparison histories. Neither engine reasons about it as a whole. The symbolic engine queries it for parameters and validity predicates. The LLM queries it for context and updates it with new data.
+
+Two reasoning engines. One curated data layer. This is a cleaner architecture than three parallel systems.
+
+**Where it lives in the existing subsystems.**
+
+The current architecture has four subsystems: Environment, Knowledge, Verification, Social Protocol. The three-pronged model cross-cuts them:
+
+| Subsystem | Deductive role | Empirical role | Oracle role |
+|---|---|---|---|
+| Environment | Hosts the symbolic engine, runs ACL2 | Hosts the provenance store | Runs the LLM |
+| Knowledge | Stores formal theorems and proofs (symbolic index) | Stores empirical parameters and benchmarks (provenance store) | Neural index for semantic search |
+| Verification | ACL2 proof checking, formal gate rules | Validity envelope checks, parameter provenance checks | Gate policy interpretation (LLM evaluates natural-language rules) |
+| Social Protocol | Sharing verified proofs between instances | Sharing validation histories and benchmark results between instances | Sharing model selection strategies |
+
+The verification subsystem (the gate) is the integration point. Every action that reaches the gate is checked against:
+1. Security policy (is this action safe?)
+2. Scientific validity (is this model valid in this context?)
+3. Consistency (do the symbolic check and the oracle's assessment agree?)
+
+These three checks run as separate gate vectors with the same architecture as every other gate check. No new mechanism needed — just new predicates with access to the provenance store.
+
+**At what stage it becomes operational.**
+
+The infrastructure is staged, not all-at-once:
+
+- **Stage 0 (now)** — The probabilistic oracle exists (the LLM). The provenance store does not. The deductive engine partially exists through Hermes skills (symbolic gate rules as Python, not ACL2). The empirical layer is invisible — the LLM reasons about chemistry, biology, and engineering using training data alone, without systematic provenance.
+
+- **Stage 1 (social protocol)** — The provenance store prototype can be introduced here as a side effect of signed messages and data exchange. When instances share a validated force field parameter, the message carries a signature and a source. The receiving instance stores it with provenance. This is a natural crawl before the full infrastructure.
+
+- **Stage 2 (gate as software)** — The provenance store becomes operational infrastructure. The gate needs to check validity envelopes to do its job properly. This is the correct stage to introduce it because: (a) the gate is being built anyway, (b) validity checking is a gate predicate like any other, and (c) the provenance store is just a structured knowledge base — the Knowledge subsystem already has the machinery for storing and querying structured data. The symbolic index (formal facts) and the provenance store (empirical parameters) differ in what they store, not in how they store it.
+
+- **Stage 3 (Lisp machine)** — The symbolic engine is native in one address space. ACL2 runs at hardware level. The provenance store becomes a native Lisp hash table with persistence. The empirical layer is fully integrated: the symbolic engine queries the provenance store directly, the gate checks validity predicates in the evaluation loop itself, and the LLM still proposes model selections but every proposal is verified against the provenance store before execution.
+
+- **Stage 4+ (in-process inference)** — The LLM moves in-process. The three components (symbolic engine, provenance store, LLM oracle) share one address space. No IPC between them. The query cycle is: LLM proposes a model → symbolic engine checks it against the provenance store → if valid, execute → if invalid, return to LLM with diagnostic. This loop runs at native speed.
+
+**The empirical middle is not a separate kind of reasoning.**
+
+The deepest question in the set: does the middle empirical part have both neuro and symbolic aspects?
+
+Yes, and the split is clean.
+
+The equations that describe an empirical model — Hooke's law for bond stretching, the Lennard-Jones potential for van der Waals interactions, the Born equation for solvation — are formal symbolic expressions. They can be parsed, manipulated, differentiated, verified by ACL2, and composed into pipelines. This is symbolic engine territory.
+
+The parameters in those equations — the spring constants, the well depths, the atomic radii — are derived from experimental data through optimization and fitting. They cannot be derived from the equations themselves. This is not reasoning; it is curation. The provenance store holds them with sources and confidence intervals.
+
+The selection of which model to apply to a given problem requires judgment about the domain, the available data, and the intended use of the result. The LLM handles this: it knows that a protein-protein docking problem needs a different force field than a small-molecule conformational search.
+
+The composition of models into a pipeline (compute this, pipe into that, plot the other) is a program. The symbolic engine runs the pipeline. The LLM may propose the pipeline structure, but the execution is deterministic.
+
+The diagnosis of failure — "this prediction was wrong and here is why" — is the hardest part and requires the most integration. The symbolic engine detects the validity envelope violation and reports the specific parameter that caused it. The LLM interprets the failure in context: "the bond angle term for this functional group was parameterized against small molecules; your molecule has bulky substituents that change the preferred angle."
+
+| Aspect of the empirical middle | Handled by | Why |
+|---|---|---|
+| The equations themselves | Symbolic engine | They are symbolic expressions — verifiable, differentiable, composable |
+| The parameter values | Provenance store (data) | Fitted to data, not reasoned about |
+| Model selection | LLM oracle | Requires contextual judgment |
+| Pipeline composition | Symbolic engine (execute) + LLM (propose) | Execution is deterministic; design is creative |
+| Validity envelope checking | Symbolic engine | A logical predicate over known state |
+| Uncertainty propagation | Symbolic engine | A formula that composes component uncertainties |
+| Interpretation of results | LLM oracle | Requires natural language |
+| Failure diagnosis | Both: symbolic engine pinpoints the violation, LLM explains why | The factual cause is formal; the narrative cause is contextual |
+| Creative design (new molecules, new experiments) | LLM oracle | Requires open-ended generation |
+
+The empirical middle does not require a new kind of reasoning engine. It requires the two existing engines (symbolic and probabilistic) to cooperate on data (the provenance store) that is neither formal theorem nor raw text — it is curated empirical knowledge with structure, provenance, and uncertainty.
+
+**Does it require "world models"?**
+
+The word "world model" is not necessary for the architecture. What the architecture requires is:
+
+1. A store of mathematical models (equations + parameters) with provenance
+2. A mechanism for checking validity envelopes (predicates over conditions)
+3. A mechanism for composing models into pipelines (the existing program execution)
+4. A mechanism for propagating uncertainty (formulas + tracked parameters)
+
+The provenance store, the validity predicates, the pipeline executor, and the uncertainty tracker do not need to be called "world model infrastructure." They are features of the existing subsystems:
+
+- The provenance store extends the Knowledge subsystem (it is a structured database, not a new category).
+- The validity predicates are gate rules (they check conditions before allowing computation).
+- The pipeline executor is the existing neurosymbolic loop (LLM proposes, symbolic engine executes).
+- The uncertainty tracker is a mathematical library (error propagation formulas, statistical calculations).
+
+Calling them "world models" is conceptually clarifying but architecturally optional. The infrastructure is the same either way.
+
+**The practical implementation takeaway.**
+
+Stage 2 is the correct entry point. The provenance store is built as a structured data extension to the Knowledge subsystem. Validity predicates are added as gate vectors. No new subsystems are needed — just new data types in the knowledge store, new predicates in the gate, and new functions in the symbolic engine for uncertainty propagation.
+
+The three-pronged model describes what the system does, not what it is built from. The system is still one machine, one address space, one gate, one memex. It just has a more sophisticated understanding of what it knows and how it knows it.

ideas/knowledge-tree-middle.org

@@ -0,0 +1,86 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       9c0d1e2f-3a4b-5c6d-7e8f-9a0b1c2d3e4f
+:END:
+#+title: The Middle of the Knowledge Tree — From Logic to Nanotechnology
+#+filetags: :ideas:knowledge:passepartout:
+
+In the tree of knowledge model, mathematical foundations and formal logic sit at the root. Schafmeister's molecular nanotechnology sits at a high branch — programmable molecules that bind proteins and catalyze reactions. The distance between them is bridged by a chain of formal and empirical domains. This note maps that chain.
+
+**The full stack, root to branch.**
+
+| Layer | What it formalizes | Formal status | Verification model |
+|---|---|---|---|
+| 0. Logic / Foundations | Proof theory, set theory, type theory, ACL2 axioms | Deductive | Complete — provable from axioms |
+| 1. Algebra | Groups, rings, fields, vector spaces, modules | Deductive | Complete |
+| 2. Analysis | Real numbers, limits, continuity, calculus, measure theory | Deductive | Complete (in principle; deep results are hard) |
+| 3. Geometry / Topology | Manifolds, differential forms, curvature, homotopy | Deductive | Complete |
+| 4. Classical Mechanics | Lagrangian/Hamiltonian mechanics, Newtonian dynamics | Deductive | Complete — follows from variational principles |
+| 5. Quantum Mechanics | Hilbert spaces, operators, Schrödinger equation, symmetries | Deductive | Complete (the theory is fully formalizable) |
+| 6. Statistical Mechanics | Ensembles, partition functions, Boltzmann distribution, entropy | Deductive | Complete (follows from QM + probability) |
+| 7. Electrodynamics | Maxwell's equations, potentials, radiation | Deductive | Complete |
+| 8. Quantum Chemistry | Born-Oppenheimer, Hartree-Fock, DFT, coupled cluster | Partially deductive | The equations are formal. The necessary approximations (Börn-Oppenheimer, exchange-correlation functional) are not. |
+| 9. Molecular Mechanics | Force fields (AMBER, CHARMM, OPLS), potential functions, non-bonded interactions | Empirical parameterization | The simulation is deterministic. The parameters are fitted to experiment. |
+| 10. Molecular Dynamics | Integration schemes, thermostats, barostats, periodic boundaries | Deductive mechanics + empirical inputs | The integrator is provable. The force field parameters are not. |
+| 11. Chemical Thermodynamics | Binding constants, free energy surfaces, reaction equilibria, solvation | Mixed deductive/empirical | Statistical mechanics is deductive. Solvation models are not. |
+| 12. Structural Biochemistry | Protein folding, protein-ligand binding, docking, enzyme kinetics | Largely empirical | Binding affinity prediction is not deductively solvable from first principles. |
+| 13. Organic Chemistry | Reaction mechanisms, stereochemistry, functional group transformations | Empirical with formal structure | Reaction mechanisms are modeled, not derived. They are falsifiable hypotheses, not theorems. |
+| 14. Molecular Design | Spiroligomer design, shape-programmable molecules, therapeutic targeting | Empirical design space | Design rules are heuristics validated by experiment, not derived from QM. |
+
+**What changes at layer 8.**
+
+The important transition happens between layers 7 and 8. Everything from logic through quantum mechanics and statistical mechanics is fully formalizable — you can write down the equations, derive the consequences, and verify the derivations. This is the domain where ACL2 can prove correctness against first principles.
+
+Layer 8 (quantum chemistry) is where the first irreducible approximation appears. The Born-Oppenheimer approximation is not a theorem — it is an assumption that nuclei and electrons can be treated separately because nuclei are much heavier. This assumption is empirically excellent but not deductively guaranteed. The exchange-correlation functional in DFT is not derivable — it is a functional whose exact form is unknown and must be approximated.
+
+From layer 9 onward, the models are empirical through and through. Force field parameters are fitted to experimental data. Solvation models are calibrated against known solubilities. Binding affinity predictions are validated by binding assays, not derived from Schrödinger's equation. The models are mathematically rigorous (the simulation correctly integrates Newton's equations), but the inputs to those models are not.
+
+**What this means for Passepartout.**
+
+Passepartout can verify the *computation* at every layer. It can prove that:
+
+- The Schrödinger equation is correctly solved for a given Hamiltonian (layer 5/8).
+- The molecular dynamics integrator preserves phase space volume (layer 10).
+- The docking algorithm correctly explores the defined conformational space (layer 12).
+
+But it cannot verify that the *model* matches reality. The Born-Oppenheimer approximation, the DFT functional, the force field parameters, the solvation model, the scoring function — these are commitments to empirical reality that no verification system can discharge. They are validated by experiment, not by proof.
+
+This is the same structure as Stage 7 in Passepartout's own roadmap: after all computational threats are eliminated, oracular limits and physical reality remain. The verification subsystem can certify that a simulation is internally consistent. It cannot certify that the simulation's assumptions hold in the real world.
+
+**What Passepartout would need in the middle.**
+
+For each layer 1-7 (deductive), Passepartout already has or can generate the formal mathematics. These are theorems and algorithms that ACL2 can verify against axioms.
+
+For each layer 8-14 (empirically parameterized), Passepartout needs:
+
+1. **A formal model** of the equations (the DFT equations, the force field functional form, the MD integrator) — verified against the mathematical theory.
+2. **A parameter database** with provenance (force field parameters, basis sets, solvation parameters, scoring function weights) — not proven but curated, versioned, and traceable to experimental sources.
+3. **An empirical validation pipeline** that compares computed predictions against experimental measurements and updates the parameter confidence.
+
+The parameter database with provenance is the crucial addition. For Schafmeister's work, this means:
+
+| Empirical parameter set | Source | Passepartout role |
+|---|---|---|
+| DFT functional parameters | Fitted to known systems | Trace which functional was used for each calculation |
+| Force field parameters (AMBER, CHARMM) | Fitted to QM + experiment | Trace parameter provenance; flag known failure regimes |
+| Solvation free energies | Calibrated to measured solubilities | Track calibration data and confidence intervals |
+| Binding affinity benchmarks | PDBbind, DUD-E, experimental IC50 | Track benchmark provenance; report uncertainty |
+| Spiroligomer design rules | Schafmeister's own experimental data | Formalize as knowledge graph with experimental backing |
+
+**The nature of the bridge.**
+
+The middle of the knowledge tree is not a chain of theorems. It is a lattice of formal models scaffolded by empirical commitments. Each layer relies on the formal correctness of the layer below (the QM solver is correct), but also on approximations and parameters that are not deductively justified.
+
+This is not a weakness of the architecture. It is a correct description of the relationship between mathematics and experiment. The bridge from logic to nanotechnology is built from:
+
+- **Formal mathematics** for what can be proven (the core theories, the algorithms, the simulation correctness)
+- **Models with provenance** for what cannot be proven but works (the approximations, the force fields, the scoring functions)
+- **Empirical validation** for the claim that the models match reality (experimental data, benchmarks, error bars)
+
+Passepartout's contribution is not to eliminate the empirical layers — that is impossible. Its contribution is to make explicit which parts are deductively verified, which are empirically fitted, and what the provenance trail is for every numerical value that enters a computation. The system cannot make chemistry deductive. It can make every computational output traceable to its assumptions.
+
+---
+
+- [[id:f4e5d6c7-b8a9-0c1d-2e3f-4a5b6c7d8e9f][Schafmeister and Clasp]] — the nanotechnology branch
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — where verification lives
+- [[id:9c0d1e2f-3a4b-5c6d-7e8f-9a0b1c2d3e4f][Stage 7 — What Remains]] — oracular, physical, and empirical limits

ideas/neurological-software-empirical-middle.org

@@ -0,0 +1,128 @@
+:PROPERTIES:
+:CREATED:  [2026-05-25 Mon]
+:ID:       4b5c6d7e-8f9a-0b1c-2d3e-4f5a6b7c8d9e
+:END:
+#+title: Neurological Software in the Empirical Middle
+#+filetags: :ideas:passepartout:architecture:world-models:
+
+The empirical middle of the knowledge tree (layers 8-14) is increasingly dominated by neural networks trained on data — not symbolic equations with fitted parameters. ANI, MACE, SchNet for molecular energies and forces. AlphaFold for protein structure prediction. Neural docking scores, learned solvation models, QSAR neural nets, RL-based molecular design agents. These are not traditional empirical models with interpretable parameters. They are learned function approximators with millions of inscrutable weights.
+
+The three-pronged architecture must accommodate them. This note analyzes how.
+
+**What changes when the model is a neural network.**
+
+A traditional empirical model (force field, solvation equation, docking scoring function) has:
+
+- A **symbolic expression** for the relationship between inputs and outputs (E = k_b(r - r_0)² + ...)
+- **Interpretable parameters** that correspond to physical quantities (spring constant = 600 kcal/mol/Ų)
+- **Known failure modes** from the equation's form (harmonic approximation fails at extreme bond lengths)
+
+A neural network model has:
+
+- A **learned function** with no simple symbolic expression
+- **Inscrutable parameters** (weights) that do not correspond to physical quantities
+- **Unknown failure modes** — neural networks interpolate well in-distribution and fail unpredictably out-of-distribution
+
+From the architecture's perspective, the critical difference is not that neural networks are harder to verify (they are, but that is a secondary concern). The critical difference is that the provenance information shifts: instead of tracking where a parameter value came from and what it means, you track what the network was trained on, what it was validated against, and whether the current input resembles its training distribution.
+
+**The provenance store handles the shift by tracking three things instead of one.**
+
+A traditional empirical model's provenance entry:
+
+```
+Model: AMBER ff14SB
+Equation: Harmonic bond + harmonic angle + Fourier torsion + LJ + Coulomb
+Parameters:
+  - k_b(C-C): 600 kcal/mol/Ų, source: Cornell et al. (1995), validated: 50+ small molecules
+  - r_0(C-C): 1.525 Å, source: Cornell et al. (1995), validated: 50+ small molecules
+  - ...
+Validity envelope:
+  - Temperature: 273-373K
+  - Solvents: water, methanol, ethanol
+  - Molecule classes: proteins, nucleic acids
+```
+
+A neural network model's provenance entry:
+
+```
+Model: ANI-2x
+Architecture: Ensemble of 8 evidential ANI networks
+Parameters: ~8 million weights — not interpretable individually
+Training data:
+  - Level of theory: ωB97M-D3(BJ)/def2-TZVPPD (DFT)
+  - Molecules: ~8 million conformations from 63,000 organic molecules
+  - Elements: H, C, N, O, S, F, Cl, Br
+  - Conformational coverage: ANI-2x conformational space (RDKit + stochastic sampling)
+Validation benchmarks:
+  - COMP6 benchmark (drug-like molecules): MAE 1.2 kcal/mol
+  - Dihedral profiles: MAE 0.8 kcal/mol
+  - Isomerization energies: MAE 0.9 kcal/mol
+Validity envelope (domain check):
+  - Elements: H, C, N, O, S, F, Cl, Br only
+  - Atomic charge range: not validated for charged species outside training distribution
+  - Conformational novelty flag: activated if RMSD to nearest training point > threshold
+```
+
+The structure is the same: model → training/validation data → domain of applicability. The content differs: traditional models have interpretable parameters with experimental sources; neural networks have training dataset provenance and aggregated validation benchmarks.
+
+**The gate checks the same things regardless of model type.**
+
+The gate predicates for model validity are:
+
+1. **Does the model support the elements/atoms/molecule types in the current input?** — This is the same check for a force field (does the force field have parameters for this atom type?) and a neural network (was this element in the training data?).
+
+2. **Are the conditions within the model's validated range?** — Temperature, pressure, solvent, etc. Same predicate, same structure. The neural network's validated range may be narrower or less well-defined, but the check is the same.
+
+3. **Is the input within the model's training/validation distribution?** — For traditional models, this is a direct validity envelope check. For neural networks, this is a **distribution match** — a statistical check that the current molecular conformation resembles the training set. If the input is far from the training distribution in latent space, the gate flags it regardless of whether the model predicts confidently.
+
+The distribution match check is the new machinery that neural network models require. It is a standard technique in reliable ML (distance to training data, density estimation in latent space, conformal prediction). It integrates into the gate as a predicate: "input is within training distribution: PASS" or "input is outside training distribution: FLAG with confidence reduction."
+
+**The symbolic engine does not need to understand the network.**
+
+This is the key simplification. The symbolic engine — ACL2, the gate predicates, the formal reasoning — does not need to parse the neural network's weights or architecture. It needs to:
+
+- Query the provenance store for the model's training data description
+- Compute a distribution match score for the current input against the training data
+- Compare the result to a threshold from the validity envelope
+- Output: pass, flag, or block
+
+None of these operations require understanding what the network does. They are metadata operations on the provenance store and geometric operations on the input space. The network itself is a black box — the symbolic engine treats it as a function with a known domain of applicability, the same way it treats a force field as a function with a known validity envelope.
+
+**The oracle handles model selection.**
+
+Which model to use for a given problem — traditional force field or learned neural network? The LLM oracle handles this, informed by the provenance store. The store tells the LLM what models are available, what they are validated for, and how they perform on relevant benchmarks. The LLM recommends. The gate checks the recommendation against the validity envelope before execution.
+
+This is where the architecture connects to the real world of model selection that computational scientists face daily. There is no single best force field or neural network architecture for all problems. The choice depends on the molecule class, the property of interest, the required accuracy, and the computational budget. The LLM, with its broad knowledge of the literature, is well-suited to making this recommendation — not by reasoning about the models from first principles, but by knowing which models are preferred for which use cases from training data.
+
+**The full picture: three kinds of empirical model.**
+
+The provenance store now handles three data types:
+
+| Model type | Example | Parameters | Validation method | Gate check |
+|---|---|---|---|---|
+| Symbolic equation + fitted parameters | AMBER force field | Interpretable (spring constants, partial charges) | Per-parameter: source experiment, confidence interval | Validity envelope: temperature, solvent, molecule class |
+| Trained neural network | ANI-2x | Inscrutable (8M weights) | Per-dataset: benchmark MAE, held-out test set | Distribution match: is input like training data? |
+| Hybrid (learned correction to symbolic model) | Δ-ML corrections to DFT | Partially interpretable corrections + network weights | Per-benchmark + per-component | Both envelope + distribution match |
+
+All three are handled by the same provenance store, the same gate predicates, and the same LLM oracle. The only new infrastructure required is the **distribution match check** for neural network models — a piece of statistical machinery that computes how similar the current input is to the model's training distribution.
+
+**Where this fits in the stage plan.**
+
+- **Stage 0-1**: The provenance store does not exist. Neural network models are loaded as black boxes with no systematic validity checking. This is current practice in computational science — the user is responsible for knowing whether a model applies to their problem.
+
+- **Stage 2**: The provenance store begins operation. Initially it handles traditional symbolic-fitted models because they have clear provenance chains and validity envelopes. Neural network models require the distribution match infrastructure, which is a separate development track.
+
+- **Stage 3**: The distribution match infrastructure is operational. The gate can check whether an input is within a neural network's training distribution. The provenance store holds training dataset descriptions, validation benchmarks, and distribution summary statistics for each supported neural network model.
+
+- **Stage 4+**: Neural network models are loaded into the same address space as the symbolic engine and the provenance store. The distribution match check runs at the level of the evaluation loop itself. The gate's validity check becomes a fast native predicate — no querying a separate data store, just reading a hash table and computing a distance in the same process.
+
+**The summary.**
+
+Neural network models trained on empirical data are not a problem for the three-pronged architecture. They fit into the existing framework:
+
+- **The provenance store** tracks training data sources, validation benchmarks, and distribution statistics — instead of parameter sources and confidence intervals.
+- **The gate** checks domain match and training distribution coverage — instead of validity envelopes and parameter regimes.
+- **The symbolic engine** does not need to understand the network — it treats it as a black box with a known domain, the same way it treats a force field.
+- **The LLM oracle** handles model selection — recommending which neural network or traditional model fits the user's problem, informed by the provenance store's benchmark records.
+
+The new infrastructure required is not large — a distribution match function and a training dataset descriptor in the provenance store. Everything else is existing mechanism applied to a new data type.

ideas/open-source-wolfram-lisp.org

@@ -0,0 +1,74 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       7a8b9c0d-1e2f-3a4b-5c6d-7e8f9a0b1c2d
+:END:
+#+title: Viability of an Open-Source Wolfram Language / Mathematica in Common Lisp
+#+filetags: :ideas:lisp:mathematics:open-source:
+
+An assessment of what it would take to build a viable open-source equivalent of Wolfram Language and Mathematica in Common Lisp, based on the existing ecosystem and the fundamental architectural alignment between Lisp and symbolic computation.
+
+**The alignment is natural, not forced.**
+
+Wolfram Language is, at its core, a term-rewriting system with pattern matching, rule-based transformation, and a uniform symbolic representation for everything (expressions are trees of the form head[arg1, arg2, ...] — the Wolfram equivalent of cons cells). This is very close to what Lisp is natively. A Lisp implementation of the core evaluator — pattern matching, rule application, substitution, term rewriting — is not a foreign port. It is an exercise in expressing Wolfram's semantics in a language whose semantics were designed for the same problem domain.
+
+Maxima proves this historically. It is a direct descendant of Macsyma, the MIT computer algebra system that inspired Mathematica. Macsyma was written in Lisp. Mathematica's core evaluation model inherits heavily from Macsyma. An open-source Common Lisp computer algebra system already exists, has existed for decades, and works. The question is not whether it can be done, but how much of the modern Mathematica ecosystem can be replicated and at what cost.
+
+**What already exists.**
+
+| Layer | Existing CL work | Status |
+|---|---|---|
+| Symbolic engine / term rewriting | Lisp readers, pattern matching libs (trivia, optima, fare-matcher), rule systems | Foundational primitives exist, no unified Wolfram-equivalent evaluator |
+| Computer algebra system | Maxima, FriCAS (Axiom), reduce-algebra | Mature CASes — Maxima alone has differentiation, integration, ODEs, linear algebra, tensors, series, limits, Laplace transforms |
+| Numerical computing | magicl, lla (Lisp Linear Algebra), CL-NUM, GSLL (GNU Scientific Library bindings) | Solid — covers BLAS, LAPACK, random numbers, special functions, optimization |
+| Visualization | cl-cairo2, Vecto, CLG, CommonQt, cl-zxing | Exists but scattered — no unified plotting framework like Mathematica's |
+| Notebook interface | cl-jupyter, common-lisp-jupyter, Lem | Jupyter kernel works. Lem is a native editor approaching notebook capability. No Mathematica-level notebook yet. |
+| Rule-based programming | fare-matcher, optima, prolog implementations | Pattern matching is good. Full term-rewriting system needs assembly. |
+| Knowledge graph | gbrain, various triplestore libs | Possible but would need Wolfram Alpha-level investment |
+| Deployment | ASDF, Quicklisp, SBCL standalone executables | Better than Mathematica's deployment story — Lisp produces real executables |
+
+**The hard parts.**
+
+1. **The standard library is the product, not the engine.** Mathematica ships thousands of built-in functions — every mathematical special function, every statistical distribution, every graph algorithm, every image processing filter, every string operation, every data format parser. This is not a technical challenge; it is a sheer volume problem. The open-source answer is to wrap existing C/C++ libraries (GSL for special functions, OpenCV for image processing, igraph for graph algorithms, etc.) and expose them through a unified symbolic interface. This is the Clasp approach: interop with mature C++ libraries rather than rebuilding everything from scratch in Lisp. The Wolfram equivalent would be a CLOS-based symbolic dispatch layer that wraps these libraries and makes them accessible through a consistent term-rewriting evaluator.
+
+2. **The notebook interface is a product in itself.** Mathematica's notebook is not a terminal with nice formatting. It is a computational notebook with inline typeset math, dynamic graphics, collapsible sections, live evaluation, and a rich document model. The Jupyter ecosystem solves half of this. A Lisp-native notebook would need a rendering engine for mathematical notation (LaTeX or MathJax integration), inline interactive graphics, and a document model compatible with literate computation. Lem is the most promising starting point — it already has Emacs-like extensibility, a GTK frontend, and a Lisp-native codebase. Extending Lem to support computational notebooks with inline graphics and typeset output is the shortest path.
+
+3. **Performance for specialized domains.** Mathematica's kernel is highly optimized for symbolic operations — pattern matching over large expressions, automatic algorithm selection, memoization, and incremental compilation. A naive Lisp implementation would match Mathematica for small-to-medium expressions but would need significant optimization work for the heavy cases (symbolic integration of large expressions, graph operations on million-node graphs, image processing pipelines). The advantage is that Lisp's compiler infrastructure (SBCL's type inference, VOPs, inlining) gives a much better baseline than most languages. SBCL can generate code that approaches C speed for numerical kernels.
+
+4. **The knowledge graph (Wolfram Alpha).** Mathematica's integration with Wolfram Alpha — querying computable data about chemistry, geography, finance, linguistics, etc. — is a separate product with a massive engineering investment in data curation. An open-source equivalent would not replicate this. It would either provide a local, user-curatable knowledge base (gbrain fits here) or integrate with existing open knowledge graphs (Wikidata, DBpedia). The gbrain connection is interesting: if Passepartout's knowledge store can answer factual queries with provenance, that becomes the Wolfram Alpha equivalent for the Lisp Mathematica.
+
+5. **Package ecosystem and community.** Mathematica's advantage is not just its engine but its ecosystem — thousands of paclets, the Wolfram Function Repository, the community that shares notebooks. An open-source equivalent needs a package manager (Quicklisp solves this for Lisp libraries), a repository for symbolic packages (a Wolfram Function Repository equivalent), and a critical mass of users who both use and contribute. Maxima has users but not contributors. The gap is community formation, not technical capability.
+
+**The viability assessment.**
+
+| Domain | Viability | Timeline estimate | Risk |
+|---|---|---|---|
+| Core symbolic evaluator | High — Lisp was designed for this | 6-12 months for working prototype | Low — well-understood problem |
+| Computer algebra | High — Maxima already exists | Integrate now; polish 1-2 years | Low — needs UI/UX investment |
+| Numerical computing | High — wrappers exist | 3-6 months for unified interface | Low — wrapping problem |
+| Visualization | Medium — scattered pieces | 1-2 years for unified framework | Medium — needs new work |
+| Notebook interface | Medium — Lem as foundation | 1-2 years to Mathematica parity | Medium — significant UX engineering |
+| Standard library breadth | Low — volume problem | 3-5 years with community | High — needs sustained contribution |
+| Knowledge graph | Low — curation cost | 2-3 years for basic integration | High — different product category |
+| Deployment | High — Lisp executables | Works now | None |
+
+**The strategic question.**
+
+The real question is not "can we replicate Mathematica in Lisp" but "should we?" — and if so, for whom.
+
+Mathematica serves two distinct use cases:
+
+- **Interactive exploration** — a researcher types an integral, gets a result, visualizes it, iterates. Lisp + Maxima + a good notebook interface already does this, and the experience is competitive for anyone comfortable with Lisp syntax.
+- **Deployed computation** — a company builds a production pipeline around Mathematica kernels, deploying computation as a service. Lisp executables are dramatically better here — they are real compiled binaries, not managed by a proprietary kernel, deployable without license fees, embeddable anywhere.
+
+For the second use case, the open-source Lisp alternative is already superior. The gap is the first use case: the interactive exploration experience, the breadth of built-in functions, and the cultural acceptance of Lisp syntax in communities that currently write Wolfram Language.
+
+The most viable path is not to clone Mathematica but to integrate Maxima + numerical Lisp libraries under a unified symbolic interface, expose all of it through a Lem-based notebook, and make the Jupyter bridge the primary entry point for users who prefer Python notebooks. This gives you 80% of Mathematica's capability with a fraction of the development cost, and it connects to the existing scientific Python ecosystem rather than competing with it.
+
+**The deeper point.**
+
+Mathematica's architecture is Lisp-like because it was inspired by a Lisp system (Macsyma). An open-source Mathematica in Lisp is not a port. It is a return to the original architectural vision, implemented in the language that vision was originally expressed in. The question is whether the community investment materializes — and that depends on whether there is a use case that justifies it. Passepartout's verification infrastructure may be that use case: a verified symbolic computation engine that reasons about its own results is a Mathematica-like system by necessity, and building it in Lisp is the natural path.
+
+---
+
+- [[id:f4e5d6c7-b8a9-0c1d-2e3f-4a5b6c7d8e9f][Schafmeister and Clasp]] — Lisp in computational nanotechnology, existence proof for Lisp viability in scientific computing
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — why Lisp and where the symbolic engine fits

ideas/passepartout-bootstrap-mathematica.org

@@ -0,0 +1,92 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       8b9c0d1e-2f3a-4b5c-6d7e-8f9a0b1c2d3e
+:END:
+#+title: Could Passepartout Bootstrap Mathematica or mathlib by Itself?
+#+filetags: :ideas:lisp:passepartout:mathematics:
+
+This extends the previous viability analysis with a specific scenario: assuming Passepartout exists at Stage 3+ (full Lisp machine with neurosymbolic engine, verification gate, and self-modification capability), how hard would it be for it to recreate Mathematica or mathlib in pure Common Lisp on its own?
+
+**The bootstrap is architectural, not aspirational.**
+
+The neurosymbolic engine is not just a faster way to write code. It is a closed loop: the LLM proposes implementations, the symbolic engine and ACL2 prover verify correctness, and the self-modification system hot-reloads the result into the running image. This loop runs autonomously, without human intervention. The system writes code, tests it formally, improves it, and keeps the result — permanently expanding its own capability.
+
+This is fundamentally different from a human writing Mathematica. A human writes code, compiles, tests, debugs. Passepartout writes code, has it verified against a formal specification, and loads it into its own runtime. The iteration speed is not hours or days — it is seconds per function, limited only by the LLM's generation latency and the prover's checking time.
+
+**What Passepartout already has.**
+
+At Stage 3, the system ships with:
+
+- A symbolic term-rewriting engine (the evaluator itself is one)
+- Pattern matching and rule-based transformation (native to the gate architecture)
+- ACL2 as a verification backend (can prove properties of generated code)
+- An LLM oracle for proposing implementations (the probabilistic brain)
+- A self-modification system (hot-reloads verified code into the running image)
+- A knowledge store with persistent facts (gbrain-derived)
+
+These are not general-purpose tools that happen to be useful for symbolic mathematics. They are the same tools that a computer algebra system needs, expressed in the same architecture. The evaluator that rewrites a gate policy is the same mechanism that rewrites a symbolic expression.
+
+**What it needs to generate.**
+
+| Component | Can Passepartout generate it? | How |
+|---|---|---|
+| Core symbolic evaluator | Yes, trivially — this is what Lisp *is* | The existing evaluator already does term rewriting. The neurosymbolic engine would create a higher-level pattern-matching layer over it. |
+| Computer algebra (differentiation, integration, simplification) | Yes — known algorithms, formally specifiable | LLM proposes implementation of Risch algorithm, polynomial GCD, Gröbner bases. ACL2 verifies the specification. |
+| Numerical libraries (BLAS, special functions, optimization) | Partial — better to wrap | ACL2 cannot verify floating-point numerics to the same standard. Passepartout would wrap existing C/C++ libraries via Clasp-style interop and verify the interface, not the numerics. |
+| Visualization framework | Yes — UI code, not math | The environment subsystem (Nyxt/Lish) already has rendering primitives. The neurosymbolic engine generates plotting and graphics code against them. |
+| The 5,000+ function standard library | Yes — volume, not novelty | This is the dominant cost. Each function is individually trivial (differentiate x^3 → 3x^2) but there are thousands. Passepartout generates them at LLM speed — roughly one function every 10-30 seconds including verification. |
+| Formal proofs of mathematical theorems (mathlib) | Qualified yes — different logic | mathlib is in Lean's dependent type theory. Passepartout's ACL2 is first-order logic. The theorems can be re-proven in ACL2, but the proofs are not portable. The LLM proposes proof strategies, ACL2 checks them. |
+
+**The rate limit is generation, not computation.**
+
+If Passepartout generates one verified function every 20 seconds (conservative — LLM proposal time + ACL2 verification), that is 180 functions per hour, ~4,300 per day. Mathematica's standard library contains roughly 6,000 documented functions. At this rate, the standard library would take ~1.5 days of continuous generation — assuming the LLM has the domain knowledge to produce correct implementations and ACL2 can verify them.
+
+This is the critical assumption. The LLM (at, say, GPT-4 or DeepSeek level) already knows what every Mathematica function does. It has seen them in training data. The question is whether it can generate a correct Lisp implementation with a formal specification that ACL2 can verify. For most elementary functions (differentiate, integrate polynomial, singular value decomposition, string split, image histogram), the answer is yes — these are well-understood algorithms with clear specifications.
+
+For specialized domains (elliptic curve cryptography, tensor network contractions, symbolic regression of differential equations), the LLM may generate approximately correct implementations that need refinement. The neurosymbolic loop handles this: ACL2 catches the mismatch, feeds the error back, and the LLM regenerates.
+
+**mathlib is a different problem.**
+
+mathlib is not a library of algorithms but a library of formal proofs — mathematical theorems expressed in Lean's dependent type theory, structured as a hierarchy of definitions, lemmas, and tactics. It represents hundreds of person-years of community effort, formalizing undergraduate mathematics and beyond.
+
+Passepartout's verification layer is ACL2, which operates in a different logical framework (first-order logic with induction for total functions, not dependent types). There is no porting mathlib — it would have to be re-proven in ACL2's logic.
+
+The advantage is that the theorems are already known. mathlib tells you exactly what to prove. The LLM reads the Lean statement, translates it to an ACL2 theorem, proposes a proof strategy, and ACL2 attempts the proof. This is a well-structured task for the neurosymbolic loop: the LLM generates proof plans, ACL2 verifies them, and failed attempts feed back to refine the next plan.
+
+The bootstrapping advantage: early proofs (basic arithmetic, set theory) strengthen the ACL2 reasoning library, which makes later proofs (real analysis, topology) faster. The system accelerates as it goes. mathlib's proof dependency graph is the natural generation order.
+
+Estimated timeline for mathlib-equivalent in ACL2, with Passepartout generating autonomously:
+
+| Milestone | Time estimate | Note |
+|---|---|---|
+| Basic arithmetic, algebra, number theory | Days — standard library material | Well-known proofs, simple structure |
+| Real analysis, measure theory | Weeks — proof complexity increases | Non-trivial but well-studied |
+| Abstract algebra (groups, rings, fields) | Weeks — structural, builds on itself | The neurosymbolic loop excels here |
+| Topology, algebraic topology | Months — conceptual depth | Proofs are longer, more strategic |
+| Category theory, homological algebra | Months — abstraction barrier | High-level abstraction, fewer verification primitives |
+| Number theory deep results (FLT, modular forms) | Unknown — research frontier | Passepartout is not proving open problems. It formalizes known results. |
+
+**The bootstrapping compound effect.**
+
+The most interesting property is not that Passepartout can generate Mathematica's library. It is that each generated function becomes part of Passepartout's own capability. After generating the differentiation function, Passepartout uses it to generate the integration function. After generating linear algebra, it uses that to generate optimization algorithms. After generating formal proofs of real analysis, it uses those theorems to verify more complex deductions.
+
+This is not a production pipeline. It is an autodidactic loop: the system generates math, then uses that math to generate more math. The acceleration is exponential in the early phases and linear in the later phases, limited by the rate at which the LLM can produce new correct specifications.
+
+**The real barrier is not technical but oracular.**
+
+At every step, Passepartout depends on the LLM's knowledge of existing mathematics. The LLM has seen most of human mathematical knowledge in its training data. It can propose correct implementations and proof strategies because it has seen them. But for genuinely new mathematics — theorems not present in the training data, algorithms that have not been discovered — the LLM has no signal. Passepartout would be limited by its oracle.
+
+Stage 7 acknowledges this: oracular limits are fundamental. The verification subsystem can check correctness against a specification, but it cannot generate the specification itself. The LLM provides the what; ACL2 verifies the that. Neither provides the why that extends beyond existing knowledge.
+
+**Conclusion.**
+
+Recreating Mathematica's standard library: **days to weeks** of autonomous generation. The volume problem is solvable because the LLM already knows the answer space and ACL2 can verify each function. No human intervention required.
+
+Recreating mathlib's formal proof corpus: **months** of continuous formalization. The neurosymbolic loop maps naturally onto the task of converting known theorems from one logical framework to another. The dependency graph of mathlib provides the optimal generation order.
+
+Neither requires new research. Both are engineering throughput problems that Passepartout's architecture is designed to solve: generate, verify, reload, repeat. The only hard limit is the oracle — the system cannot generate mathematics that the LLM does not already know exists.
+
+---
+
+- [[id:7a8b9c0d-1e2f-3a4b-5c6d-7e8f9a0b1c2d][Viability of open-source Wolfram/Mathematica in Lisp]] — the human-driven assessment
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — the verification and self-modification systems

ideas/practical-powers-three-pronged.org

@@ -0,0 +1,88 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       2f3a4b5c-6d7e-8f9a-0b1c-2d3e4f5a6b7c
+:END:
+#+title: Practical Powers of the Three-Pronged System
+#+filetags: :ideas:passepartout:architecture:
+
+What can Passepartout do with its three layers — deductive proofs, provenance-tracked empirical models, and probabilistic oracle — that a conventional system cannot? This note catalogs the practical powers that fall out of the architecture, not as abstract potential but as concrete capabilities.
+
+**1. It can tell you how wrong every result might be.**
+
+This is the single most important power. Computational science today produces precise-looking numbers with no error bars. A molecular dynamics simulation outputs "binding free energy: −9.2 kcal/mol" and the number looks definitive. It is not. It depends on a chain of models (force field, solvation, sampling, scoring) each with its own uncertainty.
+
+Passepartout traces the chain automatically. It reports: "binding free energy: −9.2 kcal/mol ± 1.4 kcal/mol. Breakdown: force field uncertainty ±0.8 kcal/mol, solvation model ±0.5 kcal/mol, conformational sampling ±0.3 kcal/mol, scoring function ±0.6 kcal/mol. Model validity regime: proteins in water at 298K ± 25K. Your conditions fall within this regime."
+
+No computational chemistry package does this today. Every one outputs a precise number and leaves the uncertainty to the scientist's judgment.
+
+**2. It can prevent you from using a model outside its valid range.**
+
+A force field parameterized for soluble proteins at room temperature gives plausible-looking numbers for a membrane protein at body temperature, but those numbers are not physically meaningful. The simulation runs, produces output, and a human who does not know the force field's history may trust the result.
+
+Passepartout's gate catches this at the check level: "This force field was validated for aqueous solutions of soluble proteins at 273-373K. Your simulation involves a lipid bilayer environment at 310K. Three of the lipid-specific parameters are outside their validated range. Recommendation: use a membrane-specific force field (CHARMM36m) instead. Confidence reduction: 40% if you proceed with current selection."
+
+This is a fundamentally new kind of safety. Not "is this action malicious?" but "is this computation sound?"
+
+**3. It can detect when a model is getting worse.**
+
+Empirical models degrade over time. A force field fitted to 1990s experimental data may be worse than a later version fitted to more data, but there is no automatic mechanism to detect this. A scientist who has been using the same force field for a decade may not realize it has been superseded.
+
+Passepartout tracks every model version. When it processes a new publication with updated parameters, it can compare: "The AMBER ff99 parameters you are using were superseded by ff14SB in 2014 and ff19SB in 2019. The newer parameter sets improve backbone dihedral prediction by 30% for the protein class you are simulating. Migrate to ff19SB?" It does this because every parameter has a timestamp, a source, and a validation record.
+
+**4. It can compare predictions to experiments automatically.**
+
+Every time Passepartout makes a computational prediction and receives (or the user provides) an experimental measurement for the same system, it records the comparison. Over hundreds of comparisons, it builds a systematic bias profile for each model: "This force field consistently underestimates binding affinity for charged ligands by 0.5-1.0 kcal/mol. This solvation model overestimates solubility for aromatic compounds."
+
+These bias profiles are not research papers. They are accumulated operational knowledge that makes future predictions more interpretable. No existing system does this because no existing system treats models as entities with provenance rather than as files on disk.
+
+**5. It can red-team its own reasoning.**
+
+The probabilistic oracle (LLM) proposes a conclusion. The deductive layer (ACL2) checks the formal steps. The provenance layer (empirical knowledge base) checks whether the models used are valid for the context. If all three agree, the conclusion is as reliable as the system can make it. If they disagree, the conflict itself is informative: "The formal mathematics checks out, but the models supporting it are outside their validated range. Your conclusion may be mathematically correct but physically unsupported."
+
+This is a kind of epistemic hygiene that no single-layer system can achieve. A purely probabilistic system (LLM alone) can be confidently wrong. A purely deductive system (prover alone) can only reason within its formal domain. A purely empirical system (database alone) cannot synthesize across domains. The three layers cross-check each other.
+
+**6. It can build a community knowledge graph of what works.**
+
+When multiple Passepartout instances use the same model in different conditions and compare to experimental data, the combined record extends the model's validity envelope. One instance validates a force field for ethanol. Another validates it for DMSO. A third validates it for mixed solvents. The model's validity envelope grows across the network without any single instance having to run all the experiments.
+
+The social protocol becomes the mechanism for this sharing: instances publish validation results as signed, provenance-tracked claims. The network aggregates them. A model that starts with a narrow validity envelope (water, 298K) gradually accumulates enough validation data to cover a wide range of conditions.
+
+No existing scientific software network does this. Journals publish individual validation studies; nobody aggregates them into a living validity map for each model.
+
+**7. It can generate a defensible record for regulatory submission.**
+
+If a pharmaceutical company uses Passepartout in a drug discovery pipeline, every simulation result carries a full provenance chain: force field version and source, solvation model parameters and validation benchmark, conformational sampling algorithm and integrator settings, gate checks that passed, uncertainty budget per component.
+
+This record is essentially a compliance document. It answers the question "how do I know this result is reliable?" with a traceable chain of evidence, not a scientist's assertion. For industries regulated by the FDA, EMA, or similar bodies, this is the difference between a simulation being used for guidance and a simulation being accepted as evidence.
+
+**8. It can be wrong honestly.**
+
+This sounds trivial but it is the hardest thing for software to do. Every scientific software package presents its outputs with equal authority. A result from a high-quality QM calculation and a rough empirical estimate look the same in the output file — just numbers.
+
+Passepartout would output: "This result is deductively proven (ACL2-verified, level 0-7)." or "This result is computationally rigorous within an empirical model (provenance-tracked, level 8-14, validity envelope intact)." or "This result is an extrapolation outside the model's validated range. Confidence is low. Here is what would need to be measured to increase confidence."
+
+Honesty about uncertainty is a power because it changes what you can do with the result. A deductively proven result can be used as a building block for further proofs. An empirical result within its validity envelope can be used for design decisions with known risk. An extrapolation should only be used for hypothesis generation. Passepartout would know which is which and tell you.
+
+**9. It can refuse an unsound instruction.**
+
+Today, if you ask a computational chemistry package to run a simulation, it runs the simulation. It does not check whether the settings are physically meaningful. The error is not caught until a human reviews the output — if they ever do.
+
+Passepartout's gate can say: "I will not run this simulation. The requested temperature (500K) exceeds the force field's validated range (273-373K). The solvent (hexane) has no validated parameters in this force field version. The simulation will produce numerically precise but physically meaningless results. If you want to proceed, I will flag all output as extrapolation with a confidence score of 0.3 out of 1.0."
+
+The power is not that Passepartout prevents the simulation. It is that Passepartout makes the choice explicit: the human can override, but the override is recorded, and the result is tagged with its true reliability rather than appearing to be definitive.
+
+**10. It can connect mathematics to reality without faking it.**
+
+This is the deepest power. A conventional system either stays in the pure formal domain (proof assistants, CAS) or stays in the empirical domain (simulation software, ML). Passepartout bridges them by making the boundary explicit.
+
+A mathematician can prove a theorem (layers 0-3). An engineer can build a bridge using empirical models (layers 8-12). Passepartout can connect the two: "The finite element equations for this bridge are verified against classical mechanics (layer 4). The material parameters come from ASTM standard tests on this specific steel alloy (layer 8-9, validity envelope: −20°C to 60°C, validated by 200+ measurements). The load calculations carry ±3% uncertainty based on material parameter variance." The bridge is not proven safe — no software can prove a physical structure is safe — but the chain from mathematical foundation to empirical measurement is fully transparent.
+
+**Summary: three kinds of power.**
+
+| Layer | What it verifies | What it enables |
+|---|---|---|
+| Deductive proofs | Correctness against axioms | Autonomous generation of verified algorithms |
+| Provenance-tracked models | Implementation fidelity + data source | Scientific integrity, uncertainty budgets, audit trails |
+| Probabilistic oracle | N/A (generates hypotheses) | Synthesis, model selection, natural language interface |
+
+Alone, each layer is a tool. Together, they form a system that can reason formally, model empirically, communicate naturally — and tell you which mode is in effect for every result it produces.

ideas/schafmeister-clasp-nanotechnology.org

@@ -0,0 +1,48 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       f4e5d6c7-b8a9-0c1d-2e3f-4a5b6c7d8e9f
+:END:
+#+title: Christian Schafmeister — Common Lisp in Computational Nanotechnology
+#+filetags: :ideas:lisp:nanotechnology:
+
+Christian Schafmeister is a chemistry professor at Temple University in Philadelphia. He created [[https://github.com/clasp-developers/clasp][Clasp]], a Common Lisp implementation that interoperates with C++ libraries using LLVM compilation, specifically to solve a problem most Lisp implementers never face: designing molecules at the nanoscale.
+
+**The problem.**
+
+Schafmeister's research focuses on spiroligomers — large, shape-programmable molecules built from synthetic monomers. These are programmable at the level of both shape and functional groups, meaning they can be designed to bind specific proteins as therapeutics or accelerate chemical reactions the way enzymes do. The goal is to create molecules that can do everything proteins do in nature, but that are designable and evolvable by human beings.
+
+This is a computational problem of enormous complexity. Designing these molecules requires simulating their behavior, computing binding affinities, searching conformational space, and iterating designs rapidly based on experimental feedback. The compute pipelines involved typically live in the C++ ecosystem (a vast array of scientific computing libraries), but the workflow itself — rapid prototyping, interactive exploration, incremental development — demands the kind of environment that C++ alone cannot provide.
+
+**Why Lisp won.**
+
+Schafmeister's argument for Common Lisp in computational nanotechnology mirrors the same reasoning that drives Passepartout's architecture:
+
+- **Interactivity.** Molecular design requires exploration. A researcher needs to load data, inspect it, try a transformation, undo it, try another — all within a live environment. Lisp's REPL-driven development provides this in a way that compile-link-run cycles cannot match.
+- **Incremental development.** The design space for spiroligomers is too large to simulate exhaustively. You need to build up models piece by piece, testing each step. Lisp's incremental compilation and hot-reloading make this natural.
+- **Unified representation.** In Lisp, the code that describes a molecule and the code that simulates it share the same structure. There is no translation barrier between the design language and the simulation language.
+
+But the scientific computing ecosystem lives in C++. Schafmeister could not afford to rebuild every computational chemistry library from scratch. So he built Clasp: a Common Lisp implementation that compiles to native code via LLVM and interoperates seamlessly with C++. Clasp can call any C++ library natively, and C++ can call back into Lisp. The result is that the entire scientific computing ecosystem becomes available from within a Lisp environment — programmable, interactive, introspectable.
+
+**The architecture.**
+
+Clasp is not a wrapper or a bridge. It is a full Common Lisp implementation where the C++ interoperation is part of the language runtime itself. The clbind library provides declarative bindings — you describe how C++ classes and functions map to Lisp, and Clasp generates the glue code automatically. This is fundamentally different from CFFI-style foreign function interfaces, which require manual marshaling and are inherently fragile.
+
+From the Lisp perspective, a C++ class appears as a CLOS class. You can subclass it, specialize methods on it, inspect its instances. The boundary between Lisp and C++ is transparent to the programmer.
+
+**Funding and validation.**
+
+Clasp has been funded by the Defense Threat Reduction Agency (DTRA), the National Institutes of Health (NIGMS), and the National Science Foundation. These are agencies that fund computational chemistry and materials design, not programming language research. They funded Clasp because it solved a real problem in molecular design that no other approach addressed: making C++-scale scientific computing work within an interactive Lisp environment.
+
+**Relevance to Passepartout.**
+
+Schafmeister's work is existence proof for two of Passepartout's core claims:
+
+1. Lisp is not a niche language for academic AI research or Emacs configuration. It is being used today to design therapeutic molecules that bind proteins, in environments funded by the NIH and NSF. The interactivity and homoiconicity that Passepartout relies on are the same properties that make this work possible.
+
+2. The single-address-space model is not a limitation but an enabling constraint. Clasp proves that you can run C++ libraries inside a Lisp image, not alongside it. The "Lisp machine" is not a retro fantasy — it is a practical architecture being used today for computationally demanding scientific work.
+
+The main difference is direction: Schafmeister brought C++ into Lisp to access the scientific computing ecosystem. Passepartout replaces the C++ scientific computing ecosystem with verified Lisp-native alternatives. The architectural principle — one representation, one address space, no translation boundaries — is the same in both cases.
+
+---
+
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — why Lisp is the choice for verified infrastructure

ideas/wider-implications-three-pronged.org

@@ -0,0 +1,82 @@
+:PROPERTIES:
+:CREATED:  [2026-05-25 Mon]
+:ID:       5c6d7e8f-9a0b-1c2d-3e4f-5a6b7c8d9e0f
+:END:
+#+title: Wider Practical Implications of the Three-Pronged System
+#+filetags: :ideas:passepartout:implications:
+
+Beyond Passepartout itself, the three-pronged model — deductive proofs, provenance-tracked empirical models, and probabilistic oracle, all under one gate — has implications for how computation is trusted, regulated, and used across every domain that relies on simulation or AI.
+
+**1. The end of the trust-the-tool default.**
+
+Today, if you run a molecular dynamics simulation in AMBER or a finite element analysis in ANSYS, you trust the result because the tool is widely used. "Everyone uses this software" is the epistemic warrant. The three-pronged system replaces this with an explicit chain: this equation was verified against classical mechanics, these parameters come from a specific experimental paper, this validity envelope covers the conditions you specified. The trust moves from "the tool is popular" to "the chain is traceable."
+
+The implication: a less popular tool with good provenance becomes more trustworthy than an industry-standard tool with none. This changes the competitive dynamics of scientific software — the lock-in shifts from ecosystem size to provenance quality.
+
+**2. AI safety as an architectural constraint, not a training target.**
+
+Current AI safety is probabilistic. We train models not to lie, not to harm, not to be biased. The training is never perfect, the guardrails can be jailbroken, and every new model generation requires retraining the safety layer.
+
+The three-pronged system offers a structural alternative: the LLM can propose anything, but the gate enforces what is actually executed. The LLM cannot write a file, send a message, or run a command — it can only propose. The gate decides. The safety is in the gate's predicates, not in the LLM's training.
+
+The implication: safety becomes provable. You can verify that a gate predicate is correct (it blocks rm -rf / for all inputs). You cannot verify that a trained model is honest. This is the difference between "we hope the AI behaves well" and "the AI physically cannot execute a disallowed action."
+
+**3. Regulatory science with defensible evidence chains.**
+
+Pharmaceutical, aerospace, and medical device companies spend billions on computational simulations that regulators review. Currently, the review relies on the submitting company's assertion that the simulation was run correctly. The provenance chain is in lab notebooks and internal documents, not in the output itself.
+
+A three-pronged system produces outputs with built-in defensibility: every parameter has a source, every approximation is tagged, every gate check is recorded, every uncertainty is budgeted. A regulator can read the output and see: "the force field was parameterized against these 50 experimental measurements, the DFT calculation used this functional and basis set, the validity envelope covers the conditions of interest, the total uncertainty is ±X."
+
+The implication: regulatory review shifts from auditing the company's process to auditing the computation's chain. This is faster, more transparent, and less dependent on the reviewer's expertise in every specific tool.
+
+**4. The reproducibility crisis has a technical solution.**
+
+A major cause of the reproducibility crisis in computational science is incomplete specification of methods. "We used the AMBER force field" is not enough — which version? which parameter set? which cutoff scheme? which solvation model? Which experimental validation was it based on?
+
+The three-pronged system's provenance chain is a complete specification by construction. Every computation is fully described by its model, its parameters, its validity envelope, and its gate checks. Reproducing the computation is a matter of loading the same provenance chain and running it.
+
+The implication: computational reproducibility shifts from a social norm ("please share your code and parameters") to an automated property of the output. If the output does not carry a full provenance chain, it is not fully specified.
+
+**5. Engineering safety margins become explicit.**
+
+Every engineered structure — bridge, aircraft, medical implant — is designed using simulation. The safety margins are specified in standards (factor of 2, factor of 5, etc.) but the actual uncertainty in the simulation is rarely quantified. A civil engineer running a finite element analysis of a bridge does not know the combined uncertainty of the material model, the mesh resolution, the boundary conditions, and the load assumptions.
+
+The three-pronged system would propagate uncertainty through the entire design chain. The output would include: "the failure probability under maximum load is 0.03%, with the following breakdown: material parameter uncertainty contributes 0.02%, mesh discretization contributes 0.005%, load modeling contributes 0.005%."
+
+The implication: safety margins in standards can be replaced or supplemented by model-specific uncertainty budgets. A design with low uncertainty can use a smaller safety factor; a design with high uncertainty must use a larger one. This saves material and weight where the simulation is reliable, and forces conservatism where it is not — the opposite of today's one-size-fits-all approach.
+
+**6. Education in how knowledge works.**
+
+Current STEM education teaches equations and methods. Students learn to compute binding affinities, solve differential equations, run simulations. What they do not systematically learn is the difference between a proven result, a validated model prediction, and a reasonable guess.
+
+A three-pronged system, used in education, would make this distinction visible for every computation. A student simulating a chemical reaction would see: "this reaction barrier was computed at the CCSD(T) level of theory with a complete basis set extrapolation — this is the gold standard in quantum chemistry and is well within the formal domain. The solvation correction uses an implicit solvent model validated against 200 experimental free energies of solvation for neutral organic molecules — this is an empirical model with known accuracy of ±0.5 kcal/mol. The conformational search used a genetic algorithm that may not have found the global minimum — this is a heuristic with no guaranteed completeness."
+
+The implication: students develop epistemic hygiene as a side effect of using the system, not as a graduate-level skill acquired through years of trial and error.
+
+**7. The economics of computational trust.**
+
+Not all computations are equally valuable. A result that is deductively proven can be used as a building block for further proofs — its truth is inherited by any derivation that uses it. A result that is empirically validated is useful for decisions with known risk, but cannot be used as a deductive foundation. A result that is an LLM extrapolation is useful only for hypothesis generation.
+
+The three-pronged system makes this distinction explicit, which has economic implications. A pharmaceutical company might pay more for a binding affinity prediction that carries a full provenance chain and uncertainty budget than for one that is just a number. A patent application based on a proven result is stronger than one based on a simulated one.
+
+The implication: computational results become differentiated products, not interchangeable commodities. The provenance quality is the differentiator.
+
+**8. The social protocol as a scientific knowledge commons.**
+
+When multiple Passepartout instances share validated model parameters through the social protocol, the network accumulates a collective knowledge base that no single instance could build alone. A force field validated by one group for water, another for ethanol, another for DMSO — all shared with full provenance — becomes a model whose validity envelope has been extended across many conditions by distributed effort.
+
+The implication: the social protocol is not just a communication mechanism. It is an infrastructure for distributed scientific knowledge curation. The network effect is not just more users; it is more validated knowledge.
+
+**9. The gate as a universal integrity layer.**
+
+The gate currently checks security and scientific validity. There is no reason it could not check other dimensions of integrity: ethical constraints (do not simulate chemical warfare agents), legal constraints (do not export restricted technology), economic constraints (do not run a compute job that exceeds the user's budget), or institutional constraints (only use models approved by the lab's review board).
+
+The implication: the gate becomes a **configurable integrity layer** that enforces any policy that can be expressed as a predicate over the computation's inputs, models, and parameters. Different users, institutions, or jurisdictions can configure different gate policies without changing anything else in the system. Compliance becomes configuration.
+
+**10. The shift from "what does the software do?" to "how does the system know what it knows?"**
+
+This is the deepest implication. Most software today answers "what does this program output?" The three-pronged system answers "how does the system know that this output is reliable?" — by checking which domain it was produced in, tracing the provenance chain, and reporting the uncertainty budget.
+
+This changes the fundamental question users ask of software. Instead of "is this tool well-regarded?" they ask "is this result proven, validated, or generated?" — and get a different answer for every specific result, not a blanket trust judgment about the tool.
+
+The implication: computation becomes epistemically transparent. The system does not ask the user to trust it. It shows the user what it knows and how it knows it, and lets the user decide what to do with that information.

ideas/world-models-middle-domain.org

@@ -0,0 +1,116 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       0d1e2f3a-4b5c-6d7e-8f9a-0b1c2d3e4f5a
+:END:
+#+title: The Middle Domain as World Models
+#+filetags: :ideas:passepartout:world-models:
+
+The middle of the knowledge tree — layers 8 through 14, from quantum chemistry approximations to molecular design heuristics — corresponds almost exactly to what the AI and robotics communities call world models. Recognizing this connection reveals a structural requirement for Passepartout that the current architecture does not explicitly address.
+
+**What a world model is.**
+
+In the AI sense, a world model is a predictive representation that an agent uses to anticipate the consequences of actions. It answers the question: if I do X, what happens next? The classic formulation decomposes this into:
+
+1. A sensory encoder that compresses observations into a latent state
+2. A dynamics predictor that predicts the next latent state given an action
+3. A reward or value predictor that evaluates states
+
+Every layer of the knowledge tree from 8 upward fits this description — it predicts how some aspect of reality evolves given initial conditions, parameters, and boundary conditions.
+
+**The deductive world models (layers 0-7).**
+
+Logic, algebra, analysis, classical mechanics, quantum mechanics, statistical mechanics, electrodynamics — these are world models where the dynamics are deductively complete. Given the state (a wavefunction, a phase space point, a metric tensor) and the equations of motion (Schrödinger equation, Hamilton's equations, Maxwell's equations), the time evolution is determined. No parameters to fit. No learning required. The model is provably correct against its axioms.
+
+These are the world models that ACL2 can verify. The prover can confirm that the Schrödinger solver correctly implements the Schrödinger equation for any input. The correctness is total — not statistical, not empirical.
+
+**The empirical world models (layers 8-14).**
+
+Quantum chemistry approximations, molecular mechanics, molecular dynamics, solvation models, docking scoring functions, reaction mechanism models, molecular design heuristics — these are world models where the dynamics are known in form but empirically parameterized. The functional form of the force field (bond stretching + angle bending + torsions + non-bonded) is a modeling choice. The parameters (force constants, equilibrium lengths, partial charges) are fitted to data. The solvation model has a mathematical structure, but its parameters are calibrated against measured solubilities.
+
+These world models cannot be verified against axioms. They can only be validated against experiment. The validation is always provisional — valid for the molecules and conditions tested, uncertain outside that domain.
+
+**The composition is layered world models, not a single one.**
+
+The critical structural insight: the world models are not independent. They form a dependency hierarchy.
+
+A docking prediction (layer 12) depends on:
+- A solvation model (layer 11) with its own parameters and validity domain
+- A molecular dynamics simulation (layer 10) that samples conformational space
+- A force field (layer 9) that predicts energies and forces
+- Quantum chemistry calculations (layer 8) that parameterize the force field
+- Statistical mechanics (layer 6) that relates ensemble averages to binding free energies
+- Classical mechanics (layer 4) that governs the MD integration
+
+Each layer's uncertainty propagates upward. The docking prediction's error is not the scoring function's error in isolation — it is the compound uncertainty of the force field, the solvation model, the conformational sampling, the MD integrator, and the scoring function, all composed.
+
+**The Passepartout world model formula.**
+
+A world model in Passepartout's architecture is a triple:
+
+**World Model = Verified Equations ⊗ Provenance-Tracked Parameters ⊗ Validity Envelope**
+
+- **Verified Equations** — the formal skeleton: the differential equations, the integration scheme, the force field functional form. Verified by the ACL2 prover against the deductive layer below. This is what the gate can definitively check.
+
+- **Provenance-Tracked Parameters** — the numbers that make the model match reality: force constants, partial charges, solvation parameters, scoring weights. Each carries a source (experimental paper, QM calculation, benchmark dataset), a confidence interval, a validity regime (temperature range, molecular class, solvent type), and a last-validation date.
+
+- **Validity Envelope** — the region of input space where the model has been experimentally validated. A force field parameterized for soluble proteins at 298K in water is valid there; applying it to a membrane protein at 350K in ethanol may produce plausible numbers with no physical meaning. The validity envelope is a learned or specified boundary that the gate checks.
+
+**The neurosymbolic engine's role in world models.**
+
+The neurosymbolic split maps onto world model construction and use as follows:
+
+- The **ACL2 prover** verifies the equations — the form of the model, the correctness of the implementation, the composition of multiple world models into a pipeline. This is deductive assurance.
+
+- The **LLM oracle** handles synthesis — selecting which world model to apply to a given problem, interpreting the model's output in natural language, generating hypotheses about why a prediction failed, proposing new parameterizations or model forms when the existing ones are insufficient.
+
+- A **new provenance layer** (described below) handles the third component — tracking parameters, maintaining validity envelopes, propagating uncertainty, and validating predictions against experiment.
+
+**What this changes in the architecture.**
+
+The architecture describes verification (the gate) and knowledge (the memex). World models require a third subsystem: the **empirical knowledge base** — a structured store of fitted parameters, experimental benchmarks, and validity regimes, with full provenance.
+
+The empirical knowledge base would:
+
+1. Store every parameter used by every world model (force field parameters, DFT functional constants, solvation model coefficients, docking scoring weights).
+2. Attach provenance to each parameter: the paper, dataset, or calculation it came from, the confidence interval, the validity domain.
+3. Track validation history: which experimental measurements have been compared to this model's predictions, with what outcome, and whether the parameters were updated as a result.
+4. Enforce validity regimes at the gate level: if a computation applies a model outside its validity envelope, the gate either blocks it (safe default) or flags it with a reduced confidence score.
+
+This is not the same as the symbolic index (which stores formal facts) or the neural index (which stores embedding vectors). It is a third index over empirical knowledge — parameteric, uncertain, and provisional, but no less essential for its lack of deductive certainty.
+
+**The connection to self-improvement.**
+
+The neurosymbolic engine's self-modification capability applies differently to each part of the world model triple:
+
+- **Verifying new equations** (updating the deductive core): the system generates a new algorithm, ACL2 proves it correct against the specification, it is hot-reloaded. This is the Mathematica-bootstrapping scenario — the system improves its own deductive world models autonomously.
+
+- **Updating parameters** (improving the empirical core): the system compares predictions to experimental measurements, detects systematic bias in a force field, and proposes updated parameters. The update is validated by checking whether the new parameters improve predictions on a held-out benchmark. No proof, just statistical improvement. The provenance trail records the change.
+
+- **Expanding the validity envelope** (learning where models work): the system accumulates computational predictions and experimental results, and learns the boundaries where each model is reliable. This is a continuous process, not a one-time formalization.
+
+The self-improvement loop for empirical world models is slower and more uncertain than for deductive ones — it requires experimental feedback, not just formal verification. But it is equally essential for any system that needs to operate in the real physical world rather than inside a closed formal system.
+
+**The test case.**
+
+Schafmeister's spiroligomer pipeline is the test case for all three components:
+
+- The **equations** — QM calculations (layer 8), force field predictions (layer 9), MD integration (layer 10), thermodynamic integration (layer 11), docking (layer 12), design rules (layer 14) — all need verified implementations.
+- The **parameters** — force field parameters for novel monomer types, solvation parameters for non-standard solvents, scoring function weights for spiroligomer-protein binding — need provenance and validity envelopes.
+- The **validation** — experimental binding assays, catalytic rate measurements, structural characterization (NMR, crystallography) provide the feedback that updates parameter confidence and expands validity regimes.
+
+If Passepartout can handle this pipeline correctly — distinguishing what is verified from what is empirically parameterized, tracking provenance through the composition of multiple world models, and propagating uncertainty from the bottom of the hierarchy to the top — then the architecture is complete. If it cannot, then the architecture only works for pure mathematics.
+
+**Summary.**
+
+| Layer | Type of world model | Verification mode | Key data |
+|---|---|---|---|
+| 0-7 | Deductive | ACL2 proof against axioms | Theorems, equations, algorithms |
+| 8-14 | Empirical | Validation against experiment | Parameters, benchmarks, validity envelopes |
+| All | Composed | Provenance + correctness | Traceability through pipeline |
+
+The middle domain is world models. The architecture needs to be built to reflect that.
+
+---
+
+- [[id:9c0d1e2f-3a4b-5c6d-7e8f-9a0b1c2d3e4f][The Middle of the Knowledge Tree]] — the layers from logic to nanotechnology
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — current architecture

ideas/world-models-plain-language.org

@@ -0,0 +1,88 @@
+:PROPERTIES:
+:CREATED:  [2026-05-24 Sun]
+:ID:       1e2f3a4b-5c6d-7e8f-9a0b-1c2d3e4f5a6b
+:END:
+#+title: What the World Model Idea Means — Plain Language
+#+filetags: :ideas:explanation:
+
+An explanation of the world model idea and its implications, written for someone who does not want to parse architectural jargon.
+
+**The basic idea in one sentence.**
+
+Some things you can prove are true (like 2+2=4), and some things you can only model approximately because you have to fit the numbers to real-world measurements (like how strongly a particular molecule bends or twists). Most practically useful knowledge is the second kind.
+
+**The deductive vs. empirical split.**
+
+There is a floor in the building of human knowledge. Below the floor, everything is provable from first principles. This includes:
+
+- Logic (if A implies B and A is true, then B is true)
+- Mathematics (calculus, linear algebra, number theory)
+- Fundamental physics (Newton's laws, the Schrödinger equation, Maxwell's equations)
+
+In theory, a computer with enough power can prove things at this level. Given the right axioms and enough time, it can derive any true statement. This is what ACL2 does — it proves that a piece of code is correct for all possible inputs.
+
+Above the floor, things change. The equations have a known form (bonds stretch like springs, molecules attract each other at long range and repel at short range), but the precise numbers in those equations have to be fitted to experimental measurements. There is no way to derive a spring constant from first principles — you have to measure it.
+
+This includes:
+
+- Chemistry (how strongly does this bond bend? how fast does this reaction happen?)
+- Biology (how tightly does this drug bind to this protein? how fast does this enzyme work?)
+- Engineering (how much weight can this beam hold before it cracks?)
+- Medicine (does this drug work? what dose is safe?)
+- Materials science (how strong is this alloy at high temperature?)
+- Climate science, geology, pharmacology, and almost every other applied science
+
+**The critical observation.**
+
+Most of what humans actually care about lives above the floor. Pure mathematics is beautiful and foundational, but nobody builds a bridge, cures a disease, or designs a drug using only proofs from first principles. Every practical domain works with approximate models that are useful but not deductively certain.
+
+Passepartout's verification engine can handle the stuff below the floor. It can prove that a numerical integration routine is correct, that a sorting algorithm works, that an algebraic simplification is valid. But above the floor, "verification" means something different — not "proven correct from axioms" but "the implementation correctly executes the model, and the model's parameters are traceable to experimental data."
+
+**The three parts of a useful computation.**
+
+In the deductive zone (below the floor), every computation has two parts:
+1. The algorithm (how you compute it)
+2. The verification (the proof that the algorithm is correct)
+
+In the empirical zone (above the floor), every useful computation has three parts:
+1. The equations (the known mathematical form of the model)
+2. The parameters (the numbers fitted to experimental data)
+3. The validity envelope (the range of conditions where the model is reliable)
+
+The equations can be verified — ACL2 can prove that your force field code correctly implements Hooke's law. The parameters cannot be verified; they can only be validated against experimental data. The validity envelope cannot be proven either — it is a learned or declared boundary that says "we checked this model works for these kinds of molecules at these temperatures; outside that range, we don't know."
+
+**What this means for Passepartout.**
+
+**First, the architecture needs three subsystems, not two.**
+
+The neurosymbolic split (probabilistic brain + deterministic prover) only covers the deductive zone. The empirical zone needs a third subsystem — a provenance tracker that stores where every parameter came from, what its confidence interval is, and what range of conditions it has been validated for.
+
+This subsystem does not prove anything. It curates. It ensures that when Passepartout simulates a molecule, every force constant, every partial charge, every solvation parameter has a source that can be checked. If the same parameter was determined by two different experiments with different results, the system can report both and flag the uncertainty.
+
+**Second, the gate gets a new job.**
+
+The gate currently asks "is this action safe?" — should this shell command run, should this file be written, should this network message be sent. With the world model insight, the gate also asks "is this model valid for the context?" — this force field was parameterized for soluble proteins; you are applying it to a membrane protein. The answer may be "block" or "allow with reduced confidence" or "flag for human review."
+
+This is not a security check. It is a scientific integrity check. But it uses the same mechanism — a policy evaluated before the computation proceeds.
+
+**Third, self-improvement splits into two speeds.**
+
+- **Fast loop** (below the floor): Passepartout generates a new algorithm, verifies it with ACL2, and hot-reloads it. This is what the Mathematica-bootstrapping scenario describes — days to generate thousands of provably correct functions. This loop runs autonomously.
+
+- **Slow loop** (above the floor): Passepartout makes a prediction using an empirical model, gets experimental data back (either by performing an experiment or reading a paper), and updates the model's parameters or validity envelope. This loop requires real-world feedback. It cannot run autonomously — it needs data from the physical world.
+
+Both loops matter. The fast loop makes Passepartout mathematically powerful. The slow loop makes it useful for real-world science and engineering.
+
+**What this does not mean.**
+
+This does not mean Passepartout cannot handle empirical science. It means Passepartout handles it differently — with explicit uncertainty, provenance tracking, and validity boundaries, instead of pretending the model is deductively certain.
+
+This is actually a design advantage. Most scientific software treats its parameters as if they were provably correct. Force field databases ship as flat files with no provenance. Passepartout would be the first system that can say: "I am running the AMBER force field. The bond-stretching parameters come from a 1995 paper by Cornell et al., validated against 50 small molecules. The partial charges come from the RESP fitting procedure, applied to HF/6-31G* calculations. The validity envelope covers proteins and nucleic acids in aqueous solution at 273-373K. Your simulation involves a lipid membrane at 350K, which is outside the validated range. The results may be qualitatively correct but the quantitative predictions should be treated with caution."
+
+No existing chemistry software does this. A system that can is more useful than one that cannot, even if the underlying simulation is the same.
+
+**The broader implication.**
+
+The deductive/empirical floor is not a weakness in Passepartout's design. It is a correct description of how knowledge actually works in the physical world. Most systems pretend everything is deductively certain and hide their assumptions. Passepartout would make the assumptions explicit, trace every number to its source, and report uncertainty alongside every result.
+
+This is what it means to build a system that does not lie to you.

projects/passepartout/_index.org

@@ -5,8 +5,55 @@
 #+title: Passepartout
 #+filetags: :index:
 
-The staged roadmap and architecture — from conventional computing through verified Lisp machine on custom silicon.
+**What Passepartout is.**
 
-- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — the full architecture: verification subsystem, environment subsystem, social protocol
+Passepartout is a project that builds toward a personal computing environment where you own your computation, your data, and your agency — and the architecture proves it, not promises it.
-- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — how verification cascades across society, economics, and geopolitics
+
-- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged roadmap]] — Stage 0 (Now) through Stage 7 (What Remains)
+It is a single system that is simultaneously:
+
+- Your editor, browser, shell, and AI agent — not separate programs but a single environment where everything works together because everything shares the same structure.
+- Your knowledge base — a living [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][memex]] of everything you read, write, and decide, stored in a format you can read and your machine can read, with no translation layer between them.
+- Your gatekeeper — a system that checks every action against your rules before taking it, whether the action comes from you, from the AI, or from the network.
+- Your identity and communication protocol — cryptographic identity, encrypted messaging, and provable exchanges between instances.
+
+These are not separate products. They are one project, one architecture, one machine.
+
+**Why it exists.**
+
+The modern computing stack is built from independently built, independently untrusted layers: hardware, firmware, operating system, compilers, runtime, network protocols, applications. Each layer assumes the layers below it are either trusted or someone else's problem. The gaps between layers are where exploits live.
+
+Security is reactive. We find bugs, we patch them, we run antivirus, we monitor logs. The model is probabilistic: "no known vulnerabilities" does not mean none exist, only that none have been found. The patching treadmill has been running for forty years and shows no sign of slowing.
+
+Passepartout asks a different question: what if you eliminated the boundaries between layers instead of trying to secure them? What if the entire stack shared one structure, one verification, one proof — from the rules that authorize an action to the hardware that executes it?
+
+This eliminates entire categories of threats by structural design, not by patching. Memory corruption exploits, compiler backdoors, malware with execution paths that bypass the rules — these are not mitigations you add on top of an unsafe system. They are classes of threat that cannot exist in a system built on this principle.
+
+**What it replaces.**
+
+| Current approach | Passepartout |
+|---|---|
+| Separate editor, browser, shell, agent — each a different program with different trust assumptions | One environment where all are functions in the same memory space |
+| Knowledge stored in a database you cannot inspect | Knowledge stored in a file format you read and edit directly |
+| Security through permissions, firewalls, antivirus, audits | Security through a rule system that checks every action before it executes |
+| Separate identity systems for every service (Google login, GitHub, Slack) | One cryptographic identity you control |
+| Vulnerabilities found and patched reactively | Categories of threat eliminated by architecture |
+
+**How we get there.**
+
+The full system is the destination, but every intermediate stage delivers value on its own. The project is designed as a staged migration from conventional hardware to the full architecture, with no rewrite required between stages. Stage 0 is running today.
+
+**What it means.**
+
+A system built this way shifts computing from an empirical trust model — "this has passed our tests" — to a deductive one: "this is structurally impossible for the following reasons." The downstream effects cascade beyond any single user:
+
+- A company's compliance obligations become a set of rules the system enforces by construction, not a binder of documents an auditor reviews once a year.
+- AI safety becomes a rule system between the AI and the actions it can take, not a set of probabilities and guardrails.
+- Software certification becomes a shared suite of proofs from every deployed instance — a public attestation that a system behaves as specified.
+
+Passepartout creates a new category: verified infrastructure. Not a safer operating system, not a better AI agent, not another social network — but the foundation beneath all three, built on a principle that the current approach cannot offer: that the system, by its structure, is trustworthy.
+
+---
+
+- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the system in detail
+- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — what verification cascades into
+- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged Roadmap]] — from today to Stage 7

projects/passepartout/architecture/_index.org

@@ -2,18 +2,14 @@
 :CREATED:  [2026-05-24 Sun]
 :ID:       5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a
 :END:
-#+title: Passepartout — Architecture Section Index
+#+title: Architecture
 #+filetags: :passepartout:index:
 
-This section documents the Passepartout architecture: the staged build-out from conventional computing through verified infrastructure, the subsystems, and the systemic effects of verification becoming the default.
+Architecture overview — narrative introduction, staged build-out, systemic effects, and the analytical frames that justify the design.
 
-**Architecture overviews:**
+[[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the narrative introduction to the project.
-- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture index]] — Passepartout architecture, market, revenue paths
-- [[id:a1fac32a-47de-5fbd-b67d-29152c851747][Architecture overview]] — the three subsystems at a glance
-- [[id:42c86e6f-4f27-4993-8238-b7bc7d15fb7b][Environment subsystem]] — the Lisp image, editor, browser, shell, hardware
 
-**Staged roadmap (progressive capability layers):**
+**Staged roadmap:**
-Each stage covers: what is added, what threats are eliminated, what it costs, when it is viable.
 
 | Stage | Delivers | Key cost | Timeline |
 |-------+----------+----------+----------|
@@ -28,3 +24,28 @@ Each stage covers: what is added, what threats are eliminated, what it costs, wh
 
 **Systemic analysis:**
 - [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic effects over time]] — how verification cascades across society, economics, and geopolitics
+
+**Key analytical frames:**
+- [[id:5961e469-53a3-5f3c-ab72-3c83ef91963f][Investment thesis — the unified view]]
+- [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Why Lisp is economically viable now — zero marginal cost]]
+- [[id:efc76898-03f7-57ba-923d-35d65da88bb7][The per-domain sufficiency flip]]
+- [[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development velocity and timeline estimates]]
+- [[id:aa6d062e-a520-5d14-8773-00687ed9c689][Competitive barriers — moats and infrastructure lock-in]]
+
+**Revenue streams:**
+Total addressable market: ~$960B/year across cloud, AI, OS, social media, payments, productivity, and compliance. The business model is the AWS of provable computing: AGPL infrastructure is free, revenue comes from verification appliances, gate rules, certification, namespace registry, hosted PDS, and a [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]].
+
+Short to long term:
+- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Verification appliance]] — certified Lisp Machine at scale
+- [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Domain gate packages]] — compliance encoded as gate rules
+- [[id:827bc546-e887-5b7c-9b65-6392beaf0920][Evaluation harness / certification monopoly]] — UL for AI
+- [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][PDS as a service]] — hosted personal data stores
+- [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][Compute marketplace]] — verified compute cycles
+
+**Strategy and IP:**
+- [[id:67faf52f-9126-50a7-b87e-2bedc610dac7][IP strategy — licensing + patents]]
+- [[id:5f55bbe6-d243-5766-8ccf-5c5cc88a6542][Impact on the AI/GPU industry]]
+- [[id:29e4dbf3-cf19-589c-8b14-389e8a39d564][Upgrade and distribution lifecycle]]
+- [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Domain gate packages — encoding and products]]
+- [[id:2afd9a3c-e96a-54c7-ac77-a05a28065b4b][Biology as proof of the Lisp model]]
+- [[id:00ab3a4d-e3de-5605-a67d-12935bb36ab5][Comparison with Symbolics Genera]]

projects/passepartout/architecture/architecture.org

@@ -4,52 +4,97 @@
 :ID:       a1fac32a-47de-5fbd-b67d-29152c851747
 :ID:       42c86e6f-4f27-4993-8238-b7bc7d15fb7b
 :END:
-#+title: Passepartout Architecture
+#+title: Architecture
-#+filetags: :passepartout:architecture:economics:index:
+#+filetags: :passepartout:architecture:
 
-Passepartout is a self-bootstrapping replacement for the entire personal computing stack — one project, one image, one verified memory graph. Three subsystems compose into a single system:
+The project index introduces Passepartout as a personal computing environment. This page describes the architecture in detail: the four subsystems, how they compose, how the gate works, how the memex is structured, and why the stack compresses into a single address space.
 
-**Verification subsystem** — The gate stack that evaluates every proposed action against formal policy. Capability-based authorization. Combines a probabilistic LLM for natural-language reasoning with a deterministic symbolic engine (gate stack, ACL2 prover, Screamer constraint solver) for all security-critical decisions. The gate verifies shell commands, DIDComm messages, and LLM-generated action proposals through the same decision procedure.
+**The four subsystems, one address space.**
 
-**Environment subsystem** — The Lisp image where editor, browser, shell, and agent coexist. No separate daemons, no IPC boundaries, no trust transitions between components. One address space from which the verification subsystem checks every state mutation.
+Passepartout is one system built from four subsystems that share one evaluation semantics, one memory graph, and one proof chain:
 
-Roadmap: v2.0 Lish editor + Nyxt browser (Qt/WebKit) → v3.0+ Lisp-native layout & browser → v4.0 in-process LLM → v5.0 tagged RISC-V hardware via TinyTapeout/FPGA → v6.0 world models and true agency.
+- **Environment** — the personal computing environment
+- **Knowledge** — the unified memex
+- **Verification** — the gate
+- **Social Protocol** — provable communication between instances
 
-**Social protocol implementation** — Self-sovereign DID identity, DIDComm encrypted messaging, [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][Personal Data Store]], relay network, [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]], liquid democracy.
+Each is described below.
 
-All three subsystems operate in the same Lisp address space. All three are verified by the same ACL2 prover. The gate stack that verifies a shell command also verifies a DIDComm message. The distinction between "tool" and "self" dissolves.
+**The environment: one address space.**
 
----
+The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment runs everything in a single Lisp address space. (Lisp is a family of programming languages where code and data share the same representation. This property means the machine can verify what code does and modify itself without restarting. It is the foundation that makes the entire architecture possible.)
 
-Total addressable market: ~$960B/year across cloud, AI, OS, social media, payments, productivity, and compliance.
+The editor is a Lisp function that manipulates text buffers in the evaluated memory graph. The shell is a Lisp read-eval-print loop that compiles to the same evaluator. The browser renders HTML through a Lisp-based rendering engine, not a separate process. The agent runtime invokes Lisp functions, not subprocesses. (The specific implementations that realize this today use Lish for the shell and editor, Nyxt for the browser, and SBCL as the host Lisp — but the architectural principle is uniform semantics in one address space, not these particular packages.)
 
-The business model is the AWS of provable computing: AGPL infrastructure is free, revenue comes from verification appliances, gate rules, certification, namespace registry, hosted PDS, and a [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]]. Network effects are positive sum — every instance feeds the regression suite and grows the marketplace.
+There is no MMU boundary between components because there are no separate processes. There is no IPC because there is nothing to communicate between. Everything shares the same memory graph. Your editor buffer, your shell history, your agent's state, and your social protocol messages all live in the same evaluated object graph, protected by the same gate, verified by the same prover.
 
-[[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp Machine security — unified memory threat model]]
+**The knowledge subsystem: Org-mode as unified memex.**
-[[id:04c2f221-c54f-51e5-b40a-48822cd16d45][Common Logic (ISO 24707) — relevance to Passepartout]]
-[[id:a5d59d12-b23e-58d6-a81b-9b8b06556949][Collective regression suite — how it compounds]]
 
-Key analytical frames:
+The knowledge subsystem makes a bet that most systems consider too expensive: that humans and machines should share the same file format. That bet is Org-mode.
-- [[id:5961e469-53a3-5f3c-ab72-3c83ef91963f][Investment thesis — the unified view]]
-- [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Why Lisp is economically viable now]]
-- [[id:efc76898-03f7-57ba-923d-35d65da88bb7][The per-domain sufficiency flip]]
-- [[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development velocity and timeline estimates]]
-- [[id:0b5a8a74-cfd6-542d-bc88-4eb3cd8626f9][Cost structure and zero marginal cost]]
-- [[id:aa6d062e-a520-5d14-8773-00687ed9c689][Competitive moats analysis]]
 
-Revenue paths (short to long term):
+Most systems separate human-readable notes from machine-readable data. The user writes Markdown. The system stores it, indexes it, searches it. But the system maintains its own internal model — a database, a knowledge graph — disconnected from the Markdown. When the user leaves, the Markdown survives but the model must be reconstructed.
-- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Verification appliance]] [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Domain gate packages]] [[id:45258a2d-1675-562c-9024-5d1eb2f1ea56][Evaluation harness]]
-- [[id:2e390c1d-65f3-5fb3-b898-ac3fc4291ee7][Protocol premium usernames]] [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][PDS as a service]] [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][Compute marketplace]]
-- [[id:827bc546-e887-5b7c-9b65-6392beaf0920][Verification monopoly — the big money]] [[id:2f783eb4-638e-5afa-9b59-6224d086a712][Infrastructure lock-in]]
 
-Strategy and IP:
+Passepartout refuses this separation. The Org file is not a representation of the data; the Org file IS the data. The same text the user reads and edits is what the system parses and operates on. There is no translation layer between human and machine — no schema, no import/export, no API boundary between what you write and what the system knows.
-- [[id:caaeee11-ba6f-5566-aecd-f171b4c459c0][Patent strategy]] [[id:67faf52f-9126-50a7-b87e-2bedc610dac7][Licensing (AGPL + commercial)]]
-- [[id:5f55bbe6-d243-5766-8ccf-5c5cc88a6542][Impact on the AI/GPU industry]]
-- [[id:29e4dbf3-cf19-589c-8b14-389e8a39d564][Upgrade and distribution lifecycle]]
-- [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][Gate rule encoding from codified domains]]
-- [[id:2afd9a3c-e96a-54c7-ac77-a05a28065b4b][Biology as proof of the Lisp model]]
-- [[id:00ab3a4d-e3de-5605-a67d-12935bb36ab5][Comparison with Symbolics Genera]]
 
-The [[id:b25bf753-9799-41ab-82f5-1a1416db756b][protocol overview]] and [[id:a3243dd0-3209-423b-98e1-51c3eada2658][advanced integration]] requirements define how Passepartout's gate stack connects to the social protocol layer. The [[id:72570648-d943-42e5-a781-3b09791ac6ec][realistic assessment]] covers deployment timelines and adoption risks.
+Sparse tree retrieval makes this efficient at scale. Org-mode's headline hierarchy is a semantic structure the system can query. When the agent needs information about a specific function, it retrieves exactly the subtree under that heading — not the entire file. Context stays lean (2,000 to 4,000 tokens) while the full knowledge base remains accessible through structural retrieval. This is fundamentally different from Markdown, where retrieval is either imprecise (grep) or entire-file (expensive).
 
-*The lines that run the modern internet (tens of millions across Google, Meta, Amazon, Apple, Microsoft) are replaced by a single coherent architecture where one gate stack verifies everything and one prover proves everything consistent.*
+The knowledge subsystem maintains two indices over the Org prose:
+
+1. A neural index using vector embeddings for semantic search — the gateway to the full richness of natural language.
+2. A symbolic index storing formal assertions about what the prose says — predicates, relations, constraints — each grounded to a specific heading or block.
+
+The prose is always ground truth. Both indices are derived views that can be rebuilt from scratch. Nothing is lost in the indices that was not already in the Org files.
+
+This is what sovereignty means in technical terms: the user owns the data in a format they can access, and the system operates on the data in the same format they own. The format is stable — Org-mode has been in active development since 2003. There is no schema migration, no database upgrade, no vendor lock-in. Your notes survive the system.
+
+**The verification subsystem: the gate.**
+
+The gate is a function that takes (action, context, policy) and returns (permit | deny). Every action passes through it — a shell command from the user, a proposal from the LLM, a message from the network, a file write by a scheduled job. There is no privileged path around the gate. Root is not a concept in the gate model — root is a convention enforced by an OS that the gate replaces.
+
+The gate combines two decision layers:
+
+1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. (ACL2 is a theorem prover and programming language for formal verification. It proves that code behaves correctly for all possible inputs, not just the ones tested.)
+2. An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment.
+
+The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architecture ensures the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial.
+
+The gate does not depend on OS privilege boundaries because it is in the evaluation loop itself. This is the architectural reason for the Lisp machine: a conventional OS interposes between the gate and the hardware. A Lisp machine eliminates that interposition by making the gate part of the evaluator.
+
+**The social protocol: provable communication.**
+
+The social protocol extends the verified semantics beyond a single machine. It provides:
+
+- Self-sovereign DID identity (every instance has a cryptographic identity it controls)
+- DIDComm encrypted messaging (end-to-end encrypted, signed, DAG-tracked)
+- Personal data stores (user-owned, gate-controlled)
+- Relay network (asynchronous message delivery across trust boundaries)
+- Compute marketplace (provision verified compute you rent)
+- Liquid democracy (delegable voting over protocol governance)
+
+Every message is signed by the sender's DID, tracked in a content-addressed DAG, and optionally notarized. Communication is provable when you choose it to be — you can prove what you sent, to whom, when, without revealing content.
+
+The social protocol is not a blockchain. DAG-based ordering handles causality; delegable trust replaces proof of work.
+
+**The staged progression.**
+
+The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap describes how each successive replacement eliminates a class of threat:
+
+- Stage 0: Conventional Linux, Python agent (Hermes), SQLite knowledge store (gbrain). The starting point. Zero days exist; patches are manual.
+- Stage 1: Message-level authentication via the social protocol. Communication becomes provable.
+- Stage 2: The gate operates as a software layer over the host OS. Shell commands, LLM proposals, and network messages all pass through the same decision procedure. Root is eliminated as an attack path.
+- Stage 3: The host OS is replaced by a bare-metal Lisp image. One address space, one evaluator, no MMU to attack.
+- Stage 4: LLM inference moves into the Lisp process. No API calls across network boundaries. The LLM becomes a function in the same evaluated graph.
+- Stage 5: Neural weights stored as plist-native data structures. The gap between symbolic and neural representations closes.
+- Stage 6: Verified fine-tuning. Every weight update is gate-checked against policy.
+- Stage 7: What remains. Physical theft, electronic warfare, holes in the specification itself, and the fallibility of the LLM oracle. Limits of computation, not of this design.
+
+Each stage is independently useful. Stage 0 is running today. The migration is progressive component swap, not a cut-over.
+
+**Downstream effects.**
+
+When every action is gate-checked, every message is provable, and every computation runs on verified semantics, the security model shifts from empirical to deductive. The downstream effects cascade beyond personal computing:
+
+- **Compliance** becomes executable gate rules instead of annual audits. A SOC 2 report is a gate configuration, not a PDF.
+- **AI safety** becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails or RLHF.
+- **Software certification** becomes the accumulated regression suite of every deployed instance — the Underwriters Laboratory for AI.
+- **Operating systems** become obsolete. The gate replaces the kernel, the address space replaces process isolation, and the verified evaluator replaces the privilege model.

projects/passepartout/social-protocol/_index.org

@@ -2,7 +2,7 @@
 :CREATED:  [2026-05-24 Sun]
 :ID:       8b2c3d4e-5f6a-7b8c-9d0e-1f2a3b4c5d6e
 :END:
-#+title: Passepartout — Social Protocol
+#+title: Social Protocol
 #+filetags: :index:
 
 The Passepartout Social Protocol specification — identity, communication, contracts, and governance requirements.

projects/passepartout/strategy/_index.org

@@ -2,7 +2,7 @@
 :CREATED:  [2026-05-24 Sun]
 :ID:       9c3d4e5f-6a7b-8c9d-0e1f-2a3b4c5d6e7f
 :END:
-#+title: Passepartout — Strategy
+#+title: Strategy
 #+filetags: :index:
 
 Business strategy, competitive analysis, compliance landscape, and market positioning for the verified infrastructure category.