@@ -1,13 +1,13 @@
 Emergent Smalltalk: Objective Bend + governed durable objects.
-Core dynamics; surface syntax encodes these terms.
+Core dynamics, not surface syntax.
 Application associates left. \x.t binds x; t[u/x] avoids capture; new binders are fresh.
 Fields/arms are ordered lists keyed by strings; lookup takes the first match.
 Values v: \x.t, Nat, Bool, String, {fields}, spec(m,e), proto(s,t), inj(k,t).
 All components of these values are unevaluated. Scalar types are disjoint.
-Types are structural, with exact row equality; fix has (C->V->C)->V->C.
+Rows compare exactly; recursive records are nominal; fix: (C->V->C)->V->C.
 Specs may bound future Self/Super rows; fix discharges those bounds.
-Activities cannot be shared in fields/arguments/payloads. Affine/linear means
-at most once; reusable closures capture only unrestricted, shareable values.
+Activities cannot be shared in fields/arguments/payloads. Affine/linear use
+is at most once; terminal linear discharge is separate. Reusable captures are shareable/unrestricted.
 
 (\x.t) u -> t[u/x]
 mix(a,b) -> \s.\p.b s (a s p)
@@ -38,16 +38,16 @@ E[perform(p)] yields p with continuation E; response r resumes as E[r].
 A nonvalue with no step or yield is stuck; infinite reduction diverges.
 
 Every layer shares final self s; p is the whole result below it.
-Call-by-name meaning; runtime thunks are shared (call-by-need).
+Call-by-name reference; sharing requires adequacy.
 
 Host object contract:
-Object = durable id, pinned code, versioned state, law, payer.
+Object = durable id, pinned code, versioned state, law.
 A reference names an object; it does not grant access. Reads and writes require
 current authority. Grants face current law; law revision is not revocation.
 A method runs pinned code on typed inputs and a current state view. Its result
 proposes effects. Commit a turn atomically only if its exact read roots still
-match, current authority/laws admit every write, and its budget is funded.
-Failed turns commit no application writes; fees may apply. No owner bypass.
+match and current authority/laws admit every write. No owner bypass.
+Failed turns commit no application writes. Funding/fees belong to the host profile.
 Delegation is explicit, scoped to callee, method, code and arguments.
 Synchronous call trees commit together. Sends enqueue durable messages and
 return answer slots; delivery is a later turn. A slot has one decider, deadline,
 
@@ -0,0 +1,111 @@
+# Emergent Smalltalk capsules
+
+Three presentations at each strict decimal budget: fewer than 1,000, 2,000 or
+3,000 UTF-8 bytes, including the title, whitespace and scope statement. All are
+ASCII. These are alternative descriptions of the same source semantics, not
+language variants. Automatafl is a separate package.
+
+| Presentation | <1 KB | <2 KB | <3 KB |
+| --- | --- | --- | --- |
+| Rewrite relation and evaluation contexts | [rewrite-1k.txt](rewrite-1k.txt) | [rewrite-2k.txt](rewrite-2k.txt) | [rewrite-3k.txt](rewrite-3k.txt) |
+| Transition algebra | [algebra-1k.txt](algebra-1k.txt) | [algebra-2k.txt](algebra-2k.txt) | [algebra-3k.txt](algebra-3k.txt) |
+| Resumable evaluator pseudocode | [machine-1k.txt](machine-1k.txt) | [machine-2k.txt](machine-2k.txt) | [machine-3k.txt](machine-3k.txt) |
+
+The byte counts and SHA-256 hashes are in [manifest.json](manifest.json).
+Run `bun docs/objective-bend/capsules/check.ts` from the repository root to
+check the exact published files and budgets.
+
+The 1 KB files explicitly describe a projection: open recursion, lazy records,
+effects and the governed object boundary. They omit other constructors and
+protocol detail. The 2 KB files cover the complete reference core dynamics,
+including primitive edge cases, demand order, raw yields and resumption, with
+a small object contract. The 3 KB files add typing constraints and durable
+interaction rules. Their typing accounts have different emphases; none is a
+complete checker, admission algorithm, source grammar or wire specification.
+Budget is not a claim of completeness beyond each file's stated scope.
+
+Start with the rewrite 3 KB capsule for the common agent contract. The machine
+2 KB capsule is the most direct implementation prompt. Algebra is useful for
+factoring demand rules and host admission into explicit mathematical relations.
+These preferences are editorial judgments, not results of a blind reconstruction
+test. The three authors consulted the implementation. The pseudocode has not
+been run as an interpreter, and prose inspection is not an equivalence proof.
+
+## Why payer is outside the object tuple
+
+The abstract object is `(id, code pin, versioned state, law)`; invocation adds
+an authenticated principal and authority. Host policy supplies execution and
+retention resources. The tuple is a semantic projection, not Mini's serialized
+record layout. Eliding storage accounting does not erase resource admission.
+
+Mini's [ObjectRecord](../../../Kernel/ObjectRecord.lean) stores a Book account
+that funds the record and state cell. `admitWrite_payer_irrelevant` and
+`judge_payer_irrelevant` prove that changing that field does not change the
+corresponding write judgment. This supports omitting it from the common object
+description. It does not prove that changing funding preserves retention,
+execution availability or every observable host behavior.
+
+The activity [escrow](../../../Kernel/ObjectiveActivity.lean) also has a field
+called `payer`, but that one is a `SubjectId` used as the activity principal in
+`factsOf`. The authenticated principal must remain. A Mini adapter still must
+populate all required accounts, signatures, reserves and principal fields;
+these capsules do not change that implementation.
+
+## A small multi-language repository
+
+A standalone conformance repository is a good destination. Keep one normative
+Lean semantics, independent implementations, a common corpus and named host
+profiles. Initially pin the relevant Mini source rather than fork its semantic
+authority. A proposed layout is:
+
+```text
+capsules/          these compact contracts and exact byte manifests
+spec/              pinned Lean terms, reductions, yields, observations
+impl/python/       small transparent reference interpreter
+impl/c/            independent evaluator or imported existing backend
+conformance/       canonical AST, scripts of replies, fixtures, shrinking
+profiles/mini/     authority, durability, resource and transport binding
+examples/automatafl/ two-player game package, separate from language
+```
+
+This is a proposed extraction, not a newly published repository. Mini already
+contains [a Lean C emitter](../../../Compiler/ObjectiveBendEmitC.lean),
+[a C demand machine](../../../native/objective-emit/runtime.c), and
+[a Python differential harness](../../../native/objective-emit/differential.py).
+The Python harness is not a Python language implementation. The C runtime is
+derived from the demand machine design and depends on Lean-generated ROM; it
+is useful existing work, not a blind independent reading of a capsule. Its
+emitter explicitly records that C refinement is not proved. No C qualification
+was rerun for this documentation experiment.
+
+Use a canonical core AST first, so parser differences do not mask evaluator
+differences. Compare ground observations, stuck outcomes, yielded plans and
+resumed traces. Probe lazy records/closures by elimination rather than comparing
+their implementation representations. Separate finite fuel exhaustion from
+semantic divergence. Independent evaluators need not take the same number of
+steps; the existing C backend's stricter state/tick comparison remains useful
+for its particular claim of matching the Lean demand machine.
+
+The next useful small swarm is a blind reconstruction experiment: one fresh
+agent per capsule, with only that capsule and a common AST/protocol interface,
+builds an interpreter. Score held-out behavioral cases and missing-rule reports,
+not just successful parses. Count the shared interface separately: it must not
+silently supply semantics omitted from the capsule. Include unused divergence,
+duplicate fields, strict AND, a wrong-typed left primitive operand followed by
+a yielding right operand, inherited methods seeing overridden self, and
+resumption under nested contexts. Test host profiles separately with stale
+roots, current law changes, duplicate resume and an unknown commit outcome.
+
+The aim is the smallest contract from which independent agents reconstruct the
+same behavior. Byte golfing is only one part of that measurement.
+
+## Source anchors
+
+- [Core terms, values, Step, Yields](../../../Theory/ObjectiveBendOpenRecursion.lean)
+- [Types and usage safety](../../../Theory/ObjectiveBendTypes.lean)
+- [Modular typing](../MODULAR-TYPING.md)
+- [Durable interaction contract](../../OBJECTIVE-BEND-EVENTS.md)
+- [Two-player Automatafl comparison](../../../world/automatafl/README.md)
+
+The original [capsule](../EMERGENT-SMALLTALK.txt) remains as a prose-oriented
+presentation; it now separates funding and fixes the typing/sharing shorthand.
@@ -0,0 +1,18 @@
+Emergent Smalltalk / algebra kernel (partial profile).
+Scope: open recursion + governed objects; omits scalars, sums, reflection,
+typing, concrete syntax/wire and resource tariffs.
+Terms: x,\x.t,t u,mix(a,b),fix(e,p),{fs},t.k,extend(t,fs),done(t),perform(t).
+V=\x.t|{fs}; fields are unevaluated ordered string-key lists; first key wins.
+Capture-free substitution; fresh s,p; application left-associates.
+(\x.t)u -> t[u/x]
+mix(a,b) -> \s.\p.b s (a s p)
+fix(e,p) -> e (fix(e,p)) p
+{fs}.k -> fs[k]
+extend({fs},gs) -> {gs++filter(key notin keys(gs),fs)}
+done(t) -> t
+Close -> ONLY under E=[]|E t|E.k|extend(E,fs).
+E[perform(p)] yields (p,E); reply r resumes E[r]. Stuck != divergence.
+Object=(id,code pin,versioned state,law); ref != authority.
+A turn proposes writes; commit atomically iff exact read roots and current
+laws/authority and budget admit; otherwise no app writes. Calls co-commit; sends defer.
+Sponsorship/budget is host context, not object identity. No owner bypass.
@@ -0,0 +1,39 @@
+Emergent Smalltalk / transition algebra.
+Scope: core dynamics + host skeleton; not typing, surface/wire syntax or tariffs.
+Application associates left; \x.t binds x; substitution avoids capture.
+fs/arms: ordered string-key lists, first match wins. N,B,S: disjoint Nat,
+Bool,String. Values v=\x.t|N|B|S|{fs}|spec(m,e)|proto(s,t)|inj(k,t);
+value components stay unevaluated. Fresh binders below.
+(\x.t)u -> t[u/x]
+mix(a,b) -> \s.\p.b s (a s p)
+fix(e,p) -> e (fix(e,p)) p
+spec(m,e)u -> e u
+reflect(proto(s,t)) -> s
+metadata(spec(m,e)) -> m
+target(proto(s,t)) -> t
+{fs}.k -> fs[k]
+extend({fs},gs) -> {gs++filter(key notin keys(gs),fs)}
+if(true,a,b) -> a; if(false,a,b) -> b
+natcase(0,z,x.b) -> z; natcase(n+1,z,x.b) -> b[n/x]
+case(inj(k,t),arms) -> b[t/x] if arms[k]=x.b
+done(t) -> t
+op(v,w) -> scalar result iff correctly typed:
+Nat +,*,-,/,%,=,<,<=; unbounded; -=truncated subtraction;
+/=floor; n/0=0; n%0=n. Bool AND (strict). String equality.
+-> is closed ONLY under
+E=[]|E t|E.k|extend(E,fs)|op(E,t)|op(v,E)|if(E,t,u)
+ |natcase(E,z,x.b)|case(E,arms)|reflect(E)|metadata(E)|target(E).
+E[perform(p)] yields (p,E); response r resumes E[r].
+No step/yield/value=stuck; infinite ->=divergence. Pure -> has no effects.
+Every layer sees identical final self; super is the whole lower result.
+
+Host: O=(id,code pin,versioned state,law). Ref != authority.
+Invoke pinned code on typed args/current view; effects propose a turn.
+Commit atomically iff exact read roots still match, every write passes current
+law/authority and host budget admits. Failure: no app writes; fees may apply.
+Sponsorship is host context, not object identity or authenticated principal.
+Calls co-commit; sends queue durable later turns with slots.
+Grants face current law; revision != revocation. No owner bypass.
+Slot=(one decider,deadline,one terminal outcome). Resume consumes a generation.
+No reply != failure: query receipt/retry SAME signed attempt. New identity
+may repeat effects. Private state requires protected reads.
@@ -0,0 +1,55 @@
+Emergent Smalltalk / demand-admission algebra.
+Scope: dynamics + typing/host sketch; not full checker/parser/wire/tariff.
+Object tuple abstracts kernel layout.
+Application left-associates; binders fresh; substitution capture-free.
+fs/arms: ordered string-key lists, first match wins. N,B,S: disjoint Nat,
+Bool,String. Values v=\x.t|N|B|S|{fs}|spec(m,e)|proto(s,t)|inj(k,t);
+Value components are unevaluated.
+(\x.t)u -> t[u/x]
+mix(a,b) -> \s.\p.b s (a s p)
+fix(e,p) -> e (fix(e,p)) p
+spec(m,e)u -> e u
+reflect(proto(s,t)) -> s
+metadata(spec(m,e)) -> m
+target(proto(s,t)) -> t
+{fs}.k -> fs[k]
+extend({fs},gs) -> {gs++filter(key notin keys(gs),fs)}
+if(true,a,b) -> a; if(false,a,b) -> b
+natcase(0,z,x.b) -> z; natcase(n+1,z,x.b) -> b[n/x]
+case(inj(k,t),arms) -> b[t/x] if arms[k]=x.b
+done(t) -> t
+op(v,w) -> scalar result iff correctly typed:
+Nat +,*,-,/,%,=,<,<=; unbounded; -=truncated subtraction;
+/=floor; n/0=0; n%0=n. Bool AND (strict). String equality.
+-> gives head contractions, NOT contextual equality.
+Demand D selects argument 1 of app,get,extend,if,natcase,case,reflect,metadata,
+target; op demands 1 if arg1 is not a value, else 2; absent otherwise.
+Only demanded child steps propagate; E nests demand positions.
+E[perform(p)] yields (p,E); response r resumes E[r].
+No step/yield/value=stuck; infinite ->=divergence. Pure -> has no effects.
+All layers share final self; super=whole lower result.
+
+Host: O=(id,code pin,versioned state,law). Ref != authority.
+Invoke pinned code on typed args/current view; effects propose a turn.
+admit(t,W)=rootsMatch(t)&funded(t)&domains(W)&all(w in W,
+ typed(w)&writerPin(w)&packageCreatorLawsNow(w)&authorityNow(w)).
+Commit iff admit: atomic app writes W, otherwise none; host fees may survive.
+Sponsorship is host context, separate from object identity and principal.
+Calls co-commit; sends queue durable later turns with answer slots.
+Grants face current law; revision != revocation. No owner bypass.
+Delegation is explicit and scoped to callee, method, code pin, arguments,
+uses/caps; callee law still applies. Nested frames inherit no principal
+merely by naming a reference.
+Slot=(one decider,deadline,one outcome: reply/refused/unknown/broken/expired). Resume consumes a generation.
+No reply != failure: query receipt; retry SAME signed attempt. New id may
+repeat effects. Private state requires protected reads.
+
+Typing sketch: exact canonical rows; supports=width bounds; recursive records
+nominal. Closed fix:(C->V->C)->V->C. Open L=(Self bound B,Super bound C,
+output F); bounds rigid at declaration. Chain L1..Ln: choose final T, seed I0;
+sigma[k]={Self=T,Super=I[k-1]}; require T supports Bk[sigma[k]], I[k-1]
+supports Ck[sigma[k]]; I[k]=Fk[sigma[k]]; I[n]=T. Instantiate, then check
+whole closed output. Affine/linear safety uses <=1; reusable closures capture only
+unrestricted shareable values. No activities in shared fields/args/payloads.
+Exhaustion != success. -> is weak-head call-by-name; sharing requires
+representation adequacy.
@@ -0,0 +1,25 @@
+import {readFileSync, readdirSync} from "node:fs";
+import {createHash} from "node:crypto";
+import {dirname, join} from "node:path";
+import {fileURLToPath} from "node:url";
+
+const here = dirname(fileURLToPath(import.meta.url));
+const manifest = JSON.parse(readFileSync(join(here, "manifest.json"), "utf8"));
+const expected = ["algebra", "machine", "rewrite"].flatMap(style =>
+  [1, 2, 3].map(size => `${style}-${size}k.txt`)).sort();
+const actual = readdirSync(here).filter(name => name.endsWith(".txt")).sort();
+if (JSON.stringify(actual) !== JSON.stringify(expected) ||
+    JSON.stringify(Object.keys(manifest.capsules).sort()) !== JSON.stringify(expected))
+  throw Error("Expected exactly three capsule families at three budgets");
+for (const name of expected) {
+  const bytes = readFileSync(join(here, name));
+  const limit = Number(name.match(/-([123])k\.txt$/)![1]) * 1000;
+  const recorded = manifest.capsules[name];
+  const sha256 = createHash("sha256").update(bytes).digest("hex");
+  if (bytes.length >= limit || bytes.some(byte => byte > 127) ||
+      bytes.length !== recorded.bytes || limit !== recorded.exclusiveLimit ||
+      sha256 !== recorded.sha256)
+    throw Error(`${name}: byte budget, ASCII or manifest mismatch`);
+  console.log(`${name}: ${bytes.length} < ${limit} bytes; hash matches`);
+}
+console.log("Byte/identity checks only; semantic equivalence is not established here.");
@@ -0,0 +1,16 @@
+OBJECTIVE BEND: coroutine sketch, not runnable code; core projection.
+W(t) returns weak-head values; all calls propagate yields, saving their stack.
+Substitution t[u/x] avoids capture; binders fresh; application left-associative.
+W(\x.t)=\x.t; W({fs})={fs}; scalar literals return themselves.
+W(f a): f=W(f); if f=\x.t return W(t[a/x]); else stuck.
+W(mix(a,b))=\s.\p.b s (a s p)
+W(fix(e,p))=W(e (fix(e,p)) p)
+W(t.k)=W(first(W(t),k))
+W(extend(t,gs))={gs++[f in W(t).fields | key(f) not in keys(gs)]}
+W(done(t))=W(t); W(perform(p))=W(yield(p))
+Records are ordered string-keyed lists. Missing/wrong shapes: stuck.
+One final self; super is the lower computation. Nothing else is forced. W may diverge.
+Host object=(id,code-pin,versioned-state,law). References confer no authority.
+Commit effects atomically iff read roots match and current law/authority admit.
+Sponsorship is host policy. Pure evaluation grants nothing.
+Omitted: other constructors/primitives, typing, messaging, wire, metering.
@@ -0,0 +1,32 @@
+OBJECTIVE BEND: coroutine pseudocode, not a tested interpreter.
+W(t) returns weak-head values. Nested calls propagate yields, retaining stack;
+yield(p) hands raw p to host; a supplied response becomes its return value.
+Capture-avoiding t[u/x]; fresh binders; left-associated application.
+Values: \x.t, Nat, Bool, String, {fs}, spec(m,e), proto(s,t), inj(k,t).
+W(v)=v: constructor children stay unevaluated; scalar types are disjoint.
+W(f a): match W(f): \x.t=>W(t[a/x]); spec(m,e)=>W(e a)
+W(mix(a,b))=\s.\p.b s (a s p)
+W(fix(e,p))=W(e (fix(e,p)) p)
+W(reflect(t)): proto(s,u)=W(t); return W(s)
+W(metadata(t)): spec(m,e)=W(t); return W(m)
+W(target(t)): proto(s,u)=W(t); return W(u)
+W(t.k): {fs}=W(t); return W(first(fs,k))
+W(extend(t,gs)): {fs}=W(t); return {gs++[f in fs | key(f) not in keys(gs)]}
+W(if(c,a,b)): match W(c): true=>W(a); false=>W(b)
+W(natcase(c,z,x.b)): match W(c): 0=>W(z); n+1=>W(b[n/x])
+W(case(c,arms)): inj(k,u)=W(c); x.b=first(arms,k); return W(b[u/x])
+W(done(t))=W(t); W(perform(p))=W(yield(p))
+W(op(a,b)): v=W(a); w=W(b); return primitive(op,v,w)
+Nat: +,*,-,/,%,=,<,<=; unbounded; subtraction saturates; floor division;
+n/0=0; n%0=n. Bool: strict AND. String: equality. Other operands: stuck.
+Fields/arms: ordered string-keyed lists; first match wins. Every missing
+case/field or shape mismatch is stuck. Infinite recursion diverges.
+Every layer shares final self s; p is the whole lower computation.
+Host: object=(id,code-pin,versioned-state,law). Reference != authority.
+An authenticated turn evaluates pinned code; effects commit atomically only
+if exact read roots match and current law/authority admit all writes.
+Pure computation grants no effects. Failed turns make no application writes.
+Sponsorship is host policy; caller principal remains semantically relevant.
+Sends return durable answer slots; delivery is a later turn. An absent reply
+is unknown: query the receipt and retry the identical request identity.
+Omitted: typing, full async protocol, wire, tariffs.