/sketch

name: sketch
description: "Something has to be made that the user cannot describe but would recognize on sight: they can then point at a version they met and say 'this is the form, for this purpose', seeing where each is."

Hypotyposis Protocol

Discover what a form should be by encountering concrete versions and reacting to them, until the user recognizes one version they encountered as the form for their 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 can be pointed at (Alexander, 1964). So the user need not specify the form first. The AI relays what the next versions will try — what they revise, how many, the medium each is realized in and what that medium can and cannot show, and where each will be — each with its basis, and then makes them. Each round shows the new versions first, in a medium in which the qualities the user's judgment concerns can be encountered, and then the standing: what the user's words set and on which version, what of the AI's they took, what rests on a check, what stays unestablished, and what changed. The user reacts in their own words — a mark, a keep, a request, a value set — and the AI revises the versions those words point to into new versions, never regenerating one from a description of it, and may also make versions it would propose. The AI's reading of the purpose grows from those reactions rather than being settled up front: each part names the person's words or the gathered material it came from, or is marked as a default of its own, and each round shows how the reading widened. The run closes when the user takes one version they encountered as the form for their purpose, its home shown in the round or named in that same turn; they can stop at any time, and the run stays as it stood, with what they ask done to the versions as they stop carried out. Once it has run, the user can point at one version as they met it and say "this is the form, for this purpose", seeing where it lives, where the passed-over versions are, what they asked done to any of them that is not yet observed done, and which values rest on their own words or on the AI's proposals they took, and what rests on checked evidence. The recognition establishes their judgment of fit for that purpose on what the version showed — not correctness against a standard outside preference, and not readiness for use.

/-!
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:
  start: what bears on the form is gathered; then your reading, on it, that this is not this
    protocol's case (`notActivated`), in plain words with its basis → not activated; otherwise
    → production, then the productions you carry on your own proposals, as `Proposes` and `reach`
    read them → round
  production(c): the intent relayed whole — your reading of the purpose, marked as yours unless
    they said it, each part with what it rests on, a default marked as one; what the next versions
    try and which versions they revise; how many; the medium each is realized in, what it can show
    and what it cannot; where each will be; the reference a standard outside preference is checked
    against — each with its basis, and on every later production what changed since the last →
    what the versions will be checked against, gathered → the versions, each
    entering c as realized → what checking them needs, gathered
  round: new versions first, each as encountered in its medium; then the standing — what the
    person's words set and on which version, what of yours they took, what you propose not yet
    taken, what rests on a check, what stays unestablished, what changed since the standing they
    last answered, where each version is; your readings and contrary grounds, each with what it
    bears on and rests on → one opening
  next utterance u, read on fuse(c, u):
    [does not bear on this run]   what their words ask done to the versions, observed; the session
                                  answers it; that answer stays in c; no round of this run
    [the person recognizes v]     what their words ask done to the versions, observed → RecognizedForm
    [otherwise]                   what is gathered now enters c; a production where
                                  `ProductionRequested` reads one; what their words ask done to
                                  the versions is done and observed; then productions you carry on
                                  your own proposals, as `Proposes` and `reach` read → round
  no utterance: nothing is recognized, written, or removed; the run holds
-/

/-! ── MORPHISM ──
FormIntentSeed
  → gather          -- what bears on the form, read or run now — the reference a standard outside preference is checked against included (focus)
  → relay_intent    -- the production intent whole with its basis, BEFORE any version is made; on a later production, with what changed
  → produce         -- versions realized in a medium that shows what the judgment concerns,