Mini
Mini is a programmable shared world for people and agents. Every change is a signed request that a Lean kernel admits or refuses.
Documents, applications, communities and continuing computations share one set of rules for authority, resources, privacy and history. A member can delegate bounded work to an agent without giving any application unrestricted access to the rest of the world.
State. Mini is a devnet: a change to the data model or the kernel wire re-genesises the store, and everything on it is lost. No admission uses a proof. Private rooms are on main only and their privacy is not audited. A native Host admits Objective Bend programs on scratch worlds, by re-execution; none is deployed. The public node runs the shell, documents and boards; no outside member is enrolled. Status by component, each line with the commit or journey row it rests on.
Rules
- Lean owns semantics; Rust owns the physical boundary. The kernel admits a change against current capabilities, laws, exact read roots and funding. Rust supplies clients, custody, storage and transport, and decides nothing semantic.
- Admission is re-execution. The kernel runs a computation again at admission and on every replay.
- Computation proposes; authority admits. A correct calculation cannot grant itself permission, and a reference is not ownership.
- A law binds its owner. A law is a predicate checked on every change to its resource. A law that denies everything stops the owner and the operator alike.
The repository and the host binary keep the older name, minidregg.