docs: replace template README and fix EXPLAINME {project-name} placeholder

README now describes nesy-solver: public proof playground at nesy-solver.dev,
multi-formalism support (SMT-LIB, Lean 4, Coq/Rocq, Idris2, Agda), and the
Hypatia+Echidna+VeriSim architecture. EXPLAINME title placeholder fixed.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

EXPLAINME.adoc

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
-= {project-name} — Show Me The Receipts
+= nesy-solver — Show Me The Receipts
 :toc:
 :icons: font
 

README.adoc

@@ -1,175 +1,48 @@
-= RSR Template Repository
-:toc: preamble
-:icons: font
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= nesy-solver
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:toc:
+:toc-placement: preamble
 
-image:https://www.bestpractices.dev/projects/TBD/badge[OpenSSF Best Practices, link="https://www.bestpractices.dev/projects/TBD"]
-image:https://api.securityscorecards.dev/projects/github.com/hyperpolymath/nesy-solver/badge[OpenSSF Scorecard, link="https://securityscorecards.dev/viewer/?uri=github.com/hyperpolymath/nesy-solver"]
-
-[TIP]
-====
-**AI-Assisted Install:** Just tell any AI assistant: +
-`Set up Nesy Solver from https://github.com/hyperpolymath/nesy-solver` +
-The AI reads the manifest, asks you a few questions, and handles everything.
-====
+Public proof playground at link:https://nesy-solver.dev[nesy-solver.dev] — submit
+proof obligations, get prover recommendations, stream verdicts back live.
 
 == Overview
 
-**The canonical template for RSR (Rhodium Standard Repository) projects.**
-
-This project follows a **Dual-Track** architecture:
-* **Root:** High-level orientation and rich documentation for humans.
-* **Sub-directories:** Machine-readable metadata and technical implementation.
-
-== ABI/FFI Standard (Verified Interface Seams)
+`nesy-solver` is the interactive frontend for the hyperpolymath neurosymbolic
+learning loop. It connects users directly to the Hypatia + Echidna + VeriSim
+pipeline:
 
-All projects with foreign function interfaces MUST follow this consolidated standard:
+1. Submit a proof obligation in SMT-LIB, Lean 4, Coq/Rocq, Idris2, or Agda
+2. The app recommends a prover strategy based on live `proof_attempts` data
+   in VeriSim
+3. Dispatches to Echidna for execution
+4. Streams the verdict back in real time
+5. Records the attempt in `verisim-api` — the playground improves its
+   recommendations over time from actual usage data
 
-* **ABI (Idris2):** `src/interface/abi/*.idr` (The Specification)
-* **FFI (Zig):** `src/interface/ffi/src/*.zig` (The Implementation)
-* **Generated:** `src/interface/generated/*.h` (The Artifacts)
+== Supported Formalisms
 
-This unification ensures that the "Truth," the "Bridge," and the "Result" are managed as a single architectural unit.
+* SMT-LIB (Z3, CVC5)
+* Lean 4
+* Coq / Rocq
+* Idris2
+* Agda
 
-== AI Gatekeeper Protocol
-
-All projects MUST include a root `0-AI-MANIFEST.a2ml`. This is the mandatory entry point for all AI agents. It prevents duplicate file errors and preserves architectural invariants across sessions.
-
-== Repository Structure
+== Architecture
 
 [cols="1,3"]
 |===
-|Directory |Purpose
-
-|`.github/`
-|Forge-specific metadata (CODEOWNERS, SECURITY.md, workflows).
-
-|`.machine_readable/`
-|Canonical project state (6 a2ml files), bot directives, and AI guides.
-
-|`container/`
-|Stapeln container ecosystem (selur-compose, vordr, rokur).
-
-|`docs/`
-|Technical documentation sorted by tracks (Theory, Practice, Architecture).
-
-|`docs/legal/`
-|Consolidated legal exhibits and full license texts.
-
-|`src/interface/`
-|Unified ABI/FFI/Generated interface unit.
+| Component | Role
+
+| `web/` | Frontend (ReScript + Deno)
+| `src/core/` | Proof dispatch and strategy selection
+| `src/interface/abi/` | Idris2 ABI for prover interface contracts
+| `src/interface/ffi/` | Zig FFI bridge to Echidna + external provers
+| `deploy/` | Container deployment (Containerfile, Podman)
+| `verisim-api` | External: records proof attempts, drives strategy recommendations
 |===
 
-== Container Ecosystem (Stapeln)
-
-This template includes a complete `container/` directory for the **Stapeln Six** tools:
-1. **selur** (Orchestration)
-2. **cerro-torre** (Verified Packaging)
-3. **svalinn** (Edge Gateway)
-4. **vordr** (Monitoring)
-5. **rokur** (Secrets)
-6. **k9-svc** (Deployment Contracts)
-
-== Quick Start
-
-[source,bash]
-----
-just init              # Interactive bootstrap
-just build             # Unified build
-just test              # Unified test
-just container-build   # Build verified OCI image
-----
-
-== Contractile System
-
-This template includes five **contractile files** in `.machine_readable/contractiles/` that make your repository's rules executable:
-
-[cols="1,2,3"]
-|===
-| Tool | File | Purpose
-
-| `must check`
-| `Mustfile.a2ml`
-| Physical state invariants (files exist, code compiles, no secrets)
-
-| `trust verify`
-| `Trustfile.a2ml`
-| Integrity verification (hashes valid, signatures correct, provenance traceable)
-
-| `dust status`
-| `Dustfile.a2ml`
-| Cleanup tasks (stale files, build artifacts, expired tokens)
-
-| `intend list`
-| `Intentfile.a2ml`
-| Design intent and roadmap tracking
-
-| `k9 eval`
-| `*.k9.ncl`
-| Nickel-based deployment validation
-|===
-
-=== Installation
-
-[source,bash]
-----
-cargo install contractile
-
-# Create symlinks for individual commands
-for cmd in must trust dust intend k9; do
-  ln -sf $(which contractile) ~/.local/bin/$cmd
-done
-----
-
-=== Usage
-
-[source,bash]
-----
-# Symlink contractiles to project root (CLI searches ./contractiles/)
-ln -sf .machine_readable/contractiles contractiles
-
-# Run checks
-must check           # Verify physical state (23 checks in typical RSR project)
-trust verify         # Verify integrity and provenance
-dust status          # Show cleanup items
-intend list          # Show design intents and roadmap
-
-# Generate Just recipes from contractile files
-contractile gen-just # Creates contractile.just (already imported by Justfile)
-
-# Then use via Just:
-just must-check
-just trust-verify
-----
-
-=== Writing Checks
-
-Contractile files use A2ML format — simple, line-oriented:
-
-[source]
-----
-### check-name
-- description: Human-readable description
-- run: shell command (exit 0 = pass, non-zero = fail)
-- severity: critical | warning | info
-----
-
-See link:https://github.com/hyperpolymath/contractiles[contractiles documentation] for the full specification.
-
-== Wondering How This Works?
-
-If you're curious about the tech behind the claims in this README, see
-link:EXPLAINME.adoc[EXPLAINME.adoc] — feature highlights with code paths
-and honest caveats. Questions welcome via issues or direct contact.
-
-== Documentation
-
-* link:EXPLAINME.adoc[Show Me The Receipts] — how headline features work
-* link:CONTRIBUTING.adoc[Contributing Guide]
-* link:GOVERNANCE.adoc[Governance Model]
-* link:docs/attribution/MAINTAINERS.adoc[Maintainers & Citations]
-* link:SECURITY.adoc[Security Policy]
-
 == License
 
-SPDX-License-Identifier: PMPL-1.0-or-later
-See link:LICENSE[LICENSE] and link:docs/legal/[docs/legal/] for details.
+PMPL-1.0-or-later. See link:LICENSE[LICENSE].