Update

1 files changed, 190 insertions, 1 deletions

diff --git a/README.md b/README.md
index f69f1e8..6e01b70 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,190 @@
-# kb
\ No newline at end of file
+# kb — Lean 4 Knowledge Base CLI
+
+A persistent, formally verified knowledge base stored as a Git repository of Lean 4 files. Every declaration is type-checked by Lean's kernel. An LLM agent interacts with it entirely through the `kb` CLI.
+
+---
+
+## Core Concepts
+
+- **Persistent**: stored as `.lean` files in a Git repository — survives across sessions.
+- **Formally verified**: every addition is type-checked by Lean's kernel at `kb check` / `kb commit` time.
+- **Domain-organised**: declarations are grouped into named domain files. Each domain is one `.lean` file. An agent can load a specific domain into its context without loading the entire KB.
+- **Version-controlled**: full history, branching, and reproducibility via Git.
+
+---
+
+## Planned Domain Structure
+
+The KB is organised into four top-level sections, each subdivided into domain files that correspond to a specific area of knowledge. The subsections are the natural unit an agent loads — for example, loading only `Physics` or only `MoneyFinance` without pulling in unrelated facts.
+
+### Mathematics
+
+| Domain file | Coverage |
+|-------------|----------|
+| `ElementaryMath` | Arithmetic, fractions, percentages; reasoning about parity and sign of underspecified values |
+| `Algebra` | Variables, number systems, algebraic operations and symbols |
+| `Geometry` | Plane, solid, coordinate, transformations, high-dimensional, packing, curves, polyforms, topology, tilings |
+| `Plotting` | Functions, equations, parametric plots, inequalities, number lines, polar plots |
+| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms, continuity, domain & range |
+| `DifferentialEquations` | Ordinary (ODE) and partial (PDE) differential equations |
+| `Statistics` | Descriptive statistics, inference, regression, random variables |
+| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special, number-theoretic, representation formulas |
+
+### Science & Technology
+
+| Domain file | Coverage |
+|-------------|----------|
+| `Physics` | Mechanics, oscillations & waves, statistical physics, thermodynamics, electricity & magnetism, optics, relativity, nuclear, quantum, particle, astrophysics, constants, principles, effects, fluid mechanics |
+| `Chemistry` | Matter from atoms and ions to biomolecules |
+| `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems |
+| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables, measurement devices |
+| `ComputationalSciences` | Cellular automata, substitution systems, Turing machines, complexity, algebraic codes, fractals, image processing, hashing |
+| `EarthSciences` | Geology, geodesy, oceanography, climatology |
+| `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants |
+| `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere |
+
+### Society & Culture
+
+| Domain file | Coverage |
+|-------------|----------|
+| `People` | Biographical and demographic data on notable individuals and public figures |
+| `ArtsMedia` | Music, films, comics, sculptures, paintings, and related media |
+| `History` | Timelines, monetary value analysis, historical events, inventions, conflicts |
+| `WordsLinguistics` | Word properties, languages, document length, notable texts, transliterations, Morse code, Soundex, encodings, emotions |
+| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income tax, sales tax |
+| `DatesTimes` | Dates, calendars, time systems |
+| `FoodNutrition` | Nutritional data and dietary guidelines |
+| `Demographics` | Health care, age/sex, gender equality, business, citizenship, crime, education, income & employment, language, race, marriage, mobility, religion, military, HDI |
+
+### Everyday Life
+
+| Domain file | Coverage |
+|-------------|----------|
+| `PersonalHealth` | Physical exercise, food and nutrition, child growth & development |
+| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, gasoline, food, electricity prices |
+| `Entertainment` | Music, films, artworks, cultural productions |
+| `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena |
+| `HouseholdMath` | Everyday calculations and measurements |
+| `Programming` | Algorithms, data structures, programming concepts |
+| `Hobbies` | Recreational activities and personal projects |
+| `TodaysWorld` | World economy, Finland economy, weather |
+
+---
+
+## Knowledge Representation
+
+| Kind | Description | Lean form |
+|------|-------------|-----------|
+| **Type** | A category or class | `opaque Person : Type` |
+| **Subtype** | A type extending another | `opaque Philosopher : Type` + coercion axiom |
+| **Instance** | A named individual | `opaque socrates : Person` |
+| **Property** | A function from a type to a value | `opaque birthYear : Person → Nat` |
+| **Relation** | A binary predicate | `opaque bornIn : Person → Place → Prop` |
+| **Fact** | An asserted value or relation | `axiom fact_birthYear_socrates : birthYear socrates = 470` |
+| **Rule** | A universally quantified axiom | `axiom ancestors_transitive : ∀ x y z, …` |
+| **Definition** | A named computable expression | `def yearsToDouble (r : Float) : Float := …` |
+
+---
+
+## CLI Commands
+
+### Adding knowledge  *(all require `in <Domain>`)*
+
+| Command | Description |
+|---------|-------------|
+| `add type <n> [extends <Parent>] in <D>` | Declare a type, optionally as a subtype |
+| `add instance <n> : <Type> in <D>` | Declare a named individual |
+| `add prop <n> : <DomType> -> <Range> in <D>` | Add a property |
+| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | Add a binary relation |
+| `add fact <fact> in <D>` | Assert a fact: `prop(inst) = val` or `rel(a, b)` |
+| `add rule <n> : <statement> in <D>` | Add a universally quantified axiom |
+| `add def <n> <params> : <Type> := <body> in <D>` | Define a reusable computed shortcut |
+
+Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows.
+
+### Inspecting knowledge
+
+| Command | Description |
+|---------|-------------|
+| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations, optionally filtered by domain |
+| `show def <n>` | Print the Lean source of a declaration |
+| `domains` | List all domains active this session with declaration counts |
+| `domains stats` | Detailed breakdown per domain and kind |
+
+### Querying
+
+| Command | Description |
+|---------|-------------|
+| `eval <expr>` | Evaluate a computable Lean expression via `#eval` |
+| `query <prop>` | Attempt to prove a proposition (Yes / No / Unknown) |
+
+### Build and version control
+
+| Command | Description |
+|---------|-------------|
+| `init <dir>` | Create a new KB repository |
+| `check` | Sync imports and run `lake build` to verify the whole KB |
+| `commit <message>` | Verify then `git commit` all changes |
+| `status` | Show `git status` and session summary |
+| `rm <n>` | Remove a declaration (warns about dependents) |
+
+---
+
+## How `check` Works
+
+`kb check` does three things before running `lake build`:
+
+1. Scans the KB root for all `*.lean` domain files.
+2. Inspects which domains reference names declared in other domains, and injects the necessary `import` lines.
+3. Rewrites `KnowledgeBase.lean` to import all domain files so `lake build` compiles everything.
+
+Add a batch of declarations, then run `check` once at the end rather than after each individual addition.
+
+---
+
+## Example Workflow
+
+```bash
+# Initialise
+kb init ./myKB
+cd myKB
+
+# Base types shared across domains
+kb add type Entity in People
+kb add type Person extends Entity in People
+kb add type Place extends Entity in People
+kb add type City extends Place in People
+
+# Properties and relations
+kb add prop birthYear : Person -> Nat in People
+kb add rel bornIn : Person -> Place -> Prop in People
+
+# Instances and facts
+kb add instance socrates : Person in People
+kb add instance athens : City in People
+kb add fact birthYear(socrates) = 470 in People
+kb add fact bornIn(socrates, athens) in People
+
+# Verify and commit
+kb check
+kb commit "Added Socrates and basic person/place ontology"
+
+# Agent loads only the People domain for a biographical query
+kb list all of People
+```
+
+---
+
+## Query Capabilities
+
+- **Computational**: `kb eval "yearsToDouble 0.05"` — runs `#eval` on any computable Lean expression.
+- **Logical**: `kb query "even (2 + 2)"` — attempts to prove the proposition using `decide`, `aesop`, or `simp`.
+- **Selective loading**: `kb list all of Physics` — an agent pulls only the Physics domain into its context for a focused query.
+
+---
+
+## Extensibility
+
+- Domain files from the planned structure are created on first use — no separate setup step.
+- Definitions (`kb add def`) become permanent reusable shortcuts stored in Lean files.
+- The KB grows incrementally across sessions — each `kb commit` is a checkpoint in Git history.