1 files changed, 165 insertions, 0 deletions
diff --git a/AGENT.md b/AGENT.md
new file mode 100644
index 0000000..f7bc695
--- /dev/null
+++ b/AGENT.md
@@ -0,0 +1,165 @@
+# Lean-Based Knowledge Base Agent Instructions
+
+You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` command-line tool. Every addition is type-checked by Lean's kernel, ensuring logical consistency.
+
+---
+
+## 1. Key Design Principle: Explicit Domains
+
+Every declaration belongs to a **domain** that you name explicitly using `in <Domain>`. Each domain is stored as a separate `<Domain>.lean` file in the KB root. There is no automatic classification.
+
+**Choose domains based on what you want an agent to load together.** For example:
+- `Ontology` — base types (`Entity`, `Person`, `Place`, …) that everything else depends on
+- `People` — instances, properties, and facts about specific people
+- `Geography` — instances and facts about places
+- `Finance` — financial formulas and data
+- `Physics` — physical constants and laws
+
+An agent loading only `People` facts into its context window would run: `kb list all of People`.
+
+---
+
+## 2. Session Start Protocol
+
+```bash
+# Orient yourself: see what domains and declarations exist
+kb list all
+kb domains stats
+
+# Recall declarations in a specific domain
+kb list all of Ontology
+kb list all of People
+```
+
+---
+
+## 3. Adding Knowledge
+
+Every `add` command requires `in <Domain>` at the end.
+
+| Command | Purpose | Example |
+|---------|---------|---------|
+| `kb add type <n> [extends <Parent>] in <D>` | Declare a type | `kb add type Person extends Entity in Ontology` |
+| `kb add instance <n> : <Type> in <D>` | Declare an individual | `kb add instance socrates : Person in People` |
+| `kb add prop <n> : <DomType> -> <Range> in <D>` | Declare a property | `kb add prop birthYear : Person -> Nat in People` |
+| `kb add rel <n> : <D1> -> <D2> -> Prop in <D>` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` |
+| `kb add fact <fact> in <D>` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` |
+| `kb add rule <n> : <statement> in <D>` | Add a logical rule | `kb add rule ancestors_transitive : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in Ontology` |
+| `kb add def <n> <params> : <Type> := <body> in <D>` | Define a shortcut | `kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance` |
+
+### Notes
+
+- Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows.
+- Fact syntax: `prop(inst) = value` or `rel(inst1, inst2)`.
+- Domains are created automatically when first used — no `create domain` step needed.
+- Put base types in a shared domain (e.g. `Ontology`) that other domains can depend on.
+
+---
+
+## 4. Querying the Knowledge Base
+
+| Command | Description | Example |
+|---------|-------------|---------|
+| `kb eval <expr>` | Compute a value | `kb eval "yearsToDouble 0.05"` |
+| `kb query <prop>` | Ask if a proposition is provable | `kb query "even (2 + 2)"` |
+| `kb list all of <Domain>` | List all declarations in a domain | `kb list all of People` |
+
+### Query semantics
+
+- `kb eval` runs Lean's `#eval` on the expression.
+- `kb query` attempts to prove the proposition using `decide`, `aesop`, or `simp`. Returns `Yes`, `No`, or `Unknown`.
+
+---
+
+## 5. Checking Consistency and Committing
+
+Add all facts first, then verify and commit in one step:
+
+```bash
+kb check
+kb commit "Added Socrates and basic ontology"
+```
+
+`kb check` rewrites `KnowledgeBase.lean` to import every domain file on disk, injects cross-domain imports where needed, then runs `lake build`. `kb commit` does the same before committing to Git.
+
+**Do not check after each individual fact.** Batch your additions, then check once.
+
+---
+
+## 6. Example Workflow
+
+```bash
+# Base ontology (shared types everything else depends on)
+kb add type Entity in Ontology
+kb add type Person extends Entity in Ontology
+kb add type Place extends Entity in Ontology
+kb add type City extends Place in Ontology
+
+# Domain-specific properties and relations
+kb add prop birthYear : Person -> Nat in People
+kb add rel bornIn : Person -> Place -> Prop in People
+
+# Instances
+kb add instance socrates : Person in People
+kb add instance athens : City in People
+
+# Facts
+kb add fact birthYear(socrates) = 470 in People
+kb add fact bornIn(socrates, athens) in People
+
+# Verify and commit everything at once
+kb check
+kb commit "Added Socrates and basic person/place ontology"
+```
+
+---
+
+## 7. Removing Declarations
+
+```bash
+kb rm <name>
+```
+
+The tool warns if other declarations depend on the one being removed. Remove dependents first.
+
+---
+
+## 8. Reusable Definitions
+
+```bash
+kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance
+kb eval "yearsToDouble 0.05"
+kb list defs
+kb show def yearsToDouble
+```
+
+---
+
+## 9. Best Practices
+
+- **Put base types in one domain** (e.g. `Ontology`) so all other domains can import it cleanly.
+- **Group by agent-loadable context**: a domain should contain what an agent needs for a specific task.
+- **Use meaningful domain names**: `People`, `Physics`, `Finance`, `Geography` — not `Domain1`.
+- **Prefer `def` over `axiom` for computed facts** — definitions are safer and evaluable.
+- **Run `kb check` once after a batch** of additions, not after each one.
+- **Commit with descriptive messages** so the KB history is readable.
+
+---
+
+## 10. Session End Protocol
+
+```bash
+kb commit "Session summary: what was added"
+kb list all        # Review final state
+kb domains stats   # Confirm counts are as expected
+```
+
+---
+
+## 11. Need Help?
+
+```bash
+kb help
+```
+
+Lean error messages are forwarded directly. A typical error like `unknown identifier 'Person'` means the type was declared in another domain file that hasn't been imported yet — run `kb check` to sync imports, or check that you added the base type before its dependents.