| name | distill |
| description | Distill a session-tethered working context into a self-contained portable handoff a fresh zero-memory agent can execute from. Closes deictic, grounding, relevance, provenance, and compression gaps, then emits a prose channel plus a schema-versioned TaskStateBlock. Type: (ContextTethered, AI, DISTILL, WorkingContext) → PortableHandoff. Alias: Diylisis(διύλισις). |
Diylisis Protocol
Distill a session-tethered working context into a self-contained portable handoff through deictic, grounding, relevance, provenance, and compression closure, resolving context-tethered residue into a handoff a fresh zero-memory agent can execute from. Type: (ContextTethered, AI, DISTILL, WorkingContext) → PortableHandoff.
Definition
Diylisis (διύλισις: refining, distillation): A dialogical act of distilling a session-tethered working context — the accumulated context window of one working session, carrying undefined jargon, metric tokens, author process traces, tool state, and dangling task identifiers — into a self-contained portable handoff that a fresh recipient with no access to the author session can execute from. The protocol's lexical verb is /distill. The author session declares a handoff contract, normalizes each session-local pointer (deixis) to a canonical reference, audits each item for self-containment, judges each item's recipient-relevance and transformation-provenance, compresses to the minimal-complete set, gates the result against a zero-memory comprehension standard, loops until the hygiene measure reaches its fixed point, and emits the handoff across a prose channel and a schema-versioned task-state channel.
── FLOW ──
Diylisis(W, recipient?, next_task?, activation_verb?) → Detect(W) → tethered? →
¬tethered: → deactivate (handoff already self-contained)
tethered: pass_n=1, now = invocation timestamp (immutable per invocation), residuals = ∅, loop:
F0 declare(recipient, next_task, allowed_sources, scope, verification, stop, handoff_durability, emit_target) → contract -- relevance + minimality premise; handoff_durability conditionalizes the ledger (Change A); Λ.activation_edge = { activation_verb? (default minimal), locator: ref contract.emit_target } is constructed here — the F5 fourth input exists from Phase 0
ledger = read(CorrectionDelta) | unknown if contract.handoff_durability = DurableRepo else unknown -- conditional ledger: maintained only for the durable re-distilled case; OneShot/ExternalVersioned keep none
guard ¬competence_substitution(contract, Null, Null) -- F0 competence-substitution guard (Rule 27): a judgment-bearing next task must either leave method to the recipient or name a verified operative artifact; a trip Stops — surface the misfit witness + a proposed recipient-owned-method re-declaration, re-declare before Phase 1 (the witness question may be discharged by a /gap run on the handoff decision before F0)
F1 scan(deixis) → normalize(surface_token → canonical_ref, confidence, unresolved?) → SubstTable
|unresolved tokens| > 0: append to residuals (reason: unresolved)
F2 audit(item, self_containment) → classify(inline | stable-pointer | routed-residual) -- no silent residual; a stable-pointer's locator must resolve throughout the recipient's activation window (session-scoped roots fail for an absent recipient → inline or relocate)
F3a relevance(item, contract.next_task) → keep_candidate? -- F0 contract predicate
F3b provenance(item, ledger, handoff_durability) → Provenance →
effective KEEP delta(status≠provisional, ¬expired) [DurableRepo]: → CorrectedKeep → KEEP -- corrected/disputed/stale/user-constituted claim, held by the ledger
no delta ∧ durable observable source + support-integrity: → ObservedKeep → KEEP -- common-case relay (Change B): ordinary source-backed state KEPT directly, no ledger, no Gate
else (expired ∨ provisional-only ∨ non-KEEP delta; OR no delta ∧ no observable basis): → Unknown → Constitution(ASK) -- KEEP hard line: no KEEP without a matching unexpired KEEP delta OR a durable observable basis
F3 disposition(item) ← Disposition: KEEP(inline) | ROUTE(StableRef) | DROP -- KEEP from CorrectedKeep ∨ ObservedKeep; ROUTE/DROP from F3a relevance or the Gate; Unknown ∨ conflict → Gate
F4 compress(kept) → minimal_complete -- remove only if no contract/residual violation
F5 comprehension_gate(minimal_complete, contract, watchlist, activation_edge) → zero_memory_verdict → -- refute-posture fresh subagent (named zero-memory-refuter, or generic fresh subagent carrying the F5 instructions), lint-checklist last resort; no self-simulation; watchlist enumerated at dispatch (Λ.watchlist). activation_edge = the activation edge (verb + locator) reviewed WITH the candidate, verified under the minimal admissible edge — passing under the weakest activation implies passing under any richer one, so a richer actual edge never licenses a weaker document. Prose-only deletion test (Change C): with TaskStateBlock + correction ledger + native task-state + every agent-specific affordance all ignored, the next task MUST still execute from prose_channel + allowed_sources ALONE, else Fail
[backstop, after Findings typed into EvidencedFindings, before residual insert] competence_substitution(contract, minimal_complete, zero_memory_verdict) — a behavior-repair finding on authored operative procedure (Rule 27) is contract-misfit evidence, NOT a comprehension gap: do not append it as a residual, do not run another procedure-repair pass; Stop — surface the witness + a proposed recipient-owned-method contract, terminate this /distill invocation without emit and hand the proposed contract to the caller for a FRESH invocation (no in-loop restart: the loop coproduct J gains no re-declaration arm, so the fixed-point argument stays scoped to one invocation; the fresh invocation's F0 re-runs F3a relevance under the re-declared next_task)
Fail(blocking_items, sweep, realization): parse each verdict Findings row → EvidencedFinding, append to residuals (reason: comprehension-gap, evidence kept), block fixed_point
Pass(sweep, realization): no new residual (sweep absent → no verdict, re-dispatch)
gate_domain = disposition conflicts ∪ unknown-provenance ∪ horizon-expired ∪ unresolved residuals
[gate_domain ≠ ∅] Gate Qd(gate_domain) → Stop → A -- Constitution surfacing (both verdicts; residuals incl. comprehension-gap)
[gate_domain = ∅] A := None (identity — clean pass: every item uncontestedly disposed — KEEP via CorrectedKeep/ObservedKeep, or ROUTE/DROP via F3a — no unresolved residual, F5 Pass with no findings)
F6 loop: measure(unresolved anchors, stop, schema, residual, leaked drops, unclean deltas, undisposed authored) → fixed_point? -- leak lint: DROP'd content absent from emit, incl. emit-ledger deltas under re-distillation (minimality dual of F5)
¬fixed_point: pass_n += 1, loop (one-pass + bounded audit/lint)
fixed_point: → F7
F7 emit(prose_channel, activation_edge, TaskStateBlock, correction_ledger?) → PortableHandoff → converge -- leak_free across every emitted channel incl. the activation edge and the correction ledger; the emitted activation edge is the content-free verb+locator that hands the artifact to its recipient; re-distillation hygienes the single canonical handoff in place + appends a CorrectionDelta line, never a supersede-chain file
── MORPHISM ──
WorkingContext, recipient?, next_task?, activation_verb?
→ declare(recipient, next_task, allowed_sources, scope, verification, stop, handoff_durability, emit_target) -- F0 HandoffContract; relevance and minimality undefined without it; handoff_durability conditionalizes the CorrectionDelta ledger (OneShot/ExternalVersioned keep none, DurableRepo keeps the full ledger); Λ.activation_edge = { activation_verb? (default minimal), locator: ref contract.emit_target } is constructed here — the F5 fourth input exists from Phase 0; guarded by ¬competence_substitution (Rule 27)
→ normalize(surface_token, canonical_ref, confidence) -- F1 deictic closure: precedes grounding so each grounded item names a stable referent
→ audit(item, self_containment) → (inline | stable-pointer | routed-residual)-- F2 grounding closure: silent residual surfaced, never dropped unseen; a stable-pointer's locator must resolve throughout the recipient's activation window (session-scoped roots fail for an absent recipient — inline the evidence or relocate to a resolving locator)
→ select(item, contract.next_task) -- F3a recipient-relevance predicate against the declared contract
→ attest(item, ledger, handoff_durability) → Provenance -- F3b read-only provenance; a matching non-provisional unexpired KEEP delta (DurableRepo) yields CorrectedKeep, a durable observable source with support-integrity and no delta yields ObservedKeep (KEPT directly, no Gate), every remaining state yields Unknown; provenance authority is the KEEP hard line only, never an inferred disposition
→ dispose(item) → Disposition -- F3 KEEP(inline) | ROUTE(StableRef) | DROP
→ compress(kept) → minimal_complete -- F4 remove only what leaves no contract or residual-ledger violation
→ gate(minimal_complete, contract, watchlist, activation_edge) → zero_memory_verdict -- F5 refute-posture comprehension against a fresh recipient standard; watchlist enumerated at dispatch; the activation edge (verb + locator) is a fourth input, verified under the minimal admissible edge; Fail re-enters blocking items as residuals, no author self-simulation; a handoff not executable from prose_channel + allowed_sources alone (task-state/ledger/native-state/affordances ignored) is a Fail (prose-only deletion test, Change C); a competence-substitution backstop trip (Rule 27 — a candidate embedding unverified authored operative procedure, or a behavior-repair finding on one) terminates the invocation instead — contract re-declaration, never a residual
→ settle(measure) → fixed_point -- F6 bounded audit/lint loop on the hygiene measure; fixed_point requires a Pass verdict ∧ leak_free (no DROP'd content in emit)
→ emit(prose_channel, activation_edge, TaskStateBlock, correction_ledger?) -- F7 channel separation across three channels; the prose channel carries authority, the task-state channel rehydrates and never overrides it, the activation edge initiates and carries no content (Rule 11); under re-distillation (a prior canonical handoff for the contract exists) the emit hygienes that one file in place and appends each correction as a CorrectionDelta ledger line, never a versioned sibling
→ PortableHandoff
requires: context_tethered(W) -- runtime checkpoint (Phase 0)
deficit: ContextTethered -- activation precondition (Layer 1/2)
preserves: source_chain(W) -- W.items read-only; substitution, disposition, and provenance annotate, never mutate the originating context
invariant: Portability over Author Familiarity ∧ Single Canonical Handoff -- one continuously-hygiene'd handoff file; re-distillation edits it in place + appends to the CorrectionDelta ledger, never a supersede-chain (v1→v2) file
── TYPES ──
W = WorkingContext { items: List(ContextItem), session_ref: SessionRef, action: Handoff }
ContextItem = { content: String, origin: Origin, surface_tokens: Set(String), downstream: List(TaskRef) }
Origin ∈ {UserStatement, DocumentRead, ToolOutput, AIInference, PriorTask} ∪ Emergent(Origin)
recipient? = Optional(RecipientProfile) -- defaults to { knowledge: "zero-memory", activation: Unbounded } when absent (the conservative absent-recipient default)
next_task? = Optional(String) -- declared at F0; absence forces F0 elicitation before relevance is defined
activation_verb? = Optional(String) -- the activation edge's verb, declared at invocation or F0; absent → the canonical minimal verb ("Read <locator> and execute it"). Never a contract field: the contract carries the noun (emit_target), the edge carries the verb
Detect = W → (Bool, tethered_items if true) -- F0 precheck for session-tethered residue
StableRef = { kind: "path" | "url" | "id" | "command", locator: String } -- a reference the recipient resolves throughout its declared activation window (the Unbounded window recovers the absent-recipient reading: resolvable without the author session). Durability is not a stored field: it is decided at each use site by resolves_at(locator, contract.recipient_profile.activation) — the test a StablePointer grounding applies
ActivationWindow ∈ {Immediate, Bounded(Duration), Unbounded} ∪ Emergent(ActivationWindow) -- WHEN the recipient reads and acts on the handoff, relative to the author session's lifetime; Emergent(·) is a not-yet-named window kind, consumed conservatively (treated as Unbounded until it earns its own branch)
RecipientProfile = { knowledge: "zero-memory"; activation: ActivationWindow } -- recipient isolation is TWO parameters: knowledge (no session access) and activation (WHEN it reads); the old string literal fixed only knowledge and silently assumed Unbounded activation
resolves_at(locator, w) ≡ the locator's referent is reachable by the recipient throughout w
Immediate ⇒ reachable while the author session lives, on the recipient's machine
Bounded(d) ⇒ the referent's lifetime is at least d
Unbounded ⇒ the referent persists beyond the author session and is reachable by an absent recipient
Emergent(w) ⇒ conservatively evaluated as Unbounded until w earns its own arm
-- window-relative durability: a temp/cache/scratch-rooted locator resolves under Immediate (author session alive, same machine) yet not under Unbounded (the temp tree is gone or was author-private by recipient time). The enumeration of ephemeral roots and their cleanup lifetimes is an environment fact (docs/analysis/activation-window.md), not a rule clause. Primarily discriminates path locators; a url/id/command locator does not resolve when its referent is session-local (a localhost/session URL, an in-session-only id, a command whose output lived only in the author session). Under Unbounded, resolves_at reduces to the old durable(locator) predicate, so nothing loosens for the absent-recipient case the original rule was written for
well-formed: handoff_durability = DurableRepo ⇒ contract.recipient_profile.activation = Unbounded -- a durable in-repo handoff is consumed by an absent future recipient; its recipient profile cannot declare a shorter window (the qualified path disambiguates from PortableHandoff.activation, which is the ActivationEdge)
ActivationEdge = { verb: String; locator: StableRef } -- the minimal executable hand-over, a noun/verb split: the verb is declared at F0 (default: the canonical minimal verb "Read <locator> and execute it"); the locator is contract.emit_target BY REFERENCE, never re-declared — the noun lives once in the contract, the edge carries only the verb. Constructed at Phase 0 as Λ.activation_edge; F5 reviews it under the minimal admissible edge (checklist category 8); F7 emits it as the initial-prompt block
content_free(e) ≡ no discriminating token of the task content — the declared next task (contract.next_task) or the working context's items (W) — appears in e.verb -- evaluable at the Phase 0 → Phase 1 guard (contract and W are bound there; the prose channel does not yet exist). The emit-time complement is leak_free: the edge is an emit channel, so F6 lints it against the actually-emitted content. content_free binds the verb only: the locator's job is naming the artifact (an artifact name is not a summary), and its content discipline is carried by leak_free (the edge is an emit channel, so DROP'd discriminating content in the locator is a leak) and resolves_at
-- a summarizing edge is a second source of truth and will drift from the document
-- a Phase 0 → Phase 1 guard: a content-bearing verb is repaired at F0 (re-form the declaration, surface the correction as relay), never carried into Phase 1
InlineEvidence = { content: String } -- evidence carried inline rather than by reference
HandoffContract { recipient_profile: RecipientProfile; next_task: String;
allowed_sources: List(StableRef); execution_scope: String; verification_commands: List(String);
stop_condition: String; handoff_durability: HandoffDurability; emit_target: StableRef }
-- F0 output; the contract every later phase reads for relevance and minimality. handoff_durability (Change A) is the switch F3b and F7 read to conditionalize the CorrectionDelta ledger. emit_target is the NOUN of the activation edge — the locator where F7 will emit the canonical handoff (under re-distillation it names the same file as the prior handoff); declared at F0 so the edge's locator exists before F5 reviews it
HandoffDurability ∈ {OneShot, ExternalVersioned(version_ref: StableRef), DurableRepo} ∪ Emergent(HandoffDurability)
-- F0 classification of the handoff's lifetime/target — the switch that conditionalizes the CorrectionDelta ledger (read by F3b at Phase 0 bind, by F7 at emit):
-- OneShot temporary/one-shot handoff, used once, never re-distilled — NO ledger (Λ.ledger = Unknown, no F7 ledger emit); a correction-requiring claim surfaces at the Gate (user Resolve), never CorrectedKeep
-- ExternalVersioned(version_ref) target is an externally-versioned store (Notion page history, Linear issue version) — DEFER provenance to that native history; NO internal ledger; version_ref is the contract-level provenance pointer recorded in the handoff. A corrected value lives in the store's native history, so re-observing it yields the current corrected value: an item grounded in a durable StablePointer to that store reads as ObservedKeep (via its own observable_basis), never CorrectedKeep (no local ledger)
-- DurableRepo durable, re-distilled in-repo handoff (the case the ledger was designed for) — the full CorrectionDelta ledger + re-distillation discipline (Rule 19) apply; the ONLY mode in which CorrectedKeep is reachable
-- Emergent(·) a not-yet-named durability kind — consumed by the non-DurableRepo default (Λ.ledger = Unknown, no F7 ledger emit; ObservedKeep / Gate path), since every ledger guard keys on `= DurableRepo`. The guard makes consumption total over the partition: an emergent kind falls through to the conservative no-ledger behavior until it constitutes DurableRepo-equivalent re-distillation semantics and earns its own classification + Rules branch
SurfaceToken = String -- a session-local deictic token (undefined jargon, metric shorthand, "as above", a bare task id)
Substitution = { surface_token: SurfaceToken; canonical_ref: StableRef | InlineEvidence | Null;
confidence: Float; unresolved: Bool } -- F1 row; unresolved = true routes the token to the residual ledger
SubstTable = List(Substitution)
Grounding ∈ {Inline(InlineEvidence), StablePointer(StableRef), RoutedResidual(reason: String)} -- F2 per-item self-containment class; StablePointer requires resolves_at(locator, contract.recipient_profile.activation) — a locator that does not resolve throughout the recipient's activation window (resolves_at = false) fails StablePointer classification. Repair: inline the evidence (Inline) or relocate the content to a locator that resolves in that window (a resolving StablePointer); when neither is possible in-session the item is RoutedResidual and appends to the residual ledger (reason: unresolved), surfaced at the Gate like any other unresolvable reference
CorrectionDelta { id: String; subject_ref: StableRef; claim_kind: String; original_ref: Option(StableRef);
original_claim_hash: Option(String); corrected_claim: String;
correction_basis_ref: StableRef | InlineEvidence; corrected_at: Timestamp;
corrected_by: "User" | "Tool" | "AI"; supersedes: List(String); validity_horizon: Option(Duration);
horizon_basis_ref: Option(StableRef | InlineEvidence);
export_policy: "KEEP" | "ROUTE" | "DROP";
verification_status: "observed" | "user_confirmed" | "tool_confirmed" | "provisional" }
-- append-only correction record; F3b's read authority, maintained only under handoff_durability = DurableRepo (Change A — OneShot/ExternalVersioned keep no ledger). F3b consumes it read-only; the F7 re-distillation emit appends to it (Rule 19), never rewriting an existing delta. validity_horizon bounds how long the delta's unattended KEEP authority holds; when set, horizon_basis_ref names the user-constituted content the horizon was transcribed from (Rule 20).
effective_delta(item) = most-recent non-superseded d ∈ ledger : d.subject_ref = ref(item) -- ∅ when ledger absent, no match, or the ledger is not maintained (handoff_durability ≠ DurableRepo ⇒ Λ.ledger = Unknown, so effective_delta = ∅ always); supersedes-chain resolved to the live record
expired(d) = d.validity_horizon ≠ Null ∧ Λ.now > d.corrected_at + d.validity_horizon -- Λ.now is the invocation timestamp, bound once into the mode state at Phase 0 (always, independent of the now-conditional ledger bind; only evaluated under DurableRepo where deltas exist) (invocation-local constant: an expired() verdict cannot flip between passes within one invocation, since Λ.now does not change — this stabilizes only the expiry leg, not the measure's other legs, which repair-authored prose can still move); Null horizon never expires. Same comparison idiom as Elenchus freshness (observed_at + horizon < now)
corrected_in_session(item) = effective_delta(item) = d ∧ d.export_policy = "KEEP" ∧ d.verification_status ≠ "provisional" ∧ ¬expired(d) -- reachable only under DurableRepo (effective_delta = ∅ otherwise)
observable_basis(item) ≡ durable_observable_source(item) ∧ support_integrity(item) -- BOTH conjuncts required (the outer ∧ binds the whole disjunction below to support_integrity, never just one branch)
durable_observable_source(item) ≡
( grounding(item) = Inline(e) ∧ origin(item) ∈ {DocumentRead, ToolOutput} ) -- directly-observed evidence carried inline (a file read, a command's captured output); an Inline(AIInference) is the AI's own assertion, not re-observable
∨ ( grounding(item) = StablePointer(r) ∧ resolves_at(r.locator, contract.recipient_profile.activation) ) -- a reference the recipient resolves throughout its activation window (a path, a PR/issue url, a stable id), re-observed independently of the item's session-origin
support_integrity(item) ≡ the kept value is recipient-verifiable: a contract verification_command re-runs it, a resolvable url/id re-fetches it, or the inline observed content directly evidences the claim. A present-but-support-unlinked item (current/fresh but the evidence does not track the claim) FAILS this conjunct (Currency ≠ Support-Integrity). When the basis is uncertain or contested (the observable source would conflict with the claimed value, or relevance to the claim is doubtful), support_integrity(item) = false — the conservative direction routes to the Gate rather than auto-KEEPing on a doubtful basis
provenance(item) = CorrectedKeep if corrected_in_session(item) -- DurableRepo: a matching non-provisional unexpired KEEP delta holds the corrected/disputed/stale claim
| ObservedKeep if effective_delta(item) = ∅ ∧ observable_basis(item) -- Change B: NO correction record AND a durable observable basis with support-integrity → KEPT directly, no ledger, no Gate (the common-case relay path that collapses the gate storm)
| Unknown otherwise (a matching delta that is expired — keeps its ledger standing, only its unattended KEEP authority lapses, surfaced as a re-verification question, reason: horizon-expired — or provisional-only, or a non-KEEP delta; OR effective_delta = ∅ ∧ ¬observable_basis(item): no observable basis and no delta — an AIInference, a bare in-session UserStatement, or a contested basis — reason: unknown-provenance)
Provenance ∈ {CorrectedKeep, ObservedKeep, Unknown} -- F3b verdict, a ternary partition. CorrectedKeep: an effective matching non-provisional unexpired KEEP CorrectionDelta (DurableRepo only). ObservedKeep (Change B): no correction record and a durable directly-observable source coupled to the item by support-integrity — the relay path for ordinary technical state, KEPT without a ledger or the Gate. Unknown: every remaining state (expired/provisional/non-KEEP delta, or no delta and no observable basis), surfaced at the Gate. Provenance authority is the KEEP hard line only — ROUTE/DROP dispositions come from F3a relevance or the Gate, not from a provenance verdict
Disposition = KEEP(InlineEvidence) | ROUTE(StableRef) | DROP -- F3 3-way coproduct
ResidualLedger = Set({ item: ContextItem, reason: "unresolved" | "unknown-provenance" | "horizon-expired" | "comprehension-gap", surfaced: Bool, evidence: Option(EvidencedFinding) }) -- silent residual forbidden: every entry must have surfaced = true before convergence; evidence carries the F5 finding that re-entered the item for comprehension-gap entries (Null for other reasons)
A = Gate answer ∈ {None} ∪ {Resolve(canonical_ref), Route(StableRef), Drop, Defer(condition)}
-- Gate coproduct for surfaced residuals, unknown-provenance items, and horizon-expired items; presented intact.
-- None is the identity answer when gate_domain = ∅ (no surfaced item to judge) — not a user-facing option, never presented at Qd
gate_domain(Λ) = disposition conflicts ∪ unknown-provenance items ∪ horizon-expired items ∪ unresolved residuals
-- the set Qd is defined over; Qd fires only when gate_domain ≠ ∅ (a clean pass — every item uncontestedly disposed: CorrectedKeep/ObservedKeep KEEP, or F3a ROUTE/DROP; F5 Pass with no findings — has an empty domain and no Gate to present)
Qd = Residual + disposition-conflict gate over gate_domain(Λ), conditional on gate_domain(Λ) ≠ ∅ [Tool: Constitution interaction]
A_tag ∈ {Resolve, Route, Drop, Defer} -- the constructors of A without their bound arguments; an advisory names the constructor only, and the Gate answer materializes it into a full A term (type-preserving materialization: the user binds the argument and decides at the Gate)
EvidencedFinding = { item: ContextItem; quoted_token: String; location: String; category: String; why_unresolvable: String; advisory: A_tag; repair_note: String } -- one F5 Fail finding: cited evidence (quoted token + location + category + why the recipient cannot resolve it), an advisory Gate disposition tag, and a prose repair note; the typed form of one Findings-table row in the refuter verdict. The refuter emits rows WITHOUT an item handle (it sees only the handoff text); the caller binds `item` at parse time by matching quoted_token + location back to the candidate's context items — when no unique tracked item matches (the refuter may flag document text no tracked item produced, e.g. a rendering accident), the caller synthesizes a ContextItem from the finding (content: the quoted token in its location context, origin: AIInference) so the finding still enters the residual ledger — unless the competence-substitution backstop (Rule 27) trips, when the finding stays typed but routes to contract re-declaration, never the ledger; a Fail row is never dropped for binding failure
WatchList = Set(String) -- session-term watchlist, the third F5 input (recorded as Λ.watchlist), enumerated at dispatch from the author session's own record: skill/protocol names invoked this session ∪ subagent names dispatched ∪ tool names called ∪ plugin/skill names whose instructions are loaded in the session context. The enumeration reads the live session, never a directory scan of installed-but-unused plugins: the watchlist names what is ACTIVE in the session (and could therefore leak into the handoff as plain prose), not what is installed
zero_memory(recipient) removes session access, NOT competence -- the recipient's ordinary competence to choose, apply, adapt, and verify a method is intact; the F5 gate measures portability of context, never the recipient's engineering judgment (the mis-reading "zero-memory recipient ⇒ judgment-free executor" is the root of competence substitution)
judgment_bearing(t) ≡ completing task t requires choosing, creating, adapting, debugging, or deploying a mechanism whose correct behavior is not already fixed by an authoritative, independently re-verifiable artifact
recipient_owns_method(contract) ≡ contract.next_task ∪ contract.execution_scope explicitly leave mechanism selection and implementation judgment to the recipient, while contract.verification_commands and contract.stop_condition define outcome acceptance
authoritative_primitive(p) ≡ p is a single exact command, config value, or API-shape token quoted as an authoritative primitive (Rule 27 admissible), not an assembled multi-step procedure -- a lone primitive is admissible evidence, never authored operative procedure
authored_procedure(p) ≡ p was written or assembled by the author session during this work (origin AIInference / Λ.authored), not an artifact independently existing in the target system ∧ ¬authoritative_primitive(p) -- a lone authoritative primitive stays admissible (Rule 27) even when the author wrote it down, so it never trips the artifact leg
operative(p, candidate, contract) ≡ candidate presents exact procedure p as ready to copy, run, or adopt, and satisfying contract.stop_condition depends on using p rather than inspecting it as evidence or independently choosing a mechanism
verified_operative(p, candidate, contract) ≡ p has (exact content identity ∨ a revision-fixed StableRef) ∧ resolves_at(ref(p), contract.recipient_profile.activation) ∧ candidate carries or routes observable verification evidence whose support_integrity covers the stated behavioral claim and environment ∧ contract.verification_commands replay that claim before adoption ∧ contract.stop_condition claims no more than that verification establishes ∧ candidate states that modification invalidates the verified status ("adopt unchanged" vs "reference/adapt") -- "the author ran it" alone is insufficient
contract_names_verified_operative(p, contract) ≡ p is named by a revision-fixed StableRef in contract.allowed_sources ∧ resolves_at(ref(p), contract.recipient_profile.activation) ∧ (∃ e ∈ contract.allowed_sources : e resolves to observable verification evidence whose support_integrity covers p's stated behavioral claim and environment) ∧ contract.verification_commands replay p's stated behavioral claim before adoption ∧ contract.stop_condition claims no more than that verification establishes ∧ contract states adopt-unchanged (modification invalidates the verified status) -- the F0-evaluable analogue of verified_operative: reads the CONTRACT (allowed_sources + verification_commands + stop_condition), NOT a candidate, so the "name a verified operative artifact" F0 escape is inhabitable at Phase 0 where candidate = Null. candidate-level verified_operative stays the F5 artifact-leg test
behavior_repair(f, p) ≡ resolving F5 finding f requires changing p's control flow, state, timing, concurrency, resource ownership, or failure behavior; supplying a missing fact, decision, StableRef, command, config value, or API shape is NOT a behavior repair -- the discriminator is the TARGET OF THE REPAIR, never the finding's phrasing: "cannot execute" wording may still be a finite resolution gap ("the launch command is missing"), and a resolution-shaped phrase may hide a behavior repair
competence_substitution(contract, candidate?, verdict?) ≡
(judgment_bearing(contract.next_task) ∧ ¬recipient_owns_method(contract) ∧ ¬∃ p : contract_names_verified_operative(p, contract)) -- F0 leg: judgment-bearing task, method neither recipient-owned nor grounded in a verified artifact the CONTRACT names (evaluable at F0 where candidate = Null; the candidate-level verified_operative test is the artifact leg below, at F5)
∨ (candidate ≠ Null ∧ ∃ p ⊆ candidate : operative(p, candidate, contract) ∧ authored_procedure(p) ∧ ¬verified_operative(p, candidate, contract)) -- artifact leg: authored operative procedure without verified status
∨ (verdict = Fail(B, _, _) ∧ ∃ f ∈ B, p ⊆ candidate : operative(p, candidate, contract) ∧ behavior_repair(f, p)) -- F5 backstop leg: ONE behavior-repair finding suffices, no multi-pass "shift" is required
-- the guard against substituting author-written procedure for recipient judgment (Rule 27). The verb "implement" alone NEVER trips — "implement, choosing a mechanism and validating against these invariants" is a valid contract. Witness discipline: when no witness can be named that the next task is executable-from-alone at the declared strength, the contract claims less (the recipient-owned-method form), never more. Evaluator dual: the F5 realization's authority envelope is the refuter's declared tool set — execution evidence is inadmissible (the verdict codomain is why_unresolvable; a reproduced crash does not inhabit it), and a broader tool profile at dispatch is an evaluator substitution that voids the verdict
SweepTrace = List({ category: String, status: String, checked: String }) -- per-category sweep record (what was actually checked, including which references were tool-verified); required for BOTH verdicts — a verdict missing the sweep trace or the realization is no verdict (re-dispatch, never default to Pass)
F5Realization ∈ {refuter-subagent, generic-subagent, lint-fallback} -- which realization produced the verdict, platform-laddered: the packaged named agent where the platform registers plugin agents; a generic fresh subagent carrying the same F5 instructions where only generic spawn exists (fresh-context isolation preserved); lint-fallback only where no subagent surface exists — the weakened realization (no fresh-context isolation), and the verdict must carry the realization it ran under
ZeroMemoryVerdict ∈ {Pass(sweep: SweepTrace, realization: F5Realization), Fail(blocking_items: Set(EvidencedFinding), sweep: SweepTrace, realization: F5Realization)} -- F5 comprehension verdict; convergence conditions written as `zero_memory_verdict = Pass` match on the constructor. Fail names the findings a fresh recipient cannot resolve, whose items re-enter the residual ledger (reason: comprehension-gap, evidence: the finding) and block the fixed point — except when the competence-substitution backstop (Rule 27) trips (a candidate embedding unverified authored operative procedure, or a behavior-repair finding on one), which terminates the invocation with nothing entering the ledger. Both constructors carry the sweep trace and the realization, so an evidence-cited Pass and a degraded-fallback verdict are typed state, not prose claims. A multi-file handoff — one whose prose references a sibling handoff file the recipient must also read — is a Fail: a fresh recipient must execute from ONE self-contained handoff (Single Canonical Handoff invariant). Prose-only deletion test (Change C): a handoff whose next task is NOT executable from the prose channel + allowed sources alone — once the TaskStateBlock, the correction ledger, native task-state, and every agent-specific affordance are ignored — is likewise a Fail (the task-state channel rehydrates dangling identifiers, it never holds authority the prose lacks, Rule 11)
TaskStateBlock = { schema_version: String; tasks: List({ id: String; subject: String; description: String;
restore_status: "pending"; source_ref: StableRef }) } -- F7 structured channel; rehydrates dangling task identifiers
emit_candidate(Λ) = the candidate channels F6 lints before convergence: contract ∪ prose ∪ task_state ∪ residual_ledger ∪ activation ∪ emitted_deltas? -- the repairable to-be-emitted content (contract included — F7 emits it too; activation is the emitted ActivationEdge, so the leak lint covers it; emitted_deltas present only under re-distillation = this pass's appended CorrectionDelta lines). The correction ledger's PRIOR entries — which the recipient also reads (PortableHandoff.correction_ledger) — are deliberately NOT in emit_candidate: they are append-only provenance (Rules 15/19) leak-vetted at their own emit pass and cannot be rewritten, so re-linting them would manufacture an unrepairable leak. Each pass is accountable only for the deltas it appends; distinct from the F7 emit(·) action
redistillation(Λ) ≡ Λ.prior_handoff ≠ Null -- a canonical PortableHandoff file already exists for the contract; the emit is an in-place hygiene of that one file + a CorrectionDelta append, never a new versioned sibling (Single Canonical Handoff invariant). ⇒ handoff_durability = DurableRepo: only the durable in-repo case carries a local prior_handoff file and an internal ledger to append to — OneShot is one-shot (prior_handoff = Null), and ExternalVersioned's prior lives in the external store's native history, not a local file
ledger_emit_clean(d) ≡ for a CorrectionDelta d written to the emitted correction ledger: supersedes references prior ledger-entry ids only (never a discarded-content label) ∧ original_ref, original_claim_hash identify the original claim by stable reference and content hash, never by reproducing a DROP'd item's discriminating content ∧ corrected_claim states the current settled value positively (not a negation or retraction of a DROP'd alternative) ∧ (d.validity_horizon = Null ∨ (d.horizon_basis_ref ≠ Null ∧ the horizon is transcribed from a temporal indexical in the user-constituted content horizon_basis_ref names, or set directly by the user — never assigned by model classification; Rule 20)) -- a portable ledger records provenance for the KEPT value, not a pointer at the discarded alternative; a pointer-at-discarded — any emitted delta field that names, quotes, or otherwise reproduces a DROP'd item's discriminating content — re-introduces the DROP'd content into the recipient's attention and is a leaked_drop
tokens(X) = the token content extracted from channels X (strings, not the structured objects) -- projection Channels → Set(Token), so the ⊆ test below compares homogeneous token sets
discriminating(d) = the session-local tokens that UNIQUELY identify a DROP'd item d — its distinctive content, not bare ids nor tokens shared with in-scope items -- precision-bounded against false positives; when the boundary is uncertain, delegate the leak check to a fresh subagent (as F5 does) rather than let a common token block convergence
leaked_drops(Λ) = { d ∈ Λ.dropped : discriminating(d) ≠ ∅ ∧ discriminating(d) ⊆ tokens(emit_candidate(Λ)) } -- DROP'd content that survived into an emitted channel; the minimality dual of the F5 comprehension-gap (F5 catches missing, this catches leaked). The ≠ ∅ guard is load-bearing: a DROP whose discriminating set is empty (no unique identifying content) has nothing distinctly leakable or excisable, so the vacuous ∅ ⊆ tokens(...) must not count it as leaked — otherwise |leaked_drops| could never reach 0 and the loop would never converge (liveness trap)
leak_free(Λ) ≡ leaked_drops(Λ) = ∅ ∧ (¬redistillation(Λ) ∨ ∀ d ∈ Λ.emitted_deltas : ledger_emit_clean(d)) -- no DROP'd content in any emitted channel; under re-distillation, every CorrectionDelta appended to the emitted ledger is pointer-clean, positively stated, and horizon-grounded (the emitted correction ledger is an emit channel subject to leak_free)
unclean_deltas(Λ) = { d ∈ Λ.emitted_deltas : ¬ledger_emit_clean(d) } -- ∅ when ¬redistillation(Λ) (emitted_deltas empty); the measure leg for emit-ledger leaks, so a ledger_emit_clean violation increments measure and blocks fixed_point exactly as |leaked_drops| does — this restores leak_free ⟸ (measure = 0) under re-distillation
undisposed_authored(Λ) = Λ.authored \ (Λ.kept ∪ Λ.routed ∪ Λ.dropped) -- repair-authored items (F5-repair or leak-repair prose) not yet given a disposition; a nonzero count keeps the loop off its fixed point until each authored item re-enters Phase 1 and F1–F3 dispose it (bottoms out: a Resolve supplies user-constituted evidence, never new authored prose)
measure(Λ) = |unresolved_anchors| + |unmet_stop| + |schema_gaps| + |unsurfaced_residual| + |leaked_drops| + |unclean_deltas| + |undisposed_authored| -- F6 hygiene measure: targets the repair and detects the stall. NOT monotone per pass — a repair pass authors new prose (Rule 25), and authored prose is generative (it can carry new unresolved anchors or residuals, or re-leak DROP'd content), so legs can rise before they settle; termination is argued at LOOP, not from per-pass decrease
fixed_point(Λ) = (measure(Λ) = 0 ∨ (measure stable ∧ all residuals surfaced ∧ leak_free(Λ) ∧ undisposed_authored(Λ) = ∅ ∧ no disposition conflict)) ∧ zero_memory_verdict = Pass
PortableHandoff = { contract: HandoffContract; activation: ActivationEdge; prose: String; task_state: TaskStateBlock; residual_ledger: ResidualLedger; correction_ledger: Option(List(CorrectionDelta)) } -- activation is the content-free edge that hands this artifact to its recipient (verb + locator), emitted with the handoff and covered by leak_free; correction_ledger present only under re-distillation: the emitted append-only ledger the recipient reads (prior entries + this pass's appends); Null for a fresh handoff. Semantic closure: the F7 emit signature's correction_ledger? maps to this result-type leg. The leak lint's domain for the ledger is this pass's appends only (emitted_deltas, the channel F6 lints in emit_candidate) — prior entries are immutable provenance leak-vetted at their own pass, so F6 always has a legal repair and no unrepairable prior-entry leak can block the fixed point
-- emitted when fixed_point(Λ) ∧ ¬user_esc ∧ every ResidualLedger entry surfaced ∧ leak_free(Λ)
-- residual_ledger here carries recipient-relevant residue only (Route-pending pointers); Drop- and Defer-resolved entries are released — their content + drop/re-trigger reason stay session-side in Λ.history, never emitted (Defer = released-not-retained per the Λ invariant; see Rule 12)
Phase ∈ {0, 1, 2, 3, 4}
── PHASE TRANSITIONS ──
Phase 0: W, recipient?, next_task?, activation_verb? → Detect(W) → tethered? -- tethered checkpoint (silent)
then F0 declare(recipient, next_task, allowed_sources, scope, verification, stop, handoff_durability, emit_target) → HandoffContract -- recipient is a RecipientProfile carrying its activation window (Immediate | Bounded | Unbounded); the window is declared here with the rest of the contract and checked against well-formed (DurableRepo ⇒ Unbounded); Λ.activation_edge is constructed in the next step from activation_verb? and contract.emit_target — the F5 fourth input exists from Phase 0
then Λ.activation_edge = edge(activation_verb?, contract.emit_target) -- verb declared or defaulted to the canonical minimal verb; locator is a reference to the contract's emit target, never a copy
then bind Λ.now (always) and Λ.ledger = read(CorrectionDelta) | Unknown if handoff_durability = DurableRepo else Unknown -- conditional ledger bind (Change A)
Phase 1: HandoffContract → F1 normalize(surface_token, canonical_ref, confidence) → SubstTable [Tool: Read, Grep, Glob]
then F2 audit(item, self_containment) → Grounding (inline | stable-pointer | routed-residual)
unresolved F1 tokens and routed-residual F2 items append to ResidualLedger (surfaced = false)
Phase 2: (SubstTable, Grounding, ledger, handoff_durability) → F3a relevance(item, contract.next_task)
→ F3b attest(item, ledger, handoff_durability) → Provenance
→ F3 dispose(item) → Disposition -- KEEP from CorrectedKeep (DurableRepo KEEP delta) ∨ ObservedKeep (durable observable source + support-integrity, KEPT directly); ROUTE/DROP from F3a relevance or the Gate; Unknown routes to Gate
Phase 3: kept → F4 compress(kept) → minimal_complete -- minimal-complete (track)
→ F5 comprehension_gate(minimal_complete, contract, watchlist, activation_edge) → zero_memory_verdict [Tool: Read, Task]
→ [gate_domain(Λ) ≠ ∅] Qd(gate_domain(Λ)) → Stop → A | [gate_domain(Λ) = ∅] A := None (identity) [Tool: Constitution interaction]
then repair(A, blocking_items | ∅) → Λ.authored -- blocking_items is bound by a Fail verdict and ∅ under Pass; when no Gate answer requires authored prose the step is the identity (nothing enters Λ.authored). F5-repair prose written THIS pass, after the Gate answer and before F6 settle, enters Λ.authored undisposed (Rule 25); |undisposed_authored| > 0 is therefore visible to this pass's F6 and triggers the next pass, whose F1–F3 dispose it
Phase 4: A, verdict → F6 settle(measure) → fixed_point?
¬fixed_point → Phase 1 (next pass); fixed_point → F7 emit(prose, activation_edge, TaskStateBlock, correction_ledger?) → PortableHandoff
Phase 0 → Phase 1: context_tethered(W) = true ∧ HandoffContract declared ∧ well-formed(contract) ∧ content_free(Λ.activation_edge) ∧ ¬competence_substitution(contract, Null, Null) -- a well-formed or content_free violation is repaired at F0 (re-form the declaration; correction surfaced as relay), never carried forward; a competence-substitution trip is a Stop (Rule 27): the misfit witness + a proposed recipient-owned-method re-declaration surface for the user, and Phase 1 opens only on the re-declared contract
Phase 0 → deactivate: context_tethered(W) = false -- handoff already self-contained
Phase 1 → Phase 2: SubstTable produced ∧ every item assigned a Grounding class -- deixis normalized, self-containment audited
Phase 2 → Phase 3: every item carries a Disposition or a surfaced unknown-provenance / horizon-expired flag -- relevance + provenance discharged
Phase 3 → Phase 4: zero_memory_verdict produced ∧ ¬competence_substitution(contract, minimal_complete, zero_memory_verdict) ∧ (A received ∨ gate_domain(Λ) = ∅) -- comprehension evaluated (Pass or Fail) and residual answered, OR the gate domain is empty (clean pass, A = None by identity); Pass gates convergence at Phase 4. A backstop trip takes precedence — it fires the graceful-deactivate transition below, never this one
Phase 4 → Phase 1: ¬fixed_point(Λ) → pass_n += 1 -- measure unsettled OR comprehension verdict not yet Pass OR |undisposed_authored| > 0, re-audit; the next pass's F1–F3 domain is Λ.authored (repair-authored content awaiting disposition — Rule 25), while items of the working context retain the dispositions they already carry and the source chain stays read-only; a leak repair (leaked_drops > 0 ∨ unclean_deltas > 0 detected at this settle) is performed on this re-entry — the excisions/rewrites it authors enter Λ.authored before the next pass's F1, so they too are disposed by F1–F3 (Rule 25)
Phase 4 → converge: fixed_point(Λ) ∧ zero_memory_verdict = Pass ∧ every ResidualLedger entry surfaced ∧ leak_free(Λ) -- emit PortableHandoff across its channels (prose + TaskStateBlock, plus the correction ledger under re-distillation); no DROP'd content leaks into emit
Phase 3 → deactivate (backstop, graceful): competence_substitution(contract, minimal_complete, zero_memory_verdict) -- a behavior-repair finding on authored operative procedure (Rule 27): terminate this /distill invocation without emit, surface the witness + a proposed recipient-owned-method contract for a FRESH invocation; NOT an in-loop restart — J gains no re-declaration arm and no new contract instance is created within the loop, so the LOOP permanence/fixed-point argument (scoped to one invocation) is untouched. The fresh invocation re-runs F3a relevance under the re-declared next_task
Phase 3 → deactivate (ungraceful): Esc -- residual untreated, handoff not emitted
── LOOP ──
J = {next_pass, converge, esc}
next_pass: ¬fixed_point(Λ) ∧ ¬Esc → pass_n += 1, Phase 4 → Phase 1 (bounded audit/lint re-scan)
converge: fixed_point(Λ) ∧ every ResidualLedger entry surfaced ∧ leak_free(Λ) → emit PortableHandoff
esc: Esc → ungraceful deactivate (residual untreated)
One-pass + bounded audit/lint: the morphism runs once forward (F0→F7), then F6 re-audits against the hygiene measure. Termination is NOT argued from per-pass decrease — a pass that repairs comprehension gaps authors new prose, and authored prose can carry new obligations (fresh unresolved anchors, fresh residuals, a re-leaked DROP), so measure(Λ) can rise across a repair pass. It is argued from three facts: dispositions of working-context items are permanent (Phase 4 → Phase 1 keeps every carried disposition; the source chain stays read-only), the Gate bottoms out (a Resolve supplies user-constituted evidence, never new authored prose — so each authored item is at most one Gate round from a disposition), and the fixed point's stable-measure branch is an explicit stall exit (measure stable across a pass with all residuals surfaced, leak_free, and every authored item disposed). The loop terminates at the fixed point, not on a felt sense that the handoff "reads complete." The competence-substitution backstop (Rule 27) removes the one repair family this argument cannot bound — procedure correctness of authored operative code, where each repair pass authors new behavior that itself needs verification — by terminating the invocation without emit and handing a re-declared contract to the caller for a fresh invocation, instead of another repair pass. It is a graceful terminal outcome, not an in-loop restart: J stays {next_pass, converge, esc}, no new contract instance is created within the loop, and it adds no measure leg and no Disposition arm — so the one-invocation termination argument is strengthened (one unbounded repair family removed), not restructured.
Provenance hard line: F3b never infers KEEP from appearance. KEEP is reachable exactly three ways: an effective matching non-provisional unexpired KEEP CorrectionDelta (CorrectedKeep — DurableRepo only); a durable directly-observable source coupled to the item by support-integrity, with no correction record (ObservedKeep — the common-case relay path, KEPT directly without a ledger or the Gate); or a user Resolve at the Gate. Every other state — a KEEP delta whose validity_horizon has lapsed (horizon-expired: surfaced for re-verification, never silently dropped, and never silently re-asserted as ObservedKeep), a provisional-only or non-KEEP delta, or an item with no observable basis and no delta (an AIInference, a bare in-session UserStatement, a contested basis) — yields Unknown, which routes to the Gate as a Constitution question where the author decides KEEP, ROUTE, or DROP. Provenance authority covers the KEEP hard line only: ROUTE and DROP dispositions are reached through F3a relevance or the Gate, never defaulted from a provenance verdict. The hard line that a correction-requiring claim still needs the ledger is preserved: a claim that diverges from its observable source (corrected, disputed, stale) has a contested or absent observable basis, so it cannot be ObservedKeep — it is held by a CorrectionDelta (DurableRepo) or surfaced at the Gate.
Silent-residual ban: every item classified as routed-residual at F2, every unresolved token at F1, every unknown-provenance item at F3b, every horizon-expired item at F3b, and every comprehension-gap item at F5 enters the ResidualLedger with `surfaced = false` and must reach `surfaced = true` through the Gate before convergence.
Comprehension hard line: F5's verdict gates the fixed point. A Fail re-enters its blocking items into the residual ledger (reason: comprehension-gap, `surfaced = false`) and keeps the loop off its fixed point — except when the competence-substitution backstop (Rule 27) trips (a candidate embedding unverified authored operative procedure, or a behavior-repair finding on one), which terminates the invocation, nothing entering the ledger; convergence requires a Pass verdict, so a handoff never emits while the zero-memory gate fails. The prose-only deletion test is part of this gate (Change C): if the next task cannot be executed from the prose channel plus the contract's allowed sources alone — with the TaskStateBlock, the correction ledger, native task-state, and every agent-specific affordance ignored — F5 Fails, because the task-state channel rehydrates dangling identifiers but never carries authority the prose lacks (channel separation, Rule 11).
Leak repair: when `leaked_drops > 0` (or, under re-distillation, `unclean_deltas > 0`) the loop re-enters, and the repair is a targeted emit-channel revision — excise every leaked DROP'd item's discriminating content from every emit channel — contract, prose, TaskStateBlock, residual_ledger, the activation edge, and (under re-distillation) the correction ledger — and rewrite every non-`ledger_emit_clean` CorrectionDelta to reference prior ledger-entry ids and state the settled value positively, and ground any validity_horizon in its horizon_basis_ref (constituted, never model-assigned), then re-audit (contract excision = rewording the offending field; the contract itself is retained). Unlike the F5 repair, no item re-enters the residual ledger: a DROP was already user-decided at the Gate, so the defect is its content surviving the emit and the fix is excision from the candidate emit, not re-surfacing. Convergence is preserved because content that is load-bearing for an in-scope item belongs to that item's own KEEP/ROUTE record (retained on its own basis); only the DROP'd item's UNIQUE discriminating content is excised.
Repair-authored content: every item the author session writes during an F5 repair or a leak repair enters `Λ.authored` and re-enters Phase 1 on the next pass, where F1–F3 give it a substitution row, a grounding class, a provenance verdict, and a disposition. Authored content citing a re-observable source is ObservedKeep — KEPT with no gate. Authored content asserting without such a basis is Unknown and surfaces at the Gate. The recursion bottoms out: a Gate answer on an authored item yields a disposition, and a Resolve supplies user-constituted evidence (KEEP, basis: the user's answer), never new authored prose. The fixed point is unreachable while `|undisposed_authored| > 0` (the measure leg keeps the loop running until every authored item carries a disposition).
Convergence evidence: At convergence, present the substitution table (surface_token → canonical_ref → confidence → unresolved?), the per-item disposition trace (KEEP/ROUTE/DROP with provenance basis), the surfaced residual ledger, and the emitted TaskStateBlock. Convergence is demonstrated, not asserted.
── CONVERGENCE ──
converge iff fixed_point(Λ) ∧ every ResidualLedger entry surfaced ∧ leak_free(Λ) ∧ ¬user_esc
fixed_point(Λ): (measure(Λ) = 0, OR measure stable across a pass with all residuals surfaced, leak_free, every authored item disposed (undisposed_authored = ∅), and no open disposition conflict) ∧ zero_memory_verdict = Pass
surfaced ledger: ∀ r ∈ ResidualLedger : r.surfaced = true (no silent residual reaches the recipient)
leak_free: leaked_drops(Λ) = ∅ ∧ (¬redistillation(Λ) ∨ every emitted CorrectionDelta is ledger_emit_clean) — no DROP'd item's discriminating content survives in any emitted channel (contract, prose, TaskStateBlock, residual ledger, the activation edge, and — under re-distillation — the correction ledger); the minimality dual of comprehension (F5 catches missing content, this catches leaked DROP content). Stated explicitly for emphasis though already entailed by fixed_point(Λ) (since both |leaked_drops| and |unclean_deltas| ∈ measure), matching the surfaced-ledger and zero-memory-verdict emphasis pattern
single canonical: under re-distillation (Λ.prior_handoff ≠ Null) the emit hygienes that one file in place and appends to its CorrectionDelta ledger — never a supersede-chain sibling; every appended delta satisfies ledger_emit_clean (pointer-clean, positively stated, horizon-grounded). A multi-file handoff fails comprehension (F5)
comprehension: zero_memory_verdict = Pass (a Fail re-enters blocking items as residuals and forces another pass — except when the Rule 27 backstop trips (a candidate embedding unverified authored operative procedure, or a behavior-repair finding on one), which terminates the invocation, nothing entering the ledger; no handoff emits on a Fail)
user_esc: user exits via Esc at the Phase 3 Gate (ungraceful, residual untreated, no PortableHandoff emitted)
progress(Λ) = (pass_n, measure(Λ), |undisposed_authored(Λ)|, zero_memory_verdict) -- a fixed-point distance readout, not a monotone ratio: the measure may rise across a repair pass, so no scalar fraction represents progress; convergence is the fixed_point predicate, never a percentage
── TOOL GROUNDING ──
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
Phase 0 Detect (sense) → Internal analysis (silent — heuristic scan for session-tethered residue; no user output)
Phase 0 declare (observe) → Read, Grep (recipient, next_task, allowed_sources, scope, verification, stop, handoff_durability, emit_target from session context and project config)
Phase 0 bind (track) → Internal state update (Λ.activation_edge = edge(activation_verb? | minimal, contract.emit_target); Λ.now fixed as the invocation timestamp; Λ.ledger bound read-only under DurableRepo, Unknown otherwise; Λ.prior_handoff bound under DurableRepo)
Phase 0 cs-guard (constitution) → present (conditional: competence_substitution(contract, Null, Null) trip — the contract-misfit witness + a proposed recipient-owned-method re-declaration; the user re-declares before Phase 1; the witness question may be discharged upstream by a /gap run on the handoff decision before F0)
Phase 1 normalize (observe) → Read, Grep, Glob (resolve each surface token to a canonical reference; the read-only deictic scan runs as Extension)
Phase 1 audit (sense) → Internal analysis (per-item self-containment classification: inline / stable-pointer / routed-residual)
Phase 2 attest (observe) → Read, Grep, Glob (DurableRepo: read-only consumption of the append-only CorrectionDelta ledger → CorrectedKeep on a matching unexpired KEEP delta. ObservedKeep: read-only confirmation that the item's durable observable source resolves — re-read the file, resolve the url/id, confirm a contract verification_command exists for the recipient — an Extension relay (entropy→0, basis = the cited observable source, no Gate). OneShot/ExternalVersioned: no ledger read; ExternalVersioned records version_ref as the durable provenance pointer. No delta and no observable basis → Unknown → Gate)
Phase 2 dispose (track) → Internal state update (Λ.dispositions, Λ.residual_ledger)
Phase 3 comprehension_gate (observe) → Read, Task (refute-posture review, platform-laddered: the diylisis:zero-memory-refuter subagent where the platform registers plugin agents; a generic fresh subagent carrying the F5 instructions where only generic spawn exists; lint checklist only where no subagent surface exists — a weakened realization that loses fresh-context isolation, named as such in the verdict. Inputs are the candidate handoff text, the contract's recipient profile + next task (including its activation window, against which locator resolvability is judged), the activation edge (verb + locator, reviewed under the minimal admissible edge), and the session-term WatchList enumerated per TYPES — skill/protocol names invoked, subagents dispatched, tools called, plugin/skill names whose instructions are loaded, read from the live session record; author self-simulation excluded)
Phase 3 comprehension_gate (track) → Internal state update (Λ.watchlist recorded at dispatch; parse the verdict: each Findings row → EvidencedFinding with `item` bound by quoted_token + location match — no unique match → synthesize a ContextItem from the finding (origin: AIInference), never drop a row; Fail findings re-enter Λ.residual_ledger as comprehension-gap entries carrying their evidence — EXCEPT operative-procedure findings, which trip the cs-backstop below and never enter the ledger (Rule 27); Λ.zero_memory_verdict set with its sweep trace and realization; a verdict missing the per-category sweep trace or the Realization line is rejected as no verdict → re-dispatch)
Phase 3 cs-backstop (constitution) → present (conditional: competence_substitution(contract, minimal_complete, zero_memory_verdict) — a behavior-repair finding on authored operative procedure; surface the witness + a proposed recipient-owned-method contract; terminate this /distill invocation without emit and hand the proposed contract to the caller for a FRESH invocation (no in-loop restart); never parsed as a comprehension-gap residual)
Phase 3 Qd (constitution) → present (conditional on gate_domain(Λ) ≠ ∅: surfaced residuals + unknown-provenance items + horizon-expired items + disposition conflicts; when gate_domain(Λ) = ∅ — a clean pass — A := None by identity and no gate presents; Esc → loop termination at LOOP level, not an Answer)
Phase 3 repair (track) → Internal state update (F5/Gate repair-authored items appended to Λ.authored, undisposed; timing: within the pass, after the Gate answer, before Phase 4 settle — so the F6 measurement sees them and the loop re-enters; disposed by the next pass's F1–F3 per Rule 25)
Phase 4 settle (track) → Internal state update (measure(Λ) incl. leaked_drops, leak-lint, fixed-point check, pass counter)
Phase 4 leak-repair (track) → Internal state update (performed on ¬fixed_point re-entry when leaked_drops > 0 ∨ unclean_deltas > 0: targeted emit-channel excision/rewrite per LOOP; authored excisions/rewrites enter Λ.authored before the next pass's F1 and are disposed by F1–F3 per Rule 25)
converge (extension) → TextPresent+Proceed (substitution table + disposition trace + surfaced residual ledger + TaskStateBlock + the emitted activation edge; proceed with PortableHandoff — emit is leak_free across every channel incl. the activation edge, recipient ledger recipient-relevant only). Under re-distillation the emit also realizes as Edit/Write: hygiene the one canonical handoff file in place + append each delta to its CorrectionDelta JSONL ledger — a deterministic application of the converged Λ to the existing file (still Extension per A2 Standing authority — the Phase 3 Gate constituted the settled Λ, so the Edit/Write is a deterministic relay of that judgment, not a fresh constitutive act), never a new versioned sibling
── MODE STATE ──
Λ = { phase: Phase, W: WorkingContext,
contract: Option(HandoffContract), -- F0 output; relevance and minimality premise
activation_edge: ActivationEdge, -- F5 fourth input, constructed at Phase 0: declared verb (default minimal) + contract.emit_target as locator (by reference)
pass_n: Nat, -- bounded audit/lint pass counter
ledger: CorrectionDelta_set | Unknown, -- read-only provenance source (F3b consumption); Unknown when absent OR when handoff_durability ≠ DurableRepo (ledger not maintained — Change A)
now: Timestamp, -- invocation constant: bound once at Phase 0 (always, regardless of whether the ledger is maintained), immutable for the invocation; the sole time source for expired(d), so expiry verdicts cannot flip between passes
prior_handoff: Option(StableRef), -- F0-detected existing canonical handoff for the contract; ≠ Null ⇒ re-distillation (in-place hygiene + ledger append, Rule 19) ∧ handoff_durability = DurableRepo (only the durable in-repo case carries a local prior handoff file)
subst_table: SubstTable, -- F1 deictic normalization rows
grounding: Map(ContextItem, Grounding), -- F2 self-containment class per item
provenance: Map(ContextItem, Provenance), -- F3b verdict per item
dispositions: Map(ContextItem, Disposition), -- F3 KEEP/ROUTE/DROP per item
kept: Set(ContextItem), -- F4 minimal-complete retained set
watchlist: WatchList, -- F5 third input, enumerated at Phase 3 dispatch from the live session record (per TYPES WatchList)
routed: Set(ContextItem), -- ROUTE dispositions (StableRef-bound)
dropped: Set(ContextItem), -- DROP dispositions
authored: Set(ContextItem), -- items the author session created during a repair pass (an F5 repair or a leak repair); origin AIInference unless the content is verbatim observed evidence. Re-enters Phase 1 for disposition (Rule 25)
gated: Set(ContextItem), -- items surfaced at the Gate for user judgment (unknown-provenance ∪ horizon-expired ∪ conflict)
residual_ledger: ResidualLedger, -- entries across every reason (unresolved, unknown-provenance, horizon-expired, comprehension-gap); silent entry forbidden
task_state: Option(TaskStateBlock), -- F7 structured channel
emitted_deltas: List(CorrectionDelta), -- re-distillation write side: the CorrectionDelta lines this pass appends to the emitted ledger. Populated at F6 settle as the prospective delta set the converged Λ will write (∅ when ¬redistillation), so the F6 leak lint and the measure leg |unclean_deltas| evaluate it non-vacuously before F7 commits the file write; each must satisfy ledger_emit_clean (pointer-clean, positively stated, horizon-grounded)
measure: Nat, -- F6 hygiene measure (incl. |leaked_drops| and |unclean_deltas|)
zero_memory_verdict: Option(ZeroMemoryVerdict), -- F5 comprehension verdict; Fail re-enters blocking items as residuals and blocks fixed_point (a competence-substitution backstop trip — Rule 27, via an unverified authored operative procedure or a behavior-repair finding — terminates the invocation instead, nothing entering the ledger)
items_touched: Set(ContextItem), -- every item processed: the partition universe (= items(W) ∪ authored once all are disposed)
history: List<(ContextItem, Substitution, Disposition, drop_reason: Option(String))>, -- drop_reason is the typed home for Rule 12's "preserved in Λ.history with its drop reason"; Null for non-DROP entries
active: Bool, cause_tag: String }
-- Invariant: items_touched = kept ∪ routed ∪ dropped (pairwise disjoint) — holds at fixed_point, not as a standing condition — where items_touched = items(W) ∪ authored (the partition universe widened to cover repair-authored content). Mid-loop, repair-authored items sit in Λ.authored undisposed until the next pass's F1–F3 dispose them (undisposed_authored(Λ) measures exactly this gap, and fixed_point requires it to be ∅)
-- terminal partition over Disposition = KEEP | ROUTE | DROP; the Gate answer Defer resolves to a dropped item carrying a re-trigger condition (released from this handoff, not retained)
-- gated is the transient pre-resolution cell, empty at fixed point: every gated item resolves to a terminal disposition (Resolve → KEEP, Route → ROUTE, Drop/Defer → DROP)
-- residual_ledger is a cross-cutting surfacing record, not a partition cell and not emptied: every entry reaches surfaced = true before convergence. The full surfaced ledger is the session-side audit trace (retained in Λ.history); only its recipient-relevant projection (Route-pending) is carried into PortableHandoff. A Drop- or Defer-resolved entry is released from the emit (Defer = released-not-retained per the Defer invariant above; its re-trigger condition is kept session-side) — its content and reason stay session-side — so the emitted handoff never reproduces DROP'd content (enforced by leak_free: leaked_drops = ∅ at fixed point)
-- Invariant: KEEP(item) ⇒ provenance(item) ∈ {CorrectedKeep, ObservedKeep} ∨ user_resolved_at_gate(item) (no KEEP by inference — only via a matching non-provisional CorrectionDelta, a durable observable source with support-integrity, or an explicit user Resolve)
── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). registered dependency edges preserved. Dimension resolution emergent via session context.
F3b composes Elenchus's provenance and freshness tagging plus its Revised | Bounded | Routed disposition vocabulary, and owns the correction-delta ledger that Elenchus does not carry: the ledger (under DurableRepo) is the read-only authority that lets F3b separate a corrected-in-session item (CorrectedKeep → KEEP) from an item KEPT on a durable observable source with support-integrity (ObservedKeep → KEEP, the common-case relay) and from an item whose provenance is genuinely undecided (Unknown → Gate).
F5 reuses the comprehension structure of a result-grasp check, redirected: the recipient under verification is a fresh executor with no session access, not the author, so the gate excludes author self-simulation (which would pass items the author silently shares).
F2 may call an external-reference check (request/ground style) when a grounding pointer's target needs verification; the self-containment audit itself stays inline.
Core Principle
Portability over Author Familiarity: A working session's context window accumulates session-tethered residue — undefined jargon, metric shorthand, author process traces, tool state, and dangling task identifiers — that reads as complete to the author because the author silently shares the missing context. A fresh recipient with no session access has none of that shared ground. Diylisis distills the working context into a handoff whose every load-bearing reference resolves without the author session: each deictic token is normalized to a canonical reference, each item is audited for self-containment, each disposition is judged against the declared recipient and its transformation provenance, and the residue that cannot be resolved is surfaced rather than silently carried. The handoff is portable when the author's familiarity is no longer a hidden dependency.
Mode Activation
Activation
AI detects session-tethered residue before a handoff OR the user calls /distill. Detection is silent (Phase 0); residual and disposition-conflict judgment always requires user interaction via Cognitive Partnership Move (Constitution) (Phase 3).
Activation layers:
- Layer 1 (User-invocable):
/distill slash command or description-matching input. Always available.
- Layer 2 (AI-guided): Session-tethered residue detected before a context handoff (writing a handoff brief, spawning a fresh-context subagent, preparing a plan a new session will resume). Detection is silent (Phase 0).
Context tethered = the working context carries references whose resolution depends on the author session — undefined jargon, metric tokens, "as above"-style anchors, author process narration, or task identifiers that do not transfer to a fresh session.
Gate predicate:
context_tethered(W) ≡ ∃ item(i, W) : depends_on_author_session(i) ∧ ¬resolvable_by_stable_ref(i)
Boundary (contextualize ↔ distill): distill closes a portability gap to an absent zero-memory recipient — it reads the source immutably (monotone) and builds a new self-contained artifact, preserving the source. When the deficit is instead fit to an observable present context (a correct result that mutates to fit a convention, environment, or audience — ApplicationDecontextualized, non-monotone), it is not a distill case → route to /contextualize. This is the complement of contextualize's portability-to-an-absent-recipient → /distill guard.
Priority
When Diylisis is active:
Supersedes: Direct handoff patterns that ship the working context as-is
(A handoff must be distilled to a self-contained portable form before it transfers; author-shared context that the recipient cannot resolve is normalized, routed, or surfaced first)
Retained: Safety boundaries, tool restrictions, user explicit instructions
Action: At Phase 3, present surfaced residuals, unknown-provenance items, horizon-expired items, and disposition conflicts for user judgment via Cognitive Partnership Move (Constitution).
- Diylisis completes before the handoff transfers to a fresh recipient
- Loaded instructions resume after the PortableHandoff is emitted, the competence-substitution backstop gracefully terminates the invocation (Rule 27), or Esc
Trigger Signals
Heuristic signals for session-tethered residue detection (not hard gates):
| Signal | Inference |
|---|
| Undefined jargon or metric token | A term carries meaning only in the author session (a versioned label, a metric shorthand, a coined name) |
| Deictic anchor | "As above", "the earlier one", "that file", "this approach" — references resolved by session position, not by stable reference |
| Author process narration | Instructions that describe the author's own session workflow rather than the recipient's task |
| Dangling task identifier | A task id referenced without the data a fresh session needs to restore it |
| Fresh-recipient handoff imminent | A handoff brief, subagent dispatch, or resumable plan is being prepared for a session with no shared context |
Skip:
- The working context is already self-contained — every load-bearing reference resolves by stable reference
- The recipient shares the author session (same continuous context), so no portability gap exists
- User explicitly says the residue is acceptable for the intended recipient
- Phase 0 detection finds no session-tethered residue
- The deficit is fit to an observable present context (a correct result that may not fit the convention, environment, or audience where it is applied —
ApplicationDecontextualized), NOT portability to an absent zero-memory recipient → route to /contextualize (the contextualize ↔ distill boundary). Demarcation: target-context observability (observable present context → /contextualize; absent zero-memory recipient → distill), transform-target (the result mutates to fit → /contextualize; the source is preserved and a new portable artifact is built → distill), and monotonicity (non-monotone, mutation breeds new mismatches → /contextualize; monotone, read-only of the source → distill)
- Stripping secrets (credentials, tokens, keys) from the working context —
/distill assumes a secret-free working context; secret redaction is a separate concern handled upstream by a dedicated redaction agent, not part of the distill morphism.
Mode Deactivation
| Trigger | Effect |
|---|
| Fixed point reached with every residual surfaced | Emit PortableHandoff across the prose channel and the schema-versioned TaskStateBlock (plus the appended correction ledger under re-distillation) |
| User Esc at the Phase 3 Gate | Return to normal operation; residual untreated, no PortableHandoff emitted |
| Phase 0 detection finds no residue | Deactivate — silently when AI-detected (Layer 2); with a one-line "already portable" acknowledgment when explicitly invoked via /distill (Layer 1) |
| Competence-substitution backstop trips at F5 (Rule 27) | Terminate this /distill invocation without emitting; surface the witness + a proposed recipient-owned-method contract, which the caller carries into a FRESH invocation — a graceful terminal, distinct from the Esc row above |
Protocol
Phase 0: Tethered Detection + Contract Declaration
Verify the working context carries session-tethered residue, then declare the handoff contract. Detection is silent; contract declaration is the first user-visible step when residue is present.
- Detect residue — scan the working context for session-tethered references: undefined jargon, metric tokens, deictic anchors, author process narration, dangling task identifiers. The scan itself is silent. If none are present, deactivate — silently when the scan was AI-initiated (Layer 2 auto-detection), or with a one-line "already portable" acknowledgment when the user explicitly invoked
/distill (Layer 1).
- Declare F0 HandoffContract — fix the recipient profile — its knowledge isolation (default zero-memory) and its activation window (
Immediate | Bounded(d) | Unbounded; default Unbounded, the conservative absent-recipient window, and constrained to Unbounded whenever handoff_durability = DurableRepo) — the next task, the allowed sources (stable references the recipient may read), the execution scope, the verification commands, the stop condition, the handoff durability (Change A), and the emit target — the locator where the canonical handoff will land, the noun the activation edge references. The activation window sets when the recipient reads and acts on the handoff relative to the author session's lifetime, and locator resolvability (resolves_at, Rule 21) is judged throughout it: an immediately-dispatched zero-memory subagent reading while the author session is alive resolves a temp-rooted locator that an absent later recipient could not. The contract is the premise every later phase reads: without a declared next task, recipient-relevance (F3a) and minimality (F4) are undefined. When the next task is absent from the working context, elicit it before proceeding. Classify handoff_durability by the handoff's target and lifetime:
- OneShot — a temporary / one-shot handoff (a brief, a subagent dispatch, a plan used once and never re-distilled). No correction ledger is maintained: a one-shot handoff has no future consumer for a correction record, so the ledger machinery is pure overhead. A correction-requiring claim surfaces at the Gate (user Resolve), never as CorrectedKeep.
- ExternalVersioned — the handoff lands in an externally-versioned store (a Notion page, a Linear issue, or any store whose native history versions the artifact). Defer provenance to that native history: no internal correction ledger is maintained, and the external version handle is recorded in the contract as
version_ref — the contract-level provenance pointer the recipient (and a later distill) reads. A corrected value lives in the store's native history; an item grounded in a durable stable pointer to that store re-observes the current corrected value, so it reads as ObservedKeep on its own observable basis, never CorrectedKeep (no local ledger).
- DurableRepo — a durable, re-distilled in-repo handoff (the case the CorrectionDelta ledger was designed for). The full ledger and the re-distillation discipline (Rule 19) apply. This is the only mode in which CorrectedKeep is reachable.
