grasp git:20260925.0005571A

Immutable. This exact content never changes and is served at /api/v1/blob/4538e2fb7d4c5fee.

---
name: grasp
description: "Verify understanding of a target in play — code, a document, a result — present in context and quotable. Type: (TargetUngrasped, User, VERIFY, Target) → VerifiedUnderstanding"
---

# 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 intent-scented entry points and progressive verification.

```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. A
`theorem` line inside a doc comment states a consequence the contract already has; it is proved
outside this block and asks nothing further of you.
-/

/-! ── FLOW ──
Katalepsis(R, U) → grasp(c, utterances), where c is the fused session context:
  Phase 0 (silent): orient on R and U → derive intent-scented entries → assess the route map
  Phase 1: the entries with the route map → entry selection → Stop
  next utterance u: c' := fuse(c, u) → an utterance that sets aside your reading of a missed
    answer as aimed at another intent reopens the gate that answer answered → verdict(c') →
    propose: record the proposal → side-branch closure → the gate it came from again
      (a proposal at the Horizon probe resumes at that task's coverage)
    withdraw: what was shown stays on record → Withdrawn
    complete, at the zero-gap finding (Confirm) or at coverage (sufficient): record the task
      completed → the next task begins, or converge once every task is completed
    cont, by the gate it answers:
      entry selection: materialize the basis, register one task per selected entry point →
        the task the selection opens begins
      a task begins: record update naming it → the task's gate, in priority order, the order
        you read said with its basis when a contradiction opens ahead of another item due, and,
        for a Horizon opening ahead of a chosen aspect, only after its answer:
        a contradiction the user holds a side of: both sides, and a request to explain how they
          fit — no verdict yet
        an admissible Horizon not yet asked: the Horizon probe (its scenario only)
        no gap at all: the zero-gap finding with its reasoning
        nothing probed and no Horizon asked: the start-aspect selector
        otherwise: coverage
      a contradiction the user holds no side of rides the next presentation as relay: one inside
        the target shown as a finding about it, one against your earlier explanation shown as your
        correction; neither is handed to the user to settle
      the contradiction's explanation: it shows how the sides fit → closure → back to the task;
        aimed at another intent → moved there as below; left standing where the target or a
        cited source settles it → read and quote that material → both sides, that material, the
        reason, and an application question; left standing with nothing to settle it → said so,
        no verdict, the user's to settle → back to the task
      the Horizon probe, or a cue: the answer reached the edge → closure → back to the task;
        the user asked for a step instead → a cue that still does not name the edge;
        it missed, aimed at another intent than the probe's → that reading offered as a
        candidate, with what it was read from and an invitation to say otherwise → the task
        serving it, or entry selection with it named; nothing disclosed
        it missed within the probe's own intent → read and quote the material the edge rests on
        → the disclosure: the edge, that material, and an application question
      a disclosure's application question, or a probe: an answer aimed at another intent →
        moved there as above; otherwise an objection you have ground to raise → the reasoning
        inquiry; none → closure → back to the task
      the reasoning inquiry: an adjudication stands → read and quote the material it rests
        on → the correction with that material → the same aspect asked again;
        none stands → closure → back to the task
      the start-aspect selector or coverage: an aspect chosen → its probe, unless a contradiction
        the user holds a side of, or an admissible Horizon not yet asked, is due first; none →
        back to the task
      the zero-gap finding (Reopen): the named gap joins the task's gaps → the task's gate
    back to the task: a contradiction the user holds a side of, then an admissible Horizon not
      yet asked, read on the fused context, preempts the task's gate; otherwise that gate
  every task completed: the convergence trace → VerifiedUnderstanding
  no utterance: the gate holds; nothing is completed
-/

/-! ── MORPHISM ──
Target
  → orient(target, user_signal)        -- infer likely comprehension intents from the target and the user's wording
  → derive_entries(intent)             -- transform inferred intent into high-scent entry points
  → assess_route(intents, entries, context) -- annotate entry-point adequacy before user selection
  → select(intent_entry_point, route_map) -- user chooses the closest intent-scented entry point
  → materialize(artifact_basis)        -- derive concrete artifact anchors for the chosen intent
  → register(tasks)                    -- track selected entry points as tasks
  → verify(comprehension)              -- Socratic probing per gap type, each adjudication against an answer attaching the material it was drawn from; a Horizon the answer missed is disclosed with its material and applied; a contradiction in the context is taken up by whose it is
  → confirm(coverage)                  -- aspect coverage check per entry point
  → 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 answer finds enough ground for adjudication
deficit:  TargetUngrasped               -- activation precondition (Layer 1)
preserves: R                            -- read-only throughout; morphism acts on user understanding only
invariant: Comprehension over Explanation
invariant: Completion by the user       -- a task is completed only by the user's Confirm or sufficient; no reading of yours closes one
-/

namespace Katalepsis

/-! ── GROUND ──
The session primitive this contract reads.
-/

inductive Origin | person | assistant | external | peer | injected | unknown
inductive Form | statement | observation | request | reasoning | summary | instruction
inductive Basis | utterance | testimony | observation | report
  deriving DecidableEq

structure Turn (P : Type) where
  origin  : Origin
  form    : Form
  content : P

abbrev Context (P : Type) := List (Turn P)

/-- What a turn may ground directly: eligibility, not truth or instruction priority. -/
def Turn.basis {P : Type} (e : Turn P) : Option Basis :=
  match e.origin, e.form with
  | .person, .statement     => some .utterance
  | .person, .observation   => some .testimony
  | .external, .observation => some .observation
  | .peer, .statement       => some .report
  | _, _                    => none

/-- Any turn a person sent, whatever its form; the form decides what it may ground
    (`Turn.basis`). -/
def Utterance (P : Type) := {e : Turn P // e.origin = .person}
def Response (P : Type) := {e : Turn P // e.origin = .assistant}
def Evidence (P : Type) := {e : Turn P //
  e.basis = some .observation ∨ e.basis = some .report ∨ e.basis = some .testimony}

def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]

structure Cite {P : Type} (c : Context P) where
  idx  : Nat
  lt   : idx < c.length
  kind : Basis
  ok   : (c[idx]'lt).basis = some kind

/-- `supports` is the model's reading. -/
structure Coord (P A : Type) where
  admits   : Basis → 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.kind)
      (supported : q.supports c (c[src.idx]'src.lt) a)

/-!
theorem fuse_extends {P : Type} (c : Context P) (u : Utterance P) :
    ∃ t, fuse c u = c ++ t

theorem ai_never_grounds {P : Type} (e : Turn P) (h : e.origin = .assistant) :
    e.basis = none
-/

/-- 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
    kind := s.kind
    ok := by rw [List.getElem_append_left s.lt]; exact s.ok }

/-! ── TYPES ── -/

noncomputable section

variable {P : Type}

/-- `R` with `U`: the comprehension target — the code, document, result, or other material
    whose understanding is sought, present in the context and quotable, whatever produced it —
    and the user's signal about what feels ungrasped, which may be empty on a bare `/grasp`.
    Both are read from the context. -/
abbrev Target (P : Type) := Context P

/-- `I`: the comprehension intent an entry point serves. -/
inductive Intent
  | orientation | rationale | impact | approval | transfer
  | emergent (name : String)

/-- An entry point, phrased as what the user will understand, decide, explain, or change by
    taking it; `anchor` is the artifact basis kept behind it as a grounding hint. -/
structure EntryPoint where
  label  : String
  intent : Intent
  anchor : String

/-- A question whose answer could change which entry point the user selects. -/
structure RouteQuestion where
  route        : String
  reason       : String
  signalNeeded : String

/-- `Fᵣ`: annotations over the entries, filtering, creating, or suppressing none of them.
    `cheapestProbe` names, per entry, the aspect a probe would most usefully target — never its
    expected answer or reasoning path. `hiddenRoutes` are entries the target supports that the
    user's signal did not name. -/
structure RouteMap where
  entries       : List EntryPoint
  cheapestProbe : List (String × String)
  hiddenRoutes  : List String
  openQuestions : List RouteQuestion

/-- **Your judgment** at Phase 0, from the target, the user's wording, and the context: the
    likely intents, the entries derived from them, and their route annotations. -/
axiom routeMap : Context P → RouteMap

/-- **Your judgment**: the cited utterance selects these entry points, in order — offered
    entries, or a path the user wrote that stays within TargetUngrasped → VerifiedUnderstanding.
    Distinct concerns the user already named become the ordered list directly. -/
axiom SelectionSupported : Context P → Turn P → List EntryPoint → Prop

/-- The selection is the user's: only their statement fills it. -/
def selectionCoord : Coord P (List EntryPoint) :=
  { admits := (· = .utterance), supports := SelectionSupported }

/-- **Your judgment**: the selection the user's latest answer at entry selection made; open
    where it made none. -/
axiom selection : (c : Context P) → Occ (selectionCoord (P := P)) c

def isFilled {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Bool
  | .open_ _   => false
  | .filled .. => true

def filledValue {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Option A
  | .open_ _     => none
  | .filled a .. => some a

/-- The identity a record-creating write returned; every later record update names it. -/
abbrev RecordId := String

/-- One task per selected entry point. -/
structure Task where
  id    : RecordId
  entry : EntryPoint

/-- **Your record**, read from the context: the registered tasks in selection order, each keyed
    by the identity its registration write returned. -/
axiom tasks : Context P → List Task

/-- **Your judgment**: the cited utterance closes task `t` — `Confirm` at its zero-gap finding,
    or `sufficient` at its coverage gate. -/
axiom CompletionSupported : RecordId → Context P → Turn P → Unit → Prop

/-- A task is completed only by the user's statement. -/
def completionCoord (t : RecordId) : Coord P Unit :=
  { admits := (· = .utterance), supports := CompletionSupported t }

/-- **Your judgment**: whether the user has closed task `t`. -/
axiom completion : (c : Context P) → (t : RecordId) → Occ (completionCoord (P := P) t) c

/-- The task verification is on: the first registered task the user has not closed. -/
def current (c : Context P) : Option Task :=
  (tasks c).find? (fun t => !isFilled (completion c t.id))

/-- **Your record**, read from the context: the task the latest selection opens — at the first
    selection, the first entry selected; at a selection made after a missed answer was read as
    aimed at another intent, the entry that selection named — the first such task the user has
    not closed. -/
axiom selectedTask : Context P → Option Task

/-- A comprehension gap type. -/
inductive GapType
  | expectation | causality | scope | sequence | horizon | contradiction
  | emergent (description : String)

/-- Whether a gap type can be offered at the start-aspect selector or at coverage: the Horizon
    and a contradiction are read from the context and taken up there, never offered. -/
def offered : GapType → Bool
  | .horizon       => false
  | .contradiction => false
  | _              => true

/-- An aspect the user can be offered and choose. -/
abbrev Selectable := {g : GapType // offered g = true}

inductive ProbeForm | qc | qs

/-- Qc for Expectation and Sequence (classificatory), Qs for Causality, Scope, and Emergent
    (open). The Horizon and a contradiction map to no form: the Horizon is probed only by its own
    scenario, and a contradiction by the request to explain how its two sides fit. -/
def probeKind : GapType → Option ProbeForm
  | .expectation   => some .qc
  | .sequence      => some .qc
  | .causality     => some .qs
  | .scope         => some .qs
  | .emergent _    => some .qs
  | .horizon       => none
  | .contradiction => none

/-- **Your reading** of the gap types relevant to task `t`'s entry point, the Horizon apart —
    an Emergent one included where a Reopen named it. -/
axiom gaps : Context P → RecordId → List Selectable

/-- **Your record**, read from the context: the aspects already probed for task `t`, the
    Horizon probe apart. -/
axiom probed : Context P → RecordId → List Selectable

/-- `HC`: a co-intended but unspoken edge inside the selected entry point. -/
structure HorizonCandidate where
  edge        : String
  anchors     : List String
  failureMode : String

/-- **Your judgment**, read again over the whole fused context after every utterance: the
    candidates that qualify for task `t` — each bound to evidence in the materialized basis,
    material (leaving the edge unprobed is predicted to keep the achievable understanding short
    of R), unspoken in the user's signal, the entry labels, and every answer so far, and neither
    a route-selection question nor a decision gap. An edge the user has since spoken no longer
    qualifies, and an answer can bring a new one into view. Whether two candidates are the same
    edge is read here. -/
axiom qualifying : Context P → RecordId → List HorizonCandidate

/-- A Horizon is admissible only where exactly one candidate qualifies; several weak ones
    competing detect none. -/
def admissible (c : Context P) (t : RecordId) : Option HorizonCandidate :=
  match qualifying c t with
  | [hc] => some hc
  | _    => none

/-- **Your judgment**, read from your own turns in the context: a Horizon probe for `hc`'s edge
    on task `t` has already been presented. The user saw only its scenario; your own turn is
    what tells you which edge it was for. -/
axiom Asked : Context P → RecordId → HorizonCandidate → Prop

/-- An admissible Horizon not yet asked. -/
def HorizonDue (c : Context P) (t : RecordId) : Prop :=
  ∃ hc, admissible c t = some hc ∧ ¬ Asked c t hc

/-- Where a contradiction's two sides come from, which decides whose it is to settle: two of the
    user's own statements, the user's stated understanding against the target, two places in the
    target itself, or an explanation you gave earlier against the target. -/
inductive ConflictSource | userUser | userTarget | targetTarget | yoursTarget

/-- A contradiction the user holds a side of — theirs to work through; the other two are the
    target's own and yours. -/
def ConflictSource.involvesUser : ConflictSource → Bool
  | .userUser   => true
  | .userTarget => true
  | _           => false

/-- One side of a contradiction, located in the context and quoted where it stands. A side is
    located, not cited as ground: the target itself or an explanation of yours can be one. -/
structure Side (c : Context P) where
  idx  : Nat
  lt   : idx < c.length
  span : String

structure Contradiction (c : Context P) where
  source : ConflictSource
  one    : Side c
  other  : Side c

/-- **Your judgment**, read again over the whole fused context after every utterance: the
    contradiction to take up now for task `t` — two statements in the context that cannot both
    hold, each quoted where it stands, with where each comes from. Admit one only where both sides
    are in the context with their sources and speak to the same scope under the same premises;
    one claim appearing again — the target, your quote of it, an explanation of yours drawn from
    it — is one side, not two. One your own turns show already taken up is not taken up again;
    one whose recognition needs something the task has not yet shown waits; which of several
    comes first is yours to read. `none` where none is due. -/
axiom conflictDue : (c : Context P) → RecordId → Option (Contradiction c)

/-- A contradiction the user holds a side of is due for task `t`. -/
def UserConflictDue (c : Context P) (t : RecordId) : Prop :=
  ∃ k, conflictDue c t = some k ∧ k.source.involvesUser = true

/-- **Your judgment**, read at the user's explanation of how a contradiction's two sides fit: it
    shows how they fit — the two do not conflict once read as they meant them. -/
axiom Dissolved : Context P → Prop

/-- **Your judgment**, read where the user's explanation left a contradiction standing: the
    target, or a source the user cited that can be read now, holds material that settles which
    side holds. Where nothing does, no verdict is given: that is said, and the contradiction stays
    the user's to settle. -/
axiom Settles : Context P → Prop

/-- How a contradiction ended: the user's explanation dissolved it; it was resolved through an
    application after both sides were shown with the target's material; it was left standing
    with nothing in the target or a cited source to settle it, said so and left to the user; a
    contradiction inside the target itself shown as a finding about it; or your own earlier
    explanation corrected. -/
inductive ConflictOutcome | dissolved | afterDisclosure | unsettled | targetFinding | yourCorrection

/-- **Your record**, read from the context: for task `t`, each contradiction taken up, where its
    sides came from, and how it ended. One still standing when its task closed is carried in the
    dissent instead. -/
axiom conflicts : Context P → RecordId → List (ConflictSource × ConflictOutcome)

/-- **Your judgment**, read at the answer to a Horizon probe or a cue: the answer reaches the
    edge. -/
axiom Reached : Context P → Prop

/-- **Your judgment**, read at the answer to a Horizon probe or a cue: instead of answering, the
    user asks to go step by step — a hint, a smaller step. -/
axiom AsksSteps : Context P → Prop

/-- **Your reading**, at an answer that missed what its question was after — a Horizon answer
    that neither reached the edge nor asked for a step, the answer to a probe, an explanation at a
    contradiction that did not dissolve it, or the answer to a disclosure's application question —
    of whether it was aimed at a different intent: another question or purpose than the probe's
    task serves, named as the entry point it points at, read from the whole fused context with
    what you read it from. `none` where the answer engaged the probe's own question. It is read,
    never asked, and offered as a candidate understanding rather than asserted: the presentation
    says what you read and from what, moves there, and invites the user to say otherwise in the
    same turn; their next utterance corrects a wrong reading. -/
axiom otherIntent : Context P → Option EntryPoint

/-- **Your reading** of which registered task the user has not closed serves `e`'s intent;
    `none` where no registered task does. -/
axiom taskFor : Context P → EntryPoint → Option Task

/-- **Your record**, read from the context: for task `t`, each answer you read as aimed at another
    intent — the aspect it answered and the intent you read, with what you read it from — and
    whether the user's next utterance set that reading aside. -/
axiom misreadings : Context P → RecordId → List (GapType × String)

/-- **Your reading** of the latest utterance: it sets aside your preceding reading of a missed
    answer as aimed at another intent — that answer was aimed at its question's own intent after
    all — and so names the gate that answer answered, to be read again as a miss within its own
    intent; `none` otherwise. -/
axiom restored : Context P → Option Gate

/-- How an aspect came to be shown: by the user on their own, through an application after you
    disclosed the edge, or through an application after a cue the user asked for. What follows a
    disclosure or a cue never reads as independent detection. -/
inductive Demonstration | independent | afterDisclosure | afterCue

/-- **Your record**, read from the context: for task `t`, each aspect shown and how — a Horizon
    edge an answer reached, on its own or after a cue, or an application after its disclosure
    that you read as reaching it; and an aspect whose adjudication the user's answer met. An
    answer merely taken, with nothing to check it against, is not shown. -/
axiom demonstrated : Context P → RecordId → List (GapType × Demonstration)

/-- **Your judgment**: turn `idx` carries the target itself — its text, or an observation of
    reading it — rather than reasoning about it. -/
axiom IsTarget : Context P → Nat → Prop

/-- What an adjudication against an answer is drawn from, quoted in place at the narrowest span
    that supports it: the target itself, in the turn that carries it — whoever produced it,
    since here it is the object being understood rather than a claim standing as evidence — or
    a source the user cited, read now. The reasoning that produced the target, and what the
    session said about it earlier, are neither. -/
inductive Measure (c : Context P)
  | target (idx : Nat) (lt : idx < c.length) (span : String) (isTarget : IsTarget c idx)
  | source (src : Cite c) (span : String) (read : src.kind = .observation)

/-- An adjudication that stands against an answer. `otherReading` is the other reading the
    material admits, said beside it; empty when there is none. -/
structure Adjudication (c : Context P) where
  correction   : String
  measure      : Measure c
  otherReading : String

/-- **Your judgment**, read at the answer and once: you have an objection to it, in whole or in
    part, with material you could attach, and have not settled it. It is not a verdict; the
    inquiry exists to hear the user's reasoning before anything is settled. -/
axiom Objection : Context P → Prop

/-- **Your judgment**, read at the user's reasoning at the inquiry: an adjudication against the
    answer still stands — the reasoning did not defeat the objection, and there is material to
    attach. -/
axiom Stands : Context P → Prop

/-- **Your judgment**, read once the material it rests on has been read: the adjudication that
    stands, with what it is drawn from. -/
axiom adjudication : (c : Context P) → Option (Adjudication c)

/-- **Your judgment**: the cited utterance chooses this aspect at the start-aspect selector or at
    coverage. -/
axiom AspectSupported : Context P → Turn P → Selectable → Prop

def aspectCoord : Coord P Selectable :=
  { admits := (· = .utterance), supports := AspectSupported }

/-- **Your judgment**: the aspect the latest answer chose; open where it chose none. -/
axiom aspectChoice : (c : Context P) → Occ (aspectCoord (P := P)) c

/-- The one shape every turn of an active run ends in. -/
inductive Gate
  /-- Phase 1: the entries, enriched by the route map where it has anything to add; opened again
      when a missed answer is read as aimed at an intent no registered task serves, with that
      intent named among the entries -/
  | entrySelection
  /-- no gap for the task: the finding with its reasoning; Confirm or Reopen(description) -/
  | zeroGap (t : RecordId)
  /-- the preempting Horizon probe: an everyday scenario and nothing else — no edge, no expected
      answer, no reason for asking -/
  | horizonProbe (t : RecordId)
  /-- the step the user asked for at a Horizon probe: a cue toward the edge that still does not
      name it -/
  | cue (t : RecordId)
  /-- the disclosure owed after a Horizon answer that missed the edge within the probe's own
      intent: the edge named, the material from the target it rests on quoted in place, and an
      application question -/
  | reveal (t : RecordId)
  /-- a contradiction the user holds a side of: both sides quoted where they stand, and a request
      to explain how they fit — no verdict yet -/
  | conflict (t : RecordId)
  /-- the contradiction the user's explanation left standing, where the target or a source they
      cited settles it: both sides, that material quoted in place, the reason one side does not
      hold, and an application question -/
  | resolve (t : RecordId)
  /-- which aspect to start with, over the task's gaps -/
  | startAspect (t : RecordId)
  /-- the probe of one aspect, in the form `probeKind` gives it, with a free-response path -/
  | probe (t : RecordId) (g : Selectable)
  /-- the reasoning inquiry on an objection to the answer to a probe, or to the application
      question after a disclosure (`g` is then the Horizon, or the contradiction) -/
  | inquiry (t : RecordId) (g : GapType)
  /-- coverage: probed and unprobed aspects; sufficient, another aspect, or a proposal -/
  | coverage (t : RecordId)

/-- The gate that asks aspect `g` again once an adjudication against its answer stands: the
    Horizon's or the contradiction's application question, or the same aspect's probe. -/
def again (t : RecordId) : GapType → Gate
  | .horizon       => .reveal t
  | .contradiction => .resolve t
  | .expectation   => .probe t ⟨.expectation, rfl⟩
  | .causality     => .probe t ⟨.causality, rfl⟩
  | .scope         => .probe t ⟨.scope, rfl⟩
  | .sequence      => .probe t ⟨.sequence, rfl⟩
  | .emergent d    => .probe t ⟨.emergent d, rfl⟩

/-- **Your record**, read from the context: the gate your latest presentation opened, a Horizon
    probe included — your own turn shows which it was, though the user saw only a scenario. -/
axiom answered : Context P → Gate

/-- Relay metadata emitted before a gate, never in place of one. `outcome` says how the round
    ended: nothing to object to, an objection the user's reasoning defeated, nothing to check
    the answer against — none of them a demonstrated aspect — a Horizon edge the user reached,
    on their own or after a cue, or one disclosed and applied, each shown and recorded with how;
    a contradiction dissolved by the user's explanation or resolved after its disclosure; a missed
    answer read as aimed at another intent, offered as that candidate reading with what it was
    read from, where the loop moves, and the invitation to say otherwise; or, for a side branch,
    that the answer was read as a proposal and recorded. -/
structure ContinuationClosure where
  outcome   : String
  branch    : Option RecordId
  nextMoves : List String

/-- What the fused context says the user did at the gate. Premise: one utterance carries one
    disposition; silence is none of them. -/
inductive Verdict
  /-- a selection, an answer, a reasoning, a chosen aspect, a Reopen, a question, or any
      reading not yet settled -/
  | cont
  /-- Confirm at the zero-gap finding, or sufficient at coverage: the user closes the task -/
  | complete
  /-- a system change that brings in matter outside the target or directs action at the
      system; explanation, navigation, and clarification requests are not proposals -/
  | propose
  /-- the user stops verifying: what the rounds so far showed stays on record, and no task the
      user did not close is completed -/
  | withdraw

/-- **Your judgment** on the whole latest utterance read with the context. -/
axiom verdict : Context P → Verdict

/-- **Your record**: contrary grounds you presented before the gate a closing utterance answered —
    an aspect you hold undemonstrated, an adjudication still standing — attached to the
    closure; empty when there were none. -/
axiom dissent : Context P → List String

/-- `VerifiedUnderstanding`: the context once every task is completed, carrying exactly what the
    rounds established and no more — for each task, each aspect shown and how, each contradiction
    taken up and how it ended, and each missed answer you read as aimed at another intent — with
    the dissent attached to the closures. -/
structure VerifiedUnderstanding (P : Type) where
  context     : Context P
  shown       : List (RecordId × List (GapType × Demonstration))
  conflicts   : List (RecordId × List (ConflictSource × ConflictOutcome))
  misreadings : List (RecordId × List (GapType × String))
  dissent     : List String

inductive Outcome (P : Type)
  | verified  (v : VerifiedUnderstanding P)
  /-- the user stopped; the context ends in the trace of what was shown, presented at the stop,
      and the dissent is attached -/
  | withdrawn (c : Context P) (dissent : List String)
  /-- the gate holds -/
  | holding   (c : Context P)

/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it, the Horizon and
contradictions included — whether one is due, whether it was taken up, and how an answer met it
are read again after every utterance.
-/

abbrev Mode (P : Type) := Context P

/-! ── PHASE TRANSITIONS ──
A round is one step of a structural recursion over the user's utterances. `respond` is your
presentation of a gate, read from the context: the closure the round owes before it — a
`ContinuationClosure` after an answer no adjudication stands against, or the side-branch one
after a proposal — or the correction with its attached material after an adjudication, or the
disclosure of a missed Horizon or of a contradiction left standing with its material, or the
candidate reading of the intent a missed answer was aimed at, then the gate itself. A
contradiction due for the task that the user holds no side of rides the next presentation as
relay: one inside the target itself shown as a finding about the target, saying which side holds
only where evidence outside it settles that, and one against an explanation of yours shown as your
correction of that explanation, with the target's material — neither asks the user to settle it.
Where a contradiction the user holds a side of opens ahead of another item due for the task, the
presentation says the order you read and why. A Horizon probe that opens ahead of an aspect the
user chose says only that their aspect comes next: the probe carries its scenario and nothing
else, so why it came first is said in the closure after its answer. Every turn of an active run ends in one `Gate`; a withdrawal ends the run
instead, with what was shown presented.
-/

/-- **Your registration** at Phase 2: the artifact basis materialized for every selected entry
    point, and one record written per entry point; each write's returned identity enters the
    context as observed. -/
axiom register : Context P → List (Evidence P)

/-- **Your record update** naming a task as its verification begins. -/
axiom touch : Context P → List (Evidence P)

/-- **Your record update** marking the closed task completed. -/
axiom update : Context P → List (Evidence P)

/-- **Your read**, once an adjudication stands, a missed Horizon is to be disclosed, or a
    contradiction the user's explanation left standing is to be shown, of whatever it rests on —
    the target, or a source the user cited that can be read now — observed and quoted at the
    narrowest span. -/
axiom attach : Context P → List (Evidence P)

/-- **Your record** of a proposal, verbatim, outside the task set; the write's returned identity
    enters the context as observed. -/
axiom eject : Context P → List (Evidence P)

inductive Step (P : Type)
  | gate      (c : Context P) (g : Gate)
  | done      (c : Context P)
  | withdrawn (c : Context P)

open Classical in
/-- Where task `t`'s verification stands, in priority order: a contradiction the user holds a side
    of comes first; then an admissible Horizon not yet asked; no gap at all is the zero-gap
    finding; nothing probed and no Horizon asked opens the start-aspect selector; otherwise
    coverage. -/
noncomputable def gateFor (c : Context P) (t : RecordId) : Gate :=
  if UserConflictDue c t then .conflict t
  else if HorizonDue c t then .horizonProbe t
  else if (gaps c t).isEmpty ∧ admissible c t = none then .zeroGap t
  else if (probed c t).isEmpty ∧ ¬ ∃ hc, Asked c t hc then .startAspect t
  else .coverage t

open Classical in
/-- A return to a task-level gate, or the probe of an aspect the user just chose: a contradiction
    the user holds a side of, then an admissible Horizon not yet asked, preempts it, read on the
    context the latest answer fused. A choice it preempts stays in the context, and the task's
    next coverage offers it again. -/
noncomputable def settle (c : Context P) (t : RecordId) (g : Gate) : Gate :=
  if UserConflictDue c t then .conflict t
  else if HorizonDue c t then .horizonProbe t else g

/-- Where a missed answer read as aimed at another intent moves: the gate of the task that serves
    it, or entry selection with that intent named where no registered task does — never a
    disclosure. -/
noncomputable def redirect (c : Context P) (e : EntryPoint) : Gate :=
  match taskFor c e with
  | some t => gateFor c t.id
  | none   => .entrySelection

open Classical in
/-- An answer to a Horizon probe or a cue: one that reaches the edge is taken and the loop
    returns to the task; a request for a step gets a cue; a miss read as aimed at another intent
    moves there, with nothing disclosed; any other miss is disclosed at once with the material
    it rests on read — never a second concealed scenario. -/
noncomputable def horizonAnswer (c : Context P) (t : RecordId) : Step P :=
  if Reached c then .gate c (settle c t (.coverage t))
  else if AsksSteps c then .gate c (.cue t)
  else match otherIntent c with
    | some e => .gate c (redirect c e)
    | none   => .gate (c ++ (attach c).map (·.val)) (.reveal t)

/-- A task begins: the record update naming it, then the task's gate. -/
noncomputable def beginTask (c : Context P) (t : Task) : Step P :=
  let c₁ := c ++ (touch c).map (·.val)
  .gate c₁ (gateFor c₁ t.id)

/-- The user closed the current task: its record updated, then the next task, or convergence. -/
noncomputable def completeStep (c : Context P) : Step P :=
  let c₁ := c ++ (update c).map (·.val)
  match current c₁ with
  | none   => .done c₁
  | some t => beginTask c₁ t

/-- The gate a proposal returns to: the one it came from, or coverage for a Horizon probe. -/
def resumeOf : Gate → Gate
  | .horizonProbe t => .coverage t
  | g               => g

noncomputable def aspectStep (c : Context P) (g : Gate) (t : RecordId) : Step P :=
  match filledValue (aspectChoice c) with
  | some a => .gate c (settle c t (.probe t a))
  | none   => .gate c (settle c t g)

open Classical in
/-- One answer, read at the gate it answers. -/
noncomputable def advance (c : Context P) : Gate → Verdict → Step P
  | g, .propose => .gate (c ++ (eject c).map (·.val)) (resumeOf g)
  | _, .withdraw => .withdrawn c
  | .zeroGap _, .complete => completeStep c
  | .coverage _, .complete => completeStep c
  | .entrySelection, _ =>
    if isFilled (selection c) then
      let c₁ := c ++ (register c).map (·.val)
      match selectedTask c₁ with
      | some t => beginTask c₁ t
      | none   => .gate c₁ .entrySelection
    else .gate c .entrySelection
  | .zeroGap t, _ => .gate c (gateFor c t)
  | .horizonProbe t, _ => horizonAnswer c t
  | .cue t, _ => horizonAnswer c t
  | .reveal t, _ =>
    match otherIntent c with
    | some e => .gate c (redirect c e)
    | none   =>
      if Objection c then .gate c (.inquiry t .horizon) else .gate c (settle c t (.coverage t))
  | .conflict t, _ =>
    if Dissolved c then .gate c (settle c t (.coverage t))
    else match otherIntent c with
      | some e => .gate c (redirect c e)
      | none   =>
        if Settles c then .gate (c ++ (attach c).map (·.val)) (.resolve t)
        else .gate c (settle c t (.coverage t))
  | .resolve t, _ =>
    match otherIntent c with
    | some e => .gate c (redirect c e)
    | none   =>
      if Objection c then .gate c (.inquiry t .contradiction)
      else .gate c (settle c t (.coverage t))
  | .probe t g, _ =>
    match otherIntent c with
    | some e => .gate c (redirect c e)
    | none   =>
      if Objection c then .gate c (.inquiry t g.val) else .gate c (settle c t (.coverage t))
  | .inquiry t g, _ =>
    if Stands c then .gate (c ++ (attach c).map (·.val)) (again t g)
    else .gate c (settle c t (.coverage t))
  | .startAspect t, _ => aspectStep c (.startAspect t) t
  | .coverage t, _ => aspectStep c (.coverage t) t

/-- The gate the latest utterance answers: the one your latest presentation opened, or, where the
    utterance sets aside your reading of a missed answer as aimed at another intent, the gate that
    answer answered. -/
def reopened (c : Context P) (g : Gate) : Gate :=
  match restored c with
  | some g₀ => g₀
  | none    => g

/-- Presenting a gate. -/
def present (respond : Context P → Gate → Response P) (c : Context P) (g : Gate) : Context P :=
  c ++ [(respond c g).val]

/-- Convergence: the trace presented, then the resolution; `trace` is your convergence
    presentation — each task with its status, the aspects detected for it, the Horizon among them
    where one was asked, each aspect shown with how it was shown, each contradiction taken up with
    where its sides came from and how it ended, and each missed answer read as aimed at another
    intent. A withdrawal presents the same trace at the stop. -/
def understanding (trace : Context P → Response P) (c : Context P) : VerifiedUnderstanding P :=
  { context     := c ++ [(trace c).val]
    shown       := (tasks c).map (fun t => (t.id, demonstrated c t.id))
    conflicts   := (tasks c).map (fun t => (t.id, conflicts c t.id))
    misreadings := (tasks c).map (fun t => (t.id, misreadings c t.id))
    dissent     := dissent c }

noncomputable def grasp (respond : Context P → Gate → Response P)
    (trace : Context P → Response P) : Context P → List (Utterance P) → Outcome P
  | c, []      => .holding c
  | c, u :: us =>
    let c' := fuse c u
    match advance c' (reopened c' (answered c)) (verdict c') with
    | .done c₁      => .verified (understanding trace c₁)
    | .withdrawn c₁ => .withdrawn (c₁ ++ [(trace c₁).val]) (dissent c₁)
    | .gate c₁ g    => grasp respond trace (present respond c₁ g) us

/-- The run begins at entry selection, over the route map Phase 0 assessed in silence. -/
noncomputable def start (respond : Context P → Gate → Response P)
    (trace : Context P → Response P) (c : Context P) (us : List (Utterance P)) : Outcome P :=
  grasp respond trace (present respond c .entrySelection) us

/-! ── LOOP ──
Every answer is read with the whole context; nothing the user said is narrowed to the gate's
options. An answer that stays in the comprehension loop takes exactly one of adjudicated or
unadjudicated; a proposal is recorded and the loop resumes where it was. No gate holds a round
cap: re-entering a gate is dialogue. A user who stops says so, and the withdrawal ends the run
with what was shown on record; leaving without saying so is the host's to deliver.
Continue until every selected task is completed, or the user withdraws. The Horizon judgment is
read again after every utterance: an edge the user has since spoken is not asked, an answer can
bring a new one into view, and one already asked is not asked again. Contradictions are read
again the same way, and taken up by whose they are: one the user holds a side of comes before
the Horizon and asks first for their explanation of how the sides fit, a verdict following only
where that explanation leaves it standing and the target or a cited source settles it — with
nothing to settle it, none is given and that is said; one inside the target is a finding about the target,
and one against an explanation of yours is yours to correct — neither is handed to the user to
settle. Before anything is disclosed, a missed answer is read for its intent: one aimed at
another question or purpose than the probe's moves to the task or entry that intent points at,
the reading offered as a candidate with what it was read from and an invitation to say otherwise,
and nothing is disclosed; the user's next utterance corrects a wrong reading. An answer that
misses the edge within the probe's own intent is followed by its disclosure, not by a second
concealed scenario; a user who asks to go step by step gets a cue first, because their utterance
steers the next presentation. Convergence
evidence: for each task, TargetUngrasped(t) → its status, with the aspects detected for it — the
Horizon among them where one was asked — and each aspect shown with how it was shown; how each
probe ended was said in the closure of the round that ran it and does not travel here.
Demonstrated, not asserted.
-/

/-!
Silence completes nothing.
theorem silence (respond : Context P → Gate → Response P) (trace : Context P → Response P)
    (c : Context P) : grasp respond trace c [] = .holding c

A contradiction the user holds a side of comes first among its task's gates, and preempts a
return to them the same way.
theorem user_conflict_first (c : Context P) (t : RecordId) (hu : UserConflictDue c t) :
    gateFor c t = .conflict t

theorem user_conflict_preempts_return (c : Context P) (t : RecordId) (g : Gate)
    (hu : UserConflictDue c t) : settle c t g = .conflict t

The gate that asks for the user's explanation opens only for a contradiction the user holds a
side of: one inside the target, or one against your own explanation, is never handed to them.
theorem conflict_only_user (c : Context P) (t : RecordId) (h : gateFor c t = .conflict t) :
    UserConflictDue c t

At a contradiction the user holds a side of, their explanation comes before any verdict: where it
shows how the sides fit, nothing is read or attached; where it leaves them standing within the
question's own intent and material settles it, that material is read and both sides are shown
with it; where nothing settles it, nothing is read or attached and no verdict follows.
theorem conflict_dissolved (c : Context P) (t : RecordId) (hd : Dissolved c) :
    advance c (.conflict t) .cont = .gate c (settle c t (.coverage t))

theorem conflict_standing_resolves (c : Context P) (t : RecordId) (hd : ¬ Dissolved c)
    (hi : otherIntent c = none) (hs : Settles c) :
    advance c (.conflict t) .cont = .gate (c ++ (attach c).map (·.val)) (.resolve t)

theorem conflict_unsettled_no_verdict (c : Context P) (t : RecordId) (hd : ¬ Dissolved c)
    (hi : otherIntent c = none) (hs : ¬ Settles c) :
    advance c (.conflict t) .cont = .gate c (settle c t (.coverage t))

An admissible Horizon not yet asked preempts every other gate of its task but a contradiction the
user holds a side of.
theorem horizon_preempts (c : Context P) (t : RecordId) (hu : ¬ UserConflictDue c t)
    (hd : HorizonDue c t) : gateFor c t = .horizonProbe t

It preempts a return to the task's gates the same way, read on the context the latest answer
fused.
theorem horizon_preempts_return (c : Context P) (t : RecordId) (g : Gate)
    (hu : ¬ UserConflictDue c t) (hd : HorizonDue c t) : settle c t g = .horizonProbe t

An edge already asked is not asked again.
theorem asked_not_reasked (c : Context P) (t : RecordId) (hc : HorizonCandidate)
    (ha : admissible c t = some hc) (hk : Asked c t hc) : gateFor c t ≠ .horizonProbe t

A Horizon answer that missed the edge within the probe's own intent, and asked for no step, is
followed by its disclosure, with the material it rests on read, and never by a second concealed
scenario.
theorem miss_discloses (c : Context P) (t : RecordId) (hm : ¬ Reached c) (hs : ¬ AsksSteps c)
    (hi : otherIntent c = none) :
    advance c (.horizonProbe t) .cont = .gate (c ++ (attach c).map (·.val)) (.reveal t)

A missed Horizon answer read as aimed at another intent moves where that intent points, with
nothing read or attached, and that move is never a disclosure.
theorem other_intent_no_disclosure (c : Context P) (t : RecordId) (e : EntryPoint)
    (hm : ¬ Reached c) (hs : ¬ AsksSteps c) (hi : otherIntent c = some e) :
    advance c (.horizonProbe t) .cont = .gate c (redirect c e) ∧ ∀ t', redirect c e ≠ .reveal t'

A probe's answer, or the answer to a disclosure's application question, read as aimed at another
intent moves there the same way, before any objection is raised against it.
theorem probe_other_intent (c : Context P) (t : RecordId) (g : Selectable) (e : EntryPoint)
    (hi : otherIntent c = some e) : advance c (.probe t g) .cont = .gate c (redirect c e)

theorem reveal_other_intent (c : Context P) (t : RecordId) (e : EntryPoint)
    (hi : otherIntent c = some e) : advance c (.reveal t) .cont = .gate c (redirect c e)

An utterance that sets aside your intent reading is read at the gate the missed answer answered.
theorem correction_reopens (c : Context P) (g g₀ : Gate) (h : restored c = some g₀) :
    reopened c g = g₀

A user who asks for a step instead of answering gets a cue that still does not name the edge.
theorem steps_cue (c : Context P) (t : RecordId) (hm : ¬ Reached c) (hs : AsksSteps c) :
    advance c (.horizonProbe t) .cont = .gate c (.cue t)

An aspect the user chose yields to an admissible Horizon not yet asked, where no contradiction the
user holds a side of comes first.
theorem choice_yields_to_horizon (c : Context P) (g : Gate) (t : RecordId)
    (hu : ¬ UserConflictDue c t) (hd : HorizonDue c t) :
    aspectStep c g t = .gate c (.horizonProbe t)

A Horizon answer that reached the edge is taken; the loop returns to the task.
theorem reached_taken (c : Context P) (t : RecordId) (hr : Reached c) :
    advance c (.horizonProbe t) .cont = .gate c (settle c t (.coverage t))

No adjudication is reached at a probe's answer: nothing is read or attached there, and the next
gate is the inquiry, a return to the task, or where an intent read in the answer points.
theorem no_adjudication_at_probe (c : Context P) (t : RecordId) (g : Selectable) :
    advance c (.probe t g) .cont = .gate c (.inquiry t g.val) ∨
      advance c (.probe t g) .cont = .gate c (settle c t (.coverage t)) ∨
      ∃ e, advance c (.probe t g) .cont = .gate c (redirect c e)

Every answer yields the next gate, convergence only on the user's completion, or the end only on
the user's withdrawal.
theorem advance_shape (c : Context P) (g : Gate) (v : Verdict) :
    (∃ c₁ g₁, advance c g v = .gate c₁ g₁) ∨
      (v = .complete ∧ ∃ t, advance c g v = .done (c ++ t)) ∨
      (v = .withdraw ∧ advance c g v = .withdrawn c)

A proposal is recorded and the loop resumes where it was.
theorem proposal_resumes (c : Context P) (g : Gate) :
    advance c g .propose = .gate (c ++ (eject c).map (·.val)) (resumeOf g)

Where the user's reasoning defeats the objection, nothing is read or attached.
theorem defeated_attaches_nothing (c : Context P) (t : RecordId) (g : GapType)
    (hs : ¬ Stands c) : advance c (.inquiry t g) .cont = .gate c (settle c t (.coverage t))
-/

/-! ── CONVERGENCE ──
converged: every selected task completed — each carried to where the user closed it. What
convergence establishes is that the loop ran out over the aspects in play: those the user
selected, every admissible Horizon, which is asked before any selection and never offered at
one, and every contradiction the context showed, taken up by whose it was. It re-evaluates no round: an aspect closed with sufficient was closed on the user's judgment
rather than by a demonstration, and an answer merely taken — nothing to object to, or nothing to
check it against — was never demonstrated. What is shown is what you read an answer to reach
against the target: a Horizon edge reached on the user's own or after a cue, an application
after a disclosure, an aspect whose adjudication the user's answer met — each recorded with how,
and what followed a disclosure or a cue never as independent detection; each round's closure said
which. Where a round settled an aspect or disclosed an edge, it did so
against your reading of the target, quoted from the target itself, so the user weighed that
material rather than your account of it. A withdrawal is its own ending: what was shown stays on
record and nothing the user did not close is completed.
-/

/-!
Verified understanding follows only a user's utterance that closed the last task.
theorem verified_by_person (respond : Context P → Gate → Response P)
    (trace : Context P → Response P) (c : Context P) (us : List (Utterance P))
    (v : VerifiedUnderstanding P) (hv : grasp respond trace c us = .verified v) :
    ∃ (c₀ : Context P) (u : Utterance P), verdict (fuse c₀ u) = .complete ∧
      ∃ t, v.context = fuse c₀ u ++ t

A run ends withdrawn only on the user's own withdrawal.
theorem withdrawn_by_person (respond : Context P → Gate → Response P)
    (trace : Context P → Response P) (c : Context P) (us : List (Utterance P))
    (c₁ : Context P) (d : List String) (hw : grasp respond trace c us = .withdrawn c₁ d) :
    ∃ (c₀ : Context P) (u : Utterance P), verdict (fuse c₀ u) = .withdraw ∧
      ∃ t, c₁ = fuse c₀ u ++ t

A task, a selection, and a chosen aspect are each filled only by the user's statement.
theorem completed_by_utterance {c : Context P} {t : RecordId} {s : Cite c}
    (ok : (completionCoord (P := P) t).admits s.kind) : s.kind = .utterance

theorem selected_by_utterance {c : Context P} {s : Cite c}
    (ok : (selectionCoord (P := P)).admits s.kind) : s.kind = .utterance

theorem aspect_by_utterance {c : Context P} {s : Cite c}
    (ok : (aspectCoord (P := P)).admits s.kind) : s.kind = .utterance

An offered or chosen aspect is never the Horizon, and never a contradiction.
theorem selectable_not_horizon (g : Selectable) : g.val ≠ .horizon

theorem selectable_not_contradiction (g : Selectable) : g.val ≠ .contradiction
-/

/-! ── TOOL GROUNDING ── -/
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
-- Interpretive transparency (Basis:) intentionally absent: Socratic verification requires AI judgment opacity — surfacing reasoning would compromise probe authenticity. Attaching the material an adjudication was drawn from is a separate axis and is not suppressed by that declaration: it fires only after an answer, only where an adjudication stands against it or a Horizon answer missed the edge, and it carries the material adjudicated or disclosed from rather than the reasoning path that selected it. Stated cost, taken rather than solved: an excerpt attached at one aspect can contain what a later probe on another aspect would have asked for; the narrowest span reduces that and nothing removes it

inductive Annot | sense | observe | track | transform | dispatch | constitution | extension

inductive Op | orient | deriveEntries | assessRoute | routeRelay | entrySelection | materialize
             | register | touch | detect | horizon | horizonProbe | cue | intent | reveal | zeroGap
             | contradiction | order | conflict | resolve | conflictRelay | startAspect
             | probe | inquiry | attach | closure | coverage | update | eject | readAnswer
             | withdrawal | converge | seam

def grounding : Op → Annot × String
  | .orient         => (.observe, "artifact read (if needed): infer likely comprehension intents from the target and the user's wording")
  | .deriveEntries  => (.sense, "Internal analysis: intent-scented entry points derived from the intents and the target")
  | .assessRoute    => (.sense, "Internal analysis: entry-point adequacy annotations — the intent each serves, its anchor hint, the cheapest probe target, hidden routes, and bounded open questions; opacity-preserving, exposing selection scent and never a probe answer")
  | .routeRelay     => (.extension, "TextPresent+Proceed: entry-fit distinctions, hidden routes, and bounded open questions from the route map; omitted when empty")
  | .entrySelection => (.constitution, "present: entry selection enriched by the route map; single by default, an ordered list when the user names several concerns; a path the user writes stays valid; opened again when a missed answer is read as aimed at an intent no registered task serves, with that intent named among the entries and the task the user then selects opened first")
  | .materialize    => (.sense, "Internal analysis: the artifact basis for every selected entry point, a path the user wrote included")
  | .register       => (.track, "record: one per selected entry point; each write returns the identity every later record update names")
  | .touch          => (.track, "record update: names the task as its verification begins")
  | .detect         => (.sense, "Internal analysis: the gap types relevant to the task's entry point, read on the fused context")
  | .horizon        => (.sense, "Internal analysis: the admissible-Horizon guard, read again after every utterance — exactly one qualifying candidate, evidence-bound, material, unspoken in the signal and every answer so far, neither a route-selection question nor a decision gap — and whether that edge was already asked, read from your own turns; never exposed before a miss")
  | .horizonProbe   => (.constitution, "present (conditional: an admissible Horizon not yet asked for the task): the preempting Horizon probe, before the start-aspect selector and before a return to the task's gates — an everyday scenario only, never a Horizon label, the edge, an expected answer, or the rationale; an answer that reaches the edge is taken, one that misses it is disclosed")
  | .cue            => (.constitution, "present (conditional: the user asked to go step by step instead of answering a Horizon probe or a cue): a cue toward the edge that still does not name it; its answer is read as a Horizon answer is")
  | .intent         => (.sense, "Internal analysis: at an answer that missed what its question was after — a Horizon answer that neither reached the edge nor asked for a step, a probe's answer, an explanation that did not dissolve a contradiction, or the answer to a disclosure's application question — whether it was aimed at a different intent than the question's task serves, read from the fused context and never asked; where it was, the closure offers that reading as a candidate — what was read, from what, and where the loop moves — with an invitation to say otherwise in the same turn, the loop moves to the task or entry that intent points at, and nothing is disclosed; an utterance that sets that reading aside reopens the gate the missed answer answered, where it is read again as a miss within its own intent")
  | .reveal         => (.constitution, "present (conditional: the answer to a Horizon probe or a cue missed the edge, asked for no step, and was not read as aimed at another intent): the disclosure — the edge named, the material from the target it rests on quoted in place at the narrowest span, and an application question; never a second concealed scenario")
  | .zeroGap        => (.constitution, "present (conditional: no gap for the task): the zero-gap finding with its reasoning; Confirm completes the task, Reopen(description) adds the named gap and resumes verification")
  | .contradiction  => (.sense, "Internal analysis: the contradiction due for the task, read again after every utterance over the fused context — two statements that cannot both hold, each quoted where it stands, admitted only where both sides are in the context with their sources and speak to the same scope under the same premises, one claim appearing again (the target, your quote of it, an explanation of yours drawn from it) counting as one side — and where its sides come from: two of the user's statements, the user's understanding against the target, two places in the target, or an explanation of yours against the target")
  | .order          => (.sense, "Internal analysis: which due item the task takes up next — a contradiction the user holds a side of first, then an admissible Horizon, then the task's gates — said in the presentation with its basis whenever a contradiction opens ahead of another item due; a Horizon opening ahead of a chosen aspect says only that the aspect comes next, its precedence said in the closure after its answer")
  | .conflict       => (.constitution, "present (conditional: a contradiction the user holds a side of is due): both sides quoted where they stand, and a request to explain how they fit — no verdict yet; an explanation that shows how they fit dissolves it, one aimed at another intent moves there, one that leaves it standing is followed by its resolution where the target or a cited source settles it, and otherwise by a closure saying nothing settles it, with no verdict")
  | .resolve        => (.constitution, "present (conditional: the user's explanation left a contradiction standing within the question's own intent, and the target or a source they cited settles it): both sides, the material from the target that bears on it quoted in place at the narrowest span, the reason one side does not hold, and an application question")
  | .conflictRelay  => (.extension, "TextPresent+Proceed: before the next gate, a contradiction the user holds no side of — one inside the target shown as a finding about the target, saying which side holds only where evidence outside it settles that; one against an explanation of yours shown as your correction of that explanation with the target's material — never handed to the user to settle")
  | .startAspect    => (.constitution, "present (conditional: gaps to offer, nothing probed yet for the task): which aspect to start with, over the task's gaps")
  | .probe          => (.constitution, "present: the probe of the bound aspect in the form probeKind gives it — Qc for Expectation and Sequence, Qs for Causality, Scope, and Emergent — after the selected artifact context and a concrete scenario, with a free-response path")
  | .inquiry        => (.constitution, "present: the reasoning inquiry on an objection to the answer, whole or partial, opened before anything is settled")
  | .attach         => (.observe, "artifact read + excerpt attachment: read whatever the standing adjudication, the missed Horizon, or the contradiction left standing rests on — the target itself, or a source the user cited that can be read now, in any form — and quote in place the narrowest span it rests on — only once an adjudication stands after the user's reasoning, a Horizon answer missed the edge within the probe's own intent asking for no step, or the user's explanation left a contradiction standing within its own intent and that material settles it; a locator the user must open is not an attachment")
  | .closure        => (.extension, "TextPresent+Proceed: the continuation closure — the round's outcome, any side branch with its record, a missed answer read as aimed at another intent offered as that candidate reading with what it was read from and an invitation to say otherwise, a contradiction dissolved or resolved, the task's status, the return point, and the next moves — before coverage or the resumed gate, never in place of a gate")
  | .coverage       => (.constitution, "present: aspect coverage — probed and unprobed aspects, the Horizon never among the offers; sufficient, another aspect, or a proposal")
  | .update         => (.track, "record update: marks the closed task completed, naming the identity its registration returned")
  | .eject          => (.track, "record: a proposal verbatim, outside the task set; the closure says it was read as a proposal and the gate it came from opens again")
  | .readAnswer     => (.sense, "Internal analysis: the whole latest utterance read with the context — its verdict, the selection, the chosen aspect, whether a Horizon answer reached the edge, whether an explanation dissolved a contradiction and whether material settles one it left standing, whether a missed answer was aimed at another intent, the objection, and whether an adjudication stands")
  | .withdrawal     => (.extension, "TextPresent+Proceed: on the user's withdrawal, what was shown so far — each aspect with how it was shown, each contradiction taken up with how it ended, and each missed answer read as aimed at another intent — and any dissent; no task the user did not close is completed")
  | .converge       => (.extension, "TextPresent+Proceed: the convergence trace, presented before VerifiedUnderstanding is returned — each task with its status, the aspects detected for it (the Horizon among them where one was asked), and each aspect shown with how it was shown: independently, or through an application after a disclosure or a cue; each contradiction taken up, where its sides came from, and how it ended — dissolved by the user's explanation, resolved after its disclosure, a finding about the target, or your correction; each missed answer read as aimed at another intent, with what was read; any dissent attached to a closure")
  | .seam           => (.extension, "TextPresent+Proceed: at a user-declared chain naming the next protocol, proceed to it citing that source; this protocol declares no wired outbound edge, and every Constitution gate inside this protocol and the next fires unchanged")

/-! ── 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.

Loaded safety boundaries, capability restrictions, and explicit user instructions continue to bind while Katalepsis is active.

## Protocol

### Intent-scented entry rendering

Derive up to three first-turn labels from the user's likely comprehension intent — Orientation, Rationale, Impact, Approval, Transfer, or an Emergent intent — and phrase each as what the user will understand, decide, explain, or change by taking that path. Keep Code, Plan, Document, Analysis, Model, or mixed artifact bases behind those labels as grounding anchors. Descriptions state what becomes clear and why it matters; route-map metadata may enrich a label but never reveal a probe answer or reasoning path. A user-authored path remains valid when it stays within `TargetUngrasped → VerifiedUnderstanding`; multiple concerns the user already named become the ordered task list directly.

### Verification rendering and safeguards

Present the selected artifact context and a concrete scenario before each probe. For non-Horizon classificatory probes, render recognizable correct, partial, and misconception trajectories with domain-specific consequences; constitutive probes invite the user's own reasoning, and every probe preserves a free-response path.

Read whether a Horizon is due again after every answer, over the whole context: an edge the user has since spoken is not asked, an answer can bring a new one into view, and one already asked is not asked again. Ask it through its everyday scenario only, never its label, suspected edge, expected answer, or rationale before the answer. An answer that reaches the edge is taken. Before disclosing anything after a missed answer — at a Horizon probe, a cue, an ordinary probe, or a disclosure's application question — read from the whole context whether it was aimed at a different intent than the probe's task serves: another question or purpose the user is actually pursuing. That reading is yours, made without asking, and you offer it as a candidate rather than assert it: where you read another intent, say in the closure what you read and from what, move to the task serving it — or reopen entry selection with that intent named when no task does — and in the same turn invite the user to say otherwise ("this reads as asking about X, so I am moving there — say so if not"); disclose nothing. The user's next utterance corrects a wrong reading: where it says the answer was aimed at the original question after all, read that answer again at the gate it answered, as a miss within its own intent. An answer that misses the edge within the probe's own intent is followed at once by the disclosure: name the edge, quote the material from the target it rests on at the narrowest span, and ask an application question — no second concealed scenario. Where the user asks to go step by step, give a cue first; their utterance steers the next presentation. Record how each aspect was shown — on their own, or through an application after a disclosure or a cue — and never present what followed a disclosure as independent detection. An answer you have an objection to first opens a reasoning inquiry grounded in the user's actual answer. Where that reasoning defeats the objection, nothing is corrected and the round closes as any other unadjudicated one does. Where an adjudication stands after it, target the correction at what that adjudication actually reaches — the disclosed mental model where that is what is wrong, the part it bears on where the rest of the answer stood — and re-probe that aspect.

Read the context for contradictions again after every answer as well: two statements that cannot both hold, each quoted where it stands. Admit one only where both sides are in the context with their sources and speak to the same scope under the same premises; one claim appearing again — the target, your quote of it, an explanation of yours drawn from it — is one side, not two. Take each up by whose it is. Where the user holds a side of it — two of their own statements, or their understanding against the target — it comes before the Horizon: show both sides and ask them to explain how the two fit, with no verdict yet. Where their explanation shows how the sides fit, record it as dissolved and move on. Where it leaves them standing within the question's own intent and the target, or a source they cited that you can read now, settles which side holds, show both sides again with that material quoted in place and the reason one side does not hold, then ask an application question. Where nothing you can attach settles it, give no verdict: say that both sides stand and that you have nothing to settle it with, and leave it theirs. A contradiction inside the target itself is a finding about the target: show it before the next gate and say which side holds only where evidence outside the target settles that. One between an explanation you gave earlier and the target is yours: correct your explanation with the target's material before the next gate, and do not hand it to the user to settle. Whenever a contradiction the user holds a side of opens ahead of another item due for the task, say the order you read and why ("I am taking this first because …"). A Horizon probe that opens ahead of an aspect the user chose says only that their aspect comes next; why the Horizon came first waits for the closure after its answer, since the probe carries its scenario and nothing else.

Treat a response as a proposal side branch only when it suggests a system change and either introduces matter outside `R` or directs action at the system; explanation, navigation, and clarification requests remain in the comprehension loop. Record a proposal verbatim, emit the side-branch closure saying the answer was read as a proposal, and open again the gate it came from — a proposal at the Horizon probe resumes at that task's coverage — without turning it into a comprehension task. The reading is yours and closes nothing: an answer the user meant as an answer is answered at that gate.

When you adjudicate against the user's answer, attach what you adjudicated from. Quote that material in place, at the narrowest span that actually supports the correction — enough that they can read it where they are and argue with it, and no wider, since a dump costs them the reading and buries what the verdict turned on. A pointer they have to go open is not an attachment. The accumulated context and what the user says steer which reading is in play; they are not what you adjudicate from. An ordinary assertion about the target does not license you to adjudicate that same assertion, and something the session said earlier does not stand as the measure against what the target says now. What does stand is the target itself, or a source they cited that you can read now. A ground you cannot attach is not a ground you can adjudicate from here — this instrument admits exactly what it can quote.

Where the attached material admits more than one reading, say which one you took and that it could go another way — beside the excerpt, so they weigh your reading against the same material rather than against your confidence in it. Where you have nothing to attach, do not adjudicate at all: take the answer, say you have no ground to check it against, and name what you would have needed. They may let the aspect stand on their own account, or move on to another; neither is a demonstrated aspect and the closure says so.

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 trace, or phase order determines whether text belongs before or inside a gate.

### Intensity

| Level | Realization |
|-------|-------------|
| Light | One Constitution probe of core understanding |
| Medium | One scenario probe of prediction or impact |
| Heavy | Decomposed probes of causal or sequential understanding |

## 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; a withdrawal during a run ends it with what was shown on record, and leaving without saying so is the host's to deliver.
- **Intent scent before artifact taxonomy**: First user-facing options name the user's likely comprehension outcome; artifact categories remain grounding material.
- **User authority**: The user's account of what they understand stands for the ground it covers. Do not probe that ground again.
- **Rebuttable adjudication**: When you adjudicate against the user's answer, attach the material you adjudicated from — the target itself, or a source they cited that you can read now — quoted in place, at the narrowest span that supports the correction, never a locator they must open and never wider than the verdict. Where that material admits another reading, say which one you took, beside it. Where you have nothing to attach, do not adjudicate: take the answer, say you cannot check it, and name what you would have needed; what follows is attested or set aside, never demonstrated.
- **Proposal ejection and continuation**: Externalize a qualifying proposal without closing Katalepsis. Keep its record reference outside the task set, say in the closure that it was read as a proposal and where the loop resumes, then open again the gate it came from.
- **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 (your own adjudication included, its evidence being the excerpt attached with it), and place analytical context before its gate.
9a. **Post-answer closure**: After an answer the comprehension loop kept and no adjudication stands against — an ejected proposal takes the continuation closure named above instead — emit the aspect's outcome as the closure records it, with current task status, the gate the loop returns to, and next available moves before coverage routing.
9b. **Active-turn fail-closed**: While a run is active, end every turn in one `Gate`; relay context and continuation metadata may precede it but never replace it.
- **Zero-gap surfacing**: The zero-gap finding carries its reasoning to its gate; only `Confirm` completes the entry, while `Reopen(description)` adds the named Emergent gap and resumes verification.
- **Intent before disclosure**: After a missed answer, read its intent before disclosing or objecting: an answer aimed at another question or purpose than the probe's moves there, and nothing is disclosed against it. Offer the reading as a candidate — what you read, from what, where you move — with an invitation to say otherwise in the same turn; it adds no question and yields to the user's next utterance.
- **Contradictions by whose they are**: A contradiction the user holds a side of comes first and asks for their explanation before any verdict; one left standing is shown with both sides, the target's material, and the reason, then applied — only where the target or a cited source settles it, and with nothing to settle it no verdict is given. One inside the target is a finding about the target; one against your own earlier explanation is yours to correct. Admit one only where both sides stand in the context with sources, same scope, same premises. Say the order you read whenever such a contradiction opens ahead of another item due; a Horizon's precedence is said only after its answer.
14a. **Horizon boundary**: Horizon is an evidence-bound comprehension edge inside the selected entry point, not route selection, a decision gap, reframing, or perspective fusion. Admit it only through `admissible`, read again on the fused context after every answer; ask each edge once, through its scenario only; disclose it with its material when the answer misses it; and demote or revise the instrumentation after repeated applicable opportunities if detections remain absent, speculative, or unhelpful.
- **Form feedback**: Derive each round's density from the current request; carry an explicit form instruction until countermanded. Change form directly. Content, wording, order, cadence, and turn boundaries fixed elsewhere remain fixed; state what changed and, where the instruction overlaps a fixed element, what stays and why.