--- name: sketch description: "Something has to be made that the user cannot describe but would recognize on sight: mark what does not fit on concrete sketches, revising until a form is recognized." --- # 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 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. ```lean /-! How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is written for: you read it, and by inference over the context you settle each element it leaves open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from the material in front of you; its doc comment says what you judge there, and nothing in this block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract. -/ /-! ── FLOW ── 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 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) -- 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 -/ namespace Hypotyposis /-! ── GROUND ── The session primitive this contract reads. -/ inductive Origin | person | assistant | external | peer | injected | unknown deriving DecidableEq /-- A turn is who sent it and what it says. What the turn does — a statement, a request, an instruction, a report of what was observed — is read from its content, never stored here. -/ structure Turn (P : Type) where origin : Origin content : P abbrev Context (P : Type) := List (Turn P) /-- An origin that may ground: the harness says who sent a turn, and that is all this admits on. The assistant's own turns, injected text, and turns of unknown origin ground nothing. -/ def Grounding := {o : Origin // o ≠ .assistant ∧ o ≠ .injected ∧ o ≠ .unknown} /-- Any turn a person sent, whatever it does. -/ def Utterance (P : Type) := {e : Turn P // e.origin = .person} def Response (P : Type) := {e : Turn P // e.origin = .assistant} /-- A turn from outside the conversation: what a tool or the environment returned, or a peer's report. A person's account of what they observed is an utterance, read as such. -/ def Evidence (P : Type) := {e : Turn P // e.origin = .external ∨ e.origin = .peer} def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val] /-- One turn of the context, with the origin it grounds on. -/ structure Cite {P : Type} (c : Context P) where idx : Nat lt : idx < c.length src : Grounding ok : (c[idx]'lt).origin = src.val /-- `admits` reads only who sent the cited turn; `supports` is the model's reading of what that turn says, including what it does — a statement, a request, a report of an observation. -/ structure Coord (P A : Type) where admits : Grounding → Prop supports : Context P → Turn P → A → Prop /-- `open_` may carry a candidate citation whose support is still short. -/ inductive Occ {P A : Type} (q : Coord P A) (c : Context P) | open_ (candidate : Option (Cite c)) | filled (a : A) (src : Cite c) (allowed : q.admits src.src) (supported : q.supports c (c[src.idx]'src.lt) a) /-- The same turn, cited from a longer context; what it supports is judged again against the context that now stands. -/ def Cite.lift {P : Type} {c : Context P} (s : Cite c) (t : Context P) : Cite (c ++ t) := { idx := s.idx lt := by have := s.lt; simp; omega src := s.src ok := by rw [List.getElem_append_left s.lt]; exact s.ok } /-! ── TYPES ── -/ noncomputable section variable {P : Type} /-- `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) -/ /-! ── MODE STATE ── Λ is the fused context and nothing else; every reading above is taken from it. -/ abbrev Mode (P : Type) := Context P /-! ── 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 through the operations `producedBy` names for the spec, one sketch per executor where delegated, each temp-isolated. -/ /-- **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) 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 ── What each operation of this contract does. An interaction with the person is one of two kinds, and its kind fixes how it continues once its text is presented. -/ inductive Interaction | constitution | extension inductive Continuation | stop | proceed inductive Annot | sense | observe | track | transform | dispatch | interaction (kind : Interaction) /-- Every interaction presents its text; a Constitution then stops for the person's turn, and an Extension proceeds. -/ def Interaction.realization : Interaction → Continuation | .constitution => .stop | .extension => .proceed inductive Op | 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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .constitution, "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 => (.interaction .constitution, "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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .extension, "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 => (.interaction .extension, "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") /-- The operations that produce a round's sketches: `.produce`, and `.produceDelegate` only for a spec with more than one brief. -/ def producedBy (s : RoundSpec) : List Op := if s.briefs.length > 1 then [.produce, .produceDelegate] else [.produce] /-! ── 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 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` — check a finished result against everywhere it lands and the intents it was meant to carry, with the fixes the user settles carried out. 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 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 `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 — 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 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 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 — 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 ``` 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**: 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.