sketch · diff

git:20260907.2d8a782 to git:20260926.4f542e6

655 added, 248 removed. Audit A to A.

---
name: sketch
description: "Recognize and revise concrete sketches to discover a form when descriptions cannot settle intent. Type: (FitUnrecognized, Hybrid, SKETCH-RECOGNIZE-CYCLE, FormIntentSeed) → RecognizedForm"
---
# Hypotyposis Protocol
Discover what a form should be by encountering concrete sketches and marking what does not fit, until the user recognizes a specific version as the form for a stated purpose. Type: `(FitUnrecognized, Hybrid, SKETCH-RECOGNIZE-CYCLE, FormIntentSeed) → RecognizedForm`.
## Definition
- **Hypotyposis** (ὑποτύπωσις): an outline or sketch — a first drawing of a position rather than its finished statement. A dialogical act for the moment when a form has to be made and the intent behind it cannot yet be settled from descriptions: the user can say what is wrong with a thing in front of them long before they can say what the thing should be, because good fit has no positive description of its own while each misfit is immediate and can be pointed at (Alexander, 1964). So the protocol runs the other way round from a specification: the AI drafts each round's focus, the perception it needs, and its variants, relays the draft with the basis that chose each, and produces the sketches; the user marks a specific version — what does not fit and what to keep — as first-class utterances, settling or sending back the round's readings in the same answer; the AI revises the retained version under those marks; and the loop ends when the user recognizes one version as the form for a stated purpose and names where it lives.
+ **Hypotyposis** (ὑποτύπωσις): an outline or sketch — a first drawing of a position rather than its finished statement. A dialogical act for the moment when a form has to be made and the intent behind it cannot yet be settled from descriptions: the user can say what is wrong with a thing in front of them long before they can say what the thing should be, because good fit has no positive description of its own while each misfit is immediate and can be pointed at (Alexander, 1964). So the protocol runs the other way round from a specification: the AI drafts what the next sketches should try and relays that draft with the basis that chose each part, then produces the sketches; the user marks a specific version — what does not fit and what to keep — as first-class utterances, settling or sending back the readings shown beside it in the same answer; the AI revises the retained version under those marks; and the run ends when the user recognizes one version as the form for a stated purpose and names where it lives.
- ```
- ── FLOW ──
- Hypotyposis(I) → detect(I, ctx) →
- [¬fit_unrecognized(I, ctx)] no_activation_relay → exit (NoActivationRelay)
- bind(I) → Λ.history (each prior item as Settled | Candidate, provenance kept) → Λ.round := 1 →
- spec_relay(draft(RoundSpec, provisional(Λ))) → Λ.spec := draft → produce(spec, Λ) → Sk →
- present(Sk) → Qfit(Sk, spec.focus) → Stop → M →
- [M = Marks(ms, acts)] act(acts) → record(ms) → interpret(ms) → record(Proposed) → Λ.round += 1 → spec_relay
- [M = Fit(w, acts)] act(acts) → w.context_revision := Λ.context_revision → Λ.fit_witnesses ∪= {w} → Λ.round += 1 → spec_relay -- one focus adequate; the loop continues
- [free response: spec revision] revise(draft, rev) → spec_relay (scoped to the revision; no new round counted)
- [M = Finish(rec, acts)] act(acts) → rec.context_revision := Λ.context_revision → Λ.recognition := Some(rec) → Qplace → Stop → P → harvest → account →
- [retention verified] RecognizedForm
- [retention failed] declare → Qplace (re-presented with the failure; the same location is admissible)
- [M = Withdraw] account → EarlyExit
- [either party, at the spec relay or at any gate: recognition needs no further encounter ∨ activation premise collapsed]
- dissolution_relay → account → DissolutionExit
- [either party, at the spec relay or at any gate: a sibling deficit is demonstrated ∨ a realization the round requires is unavailable]
- boundary_relay → account → BoundaryExit
+ ```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.
+ -/
- ── MORPHISM ──
+ /-! ── FLOW ──
+ Hypotyposis(I) → start(c) → sketch(c, utterances), where c is the fused session context:
+ [fitUnrecognized fails] the non-activation basis → not activated
+ [a realization the run needs is shown unsuppliable] the boundary relay → account → BoundaryExit
+ round(c): the spec relay — what the next sketches try, the perception the judgment needs, the
+ variant briefs, and every provisional reading, each with its basis; it yields no turn →
+ produce → present → Qfit → Stop
+ next utterance u: c' := fuse(c, u), every reading below taken afresh on c' →
+ [the person withdraws] account → EarlyExit
+ [the person accepts that no form is owed, its ground and your contrary grounds in view]
+ account → DissolutionExit
+ [the person names where the run goes next, its ground and your contrary grounds in view]
+ account → Routed
+ (either closing taken without them in view: the gate again, with them shown)
+ [a realization the run needs is shown unsuppliable] the boundary relay → account → BoundaryExit
+ [a recognition and a placement stand on c', taken with what they need in view]
+ retain and verify → every placed reference resolves: release the rest → RecognizedForm
+ | a reference failed: Qplace again with the failure and every copy
+ already written shown; nothing released
+ [a recognition stands, unplaced] Qplace
+ [the answer calls for new sketches] round(c') → Qfit
+ [otherwise — an interrogation, an answer with no marks and no acts] the gate again
+ no utterance: the gate holds; nothing is recognized, placed, or released
+ -/
+
+ /-! ── MORPHISM ──
FormIntentSeed
- → detect -- deficit predicate over the utterance and accumulated context (silent analysis)
- → bind -- prior material enters the history as Settled or Candidate, provenance kept
- → relay_round -- Extension: focus, realization, and targets drafted with the basis that chose each, relayed beside the provisional coordinates; nothing is settled here
- → produce -- transform: one sketch per brief — a brief naming a parent revises that retained version, a parentless brief generates from the material it names or from prior material — and declares what producing it determined that no coordinate covered
- → present -- relay: each sketch from its typed concretum, what this round can and cannot expose, and whether an artifact was observed
- → recognize -- Constitution: marks on a specific version — Marks | Fit | Finish | Withdraw; the same answer promotes, supersedes, or holds the coordinates in view
- → record -- track: every mark, and every interpretation read from it, enters the append-only history; interpretations stay provisional
- → place -- Constitution: where the recognized concretum lives beyond the session, and which versions the run passed over are kept as revert points; no default for either
- → harvest -- active commitments, recognition witness, trace, and residual recorded before release
- → account -- per-sketch retain-or-release disposition, verified
+ → detect -- deficit predicate over the utterance and the context (silent analysis)
+ → bind -- prior material read from the context: settled where a person's utterance in it settled it, a candidate otherwise, provenance kept
+ → relay_round -- what the next sketches try, the perception the judgment needs, and the variant briefs, drafted with the basis that chose each and relayed beside the provisional readings; nothing is settled here
+ → produce -- one sketch per brief: a brief naming parents revises those retained versions, a brief naming none generates from the material it names or from prior material; each declares what producing it determined that no settled value covered
+ → present -- each sketch from its concretum, what this realization cannot expose, whether an artifact was observed, what it was checked against, what it moved from a value the person settled, where the run stands, and any contrary ground held about it
+ → recognize -- the person's words on a specific version: what does not fit, what to keep, an aspect that is right, the version that is the form for a stated purpose — and, in the same answer, the readings they settle, replace, or retire
+ → place -- the person names where the recognized version lives and which passed-over versions are kept as revert points; no default for either
+ → account -- every placed reference retained and verified, every other sketch released and verified, every copy written accounted for where it was written
→ RecognizedForm
requires: form_purpose_in_scope(I) -- runtime checkpoint (Phase 0): the work is about to make a form
deficit: FitUnrecognized -- activation precondition (Layer 1/2)
- preserves: utterance(I) -- I.utterance is read-only; the history accumulates beside it
- invariant: Concretum Retention -- a brief that revises does so on a retained parent; a sketch under judgment is never regenerated from coordinates alone
- invariant: Commitment Provenance Preservation -- a prior constitutive act stays recorded; a later user act may supersede its operative determination; AI inference alone never supersedes a user commitment
- invariant: Recognition over Description -- fit is the user's recognition of a specific version for a stated purpose
+ preserves: utterance(I) -- the context only grows; the seed is never rewritten
+ invariant: Concretum Retention -- a brief that revises does so on retained parents; a sketch under judgment is never regenerated from settled values alone
+ invariant: Commitment Provenance Preservation -- a value is settled only by a person's utterance, on the scope their words reach; a later one may replace what an earlier one settled; AI inference alone settles or replaces nothing
+ invariant: Recognition over Description -- fit is the person's recognition of a specific version, as it was presented, for a stated purpose
+ invariant: the person recognizes, places, and closes; your judgments stand as proposals and contrary grounds
+ -/
- ── TYPES ──
- I = FormIntentSeed { utterance: String, prior: List(ReferencedMaterial) }
- -- Input type: morphism processes I uniformly; prior is source-neutral — a settled direction, a resolved intent,
- -- a candidate field, an existing artifact, a prior session's record — each named by the user or already in context
- ReferencedMaterial = { source: String, content: String } -- what it is and where it came from; no sibling type is a runtime dependency
- Binding = Settled(Coordinate) | Candidate(ReferencedMaterial) -- how a prior item enters the history at bind: a commitment the user already made, or material to draw on
- fit_unrecognized(I, ctx) = a form-making purpose is in scope
- ∧ decision-relevant intent remains underdetermined
- ∧ encountering and revising a concrete proposal is what would constitute that intent
- ∧ the resolution sought is a recognized form with its commitments and residuals
- Axis = String -- emergent label: "information unit", "reading order", "density", "tone"
- Focus = Axis | Question(String) -- what this round filters attention toward; an unexpected misfit on any other axis stays admissible
- Value = String -- a determination on an axis, in the user's words or read off the sketch
- Realization = capability description -- what this round's judgment needs in order to be possible: the perception it rests on
- -- (narration, spatial layout, interaction, sound, …) and, where the focus opens an axis carrying a standard
- -- outside both parties' preference, the referent it is checked against. Open, named per round — and a referent
- -- the round requires that this session cannot supply is the boundary arm's condition rather than something to
- -- proceed without
- VariantBrief = { parent: Optional(SketchRef), source: Optional(ReferencedMaterial), commits: Map(Axis, Value) }
- -- one sketch to produce. Some(parent): revise that retained version. None: generate from active_coords and
- -- from the material `source` names, or from the bound prior material where it names none — every brief of round 1's
- -- first pass, and a fresh start the user names at Qfit for a later round; a SpecRevision re-entry that keeps a version
- -- names it as parent, so the re-drafted round revises the retained version rather than regenerating it
- -- a round that changes where the material comes from is a parentless brief naming the new source, not a
- -- different kind of round: what the loop does is unchanged, and what moved is only what "generate" draws on
- RoundSpec = { focus: Focus, realization: Realization, targets: NonEmptyList(VariantBrief) }
- -- k = |targets| is drafted here; a count the user settled at a recognition gate holds until they revise it
- Supersession = { of: Coordinate, by: Optional(Coordinate) } -- the user's act on a coordinate in view: by = Some(c') replaces it with a determination the user states (c' enters Settled, basis Utterance), by = None retires it with nothing in its place
- CoordinateActs = { settlements: Set(Coordinate), supersessions: Set(Supersession) }
- -- the user's acts on the coordinates in view, riding the recognition answer: which provisional coordinates become
- -- Settled and which coordinates — Provisional or Settled — they supersede; either set possibly empty
- SpecRevision = a change to this round's focus, realization, or targets, named by the user as a free response at the recognition
- gate; the spec relay re-presents scoped to it and no new round is counted
- SketchRef = { id: ℕ, round: ℕ } -- identity of one version; the harvest and every mark point at one of these
- Concretum = Text(value) | Artifact(versioned_ref) -- Text: narration carried in session text; Artifact: a file under temp isolation, versioned at creation
- Sketch = { ref: SketchRef, parents: List(SketchRef), concretum: Concretum, rendered_from: snapshot(active_coords), focus: Focus }
- -- what it was rendered under that no Settled or Provisional coordinate covered — its brief's commits and what producing it determined — reaches the history as Proposed coordinates basis Production(ref),
- -- so a sketch's own determinations are read back by its reference rather than stored a second time
- Anchor = Element(locator) | Region(bounds) | Whole | Span(text) -- where on a sketch a mark points; Whole admits "something is missing here" with nothing to point at
- -- premise: a mark points at a place. A property recurring across the sketch sits at none, and arrives as Whole
- -- with the property itself in the mark's utterance and, where it names one, its axis — carried whole, not classified
- Mark = Misfit { sketch: SketchRef, anchor: Anchor, utterance: String, axis: Optional(Axis) }
- | Keep { sketch: SketchRef, anchor: Anchor, utterance: String }
- -- a user utterance anchored on a version; Keep is the positive half of mixed feedback and is retained, never dropped
- Status = Provisional | Settled
- Coordinate = { axis: Axis, value: Value, basis: Mark | Binding | Utterance | Production(SketchRef), status: Status, round: ℕ }
- -- interpret() yields Provisional only; Settled requires the user's act at Qfit or a convention already on record
- -- Production(ref): a determination rendered into that sketch that no Settled or Provisional coordinate covered — drafted in its brief or made while producing.
- -- Provisional like any reading, and settled or superseded only by the user's act at the next recognition gate —
- -- production introduces determinations, it never settles them
- Event = Bound(Binding) | Marked(Mark) | Proposed(Coordinate) | Promoted(Coordinate) | Superseded(Coordinate, by: Optional(Coordinate)) | Witnessed(FitWitness)
- -- Superseded is appended by supersede at Qfit and nowhere else: the user's act is its only producer, so an AI interpretation the user rejects leaves provisional(Λ) and a determination the user replaces leaves active_coords
- -- Proposed is appended by interpret and by produce: a coordinate the AI puts forward, whichever step reached it.
- -- Its basis says which, and its lifecycle is one — presented at the spec relay and again beside the sketch at Qfit, promoted or superseded there, residual otherwise
- active_coords(Λ) = fold(Λ.history) -- the operative determinations now: per axis, the latest Settled coordinate with no Superseded(it, _) after it — Superseded(c, Some(c')) makes c' operative in c's place, Superseded(c, None) retires c with nothing in its place; Provisional ones shown beside
- provisional(Λ) = { c : Proposed(c) ∈ Λ.history ∧ ¬∃ Promoted(c) ∈ Λ.history ∧ ¬∃ Superseded(c, _) ∈ Λ.history }
- -- what the AI read from a mark or decided while producing, awaiting the user's act at Qfit; derived from the history, never stored apart
- FitWitness = { sketch: SketchRef, context_revision: ℕ, scope: Focus, utterance: String }
- -- adequacy on one focus for one version; bound to the context revision the answer carrying it left, acts included; stale once its sketch is superseded or the context revision moves — shown as stale, never reused silently
- Recognition = { target: SketchRef, context_revision: ℕ, purpose_scope: String, residual: Set(Axis) }
- -- target must be a presented, retained version; Finish is recognition of the assembled form, not of one focus
- M = Recognition gate answer ∈ {Marks(Set(Mark), CoordinateActs), Fit(FitWitness, CoordinateActs), Finish(Recognition, CoordinateActs), Withdraw}
- -- the acts ride Marks, Fit, and Finish: the answer that judges the version also settles or sends back the readings shown
- -- beside it, and an answer naming none carries empty sets; a settlement stated in the Finish answer reaches commitments
- -- through the same act, and what is still Provisional after it is declared in the result's provisional set; Withdraw
- -- carries none — nothing it settled would be read
- -- Marks(∅, ∅) is read as Stop, never as Fit; Marks(∅, acts) with acts non-empty moves the coordinates and re-enters the
- -- next round as any Marks does; silence yields the turn again; a response carrying both marks and a finish is parsed
- -- as Marks — recognition names an unmarked version
- -- premise: one answer settles this version. An answer also naming what a later round should take up departs from
- -- that premise rather than breaking it — it is parsed by its constructor, and the rest is recorded as itself
- Location = a reference the user judges to outlive the session -- the capability the placement gate asks the user to bind; the protocol supplies no default
- -- the durability is their judgment, not a checked fact: account verifies that the reference resolves to that
- -- version's concretum AT THE MOMENT IT IS CHECKED, which is the narrower of the two claims
- P = Placement gate answer ∈ {Place(Location, kept: Map(SketchRef, Location))}
- -- where the recognized version lives, and which versions that were not recognized are kept as revert points and
- -- where; kept may be empty. On a re-presentation after RetainFailed, either may be the same or another; a
- -- free-response withdrawal here is EarlyExit with the recognition in the partial trace
- Fixture = { ref: Location, target: SketchRef, scope: String, residual: Set(Axis), kept: Map(SketchRef, Location) }
- -- status: recognition witness. It carries no implementation commitment and is not an executable specification
- -- kept: what a later reversal would otherwise have to rebuild. A version the loop passed over is what the
- -- decision could return to, and returning to it costs rebuilding unless it survives as itself
- Disposition ∈ {Retained(Location), Released, ReleaseFailed(reason), RetainFailed(reason)}
- -- Retained is written only once verification holds: the reference resolves to the recognized version's exact concretum. RetainFailed sends control back to Qplace; ReleaseFailed is declared with a handoff
- TraceEntry = (Mark → Optional(Coordinate) → Optional(SketchRef) → Recognized | Superseded | Residual)
- -- what each mark became: its interpretation, the revision it drove, and how it ended
- ExitCause ∈ {NotActivated, Recognized, Withdrawn, BoundaryReached, Dissolved}
- RecognizedForm = single record { commitments: Set(Coordinate) (Settled only), witness: Fixture, recognition: Recognition,
- trace: List(TraceEntry), residual: Set(Axis ⊎ ReferencedMaterial), provisional: Set(Coordinate) }
- -- assembled after account: the retained concretum is reachable through witness.ref, and what the user named for a
- -- round that never came is declared rather than dropped
- NoActivationRelay = the non-activation basis stated: the failed predicate with its evidence; a sibling deficit visible in the same scan is named as a finding and left to the session
- EarlyExit = withdrawal at any gate: partial trace over completed rounds + account enforced + residual declared (no RecognizedForm returned; any prior recognition remains in the partial trace)
- BoundaryExit = the unresolved obligation named — a sibling deficit demonstrated, or a realization the round requires that this session cannot supply — with account enforced; which protocol takes it is the session's, never this record's
- DissolutionExit = the deficit dissolved during a circulation: the sharpened description made the form recognizable without a further encounter, or the activation premise collapsed; declared by either party with its basis, the surviving determinations relayed, account enforced
- Phase ∈ {0, 1, 2, 3, 4, 5, 6}
+ namespace Hypotyposis
- ── A-BINDING ──
+ /-! ── 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)
+
+ /-!
+ theorem fuse_extends {P : Type} (c : Context P) (u : Utterance P) :
+ ∃ t, fuse c u = c ++ t
+
+ theorem cited_not_assistant {P : Type} {c : Context P} (s : Cite c) :
+ (c[s.idx]'s.lt).origin ≠ .assistant
+
+ theorem cited_not_injected {P : Type} {c : Context P} (s : Cite c) :
+ (c[s.idx]'s.lt).origin ≠ .injected
+ -/
+
+ /-- 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}
+
+ /-- `I`, `FormIntentSeed`: the utterance that asks for a form, and the prior material it names
+ or the context already holds — a settled direction, a resolved intent, a candidate field,
+ an existing artifact, a prior session's record. Source-neutral; read from the context. -/
+ abbrev FormIntentSeed (P : Type) := Context P
+
+ /-- **Your judgment** at Phase 0: a form-making purpose is in scope, decision-relevant intent
+ remains underdetermined, encountering and revising a concrete proposal is what would
+ constitute that intent, and the resolution sought is a recognized form with its
+ commitments and residuals. -/
+ axiom fitUnrecognized : Context P → Prop
+
+ /-- An emergent label: "information unit", "reading order", "density", "tone". -/
+ abbrev Axis := String
+
+ /-- A determination on an axis, in the person's words or read off a sketch. -/
+ abbrev Value := String
+
+ /-- The identity of one version; every mark, placement, and disposition points at one. -/
+ structure SketchRef where
+ id : Nat
+
+ /-- What prior material is and where it came from. -/
+ structure ReferencedMaterial where
+ source : String
+ content : String
+
+ /-- One sketch to produce. With no parents, generate from the settled values and from the
+ material `source` names, or from the bound prior material where it names none — the first
+ sketches, and a fresh start the person names. With one parent, revise that retained version;
+ with several, draw on each as the person's words or the brief say — how they combine is your
+ judgment, stated in the brief, never a fixed merge. A spec revision that keeps a version
+ names it as parent, so the re-drafted sketches revise it rather than regenerating it. A brief
+ may name parents and a new source together: changing where the material comes from does not
+ itself abandon a parent. -/
+ structure VariantBrief where
+ parents : List SketchRef
+ source : Option ReferencedMaterial
+ commits : List (Axis × Value)
+
+ /-- The draft a spec relay presents. What the next sketches try, what perception the judgment
+ needs, and how many variants to produce are your judgment, drafted from the whole context:
+ try what the person's latest words leave most open; where it opens an axis carrying a
+ standard outside both parties' preference, name the referent each sketch is checked against
+ — a referent this session cannot supply is `Unsuppliable`, never something to proceed
+ without; a count the person stated holds on the scope their words reach. -/
+ structure RoundSpec where
+ focus : String
+ realization : String
+ briefs : List VariantBrief
+ nonempty : briefs ≠ []
+
+ /-- `text`: narration carried in session text. `artifact`: a file under temp isolation,
+ versioned at creation. -/
+ inductive Concretum
+ | text (value : String)
+ | artifact (versionedRef : String)
+
+ structure Sketch where
+ ref : SketchRef
+ concretum : Concretum
+
+ /-- **Your record**, read from the context: every version produced so far, each retained for
+ revision until account. -/
+ axiom sketches : Context P → List Sketch
+
+ /-- **Your record**: the round spec your latest relay presented; `none` before the first. -/
+ axiom spec : Context P → Option RoundSpec
+
+ /-- A reference the person judges to outlive the session. The durability is their judgment;
+ account checks only that the reference resolves to that version's concretum when
+ checked. -/
+ abbrev Location := String
+
+ /-- One copy the run wrote: which version, and where — its temp-isolated reference at creation,
+ session text for a Text sketch, or a location the person named. -/
+ structure Copy where
+ ref : SketchRef
+ loc : Location
+
+ /-- **Your record**, read from the context: every copy the run has written, at creation and at
+ every placement attempt. -/
+ axiom written : Context P → List Copy
+
+ inductive Disposition
+ | retained
+ | released
+ | releaseFailed (reason : String)
+ | retainFailed (reason : String)
+
+ /-- **Your reading** of the account observations: what became of each copy — one entry per copy,
+ the latest standing. `retained` is read only where the observation shows the reference
+ resolving to that version's exact concretum. -/
+ axiom dispositions : Context P → List (Copy × Disposition)
+
+ /-- What every spec a relay presents owes (Concretum Retention): each parent a brief names is a
+ version produced with a copy still unreleased. -/
+ def SpecOwes (c : Context P) (s : RoundSpec) : Prop :=
+ ∀ b ∈ s.briefs, ∀ p ∈ b.parents,
+ (∃ x ∈ sketches c, x.ref = p) ∧
+ ∃ w ∈ written c, w.ref = p ∧ (w, Disposition.released) ∉ dispositions c
+
+ /-- A mark: a person's utterance on a version, cited as said. What it points at, whether it
+ names a misfit or something to keep, and which axis it reaches are your reading of it,
+ carried with its basis; a keep is retained, never dropped, and a concern the version's
+ focus did not ask about stays admissible. -/
+ structure Mark (c : Context P) where
+ sketch : SketchRef
+ src : Cite c
+ byPerson : src.src.val = .person
+
+ /-- **Your reading** of every mark the person's utterances placed. -/
+ axiom marks : (c : Context P) → List (Mark c)
+
+ /-- **Your judgment**: the cited turn states or settles value `v` on axis `a` — a settlement of a
+ reading shown beside a version, a replacement the person stated, a statement that a version is
+ right on an aspect (the value as that version shows it), or a commitment they made earlier in
+ this context — read against the context as it now stands, on the scope the person's words
+ reach. -/
+ axiom AxisSupported : Axis → Context P → Turn P → Value → Prop
+
+ /-- A value is settled only by a person's turn. A record of a commitment made in an earlier
+ session is a candidate for it, never its fill. -/
+ def axisCoord (a : Axis) : Coord P Value :=
+ { admits := (·.val = .person), supports := AxisSupported a }
+
+ /-- **Your reading**: how axis `a` stands in `c` — filled by the person's latest turn that
+ settles or replaces it; open where nothing settles it, and where the person retired it with
+ nothing in its place. An open axis carries as candidate the material that proposes a value
+ without settling it, a record of an earlier session's commitment included. A later version
+ that moves a settled value does not unsettle it: the move is a ledger line shown before the
+ next gate. -/
+ axiom operative : (c : Context P) → (a : Axis) → Occ (axisCoord (P := P) a) c
+
+ /-- A determination the AI puts forward: read from a mark, or rendered into a sketch that no
+ settled value covered. It settles nothing; it is shown at the spec relay and again beside
+ the version at Qfit. -/
+ structure Proposal (c : Context P) where
+ axis : Axis
+ value : Value
+ /-- the mark it was read from; `none` for a production's own determination -/
+ mark : Option (Cite c)
+ /-- the version it was rendered into; `none` for a reading of a mark -/
+ sketch : Option SketchRef
+
+ /-- **Your record**, read from the context: the provisional readings — every proposal the person
+ has neither settled, replaced, nor rejected. -/
+ axiom provisional : (c : Context P) → List (Proposal c)
+
+ /-- Recognition of the assembled form, not of one aspect. -/
+ structure Recognition where
+ target : SketchRef
+ purposeScope : String
+ residual : List Axis
+
+ /-- **Your judgment**: the cited turn recognizes `r` — its target a version presented as it
+ stands and still retained, for the purpose it states. Read against the context as it now
+ stands: a later turn that marks the form again, or asks for a version not yet presented,
+ leaves no recognition standing; words about where it lives or which versions are kept leave
+ it standing. Where a turn could be a recognition or a statement that one aspect is right,
+ show your reading before the next gate rather than acting on it. -/
+ axiom RecognitionSupported : Context P → Turn P → Recognition → Prop
+
+ def recognitionCoord : Coord P Recognition :=
+ { admits := (·.val = .person), supports := RecognitionSupported }
+
+ /-- **Your reading**: the recognition that stands on the context as it now stands; `open_`
+ before a finish, and again once a later turn of the person's reopens the form. -/
+ axiom recognition : (c : Context P) → Occ (recognitionCoord (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
+
+ /-- Qplace is open: a recognition stands on the context. -/
+ def Placing (c : Context P) : Prop := isFilled (recognition c) = true
+
+ /-- Where the recognized version lives, and which passed-over versions are kept as revert
+ points and where; `kept` may be empty. -/
+ structure Placement where
+ location : Location
+ kept : List (SketchRef × Location)
+
+ /-- **Your judgment**: the cited turn names this placement for the recognition now standing. -/
+ axiom PlacementSupported : Context P → Turn P → Placement → Prop
+
+ /-- Placement has no default: only the person's turn fills it. -/
+ def placementCoord : Coord P Placement :=
+ { admits := (·.val = .person), supports := PlacementSupported }
+
+ /-- **Your reading**: the placement the person's latest answer at Qplace named. -/
+ axiom placement : (c : Context P) → Occ (placementCoord (P := P)) c
+
+ /-- `Fixture`: a recognition witness. It carries no implementation commitment and is not an
+ executable specification. -/
+ structure Fixture where
+ ref : Location
+ target : SketchRef
+ scope : String
+ residual : List Axis
+ kept : List (SketchRef × Location)
+
+ def fixture (c : Context P) : Option Fixture :=
+ match filledValue (recognition c), filledValue (placement c) with
+ | some r, some p => some ⟨p.location, r.target, r.purposeScope, r.residual, p.kept⟩
+ | _, _ => none
+
+ /-- **Your judgment**, the adoption condition: what the person's answer closes on was shown, on a
+ gate the person answered, with what it takes. For a recognition and a placement: what
+ producing the recognized version determined, what it was checked against and how that came
+ out, what it moved from a value the person settled, your contrary grounds, and, after a
+ failed retention, every copy already written and where. For a dissolution or a route: the
+ ground the closing rests on, and your contrary grounds — a doubt about the dissolution, a
+ sibling deficit you read otherwise. A value the answer itself states counts where its
+ consequences were in view. Where anything would be taken unseen, the gate is drawn again
+ with it shown. A withdrawal needs nothing in view: the person may stop at any gate. -/
+ axiom Covered : Context P → Prop
+
+ /-- Every placed reference verified, and no version kept as a revert point is the recognized
+ one: those are the versions the run passed over. -/
+ def Verified (c : Context P) (f : Fixture) : Prop :=
+ (∀ k ∈ f.kept, k.1 ≠ f.target) ∧
+ (⟨f.target, f.ref⟩, Disposition.retained) ∈ dispositions c ∧
+ ∀ k ∈ f.kept, (⟨k.1, k.2⟩, Disposition.retained) ∈ dispositions c
+
+ /-- Every copy the run wrote has a declared disposition. -/
+ def Accounted (c : Context P) : Prop := ∀ w ∈ written c, ∃ d, (w, d) ∈ dispositions c
+
+ /-- A value on the record, named as the presentation shows it — a settled axis, the recognition,
+ the placement, a kept version. -/
+ abbrev Entry := String
+
+ /-- **Your reading**: the values the record holds as the context now stands. -/
+ axiom entries : Context P → List Entry
+
+ /-- Who first put a value forward. Kept apart from how it came to stand: a reading you proposed
+ that the person settled was proposed by you and set by the person's taking. -/
+ inductive Proposer | draft | person
+
+ /-- **Your reading**: the position of the turn that first put forward what `e` holds now. -/
+ axiom introducedAt : Context P → Entry → Nat
+
+ def proposer (c : Context P) (e : Entry) : Proposer :=
+ match c[introducedAt c e]? with
+ | some ⟨.person, _⟩ => .person
+ | _ => .draft
+
+ /-- How a value came to stand: the person's words set it, or their answer adopted yours. -/
+ inductive Standing | set | adopted
+
+ /-- **Your reading**: the person's turn set what `e` holds now — named it or edited it — on the
+ scope their words reach. -/
+ axiom setByPerson : Context P → Entry → Bool
+
+ def standing (c : Context P) (e : Entry) : Standing := if setByPerson c e then .set else .adopted
+
+ structure Provenance where
+ entry : Entry
+ proposer : Proposer
+ standing : Standing
+
+ def provenance (c : Context P) : List Provenance :=
+ (entries c).map (fun e => ⟨e, proposer c e, standing c e⟩)
+
+ /-- What a ledger line records. -/
+ inductive LedgerKind
+ /-- the person's own edit -/
+ | personEdit
+ /-- a change the person's words force -/
+ | necessary
+ /-- a change you propose, a later version moving a value the person settled included -/
+ | proposal
+
+ /-- One change since the last gate: what changed, the value it touches, and its kind. -/
+ structure LedgerLine where
+ change : String
+ cause : Option Entry
+ kind : LedgerKind
+
+ /-- **Your record**: what the latest turn and the sketches produced since changed, the person's
+ edits first. -/
+ axiom ledger : Context P → List LedgerLine
+
+ /-- **Your record**: the contrary grounds you presented before the gate the closing answer
+ answered — a version failing a referent it was checked against, a commitment it breaks, a
+ defect found after the person judged it, a dissolution you doubt, a sibling deficit you
+ read — attached to the closure; empty when there were none. -/
+ axiom dissent : Context P → List String
+
+ /-- How the person ends the run without a recognized form. -/
+ inductive Closing
+ /-- stop here -/
+ | withdraw
+ /-- no form is owed: the sharpened description made it recognizable without a further
+ encounter, or the activation premise collapsed -/
+ | dissolve
+ /-- go on to what the person names — a sibling deficit, another protocol -/
+ | route (target : String)
+
+ /-- **Your judgment**: the cited turn closes the run this way, read against the context as it now
+ stands. Your own reading that no further encounter is owed, or that a sibling deficit is what
+ is going on, closes nothing: it is stated with its basis before the gate, and the person's
+ answer closes. -/
+ axiom ClosingSupported : Context P → Turn P → Closing → Prop
+
+ /-- Only the person closes. -/
+ def closeCoord : Coord P Closing :=
+ { admits := (·.val = .person), supports := ClosingSupported }
+
+ /-- **Your reading**: the person's closing; `open_` until one reaches it. -/
+ axiom closing : (c : Context P) → Occ (closeCoord (P := P)) c
+
+ /-- **Your judgment**, on reachable evidence only: a realization the next sketches or the
+ placement need is one this session cannot supply — a capability the host lacks, a referent
+ it cannot reach. A failed attempt alone is not this; where an alternative or a narrower scope
+ would need a judgment, present it and hold. The boundary relay then takes the place of the
+ next presentation. -/
+ axiom Unsuppliable : Context P → Prop
+
+ /-- **Your judgment**: the latest answer, read with the context, calls for new sketches — marks,
+ an aspect found right with another to try, a fresh start, a spec revision. An interrogation
+ answered within the sketch's placeholder status, and an answer with no marks and no acts,
+ present the gate again with nothing produced. -/
+ axiom Redraws : Context P → Prop
+
+ /-- The record an exit that recognizes nothing carries: the context after account, the dissent
+ attached to the closure, and how each value came to stand. -/
+ structure Closed (P : Type) where
+ context : Context P
+ dissent : List String
+ provenance : List Provenance
+
+ /-- `RecognizedForm`, read from the context at the verified placement, before any release: the
+ settled values (`operative`), the fixture, the recognition, the trace of every mark, the
+ residual — axes left open and material the person entrusted to sketches that never came —
+ the readings still `provisional`, every copy written with its disposition, the dissent, and
+ how each value came to stand. It is assembled before any release, and the RecognizedForm
+ entire is the durable record of the run: sketch content beyond what placement retains stays
+ session-local. -/
+ structure RecognizedForm (P : Type) where
+ context : Context P
+ fixture : Fixture
+ dissent : List String
+ provenance : List Provenance
+
+ inductive Outcome (P : Type)
+ /-- `NoActivationRelay`: the failed predicate with its evidence; nothing produced -/
+ | notActivated (c : Context P)
+ | recognized (f : RecognizedForm P)
+ /-- `DissolutionExit`: a convergent stand-down the person closed, no form owed; its basis stated -/
+ | dissolved (r : Closed P)
+ /-- `Routed`: the person named where the run goes next; that is the session's to take up -/
+ | routed (target : String) (r : Closed P)
+ /-- `EarlyExit`: the partial trace; any recognition stays in it -/
+ | withdrawn (r : Closed P)
+ /-- `BoundaryExit`: a realization shown unsuppliable, the obligation named -/
+ | boundary (r : Closed P)
+ | holding (c : Context P)
+
+ /-! ── A-BINDING ──
bind(I) = explicit_arg ∪ recent_form_intent ∪ surfaced_fit_gap
Priority: explicit_arg > recent_form_intent > surfaced_fit_gap
+ /sketch "what to make" → I = the utterance, with the material it names or the context holds
+ /sketch (alone) → I = the most recent form-making intent in session
+ "I'd know it when I see it" → I = the utterance under discussion (AI-detected path: the spec
+ relay cites the evidence of FitUnrecognized as the run's basis;
+ a decline of the run is a withdrawal at the first Qfit)
+ -/
- /sketch "what to make" → I = FormIntentSeed with utterance; prior = material the utterance names or that is already in context
- /sketch (alone) → I = the most recent form-making intent in session
- "I'd know it when I see it" → I = the utterance under discussion (AI-detected path: the spec relay cites the evidence of FitUnrecognized as the run's basis; a decline of the run is a withdrawal at the first Qfit)
+ /-! ── MODE STATE ──
+ Λ is the fused context and nothing else; every reading above is taken from it.
+ -/
- ── PHASE TRANSITIONS ──
- Phase 0: I → detect(I, ctx) → fit_unrecognized? -- silent analysis
- [false] Λ.exit := NotActivated → no_activation_relay → exit (NoActivationRelay)
- [true] → Phase 1
- Phase 1: bind(I) → Λ.history := Bound(each prior item) → Λ.round := 1 → Phase 2 -- track; Settled where the user already committed, Candidate otherwise
- Phase 2: draft(RoundSpec, provisional(Λ)) → spec_relay(draft, provisional(Λ)) → commit(Λ.spec := draft) → Phase 3 -- round-spec relay [Tool]
- -- the relay yields no turn: it lays out this round's focus, what the judgment needs, the variant briefs, each with the basis that chose it, and each provisional coordinate with where it came from; nothing is settled here — a coordinate is promoted or superseded only by the user's act at Qfit
- -- RE-ENTERED from Qfit on a SpecRevision: revise(draft, rev) first, then the relay goes out scoped to the revision and no new round is counted
- -- on the AI-detected path the relay cites the evidence of FitUnrecognized as the run's basis; a decline of the run is the withdrawal arm at the first Qfit (Phase 6, EarlyExit arm — account enforced, since a sketch exists by then)
- Phase 3: produce(Λ.spec, Λ) → Sk : NonEmptyList(Sketch) → Λ.sketches ++= Sk
- → Λ.history ++= Proposed(each determination rendered into Sk that no Settled or Provisional coordinate covered — its brief's own commits included, since the relayed draft settled nothing — basis Production(its ref)) -- transform [Tool]
- [|Λ.spec.targets| > 1, conditional] produce_delegate(∥ one sketch per executor, temp-isolated) [Tool]
- -- dispatch on brief.parent: Some(ref) → revise(ref retained, active_coords, marks since ref, brief.source where it names one); None → generate(brief.source where it names one else prior material, active_coords, brief.commits) — a brief may name both, and changing the material does not itself abandon the parent
- -- every sketch records its concretum and a versioned reference at creation; existing project files stay unchanged
- Phase 4: present(Sk) → acquire(marks) → Qfit(Sk, Λ.spec.focus) → Stop → M -- recognition gate [Tool]
- [M = Marks(ms, acts)] act(acts) → Λ.history ++= Marked(each) → interpret(ms) → Δ → Λ.history ++= Proposed(each c ∈ Δ) → stale(Λ.fit_witnesses over superseded sketches) → Λ.round += 1 → Phase 2
- [M = Fit(w, acts)] act(acts) → w.context_revision := Λ.context_revision → Λ.fit_witnesses ∪= {w} → Λ.history ++= Witnessed(w) → Λ.round += 1 → Phase 2 -- the witness is bound to the revision the same answer left, so the acts riding it do not stale it on arrival
- [M = Finish(rec, acts)] act(acts) → rec.context_revision := Λ.context_revision → Λ.recognition := Some(rec) → Phase 5 -- the recognition is bound to the revision its own acts left, as a Fit witness is
- [M = Withdraw] → Phase 6 (EarlyExit arm)
- -- act(acts): promote(acts.settlements) → Λ.history ++= Promoted(each) → supersede(acts.supersessions) → Λ.history ++= Superseded(each of, by) → Λ.context_revision += 1 where either set is non-empty; it runs before interpret, so a reading is drawn against what the user just settled
- -- free responses declared pre-gate: interrogate a sketch (answered within its placeholder status, gate re-presented); send back this round's focus, realization, or variants (a SpecRevision — Phase 2 with the revision named, no new round counted); contest the premise (dissolution arm); name a boundary (boundary arm)
- -- Marks(∅, ∅) is Stop; a mixed response keeps its Keep marks; a response naming a version that was not presented is answered, never parsed as Finish
- Phase 5: Qplace(Λ.recognition.target) → Stop → P -- placement gate [Tool]
- [P = Place(location, kept)] Λ.fixture := Some({ref: location, target, scope, residual, kept}) → harvest → Phase 6 (RecognizedForm arm)
- -- the protocol names the capability (a reference the user judges to outlive the session) and supplies no default, for the recognized version or for any kept one; a withdrawal here is the EarlyExit arm with the recognition recorded in the partial trace
- -- RE-ENTERED from Phase 6 on RetainFailed: the failure is declared before the gate; the user names a location again — the same one is admissible — or withdraws
- Phase 6: account → [a terminal arm] Λ.exit := cause → terminal -- all arms [Tool]; the RetainFailed arm returns to Phase 5 with Λ.exit still None
- [from Phase 5 — recognized and placed] retain(recognition.target at Λ.fixture.ref) ∧ ∀ (s, loc) ∈ Λ.fixture.kept: retain(s at loc)
- → verify(resolves(Λ.fixture.ref, concretum(recognition.target)) ∧ ∀ (s, loc) ∈ Λ.fixture.kept: resolves(loc, concretum(s)))
- [all verified] Λ.dispositions ++= (target, Retained(Λ.fixture.ref)) and (s, Retained(loc)) for each kept
- → release(every sketch neither recognized nor kept) → Λ.exit := Recognized → assemble → RecognizedForm
- [any failed after one retry] Λ.dispositions ++= (each that failed, RetainFailed(reason)) → Λ.fixture := None → Phase 5 (Qplace re-presented with every failure declared; harvest re-runs with the next fixture)
- -- ONE rule for the recognized version and for a kept one: a reference that does not resolve returns the placement to the user rather than being closed over, since accounted demands every reference the result needs
- -- nothing is released on this arm: every sketch stays retained until a terminal is reached, so a later Place still finds the target and each kept version
- [withdrawal at any gate] release(all) → EarlyExit
- [dissolution arm] release(all) → DissolutionExit
- [boundary arm] release(all) → BoundaryExit
- -- release: per sketch, the destruction read off its concretum (a no-op for Text) → verify absence → Disposition; a failure retries once, then is declared ReleaseFailed with a handoff, never silent
- -- Λ.dispositions is append-only; a sketch's disposition is its latest entry, so a RetainFailed is superseded by the Retained a later Place verifies
+ abbrev Mode (P : Type) := Context P
- ── LOOP ──
- Each round re-enters Phase 2 with the history it accumulated; the round counter is visible at every spec relay and Qfit.
- No fixed round cap: a round that re-enters a Constitution gate is dialogue, and the user can withdraw at any gate.
- Variant count is drafted per round at the spec relay; a count the user settled at a recognition gate holds until they revise it.
- Continue until: RecognizedForm (Finish + placement + account) OR EarlyExit OR DissolutionExit OR BoundaryExit.
- Convergence evidence: at RecognizedForm, present the trace — each mark → its interpretation → the revision it drove → how it ended (recognized, superseded, or residual) — beside the recognized version, its placement, the versions kept as revert points, the Settled commitments, the coordinates still Provisional and the residual — axes left open and material the user entrusted to a round that never came. Each other terminal presents its own payload (TOOL GROUNDING). Demonstrated, not asserted.
+ /-! ── PHASE TRANSITIONS ──
+ A step is one arm of a structural recursion over the person's utterances. `relay` is the spec
+ relay: it presents `spec`, a `RoundSpec` carrying `SpecOwes`, and yields no turn; where
+ `Unsuppliable` holds, the boundary relay takes its place. The sketches are then produced
+ (`.produce`; in parallel through `.produceDelegate` when a spec has more than one brief, one
+ sketch per executor, each temp-isolated).
+ -/
- ── CONVERGENCE ──
- disposition(s) = the latest entry for s.ref in Λ.dispositions
- accounted(Λ) = ∀ s ∈ Λ.sketches: disposition(s) is defined -- every sketch has a declared disposition
- ∧ (Λ.fixture = Some(f) ⇒ resolves(f.ref, concretum(f.target))
- ∧ ∀ (s, loc) ∈ f.kept: resolves(loc, concretum(s))) -- each reference resolves to that version's exact concretum, verified at the moment it is checked, and to nothing else
- ∧ ∀ s: disposition(s) ∈ {ReleaseFailed(_), RetainFailed(_)} ⇒ handoff_declared(s) -- failures are declared, never silent
- recognition_ready(Λ) = Λ.recognition = Some(rec)
- ∧ rec.target ∈ presented(Λ.sketches) ∧ disposition(rec.target) = Retained(Λ.fixture.ref) -- retention verified, never assumed
- ∧ rec.context_revision = Λ.context_revision
- ∧ Λ.fixture ≠ None -- Qplace settled
- ∧ residual_declared(Λ) ∧ trace_declared(Λ)
- converged(Λ) = accounted(Λ) ∧ ((Λ.exit = Recognized ∧ recognition_ready(Λ)) ∨ (Λ.exit = Dissolved ∧ basis_declared(Λ)))
- result equations:
- NoActivationRelay ⇔ Λ.exit = NotActivated -- nothing produced; nothing to account
- RecognizedForm ⇔ Λ.exit = Recognized ∧ recognition_ready(Λ) ∧ accounted(Λ)
- EarlyExit ⇔ Λ.exit = Withdrawn ∧ accounted(Λ) -- non-convergent
- BoundaryExit ⇔ Λ.exit = BoundaryReached ∧ obligation_named(Λ) ∧ accounted(Λ) -- non-convergent; the session routes it
- DissolutionExit ⇔ Λ.exit = Dissolved ∧ basis_declared(Λ) ∧ accounted(Λ) -- convergent stand-down: no form was owed
+ /-- **Your production** under the relayed spec: each Artifact sketch as observed at creation,
+ its versioned reference registered then. A Text sketch is narration the presentation carries
+ as recorded. Existing project files stay unchanged. -/
+ axiom produce : Context P → List (Evidence P)
- ── TOOL GROUNDING ──
+ def runRound (relay : Context P → Response P) (c : Context P) : Context P :=
+ let c₁ := c ++ [(relay c).val]
+ c₁ ++ (produce c₁).map (·.val)
+
+ /-- **Your account** at a placement: retain the recognized version and each kept one at its
+ location, and verify that each reference resolves to that version's exact concretum — one
+ retry, then the failure is observed. Nothing is retained before a recognition and a
+ placement stand and were taken with what they need in view. -/
+ axiom retain : Context P → List (Evidence P)
+
+ /-- **Your account** at a terminal: release every sketch the context leaves unplaced — all of
+ them on a withdrawal, a dissolution, a route, or a boundary — and verify each absence; a
+ failure retries once, then is observed and declared with a handoff. A copy an earlier
+ placement attempt wrote to a location the person has since moved from is released only where
+ the person's words reach it; otherwise it is left where it is and declared. New evidence that
+ breaks a recognition or a value the person settled is shown before any release. What it
+ leaves is `Accounted`. -/
+ axiom release : Context P → List (Evidence P)
+
+ def settle (c : Context P) : Context P := c ++ (retain c).map (·.val)
+
+ def closed (c : Context P) : Closed P :=
+ { context := c ++ (release c).map (·.val), dissent := dissent c, provenance := provenance c }
+
+ def recognize (c : Context P) (f : Fixture) : RecognizedForm P :=
+ { context := c ++ (release c).map (·.val), fixture := f, dissent := dissent c,
+ provenance := provenance c }
+
+ open Classical in
+ /-- `respond` presents the gate: Qplace while a recognition stands, Qfit otherwise. Before it:
+ each sketch from its concretum — Text as recorded, an Artifact walked through at its
+ reference, reporting what was observed there or that it was not observed and what was tried;
+ what this realization cannot expose; what each sketch was checked against and how it came
+ out; which content came from the person and which is your proposal; what each sketch's own
+ production determined; the ledger, the person's edits first, a later version moving a value
+ they settled included; where the run stands — what is settled, what is still open, what was
+ entrusted to later sketches; and your contrary grounds, a reading that no further encounter
+ is owed or that a sibling deficit is what is going on included. At Qplace, the versions the
+ run passed over and, after a failed retention, the failure and every copy already written. -/
+ def sketch (relay respond : Context P → Response P) :
+ Context P → List (Utterance P) → Outcome P
+ | c, [] => .holding c
+ | c, u :: us =>
+ let c' := fuse c u
+ match filledValue (closing c') with
+ | some .withdraw => .withdrawn (closed c')
+ | some .dissolve =>
+ if Covered c' then .dissolved (closed c')
+ else sketch relay respond (c' ++ [(respond c').val]) us
+ | some (.route t) =>
+ if Covered c' then .routed t (closed c')
+ else sketch relay respond (c' ++ [(respond c').val]) us
+ | none =>
+ if Unsuppliable c' then .boundary (closed (c' ++ [(relay c').val]))
+ else
+ match fixture c' with
+ | some f =>
+ if Covered c' then
+ let c₁ := settle c'
+ if Verified c₁ f then .recognized (recognize c₁ f)
+ else sketch relay respond (c₁ ++ [(respond c₁).val]) us
+ else sketch relay respond (c' ++ [(respond c').val]) us
+ | none =>
+ if Placing c' ∨ ¬ Redraws c' then sketch relay respond (c' ++ [(respond c').val]) us
+ else
+ let c₁ := runRound relay c'
+ sketch relay respond (c₁ ++ [(respond c₁).val]) us
+
+ open Classical in
+ def start (relay respond : Context P → Response P) (c : Context P)
+ (us : List (Utterance P)) : Outcome P :=
+ if ¬ fitUnrecognized c then .notActivated c
+ else if Unsuppliable c then .boundary (closed (c ++ [(relay c).val]))
+ else
+ let c₁ := runRound relay c
+ sketch relay respond (c₁ ++ [(respond 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. A person's value stands on the scope their
+ words reach; a later sketch that moves it is a ledger line, never a silent change. No fixed cap:
+ each gate is dialogue, and the person can withdraw, dissolve, or route at any gate. At every spec
+ relay, re-present the material the person entrusted to later sketches; a later answer of theirs
+ takes it up or withdraws it.
+ -/
+
+ /-! ── CONVERGENCE ──
+ converged: a recognized form, its recognition and placement taken with what they need in view
+ (`Covered`) and every placed reference verified (`Verified`); or a dissolution the person closed,
+ with its basis. Every other exit is non-convergent and keeps its partial record. Convergence
+ evidence: at RecognizedForm, present the trace — each mark → its reading → the revision it drove
+ → how it ended (recognized, replaced, or residual) — beside the recognized version, its placement,
+ the versions kept as revert points, the settled values with who proposed each and how it came to
+ stand, the readings still provisional, the residual — axes left open and material entrusted to
+ sketches that never came — every copy written with its disposition, and the dissent attached to
+ the closure. Every sketch's disposition is shown (`Accounted`); a failure is declared with its
+ handoff, never silent. Each other terminal presents its own payload (TOOL GROUNDING).
+ Demonstrated, not asserted.
+ -/
+
+ /-! ── TOOL GROUNDING ── -/
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
- Phase 0 detect (sense) → Internal analysis (deficit predicate over the utterance and accumulated context; no external tool)
- Phase 0 no_activation_relay (extension) → TextPresent+Proceed (the non-activation basis — the failed predicate with its evidence; a sibling deficit seen in the scan is named as a finding and left to the session; not activated)
- Phase 1 bind (track) → Internal state update (prior material enters Λ.history as Settled or Candidate with provenance; the round counter starts)
- Phase 2 draft (sense) → Internal analysis (focus, realization, and target briefs proposed from the accumulated history — the operative commitments, the provisional readings, the bound prior material, and every mark so far — read together rather than from any one of them)
- Phase 2 spec_relay (extension) → TextPresent+Proceed (the round's draft whole: this round's focus, what the judgment needs, the variant briefs, each with the basis that chose it, and each provisional coordinate with where it came from — laid out so that any of it can be settled, sent back, or replaced at the recognition gate, as can any Settled coordinate in view; fires BEFORE anything is produced and settles nothing; on the AI-detected path it cites the evidence of FitUnrecognized as the run's basis; re-presented scoped to a SpecRevision the recognition gate named, without counting a round)
- Phase 2 revise (track) → Internal state update (a SpecRevision named at Qfit: the draft revised as named before the spec relay re-presents)
- Phase 2 commit (track) → Internal state update (Λ.spec := the relayed draft; no coordinate moves here — the user's acts on coordinates are written at Qfit's record step)
- Phase 3 produce (transform) → artifact write, environment run (temp-isolated sketches, each with its concretum and a versioned reference registered at creation; a brief naming a parent revises that retained version, a parentless brief generates from the material its source names or from prior material; existing project files are never modified; Text concreta are session text only. Each sketch proposes as coordinates what it was rendered under that no Settled or Provisional coordinate covered — its brief's own commits and what producing it determined beyond them, since the relayed draft settles nothing — so the user meets those determinations beside the sketch at Qfit rather than only their consequences on the screen)
- Phase 3 produce_delegate (dispatch) → delegate (conditional: more than one target; parallel topology: one sketch per executor, each temp-isolated with its reference registered; subordinate to the active runtime policy)
- Phase 4 present (extension) → TextPresent+Proceed (each sketch from its typed concretum — Text re-presented as recorded, an Artifact walked through at its reference, reporting what was observed there or that it was not observed and what was tried — since Text is read as recorded while an Artifact is only ever presented as far as it was seen — then this round's focus, what this realization cannot expose, which content came from the user and which is the AI's proposal, what this sketch's own production determined, and every fit witness now stale)
- Phase 4 acquire (observe) → a channel returning utterances anchored on a sketch (read-only: the marks arrive as the user's utterances; the channel is a capability the host supplies, named here and bound nowhere in this contract. What a host must satisfy is that the user can point at what they saw and that the pointing arrives with the utterance; how it does so is read at the round against the host in front of it)
- Phase 4 Qfit (constitution) → present (mandatory recognition gate on a specific version: Marks, Fit on this focus, Finish for a stated purpose, Withdraw — and, riding Marks, Fit, or Finish, the user's acts on the coordinates in view: which provisional readings they settle, and which coordinates they supersede or retire; Marks(∅, ∅) is Stop; the pre-gate text declares the free-response paths — interrogate, send back this round's focus, realization, or variants, contest the premise, name a boundary)
- Phase 4 record (track) → Internal state update (the user's acts on coordinates written first — each settled coordinate takes a Promoted event, each superseded one a Superseded event with the replacement they stated or none, and the context revision advances where either set is non-empty; then every mark appended to Λ.history as itself, then each Provisional coordinate interpret read from it appended as Proposed; a fit witness appended, bound to the context revision those acts left; witnesses over superseded sketches marked stale)
- Phase 4 interpret (sense) → Internal analysis (marks, read against the accumulated history, → Provisional coordinates, each carrying the mark it came from; never Settled here; what it yields reaches Λ only through record)
- Phase 5 Qplace (constitution) → present (mandatory placement gate: the recognized version and the capability it needs — a reference the user judges to outlive the session — together with the versions this run passed over, since those are what a later reversal would otherwise rebuild; the user names the location and which of the others are kept and where; no default is offered for either)
- Phase 6 harvest (track) → Internal state update (Settled commitments, the fixture, the recognition, the trace, the residual axes, and the coordinates still Provisional, recorded before any release; the durable record is the RecognizedForm entire — sketch content beyond what placement retains stays session-local)
- Phase 6 account (transform) → artifact write, environment run (retain the recognized version at the settled location and verify the reference resolves to that exact concretum — one retry, then RetainFailed is declared and Qplace is re-presented with nothing released; once every placed version is retained, release the sketches placement did not keep and verify each — one retry, then ReleaseFailed declared with a handoff)
- dissolution_relay (extension) → TextPresent+Proceed (either party, at the spec relay or at any gate: the sharpened description made the form recognizable without a further encounter, or the activation premise collapsed; state the basis, relay the Settled commitments and every mark recorded, run account, stand down as DissolutionExit — a success, not an abandonment)
- boundary_relay (extension) → TextPresent+Proceed (either party, at the spec relay or at any gate: a sibling deficit is demonstrated, or a realization this round requires is one this session cannot supply; name the obligation and its basis, relay the harvest so far, run account, exit as BoundaryExit; the next protocol is the session's to choose)
- withdraw (extension) → TextPresent+Proceed (explicit free-response exit at any gate: partial trace + residual declared; account enforced; EarlyExit. A hard interrupt yields no turn, so account cannot run: temp isolation's bounded lifecycle is the backstop)
- converge (extension) → TextPresent+Proceed (transformation trace: marks → interpretations → revisions → recognition; the recognized version, its placement, Settled commitments, Provisional coordinates, residual axes, and every disposition)
- seam (extension) → TextPresent+Proceed (fires at deactivation: a user-declared chain naming the next protocol settles the next move — proceed to it, citing that settling source; the RecognizedForm enters it as prior material, its fixture a recognition witness and nothing more. This protocol declares no wired outbound edge of its own. Every Constitution gate inside this protocol and inside the next fires unchanged)
- ── MODE STATE ──
- Λ = { phase: Phase, I: FormIntentSeed, round: ℕ,
- context_revision: ℕ, -- advances when the accumulated context moves outside the marks: a new user utterance about the form, a spec revision, a promoted or superseded coordinate
- history: List(Event ⊎ ReferencedMaterial), -- append-only; the typed events and, beside them, each gate answer as the
- -- user said it, so what a constructor does not reach still survives the round
- -- it was said in; active_coords and provisional are folded from it, never stored apart
- spec: Option(RoundSpec), -- this round's relayed draft; None until the spec relay goes out
- sketches: List(Sketch), -- every version produced, retained for revision until account
- fit_witnesses: Set(FitWitness), -- with staleness derived from sketches and context_revision
- recognition: Option(Recognition),
- fixture: Option(Fixture),
- dispositions: List<(SketchRef, Disposition)>, -- append-only; a sketch's disposition is its latest entry, one defined per sketch by terminal (invariant: accounted)
- exit: Option(ExitCause),
- active: Bool, cause_tag: String }
- -- Guard: no sketch is produced before the spec relay presented its brief with its basis — on round 1's first pass, phase < 3 ⇒ sketches = ∅; a re-entry on a SpecRevision, and every later round, holds the sketches already produced and produces nothing until its spec relay has gone out again
- -- Guard: a Coordinate enters Settled only through Promoted (a user act at Qfit), Bound(Settled) (a commitment already on record), or as the `by` of a Superseded the user stated at Qfit; a Proposed event is the only way a Provisional coordinate enters the history, and it stays Provisional until Promoted or Superseded
+ inductive Annot | sense | observe | track | transform | dispatch | constitution | extension
- ── COMPOSITION ──
+ inductive Op | detect | noActivationRelay | bind | draft | specRelay | produce | produceDelegate
+ | present | acquire | qfit | interpret | readAnswer | qplace | account | assemble
+ | dissolutionRelay | routeRelay | boundaryRelay | withdraw | converge | seam
+
+ def grounding : Op → Annot × String
+ | .detect => (.sense, "Internal analysis: the deficit predicate over the utterance and the context; no external tool")
+ | .noActivationRelay => (.extension, "TextPresent+Proceed: the non-activation basis — the failed predicate with its evidence; a sibling deficit seen in the scan is named as a finding and left to the session; not activated")
+ | .bind => (.sense, "Internal analysis: prior material read from the context — settled where a person's utterance in this context settles it, a candidate otherwise, with where it came from; a record of a commitment made in an earlier session is a candidate")
+ | .draft => (.sense, "Internal analysis: what the next sketches try, the perception the judgment needs, the referent a standard outside both parties' preference is checked against, and the variant briefs, drafted from the whole context — the settled values, the provisional readings, the prior material, every mark, and any spec revision the person named — read together rather than from any one of them")
+ | .specRelay => (.extension, "TextPresent+Proceed: the draft whole — what the next sketches try, what the judgment needs, the variant briefs, each with the basis that chose it, and each provisional reading with where it came from — laid out so that any of it can be settled, sent back, or replaced at Qfit; fires before anything is produced and settles nothing; on the AI-detected path it cites the evidence of FitUnrecognized as the run's basis; after a spec revision it is re-presented scoped to that revision")
+ | .produce => (.transform, "artifact write, environment run: temp-isolated sketches, each with its concretum and a versioned reference registered at creation; a brief naming parents revises those retained versions, a brief naming none generates from the material its source names or from prior material; existing project files are never modified; Text concreta are session text only. Each sketch proposes as readings what it was rendered under that no settled value covered, so the person meets those determinations beside the sketch at Qfit")
+ | .produceDelegate => (.dispatch, "delegate (conditional: more than one brief; parallel topology: one sketch per executor, each temp-isolated with its reference registered; subordinate to the active runtime policy)")
+ | .present => (.extension, "TextPresent+Proceed: each sketch from its concretum — Text as recorded, an Artifact walked through at its reference, reporting what was observed there or that it was not observed and what was tried — then what this realization cannot expose, what each sketch was checked against and how it came out, which content came from the person and which is the AI's proposal, what each sketch's own production determined, the ledger, where the run stands, and any contrary ground held — a defect found after the person judged a version, a reading that no further encounter is owed, a sibling deficit read — each stated with its basis and closing nothing")
+ | .acquire => (.observe, "channel read: utterances anchored on a sketch; the marks arrive as the person's utterances. The channel is a capability the host supplies, named here and bound nowhere in this contract: the person can point at what they saw, and the pointing arrives with the utterance")
+ | .qfit => (.constitution, "present: mandatory recognition gate on a specific version — Mark, Fit on this focus, Finish for a stated purpose — and, riding the same answer, which readings shown beside it the person settles, replaces, or retires; an answer with no marks and no acts presents the gate again; the pre-gate text declares interrogating a sketch, sending back what the next sketches try, contesting the premise, naming where the run goes next, and withdrawing")
+ | .interpret => (.sense, "Internal analysis: marks read against the version they name, that version's brief, and how it was realized → provisional readings, each citing the mark it came from; whether a mark reaches the form or the realization is carried unresolved where the evidence does not settle it; never settled here")
+ | .readAnswer => (.sense, "Internal analysis: the latest utterance, and every earlier turn of the person's it bears on, read whole against the fused context as it now stands — its marks, the values it settles and their scope, a recognition or its reopening, a placement, a closing — whatever form it takes")
+ | .qplace => (.constitution, "present: mandatory placement gate — the recognized version and the capability it needs, a reference the person judges to outlive the session, beside the versions this run passed over; the person names the location and which of the others are kept and where; no default for either; after a retention failure the failure and every copy already written are shown before the gate, and the same location stays admissible")
+ | .account => (.transform, "artifact write, environment run: only on a recognition and placement taken with what they need in view, retain every placed version and verify each reference resolves to that exact concretum — one retry, then the failure is declared and Qplace presented again with nothing released; once every placed version is verified, release the sketches placement did not keep and verify each — one retry, then ReleaseFailed declared with a handoff; each copy is accounted for where it was written, and a copy at a location the person moved from is released only where their words reach it")
+ | .assemble => (.sense, "Internal analysis: RecognizedForm read from the context at the verified placement, before any release — the settled values with who proposed each and how it came to stand, the fixture, the recognition, the trace, the residual, the readings still provisional, every copy with its disposition, and the dissent attached to the closure; the RecognizedForm entire is the durable record of the run, and sketch content beyond what placement retains stays session-local")
+ | .dissolutionRelay => (.extension, "TextPresent+Proceed: when the person accepts or declares that no further encounter is owed — the sharpened description made the form recognizable without one, or the activation premise collapsed — state the basis, relay the settled values and every mark, attach any dissent, run account, stand down as DissolutionExit — a success, not an abandonment")
+ | .routeRelay => (.extension, "TextPresent+Proceed: when the person names where the run goes next — a sibling deficit, another protocol — relay the record so far with that target and its basis, attach any dissent, run account, exit as Routed; taking it up is the session's")
+ | .boundaryRelay => (.extension, "TextPresent+Proceed: where reachable evidence shows a realization the next sketches or the placement need cannot be supplied in this session — name the obligation and its basis, relay the record so far, run account, exit as BoundaryExit; the next protocol is the session's to choose")
+ | .withdraw => (.extension, "TextPresent+Proceed: explicit exit at any gate — the partial trace and residual declared, account enforced; EarlyExit. A hard interrupt yields no turn, so account cannot run: temp isolation's bounded lifecycle is the backstop")
+ | .converge => (.extension, "TextPresent+Proceed: the transformation trace — marks → readings → revisions → recognition — with the recognized version, its placement, the settled values and their provenance, the provisional readings, the residual, the dissent, and every copy's disposition")
+ | .seam => (.extension, "TextPresent+Proceed: at a user-declared chain naming the next protocol, proceed to it citing that source; the RecognizedForm enters it as prior material, its fixture a recognition witness and nothing more; 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₂). Form resolution emergent via session context.
+ -/
+
+ end
+
+ end Hypotyposis
```
## Scope Boundary
- The transformation the moment needs decides between neighbors; a sibling deficit seen in the scan or demonstrated in a round is named as a finding at the boundary, and the session chooses what takes it.
+ The transformation the moment needs decides between neighbors; a sibling deficit seen in the scan or demonstrated in a round is named as a finding before the gate, and the user chooses whether the run goes there.
- `/preview` — recognize and settle a direction among named alternatives; its probes are discarded. Here the resolution sought is a form, and the recognized version is kept; a direction settled by `/preview` can enter as prior material.
- `/elicit` — resolve intent by reverse-tracing decision coordinates from externalized cognition. Here encountering and revising sketches constitutes the remaining form intent; readable prior material may already exist.
- `/contextualize` — adjudicate a result's fit against application context held fixed within the run, with adaptation directed by the user. Here encountering sketches develops the form intent itself.
- `/ideate` — a thin field of ideas widened, nothing selected. Here a form is recognized.
## Mode Activation
`/sketch` is directly invocable. On the AI-detected path — the session routing the utterance here — cite the evidence of `FitUnrecognized` at the spec relay; a decline of the run is a withdrawal at the first `Qfit`. Loaded safety boundaries, capability restrictions, and explicit user instructions continue to bind while Hypotyposis is active.
Heuristic discovery cues are a plan that cannot reach its first draft, a description rewritten instead of made, a request to see something before saying more, and an explicit "I'd know it when I see it". They establish grounds to run Phase 0 rather than activation predicates.
## Protocol
### Phase 0: Detection (Silent)
Apply the deficit predicate in the Definition and cite the basis.
### Phase 1: Bind
- Bring each prior item into the history as `Settled` only where the user settled it, as `Candidate` otherwise, with where it came from.
+ Read each prior item from the context as settled only where a person's utterance in this context settled it, and as a candidate otherwise — a record of a commitment made in an earlier session included — with where it came from.
### Phase 2: Round Spec Relay
- Lay out the draft TOOL GROUNDING's `spec_relay` entry names — the focus, the perception it needs, each variant brief with the basis that chose it, and each provisional coordinate with the mark or production it came from — then produce without yielding the turn. Say in one line that any of it can be settled, sent back, or replaced at the recognition gate.
+ Lay out the draft TOOL GROUNDING's `specRelay` entry names — what the next sketches try, the perception it needs, the referent a standard is checked against where the focus carries one, each variant brief with the basis that chose it, and each provisional reading with the mark or production it came from — then produce without yielding the turn. Say in one line that any of it can be settled, sent back, or replaced at the recognition gate. Where reachable evidence shows a realization the sketches need cannot be supplied in this session, say so here and exit at the boundary before producing.
### Phase 3: Production (Transform)
Produce under the relayed spec as TOOL GROUNDING's `produce` entry states; every sketch carries its placeholder status visibly.
### Phase 4: Recognition Gate (Constitution)
- Present as TOOL GROUNDING's `present` entry states, acquire the marks through the channel the host supplies, then render `Qfit`:
+ Present as TOOL GROUNDING's `present` entry states — where the run stands, what a new version moved from a value the user settled, and any defect found in a version after the user judged it included — acquire the marks through the channel the host supplies, then render `Qfit`:
```
Which version are you marking, and what do you see?
Options:
1. **Mark** — point at what does not fit (and what to keep) on a named version; I revise from there
- 2. **Fit on this focus** — this version is adequate on this round's focus; the next round takes another focus
+ 2. **Fit on this focus** — this version is right on this aspect; the next sketches try another
3. **Finish** — this version is the form, for the purpose you state, with the axes you leave open
```
- With Mark, Fit, or Finish, name which of the readings shown beside the version you settle, reject, or replace; unnamed ones stay as they were. Name interrogating a sketch, sending back this round's focus, perception, or variants, contesting the premise, naming a boundary, and withdrawing as free-response paths; they are not numbered options.
+ With Mark, Fit, or Finish, name which of the readings shown beside the version you settle, reject, or replace; unnamed ones stay as they were. Name interrogating a sketch, sending back what the next sketches try, contesting the premise, naming where the run goes next, and withdrawing as free-response paths; they are not numbered options. An interrogation is answered within the sketch's placeholder status, and an answer with no marks and no acts presents the gate again; neither produces new sketches. Read each answer whole: where one answer could be a finish or a fit on one aspect, show your reading before the next gate rather than acting on it. Where you read that no further encounter is owed, or that a sibling deficit is what is going on, say so before the gate with its basis; the run ends there only when the user closes it.
### Phase 5: Placement Gate (Constitution)
- Present the recognized version and the capability it needs — a reference that outlives the session — and render `Qplace` with no default:
+ Present the recognized version and the capability it needs — a reference that outlives the session — beside the versions the run passed over, and render `Qplace` with no default:
```
Where does the recognized version live from here?
Options:
1. **Place** — name the location; the version is retained there and verified. Name any other versions worth keeping as revert points and where they go; the rest are released
```
- When a retention failed, say so before re-presenting; the same location stays admissible.
+ A version kept as a revert point is one the run passed over, never the recognized one. Nothing is written to a location before the user names it. When a retention failed, say so before re-presenting, together with every copy already written and where; the same location stays admissible, and a copy at a location the user moves away from stays where it is unless their words reach it. An answer here that marks the form again reopens the recognition, and the next sketches follow. Where reachable evidence shows the placement needs a capability this session cannot supply, say so with its basis and exit at the boundary.
## Rules
- - **Utterance continuity**: At every gate, append the user's answer as it was said to `Λ.history` beside the typed events read from it. At the spec relay, re-present outstanding material they entrusted to a later round; a subsequent act of theirs settles whether it is taken up or withdrawn. Whatever remains is declared in the terminal's residual.
- - **Ground interpretations**: Read each mark against the version it names, that version's brief, and how the round realized it. What the evidence supports about the form and about the realization is the judgment; carry it with its basis, and where the evidence does not settle which of the two a mark reaches, carry that unresolved into the provisional reading the spec relay presents.
- - **Draft relayed with its basis**: relay the round's focus, realization, and variant briefs with the basis that chose each, the provisional coordinates beside them, and the affordance to send any of it back, then produce; the recognition gate is where the user settles a coordinate or sends the draft back.
+ - **Utterance continuity**: Every gate answer joins the context as it was said, and the readings drawn from it are shown beside it as the AI's. Each answer is read against the context as it now stands; a value the user settled stands on the scope their words reach, and a later version that moves it is shown as a change before the next gate, never silently. At the spec relay, re-present outstanding material the user entrusted to later sketches; a subsequent act of theirs settles whether it is taken up or withdrawn. Whatever remains is declared in the terminal's residual.
+ - **Ground interpretations**: Read each mark against the version it names, that version's brief, and how it was realized. What the evidence supports about the form and about the realization is the judgment; carry it with its basis, and where the evidence does not settle which of the two a mark reaches, carry that unresolved into the provisional reading the spec relay presents. Where the focus carries a standard outside both parties' preference, check each sketch against its referent before presenting, and show how it came out.
+ - **Draft relayed with its basis**: relay what the next sketches try, the perception they need, and the variant briefs with the basis that chose each, the provisional readings beside them, and the affordance to send any of it back, then produce; the recognition gate is where the user settles a value or sends the draft back.
+ - **Closure by the user**: A recognition, a placement, a dissolution, and a route are closed only by the user's utterance, and taken only with what they need in view; a withdrawal needs nothing more than the user's word. Before each gate, show any contrary ground you hold about the version or the placement; where the user closes with that ground standing, attach it to the closure record. Evidence found later that breaks a recognition or a value the user settled is shown before the next gate, and always before any release; the closed value itself is never rewritten by you. Record for each settled value who proposed it and whether the user's words set it or their answer adopted yours.
- **Placement has no default**: The protocol names what the retained version needs — a reference the user judges to outlive the session — and the user names where, together with which other versions are kept and where. The fixture that results is a recognition witness and carries no implementation commitment.
- **Round composition**: Use everyday language, put evidence and differential implications before the gate, and leave the gate to the question and options. Read `references/round-composition.md` before composing when wording must persist across rounds or phase placement is material.
- **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.