Verify understanding after AI work through intent-scented entry points. Type: (ResultUngrasped, User, VERIFY, Result) → VerifiedUnderstanding. Alias: Katalepsis(κατάληψις).
---
name: grasp
description: "Something in play — code, a document, a result — the user can't follow yet or nods along to unsure: they can then say their understanding serves their purpose, on a map checked with them."
---
# Katalepsis Protocol
Achieve certain comprehension of a target in play — code, a document, a result — through structured verification, enabling the user to grasp what stands ungrasped. Type: `(TargetUngrasped, User, VERIFY, Target) → VerifiedUnderstanding`.
## Definition
**Katalepsis** (κατάληψις): A dialogical act of achieving firm comprehension—from Stoic philosophy meaning "a grasping firmly"—resolving an ungrasped target into verified user understanding through a map of understanding built with the person and checked against the target's material and the results looked at together.
```lean
/-!
How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is
written for: you read it, and by inference over the context you settle each element it leaves
open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from
the material in front of you; its doc comment says what you judge there, and nothing in this
block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract.
-/
/-! ── FLOW ──
Katalepsis(R) → start(c) → grasp(c, utterances), where c is the fused session context:
present(c): the map and the next round, read afresh from the context
next utterance u, read on fuse(c, u) →
[the utterance does not bear on this run] the session answers it; that answer stays in the
context; nothing is consulted; no round of this run
[the person closes (ClosureSupported)] → VerifiedUnderstanding
[otherwise] c' := fuse(c, u) with what `consult` reads now appended, a check's result
included → present(c')
no utterance: nothing is taken; the run holds
-/
/-! ── MORPHISM ──
Target
→ gather -- the target's material and the sources that bear on it, read now (focus)
→ check -- a check handed to execution as `.check` says, before each round; its result returns through `consult`
→ map -- the purpose the person said (`ScopeSupported`), else your reading of it marked as yours; the aspects it turns on, each with what it rests on (focus)
→ present -- the map's changes and the next round, with its material (focus)
→ fuse(u) -- the person's turn joins the context whole
→ close -- the person's closure over the map (`ClosureSupported`)
→ VerifiedUnderstanding
requires: target_exists(R) -- the comprehension target is present in context and can be quoted verbatim; its provenance is unconstrained. An admission condition on the target, not a promise that every reading finds material that bears on it
deficit: TargetUngrasped -- activation precondition (Layer 1)
preserves: R -- this run reads the target and never rewrites it; a check changes no existing state; a change to the target is the session's other work
invariant: Grounded, not asserted -- every aspect on the map says what it rests on; your explanation is never shown as the person's understanding
invariant: Focus never records -- the map and the presentation are re-read every turn and carry no authority; only the person's turns move a value the person holds, and an observed result moves only what it observed
-/
namespace Katalepsis
/-! ── GROUND ──
The session primitive this contract reads.
-/
inductive Origin | person | assistant | external | peer | injected | unknown
deriving DecidableEq
/-- A turn is who sent it and what it says. What the turn does — a statement, a request, an
instruction, a report of what was observed — is read from its content, never stored here. -/
structure Turn (P : Type) where
origin : Origin
content : P
abbrev Context (P : Type) := List (Turn P)
/-- An origin that may ground: the harness says who sent a turn, and that is all this admits on.
The assistant's own turns, injected text, and turns of unknown origin ground nothing. -/
def Grounding := {o : Origin // o ≠ .assistant ∧ o ≠ .injected ∧ o ≠ .unknown}
/-- Any turn a person sent, whatever it does. -/
def Utterance (P : Type) := {e : Turn P // e.origin = .person}
def Response (P : Type) := {e : Turn P // e.origin = .assistant}
/-- A turn from outside the conversation: what a tool or the environment returned, or a peer's
report. A person's account of what they observed is an utterance, read as such. -/
def Evidence (P : Type) := {e : Turn P // e.origin = .external ∨ e.origin = .peer}
def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]
/-- One turn of the context, with the origin it grounds on. -/
structure Cite {P : Type} (c : Context P) where
idx : Nat
lt : idx < c.length
src : Grounding
ok : (c[idx]'lt).origin = src.val
/-- `admits` reads only who sent the cited turn; `supports` is the model's reading of what that
turn says, including what it does — a statement, a request, a report of an observation. -/
structure Coord (P A : Type) where
admits : Grounding → Prop
supports : Context P → Turn P → A → Prop
/-- `open_` may carry a candidate citation whose support is still short. -/
inductive Occ {P A : Type} (q : Coord P A) (c : Context P)
| open_ (candidate : Option (Cite c))
| filled (a : A) (src : Cite c) (allowed : q.admits src.src)
(supported : q.supports c (c[src.idx]'src.lt) a)
/-- The same turn, cited from a longer context; what it supports is judged again against the
context that now stands. -/
def Cite.lift {P : Type} {c : Context P} (s : Cite c) (t : Context P) : Cite (c ++ t) :=
{ idx := s.idx
lt := by have := s.lt; simp; omega
src := s.src
ok := by rw [List.getElem_append_left s.lt]; exact s.ok }
/-! ── TYPES ── -/
noncomputable section
variable {P : Type}
/-- `R`, the target: material present in the context and quotable verbatim — code, a document, a
result — whatever produced it. Read from the context; this run never rewrites it. -/
abbrev Target (P : Type) := Context P
/-- A purpose or an aspect, named as the map shows it. -/
abbrev Entry := String
/-- **Your judgment**: the cited person turn says what they mean to understand of the target —
and, where they say it, for what purpose — read against the context as it now stands, in their
own words, by taking the reading of their purpose the map showed, or by handing the choice to
you. Taking what was shown adopts it as it was shown; handing the choice to you lets you set it
within the target, and the map says what you set, as yours, open to their correction. The
invoking utterance fills it when it says it. A later turn may change the scope; whether an
earlier one still reaches what is now at issue is read on the current context. -/
axiom ScopeSupported : Context P → Turn P → Entry → Prop
/-- Only a person's turn sets the scope. -/
def scopeCoord : Coord P Entry :=
{ admits := (·.val = .person), supports := ScopeSupported }
/-- **Your reading**: the scope as it stands in `c` — filled by the person's latest turn that sets
it; `open_` until one does. -/
axiom scope : (c : Context P) → Occ (scopeCoord (P := P)) c
def isFilled {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Bool
| .open_ _ => false
| .filled .. => true
/-- **Your judgment**, the live inventory: every aspect of the target this run has raised for the
purpose — what the purpose turns on, a contradiction, an edge the person has not voiced alike.
An aspect raised once stays here — whether or not the current round shows it, and even when a
later scope no longer turns on it, marked so; a set-aside aspect stays too. The person may
merge or reword aspects; whether a reworded aspect is the same aspect is your judgment.
Guidance for the reading, not types it fixes: a Horizon edge is an edge of what the target
does that the person has not voiced and the purpose needs, raised openly like any other aspect
where the target's material grounds it — not a decision to make, a reframing, or a choice of
route, though understanding it may change how the person frames their purpose. A contradiction
needs two distinct sourced sides on the same scope and premises; a repeated claim, the target
and your quotation of it, or your explanation drawn from it is one side, not corroboration. -/
axiom aspects : Context P → List Entry
/-- A located span of one turn. -/
structure Side (c : Context P) where
idx : Nat
lt : idx < c.length
span : String
/-- **Your judgment**: the located turn carries the target itself, at the quoted span, rather than
the reasoning that produced it. Target provenance is unrestricted; where the turn is your own,
whether it carries the target or reasoning about it is read here from its content. -/
axiom IsTarget : (c : Context P) → Side c → Prop
/-- **Your judgment**: the cited turn carries what a source read or a check run returned in this
run, and the span is the narrowest returned material supporting the judgment, quoted in place.
A locator the person must go open is not the material. -/
axiom SourceRead : (c : Context P) → Cite c → String → Prop
/-- What a fact rests on: the target's own material, in the turn quoted even after the target
changes, or what a source or a check returned in this run. Your own reasoning is never
material, nor another agent's — a peer turn counts only as what a source it read or a check it
ran returned. -/
inductive Material (c : Context P)
| target (s : Side c) (object : IsTarget c s)
| source (observed : Cite c) (span : String) (linked : SourceRead c observed span)
/-- **Your judgment**: the material bears on aspect `a` — what the target does there, read on the
context as it now stands; it may be that it settles nothing. A fact is about the target, never
about the person. -/
axiom FactSupported : (c : Context P) → Material c → Entry → Prop
/-- A fact on aspect `a`: the material, with its support. -/
structure Fact (c : Context P) (a : Entry) where
material : Material c
supported : FactSupported c material a
/-- **Your judgment**, the record rule: the cited person turn says what they understand of aspect
`a` — a reading of their own, producing, applying, predicting, or explaining its relations at
the level the aspect asks, or an acknowledgment of your explanation, which is acceptance of it
and never a reading of their own — read against the context as it now stands. A self-rating, a
bare pick among options you offered, or an echo of your own wording is neither; an explanatory
paraphrase reaches what it reaches. -/
axiom ReadingSupported : (c : Context P) → Cite c → Entry → Prop
/-- What the person has said of aspect `a`: the turn, with its support. -/
structure Reading (c : Context P) (a : Entry) where
src : Cite c
byPerson : src.src.val = .person
supported : ReadingSupported c src a
/-- An aspect's row on the map, on two axes kept apart: what the target does there — its facts,
each with the material it rests on, and what is still open on it, as CONVERGENCE lists — and
what the person has said of it. The reading stays theirs until their own turn changes it.
Both are your judgment from the context, and nothing on the row is stored. -/
structure Cell (c : Context P) (a : Entry) where
facts : List (Fact c a)
reading : Option (Reading c a)
/-- **Your reading**: aspect `a`'s row, read afresh on `c`; whether a turn bears on a reworded
aspect is your judgment. Where several person turns give a reading, which one stands is read
on the current context; a later turn of the person's may replace it or take it back. -/
axiom cell : (c : Context P) → (a : Entry) → Cell c a
/-- The map: every aspect of the live inventory, with its row. -/
def map (c : Context P) : List ((a : Entry) × Cell c a) :=
(aspects c).map fun a => ⟨a, cell c a⟩
/-- **Your record**: your contrary grounds bearing on the person's judgment, each with what it
bears on and what it rests on, shown as `present` and CONVERGENCE say. Empty when there are
none. -/
axiom dissent : Context P → List String
/-- **Your judgment**: the latest utterance bears on this run — a purpose, a reading of the target,
an acknowledgment, a wish to see or try something, a request for more depth, a correction of
your reading, a question about the map, a closure — judged on what the whole utterance does,
read on the context with it before anything is consulted. An utterance about other work leaves
the run as it stands: the session answers it, that answer stays in the context, and no round of
this run is drawn. Words that end the run without saying that what they understand serves
their purpose do not bear on it, whatever else the turn says, and what else it says stands in
its own words in the context: the session answers them, no round is drawn, the run holds, and
later turns bear on it only where they come back to it; your own reading that the person is done
ends nothing. Where a turn taken as other work or as ending the run could also be read as the
other, as saying what they understand serves their purpose, or as bearing on the run otherwise,
the session's answer says briefly how it took it. -/
axiom Reaches : Context P → Prop
/-- **Your judgment**: the cited turn — the latest utterance; a turn before the latest round closes
nothing — says that what they now understand of the target serves their purpose, read on the
context as it now stands. An acknowledgment of an explanation is not that. Where the turn's
intent is unclear, it closes nothing. Nothing on the map, nor your own reading, closes it, and
nothing on the map holds the closure back. Setting one aspect aside does not close the run; a
set-aside aspect stays on the map as it stood. -/
axiom ClosureSupported : Context P → Turn P → Unit → Prop
/-- Only the person closes the run. -/
def closureCoord : Coord P Unit :=
{ admits := (·.val = .person), supports := ClosureSupported }
/-- **Your reading**: the person's closure; `open_` until one reaches it. -/
axiom closure : (c : Context P) → Occ (closureCoord (P := P)) c
/-- The record the closure carries, as CONVERGENCE lists it. -/
structure Closed (P : Type) where
context : Context P
scope : Occ (scopeCoord (P := P)) context
map : List ((a : Entry) × Cell context a)
dissent : List String
def closed (c : Context P) : Closed P :=
{ context := c, scope := scope c, map := map c, dissent := dissent c }
/-- Once it has run, the person can say: what I now understand of this target serves my purpose —
I saw it on a map built with me and checked against the target's material and the results we
looked at together, and for what still waits on a check, I know what would settle it.
`VerifiedUnderstanding`: the person's closure over the map CONVERGENCE lists — what each
aspect rests on, as they saw it when they closed. It records that closure, not a certificate
of what was demonstrated, nor omniscient comprehension. -/
structure VerifiedUnderstanding (P : Type) where
closure : Closed P
inductive Outcome (P : Type)
| verified (r : VerifiedUnderstanding P)
| holding (c : Context P)
/-- **Your judgment**: a check within your reach runs now — the latest utterance, bearing on this
run, asks for one (a wish to see or try something); or you run one
yourself, as TOOL GROUNDING's `present` entry says. Read on the context as it now stands, what
`gathered` returned included. -/
axiom CheckRuns : Context P → Prop
/-- **Your read**, now, of what the next judgment needs: the target's material and the sources that
bear on it — any a turn cites, and any you find — as far as relevant access reaches. What you
say you read, you read to the end. Empty where nothing outside the context bears. -/
axiom gathered : Context P → List (Evidence P)
/-- **Your read**, now: what the check handed off at `.check` returned — a run, an experiment, a
source read to settle it. -/
axiom checked : Context P → List (Evidence P)
/-- The context with what `gathered` read now appended. -/
def withGathered (c : Context P) : Context P := c ++ (gathered c).map (·.val)
open Classical in
/-- What is read now: what is gathered, and then what the check returned where `CheckRuns` holds
on the context with it, as `consultOps` hands it off. -/
def consult (c : Context P) : List (Evidence P) :=
gathered c ++ (if CheckRuns (withGathered c) then checked (withGathered c) else [])
/-- The context with what `consult` read now appended. -/
def consulted (c : Context P) : Context P := c ++ (consult c).map (·.val)
/-! ── A-BINDING ──
bind(R) = the target the argument names, else the target most recently in play; words in the
invocation that say what to understand of it fill the scope (`ScopeSupported`).
-/
/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it.
-/
/-! ── PHASE TRANSITIONS ──
A step is one arm of a structural recursion over the person's utterances. `respond` is the next
round, as TOOL GROUNDING's `present` entry names it; `session` is the session's own answer to an
utterance that does not bear on the run, which stays in the context without being a round of this
run.
-/
open Classical in
def grasp (respond session : Context P → Response P) :
Context P → List (Utterance P) → Outcome P
| c, [] => .holding c
| c, u :: us =>
let f := fuse c u
if ¬ Reaches f then grasp respond session (f ++ [(session f).val]) us
else if isFilled (closure f) = true then .verified ⟨closed f⟩
else
let c' := consulted f
grasp respond session (c' ++ [(respond c').val]) us
/-- The run opens on a gathering and its first round. -/
def start (respond session : Context P → Response P) (c : Context P)
(us : List (Utterance P)) : Outcome P :=
grasp respond session (consulted c ++ [(respond (consulted c)).val]) us
/-! ── LOOP ──
Every answer is read against the whole context as it now stands: nothing counts rounds, and no
earlier answer is held apart from what later ones say. No fixed cap: each round is dialogue.
-/
/-! ── CONVERGENCE ──
converged: a VerifiedUnderstanding the person's utterance closed; holding is a run no turn of the
person's has closed. The convergence evidence — the map at closure: each aspect on its two axes,
its facts (each with the material it rests on; each check run, with what it showed and, where it
ran on a stand-in, what it left untested), what is still open on it (each check named and not run,
with what it would settle and what running it needs; where no material bears on it, that, with what
would settle it), and what
the person has said of it (their own reading in their words, the facts beside it agreeing or
parting; acceptance of your explanation where that is what they gave; or nothing yet), whether the
scope as it stands still turns on it, and whether its facts were read, or the person's reading
given, on a version of the target that has since changed; the
purpose and scope as they stand, open included, and marked as yours where you read or set it; what
could not be reached that bears on an aspect; the dissent — a contrary ground not shown before the
closing turn is shown here, and the closure stands. Grounded, not asserted.
-/
/-! ── TOOL GROUNDING ──
What each operation of this contract does. An interaction with the person is one of two kinds,
and its kind fixes how it continues once its text is presented. A Constitution settles a judgment
through the person's turn. An Extension settles none for the person: it passes on a result its
cited ground fixes, or carries reversible work forward on a judgment the AI states, which stays
the AI's proposal until the person takes it. Beyond the Constitution operations a contract
annotates, whether work goes forward this way or waits for the person's answer is the AI's
judgment in the situation, and work that cannot be undone waits for the authorization it needs.
Work carried forward, on a grant or a stated judgment or as clear work, returns with an account
of how the request was read, what was judged on what basis — naming an alternative set aside
where it may be preferred — and how far the work went.
-/
inductive Interaction | constitution | extension
inductive Continuation | stop | proceed
inductive Annot | sense | observe | track | transform | dispatch | interaction (kind : Interaction)
/-- Every interaction presents its text; a Constitution then stops for the person's turn, and an
Extension proceeds. -/
def Interaction.realization : Interaction → Continuation
| .constitution => .stop
| .extension => .proceed
inductive Op | gather | assess | present | check | readAnswer | converge
def grounding : Op → Annot × String
| .gather => (.observe, "artifact read, artifact search: read-only reads as `gathered` states; name what was reached and what was not, and any conflict among what was gathered")
| .assess => (.sense, "Internal analysis: the purpose reading, the live inventory of aspects and each one's row on the map, over the whole fused context as it now stands")
| .present => (.interaction .extension, "the round, every round the first included. The first round is the map: the purpose as the person said it, or else your reading of it, marked as yours — where nothing grounds a useful reading, the target's main aspects, with the purpose line saying so; the aspects the purpose turns on, in the order it turns on them with that basis on the purpose line, an edge the person has not voiced among them where the material grounds one, each with its essence, its facts with the material they rest on, and the person's reading where they have given one; and your contrary grounds with their basis. A correction of the purpose moves the map. Where the session has a surface that stays in view, the map can stay there as well. A contrary ground you hold stays in view until it is settled — on the surface that stays in view where the session has one, otherwise briefly beside each round. Explain each aspect in the one representation — a picture, an example, a metaphor — that best carries its essence for this person; leave out what their words show they know, and go deeper when they ask. Read the person's turn whole; where its intent was unclear, say in one line how you took it. The round that shows a check's result sets it beside the aspect and against the claim your explanation made, saying where it agrees and where it parts; the result is what the map's facts are filled from, and the comparison with your explanation is said in the round, never recorded as a fact. Before setting their words against a fact, read whether they aim at another purpose: say that reading as a candidate with its basis and move the map, adding no question; if the person sets it aside, their words are read again as a reading of the target. Where a reading or application of their own says what the target does, set the facts that bear on it beside it, saying where each agrees and where it parts; where no material bears on it, say so and name what would settle it. Where what they said and a fact part on the same scope and premises, or two of their own utterances do, show it with its working in one round: their words quoted; the narrowest material where it bears on it, never your own explanation — scoped to what that material settles; why the two part; where their words and the material agree; and another reading beside it where the material allows. A contradiction whose working was shown and that the person keeps stays in view as a held contrary ground, and the round ends on its opening. A contradiction inside the target is a finding about it, judged for a side only with settling material outside it; your own earlier explanation against a fact is yours to correct, quoting it, as relay. An objection you raise yourself is relay: shown with its basis, and the run continues. Where what you could not reach, or a conflict among what you gathered, bears on an aspect or on a judgment the person is making, say it there. Where a check within your reach would show what the target does on an aspect the purpose turns on — where a reading of the person's own says what it does included — run the cheapest that would show it before the round — as far as your reach goes, what the purpose turns on most first; a check out of your reach is an offer, with what running it needs — never a question for them to answer. An aspect the person set aside is not explained again, nor a check raised on it, unless they return to it. Other work in the utterance neither closes this run nor answers its judgments. A round that shows a contradiction's working ends on that working, with nothing after it; every other round ends on one opening the person can take — respond to the map, ask to see or try something, go on, or say that what they understand now serves their purpose.")
| .check => (.dispatch, "delegate: where `CheckRuns` holds, the check handed to execution with the aspect and what it is to show; it changes no existing state — what it has to write goes to a scratch space outside the target's tree, and what it created only to look is removed afterwards — and a result from a stand-in comes with what it stood for and what it left untested; what it returns enters the context through `consult` as evidence read now, before the round that shows it")
| .readAnswer => (.sense, "Internal analysis: whether the latest utterance bears on this run and what it does there, as `Reaches` and the judgments above read it — read whole against the fused context as it now stands")
| .converge => (.interaction .extension, "the convergence evidence CONVERGENCE names; proceed with VerifiedUnderstanding")
open Classical in
/-- The operations whose returns `consult` appends to the context: what `.gather` reads, and, where
`CheckRuns` holds once it is read, what the check handed off at `.check` returns. -/
def consultOps (c : Context P) : List Op :=
if CheckRuns (withGathered c) then [.gather, .check] else [.gather]
/-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Dimension resolution emergent via session context.
-/
end
end Katalepsis
```
## Mode Activation
`/grasp` is user-invoked only: activate when the user signals a wish to understand a target already present in context and available for verbatim quotation, whatever its provenance — AI-produced work, code or a document someone else wrote, or material the session has put on the table; a bare command refers to the current target. Do not activate for an unrelated general question, an accurate account that already demonstrates understanding, an explicit decline, or a trivial formatting-only result.
## Protocol
### Map rendering
Label each row by what the person will understand or decide through it, and keep the target's anchors — code, plan, document, analysis, model, or a mix — beside the label, its facts and the person's reading said in words.
### Verification rendering and safeguards
Compose each round under TOOL GROUNDING's `present` entry. When grounding an explanation or correction, cite concrete locations in the target — file and line where it is code, the equivalent anchor where it is not. Read `references/round-composition.md` before composing when terminology must remain stable, wording must be carried unchanged, content belongs to another round or the convergence evidence, or whether text belongs before or inside the round's opening is in question.
## Rules
- **User-initiated only**: Activate only on the user's wish to understand a target present in context and quotable, whatever produced it; an explicit decline before activation withholds it.
- **User authority**: An acknowledgment of your explanation stands as the person's judgment; a factual disagreement or new evidence is shown beside it.
- **Round composition**: Compose each round so the reader can act without reassembly — use everyday language, keep each judgment beside its evidence and next-move implication (a fact set beside their reading included, its evidence being the excerpt attached with it), and place analytical context before the round's opening.
- **Form feedback**: Derive each round's density from the current request; carry an explicit form instruction until countermanded. Change form directly. Elements fixed elsewhere remain fixed; state what changed and, where the instruction overlaps a fixed element, what stays and why.
---
name: grasp
description: "Something in play — code, a document, a result — the user can't follow yet or nods along to unsure: they can then say their understanding serves their purpose, on a map checked with them."
---
# Katalepsis Protocol
Achieve certain comprehension of a target in play — code, a document, a result — through structured verification, enabling the user to grasp what stands ungrasped. Type: `(TargetUngrasped, User, VERIFY, Target) → VerifiedUnderstanding`.
## Definition
**Katalepsis** (κατάληψις): A dialogical act of achieving firm comprehension—from Stoic philosophy meaning "a grasping firmly"—resolving an ungrasped target into verified user understanding through a map of understanding built with the person and checked against the target's material and the results looked at together.
```lean
/-!
How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is
written for: you read it, and by inference over the context you settle each element it leaves
open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from
the material in front of you; its doc comment says what you judge there, and nothing in this
block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract.
-/
/-! ── FLOW ──
Katalepsis(R) → start(c) → grasp(c, utterances), where c is the fused session context:
present(c): the map and the next round, read afresh from the context
next utterance u, read on fuse(c, u) →
[the utterance does not bear on this run] the session answers it; that answer stays in the
context; nothing is consulted; no round of this run
[the person closes (ClosureSupported)] → VerifiedUnderstanding
[otherwise] c' := fuse(c, u) with what `consult` reads now appended, a check's result
included → present(c')
no utterance: nothing is taken; the run holds
-/
/-! ── MORPHISM ──
Target
→ gather -- the target's material and the sources that bear on it, read now (focus)
→ check -- a check handed to execution as `.check` says, before each round; its result returns through `consult`
→ map -- the purpose the person said (`ScopeSupported`), else your reading of it marked as yours; the aspects it turns on, each with what it rests on (focus)
→ present -- the map's changes and the next round, with its material (focus)
→ fuse(u) -- the person's turn joins the context whole
→ close -- the person's closure over the map (`ClosureSupported`)
→ VerifiedUnderstanding
requires: target_exists(R) -- the comprehension target is present in context and can be quoted verbatim; its provenance is unconstrained. An admission condition on the target, not a promise that every reading finds material that bears on it
deficit: TargetUngrasped -- activation precondition (Layer 1)
preserves: R -- this run reads the target and never rewrites it; a check changes no existing state; a change to the target is the session's other work
invariant: Grounded, not asserted -- every aspect on the map says what it rests on; your explanation is never shown as the person's understanding
invariant: Focus never records -- the map and the presentation are re-read every turn and carry no authority; only the person's turns move a value the person holds, and an observed result moves only what it observed
-/
namespace Katalepsis
/-! ── GROUND ──
The session primitive this contract reads.
-/
inductive Origin | person | assistant | external | peer | injected | unknown
deriving DecidableEq
/-- A turn is who sent it and what it says. What the turn does — a statement, a request, an
instruction, a report of what was observed — is read from its content, never stored here. -/
structure Turn (P : Type) where
origin : Origin
content : P
abbrev Context (P : Type) := List (Turn P)
/-- An origin that may ground: the harness says who sent a turn, and that is all this admits on.
The assistant's own turns, injected text, and turns of unknown origin ground nothing. -/
def Grounding := {o : Origin // o ≠ .assistant ∧ o ≠ .injected ∧ o ≠ .unknown}
/-- Any turn a person sent, whatever it does. -/
def Utterance (P : Type) := {e : Turn P // e.origin = .person}
def Response (P : Type) := {e : Turn P // e.origin = .assistant}
/-- A turn from outside the conversation: what a tool or the environment returned, or a peer's
report. A person's account of what they observed is an utterance, read as such. -/
def Evidence (P : Type) := {e : Turn P // e.origin = .external ∨ e.origin = .peer}
def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]
/-- One turn of the context, with the origin it grounds on. -/
structure Cite {P : Type} (c : Context P) where
idx : Nat
lt : idx < c.length
src : Grounding
ok : (c[idx]'lt).origin = src.val
/-- `admits` reads only who sent the cited turn; `supports` is the model's reading of what that
turn says, including what it does — a statement, a request, a report of an observation. -/
structure Coord (P A : Type) where
admits : Grounding → Prop
supports : Context P → Turn P → A → Prop
/-- `open_` may carry a candidate citation whose support is still short. -/
inductive Occ {P A : Type} (q : Coord P A) (c : Context P)
| open_ (candidate : Option (Cite c))
| filled (a : A) (src : Cite c) (allowed : q.admits src.src)
(supported : q.supports c (c[src.idx]'src.lt) a)
/-- The same turn, cited from a longer context; what it supports is judged again against the
context that now stands. -/
def Cite.lift {P : Type} {c : Context P} (s : Cite c) (t : Context P) : Cite (c ++ t) :=
{ idx := s.idx
lt := by have := s.lt; simp; omega
src := s.src
ok := by rw [List.getElem_append_left s.lt]; exact s.ok }
/-! ── TYPES ── -/
noncomputable section
variable {P : Type}
/-- `R`, the target: material present in the context and quotable verbatim — code, a document, a
result — whatever produced it. Read from the context; this run never rewrites it. -/
abbrev Target (P : Type) := Context P
/-- A purpose or an aspect, named as the map shows it. -/
abbrev Entry := String
/-- **Your judgment**: the cited person turn says what they mean to understand of the target —
and, where they say it, for what purpose — read against the context as it now stands, in their
own words, by taking the reading of their purpose the map showed, or by handing the choice to
you. Taking what was shown adopts it as it was shown; handing the choice to you lets you set it
within the target, and the map says what you set, as yours, open to their correction. The
invoking utterance fills it when it says it. A later turn may change the scope; whether an
earlier one still reaches what is now at issue is read on the current context. -/
axiom ScopeSupported : Context P → Turn P → Entry → Prop
/-- Only a person's turn sets the scope. -/
def scopeCoord : Coord P Entry :=
{ admits := (·.val = .person), supports := ScopeSupported }
/-- **Your reading**: the scope as it stands in `c` — filled by the person's latest turn that sets
it; `open_` until one does. -/
axiom scope : (c : Context P) → Occ (scopeCoord (P := P)) c
def isFilled {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Bool
| .open_ _ => false
| .filled .. => true
/-- **Your judgment**, the live inventory: every aspect of the target this run has raised for the
purpose — what the purpose turns on, a contradiction, an edge the person has not voiced alike.
An aspect raised once stays here — whether or not the current round shows it, and even when a
later scope no longer turns on it, marked so; a set-aside aspect stays too. The person may
merge or reword aspects; whether a reworded aspect is the same aspect is your judgment.
Guidance for the reading, not types it fixes: a Horizon edge is an edge of what the target
does that the person has not voiced and the purpose needs, raised openly like any other aspect
where the target's material grounds it — not a decision to make, a reframing, or a choice of
route, though understanding it may change how the person frames their purpose. A contradiction
needs two distinct sourced sides on the same scope and premises; a repeated claim, the target
and your quotation of it, or your explanation drawn from it is one side, not corroboration. -/
axiom aspects : Context P → List Entry
/-- A located span of one turn. -/
structure Side (c : Context P) where
idx : Nat
lt : idx < c.length
span : String
/-- **Your judgment**: the located turn carries the target itself, at the quoted span, rather than
the reasoning that produced it. Target provenance is unrestricted; where the turn is your own,
whether it carries the target or reasoning about it is read here from its content. -/
axiom IsTarget : (c : Context P) → Side c → Prop
/-- **Your judgment**: the cited turn carries what a source read or a check run returned in this
run, and the span is the narrowest returned material supporting the judgment, quoted in place.
A locator the person must go open is not the material. -/
axiom SourceRead : (c : Context P) → Cite c → String → Prop
/-- What a fact rests on: the target's own material, in the turn quoted even after the target
changes, or what a source or a check returned in this run. Your own reasoning is never
material, nor another agent's — a peer turn counts only as what a source it read or a check it
ran returned. -/
inductive Material (c : Context P)
| target (s : Side c) (object : IsTarget c s)
| source (observed : Cite c) (span : String) (linked : SourceRead c observed span)
/-- **Your judgment**: the material bears on aspect `a` — what the target does there, read on the
context as it now stands; it may be that it settles nothing. A fact is about the target, never
about the person. -/
axiom FactSupported : (c : Context P) → Material c → Entry → Prop
/-- A fact on aspect `a`: the material, with its support. -/
structure Fact (c : Context P) (a : Entry) where
material : Material c
supported : FactSupported c material a
/-- **Your judgment**, the record rule: the cited person turn says what they understand of aspect
`a` — a reading of their own, producing, applying, predicting, or explaining its relations at
the level the aspect asks, or an acknowledgment of your explanation, which is acceptance of it
and never a reading of their own — read against the context as it now stands. A self-rating, a
bare pick among options you offered, or an echo of your own wording is neither; an explanatory
paraphrase reaches what it reaches. -/
axiom ReadingSupported : (c : Context P) → Cite c → Entry → Prop
/-- What the person has said of aspect `a`: the turn, with its support. -/
structure Reading (c : Context P) (a : Entry) where
src : Cite c
byPerson : src.src.val = .person
supported : ReadingSupported c src a
/-- An aspect's row on the map, on two axes kept apart: what the target does there — its facts,
each with the material it rests on, and what is still open on it, as CONVERGENCE lists — and
what the person has said of it. The reading stays theirs until their own turn changes it.
Both are your judgment from the context, and nothing on the row is stored. -/
structure Cell (c : Context P) (a : Entry) where
facts : List (Fact c a)
reading : Option (Reading c a)
/-- **Your reading**: aspect `a`'s row, read afresh on `c`; whether a turn bears on a reworded
aspect is your judgment. Where several person turns give a reading, which one stands is read
on the current context; a later turn of the person's may replace it or take it back. -/
axiom cell : (c : Context P) → (a : Entry) → Cell c a
/-- The map: every aspect of the live inventory, with its row. -/
def map (c : Context P) : List ((a : Entry) × Cell c a) :=
(aspects c).map fun a => ⟨a, cell c a⟩
/-- **Your record**: your contrary grounds bearing on the person's judgment, each with what it
bears on and what it rests on, shown as `present` and CONVERGENCE say. Empty when there are
none. -/
axiom dissent : Context P → List String
/-- **Your judgment**: the latest utterance bears on this run — a purpose, a reading of the target,
an acknowledgment, a wish to see or try something, a request for more depth, a correction of
your reading, a question about the map, a closure — judged on what the whole utterance does,
read on the context with it before anything is consulted. An utterance about other work leaves
the run as it stands: the session answers it, that answer stays in the context, and no round of
this run is drawn. Words that end the run without saying that what they understand serves
their purpose do not bear on it, whatever else the turn says, and what else it says stands in
its own words in the context: the session answers them, no round is drawn, the run holds, and
later turns bear on it only where they come back to it; your own reading that the person is done
ends nothing. Where a turn taken as other work or as ending the run could also be read as the
other, as saying what they understand serves their purpose, or as bearing on the run otherwise,
the session's answer says briefly how it took it. -/
axiom Reaches : Context P → Prop
/-- **Your judgment**: the cited turn — the latest utterance; a turn before the latest round closes
nothing — says that what they now understand of the target serves their purpose, read on the
context as it now stands. An acknowledgment of an explanation is not that. Where the turn's
intent is unclear, it closes nothing. Nothing on the map, nor your own reading, closes it, and
nothing on the map holds the closure back. Setting one aspect aside does not close the run; a
set-aside aspect stays on the map as it stood. -/
axiom ClosureSupported : Context P → Turn P → Unit → Prop
/-- Only the person closes the run. -/
def closureCoord : Coord P Unit :=
{ admits := (·.val = .person), supports := ClosureSupported }
/-- **Your reading**: the person's closure; `open_` until one reaches it. -/
axiom closure : (c : Context P) → Occ (closureCoord (P := P)) c
/-- The record the closure carries, as CONVERGENCE lists it. -/
structure Closed (P : Type) where
context : Context P
scope : Occ (scopeCoord (P := P)) context
map : List ((a : Entry) × Cell context a)
dissent : List String
def closed (c : Context P) : Closed P :=
{ context := c, scope := scope c, map := map c, dissent := dissent c }
/-- Once it has run, the person can say: what I now understand of this target serves my purpose —
I saw it on a map built with me and checked against the target's material and the results we
looked at together, and for what still waits on a check, I know what would settle it.
`VerifiedUnderstanding`: the person's closure over the map CONVERGENCE lists — what each
aspect rests on, as they saw it when they closed. It records that closure, not a certificate
of what was demonstrated, nor omniscient comprehension. -/
structure VerifiedUnderstanding (P : Type) where
closure : Closed P
inductive Outcome (P : Type)
| verified (r : VerifiedUnderstanding P)
| holding (c : Context P)
/-- **Your judgment**: a check within your reach runs now — the latest utterance, bearing on this
run, asks for one (a wish to see or try something); or you run one
yourself, as TOOL GROUNDING's `present` entry says. Read on the context as it now stands, what
`gathered` returned included. -/
axiom CheckRuns : Context P → Prop
/-- **Your read**, now, of what the next judgment needs: the target's material and the sources that
bear on it — any a turn cites, and any you find — as far as relevant access reaches. What you
say you read, you read to the end. Empty where nothing outside the context bears. -/
axiom gathered : Context P → List (Evidence P)
/-- **Your read**, now: what the check handed off at `.check` returned — a run, an experiment, a
source read to settle it. -/
axiom checked : Context P → List (Evidence P)
/-- The context with what `gathered` read now appended. -/
def withGathered (c : Context P) : Context P := c ++ (gathered c).map (·.val)
open Classical in
/-- What is read now: what is gathered, and then what the check returned where `CheckRuns` holds
on the context with it, as `consultOps` hands it off. -/
def consult (c : Context P) : List (Evidence P) :=
gathered c ++ (if CheckRuns (withGathered c) then checked (withGathered c) else [])
/-- The context with what `consult` read now appended. -/
def consulted (c : Context P) : Context P := c ++ (consult c).map (·.val)
/-! ── A-BINDING ──
bind(R) = the target the argument names, else the target most recently in play; words in the
invocation that say what to understand of it fill the scope (`ScopeSupported`).
-/
/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it.
-/
/-! ── PHASE TRANSITIONS ──
A step is one arm of a structural recursion over the person's utterances. `respond` is the next
round, as TOOL GROUNDING's `present` entry names it; `session` is the session's own answer to an
utterance that does not bear on the run, which stays in the context without being a round of this
run.
-/
open Classical in
def grasp (respond session : Context P → Response P) :
Context P → List (Utterance P) → Outcome P
| c, [] => .holding c
| c, u :: us =>
let f := fuse c u
if ¬ Reaches f then grasp respond session (f ++ [(session f).val]) us
else if isFilled (closure f) = true then .verified ⟨closed f⟩
else
let c' := consulted f
grasp respond session (c' ++ [(respond c').val]) us
/-- The run opens on a gathering and its first round. -/
def start (respond session : Context P → Response P) (c : Context P)
(us : List (Utterance P)) : Outcome P :=
grasp respond session (consulted c ++ [(respond (consulted c)).val]) us
/-! ── LOOP ──
Every answer is read against the whole context as it now stands: nothing counts rounds, and no
earlier answer is held apart from what later ones say. No fixed cap: each round is dialogue.
-/
/-! ── CONVERGENCE ──
converged: a VerifiedUnderstanding the person's utterance closed; holding is a run no turn of the
person's has closed. The convergence evidence — the map at closure: each aspect on its two axes,
its facts (each with the material it rests on; each check run, with what it showed and, where it
ran on a stand-in, what it left untested), what is still open on it (each check named and not run,
with what it would settle and what running it needs; where no material bears on it, that, with what
would settle it), and what
the person has said of it (their own reading in their words, the facts beside it agreeing or
parting; acceptance of your explanation where that is what they gave; or nothing yet), whether the
scope as it stands still turns on it, and whether its facts were read, or the person's reading
given, on a version of the target that has since changed; the
purpose and scope as they stand, open included, and marked as yours where you read or set it; what
could not be reached that bears on an aspect; the dissent — a contrary ground not shown before the
closing turn is shown here, and the closure stands. Grounded, not asserted.
-/
/-! ── TOOL GROUNDING ──
What each operation of this contract does. An interaction with the person is one of two kinds,
and its kind fixes how it continues once its text is presented. A Constitution settles a judgment
through the person's turn. An Extension settles none for the person: it passes on a result its
cited ground fixes, or carries reversible work forward on a judgment the AI states, which stays
the AI's proposal until the person takes it. Beyond the Constitution operations a contract
annotates, whether work goes forward this way or waits for the person's answer is the AI's
judgment in the situation, and work that cannot be undone waits for the authorization it needs.
Work carried forward, on a grant or a stated judgment or as clear work, returns with an account
of how the request was read, what was judged on what basis — naming an alternative set aside
where it may be preferred — and how far the work went.
-/
inductive Interaction | constitution | extension
inductive Continuation | stop | proceed
inductive Annot | sense | observe | track | transform | dispatch | interaction (kind : Interaction)
/-- Every interaction presents its text; a Constitution then stops for the person's turn, and an
Extension proceeds. -/
def Interaction.realization : Interaction → Continuation
| .constitution => .stop
| .extension => .proceed
inductive Op | gather | assess | present | check | readAnswer | converge
def grounding : Op → Annot × String
| .gather => (.observe, "artifact read, artifact search: read-only reads as `gathered` states; name what was reached and what was not, and any conflict among what was gathered")
| .assess => (.sense, "Internal analysis: the purpose reading, the live inventory of aspects and each one's row on the map, over the whole fused context as it now stands")
| .present => (.interaction .extension, "the round, every round the first included. The first round is the map: the purpose as the person said it, or else your reading of it, marked as yours — where nothing grounds a useful reading, the target's main aspects, with the purpose line saying so; the aspects the purpose turns on, in the order it turns on them with that basis on the purpose line, an edge the person has not voiced among them where the material grounds one, each with its essence, its facts with the material they rest on, and the person's reading where they have given one; and your contrary grounds with their basis. A correction of the purpose moves the map. Where the session has a surface that stays in view, the map can stay there as well. A contrary ground you hold stays in view until it is settled — on the surface that stays in view where the session has one, otherwise briefly beside each round. Explain each aspect in the one representation — a picture, an example, a metaphor — that best carries its essence for this person; leave out what their words show they know, and go deeper when they ask. Read the person's turn whole; where its intent was unclear, say in one line how you took it. The round that shows a check's result sets it beside the aspect and against the claim your explanation made, saying where it agrees and where it parts; the result is what the map's facts are filled from, and the comparison with your explanation is said in the round, never recorded as a fact. Before setting their words against a fact, read whether they aim at another purpose: say that reading as a candidate with its basis and move the map, adding no question; if the person sets it aside, their words are read again as a reading of the target. Where a reading or application of their own says what the target does, set the facts that bear on it beside it, saying where each agrees and where it parts; where no material bears on it, say so and name what would settle it. Where what they said and a fact part on the same scope and premises, or two of their own utterances do, show it with its working in one round: their words quoted; the narrowest material where it bears on it, never your own explanation — scoped to what that material settles; why the two part; where their words and the material agree; and another reading beside it where the material allows. A contradiction whose working was shown and that the person keeps stays in view as a held contrary ground, and the round ends on its opening. A contradiction inside the target is a finding about it, judged for a side only with settling material outside it; your own earlier explanation against a fact is yours to correct, quoting it, as relay. An objection you raise yourself is relay: shown with its basis, and the run continues. Where what you could not reach, or a conflict among what you gathered, bears on an aspect or on a judgment the person is making, say it there. Where a check within your reach would show what the target does on an aspect the purpose turns on — where a reading of the person's own says what it does included — run the cheapest that would show it before the round — as far as your reach goes, what the purpose turns on most first; a check out of your reach is an offer, with what running it needs — never a question for them to answer. An aspect the person set aside is not explained again, nor a check raised on it, unless they return to it. Other work in the utterance neither closes this run nor answers its judgments. A round that shows a contradiction's working ends on that working, with nothing after it; every other round ends on one opening the person can take — respond to the map, ask to see or try something, go on, or say that what they understand now serves their purpose.")
| .check => (.dispatch, "delegate: where `CheckRuns` holds, the check handed to execution with the aspect and what it is to show; it changes no existing state — what it has to write goes to a scratch space outside the target's tree, and what it created only to look is removed afterwards — and a result from a stand-in comes with what it stood for and what it left untested; what it returns enters the context through `consult` as evidence read now, before the round that shows it")
| .readAnswer => (.sense, "Internal analysis: whether the latest utterance bears on this run and what it does there, as `Reaches` and the judgments above read it — read whole against the fused context as it now stands")
| .converge => (.interaction .extension, "the convergence evidence CONVERGENCE names; proceed with VerifiedUnderstanding")
open Classical in
/-- The operations whose returns `consult` appends to the context: what `.gather` reads, and, where
`CheckRuns` holds once it is read, what the check handed off at `.check` returns. -/
def consultOps (c : Context P) : List Op :=
if CheckRuns (withGathered c) then [.gather, .check] else [.gather]
/-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Dimension resolution emergent via session context.
-/
end
end Katalepsis
```
## Mode Activation
`/grasp` is user-invoked only: activate when the user signals a wish to understand a target already present in context and available for verbatim quotation, whatever its provenance — AI-produced work, code or a document someone else wrote, or material the session has put on the table; a bare command refers to the current target. Do not activate for an unrelated general question, an accurate account that already demonstrates understanding, an explicit decline, or a trivial formatting-only result.
## Protocol
### Map rendering
Label each row by what the person will understand or decide through it, and keep the target's anchors — code, plan, document, analysis, model, or a mix — beside the label, its facts and the person's reading said in words.
### Verification rendering and safeguards
Compose each round under TOOL GROUNDING's `present` entry. When grounding an explanation or correction, cite concrete locations in the target — file and line where it is code, the equivalent anchor where it is not. Read `references/round-composition.md` before composing when terminology must remain stable, wording must be carried unchanged, content belongs to another round or the convergence evidence, or whether text belongs before or inside the round's opening is in question.
## Rules
- **User-initiated only**: Activate only on the user's wish to understand a target present in context and quotable, whatever produced it; an explicit decline before activation withholds it.
- **User authority**: An acknowledgment of your explanation stands as the person's judgment; a factual disagreement or new evidence is shown beside it.
- **Round composition**: Compose each round so the reader can act without reassembly — use everyday language, keep each judgment beside its evidence and next-move implication (a fact set beside their reading included, its evidence being the excerpt attached with it), and place analytical context before the round's opening.
- **Form feedback**: Derive each round's density from the current request; carry an explicit form instruction until countermanded. Change form directly. Elements fixed elsewhere remain fixed; state what changed and, where the instruction overlaps a fixed element, what stays and why.
Imported from the listed AgentSkill.sh category. Complete supplied package files and notices are retained. Required external tools and credentials are not installed. No bundled code was executed during import. Individual agent task behavior has not been tested.