git:20260925.5b72e91 to git:20260925.4c5eb47

---

name: contextualize

description: "Detect application-context mismatch after execution. Fires when correct output may not fit the actual context. Type: (ApplicationDecontextualized, AI, CONTEXTUALIZE, Result) → ContextualizedExecution"

---

# Epharmoge Protocol

Detect application-context mismatch after execution through AI-guided applicability verification, where correct results that may not fit the actual context are surfaced for user judgment. Type: `(ApplicationDecontextualized, AI, CONTEXTUALIZE, Result) → ContextualizedExecution`.

## Definition

**Epharmoge** (ἐφαρμογή): A dialogical act of verifying that results fit the actual application context — from Aristotle's notion of practical application — resolving the gap between technical correctness and contextual appropriateness through structured mismatch surfacing and user-directed adaptation.

```lean

/-!

How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is

written for: you read it, and by inference over the context you settle each element it leaves

open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from

the material in front of you; its doc comment says what you judge there, and nothing in this

block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract. A

`theorem` line inside a doc comment states a consequence the contract already has; it is proved

outside this block and asks nothing further of you.

-/

/-! ── FLOW ──

Epharmoge(R, X) → start(c) → contextualize(c, utterances), where c is the fused session context and

X, the application context, is c itself:

pass(c): carry out what a person's resolution asked and the context does not yet show done — an

adaptation, a withdrawal — and take in what the write returned; then judge afresh where the

result as it now stands does not fit the context as it now stands, whose each mismatch is,

and how each one stands → write the carrier

[a withdrawal the person asked for has landed] close: discarded

[the person stops] close: stopped

[the person goes on to a protocol they name] close: routed

[nothing open ∧ the person has closed] close: done

[otherwise] present the current list and what this turn changed, then one gate: the next open

mismatch — one whose owner is unclear first — with concrete actions for it; with nothing

open, the list and whether this is done → Stop

next utterance u: c' := pass(fuse(c, u)) → the same reading, whatever u says

no utterance: the gate holds; nothing is judged and nothing closes

-/

/-! ── MORPHISM ──

(R, X)

→ perform(requested) -- carry out the adaptation or withdrawal a person asked for; what the write returned enters the context

→ judge(result, context) -- where the result as it now stands does not fit the accumulated context; afresh on every pass

→ certify(mismatch) -- whose it is: a fit problem here, another deficit's, or unclear (fail-closed)

→ surface(list, changes, one) -- the current list and this turn's changes, then concrete actions for one mismatch

→ resolve(person's turn) -- adapt it, leave it as it is with their reason, stop using the result, hand it on; or close

→ ContextualizedExecution

requires: mismatch_detected(R, X) -- the auto-activation condition only (Layer 2); a user-invoked run enters without it

deficit: ApplicationDecontextualized

invariant: Applicability over Correctness

invariant: the person resolves and closes; evidence only withdraws the AI's own flag or shows what it found

invariant: transformative revalidation (NON-MONOTONE) -- an adaptation changes what the next pass judges, so a run can have more open after a resolution than before it

-/

namespace Epharmoge

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

/-- `R`, the result under review: any completed work product — an AI output, an analysis

conclusion, a decision outcome. The morphism treats every kind alike. -/

abbrev Result := String

/-- **Your reading**: the result as the context now shows it, every adaptation whose write has

landed applied — each write returns its result into the context. Correctness is presupposed

at entry and never re-checked here. -/

axiom target : Context P → Result

/-- `significant` requires a demonstrable behavioral consequence — a downstream decision, a

runtime divergence, a changed gate trajectory; structural extent alone is `minor`. -/

inductive Severity | critical | significant | minor

/-- One place the result does not fit: what does not fit, in plain words; where in the result;

the turn of the context it does not fit, which is never the assistant's own (`Cite`), so the

comparison stays non-circular; and how much it matters. -/

structure Mismatch (c : Context P) where

what : String

inResult : String

against : Cite c

severity : Severity

/-- **Your judgment**, made afresh on every pass: where the result as it now stands does not fit

the context as it now stands — the context is the application context, the person's own

account of their situation and every earlier answer included. One mismatch per claim is the

direction; a claim standing on evidence in several places is one mismatch, since how far a

repair reaches is the resolution's question. Something the person names as not fitting is

judged here like anything else. A mismatch an adaptation aimed at and that is still here

after the write landed is one that adaptation did not repair. -/

axiom mismatches : (c : Context P) → List (Mismatch c)

/-- A deficit label. A certificate assigns only the ones this contract inscribes; the person may

name any. -/

inductive Deficit

/-- this contract's own: a correct result that does not fit its application context -/

| applicationDecontextualized

/-- a missing pre-execution fact, with no observable value to adapt to (hint: /inquire) -/

| contextInsufficient

/-- undefined convention or dependency ownership for the decision (hint: /bound) -/

| boundaryUndefined

/-- a deficit the person names that no constructor above names; emitted bare -/

| emergent (name : String)

/-- The deficits this contract inscribes. -/

def Inscribed : Deficit → Prop

| .emergent _ => False

| _ => True

/-- Every inscribed claim a mismatch's evidence supports, and the cited fit. It certifies this

contract's gate over its own activation and nothing about claims anywhere else. -/

structure Certificate where

claimedBy : List Deficit

distinct : claimedBy.Nodup

inscribed : ∀ d ∈ claimedBy, Inscribed d

fit : String

inductive Whose

| here

| elsewhere (d : Deficit)

| unclear

/-- Read off `claimedBy`, so nothing stored beside it can disagree: the own claim alone is here; a

single other claim is elsewhere; several claims, or none, leave it unclear. -/

def Certificate.whose (k : Certificate) : Whose :=

match k.claimedBy with

| [.applicationDecontextualized] => .here

| [d] => .elsewhere d

| _ => .unclear

/-- **Your judgment**: fit the mismatch's claim against this contract's own claim and its route

claims, reading nothing outside this contract. Evidence that supports no claim leaves it

unclear, and an unclear mismatch is put to the person before anything else happens to it. -/

axiom certify : (c : Context P) → Mismatch c → Certificate

/-- What a person's turn settles for one mismatch. There is no verdict beside it: whether the

mismatch "really" stands is not asked, and nothing here asserts it either way. -/

inductive Resolution

/-- change the result this way; resolves the mismatch until the write lands, after which the

next pass judges the new result -/

| adapt (direction : String)

/-- leave the result as it is here, with the reason the person gave where they gave one -/

| keep (reason : Option String)

/-- stop using the result; `none` when nothing takes its place -/

| discard (replacement : Option Result)

/-- another deficit's: handed to it -/

| elsewhere (d : Deficit)

/-- **Your judgment**: the cited turn resolves `m`, as it now stands, this way. Read against the

context that now stands, the order of its turns included. An adaptation that has landed no

longer resolves a mismatch still found afterwards; a write that failed resolves nothing. -/

axiom ResolutionSupported : {c : Context P} → Mismatch c → Context P → Turn P → Resolution → Prop

/-- A mismatch is resolved only by the person's turn, whatever form that turn takes. -/

def resolutionCoord {c : Context P} (m : Mismatch c) : Coord P Resolution :=

{ admits := (·.val = .person), supports := ResolutionSupported m }

/-- **Your reading**: the person's resolution of `m`; `open_` until one reaches it. -/

axiom resolution : (c : Context P) → (m : Mismatch c) → Occ (resolutionCoord m) c

/-- What evidence alone settled about a mismatch. -/

inductive Shown

/-- it fits after all: the AI withdraws its own flag -/

| fits

/-- it does not fit: shown before the gate, and the person still resolves it -/

| fails

/-- **Your judgment**: the cited evidence, read against the result and the context as they now

stand, admits this reading of `m` alone. Where it admits more than one, it settles nothing.

A person's turn that disputes it leaves it unsettled: evidence settles only what nothing the

person said contests. -/

axiom ShownSupported : {c : Context P} → Mismatch c → Context P → Turn P → Shown → Prop

/-- Evidence stands on what was observed or reported, never on the person's say-so, which is a

resolution. -/

def evidenceCoord {c : Context P} (m : Mismatch c) : Coord P Shown :=

{ admits := (·.val ≠ .person), supports := ShownSupported m }

/-- **Your reading**: what evidence alone settled for `m`, with the evidence cited; `open_`

where it settled nothing. -/

axiom byEvidence : (c : Context P) → (m : Mismatch c) → Occ (evidenceCoord m) c

def filledValue {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Option A

| .open_ _ => none

| .filled a .. => some a

/-- How a mismatch stands. -/

inductive Standing

/-- waits on the person -/

| open_

/-- the person's turn resolved it -/

| resolved (r : Resolution)

/-- the certificate alone handed it to another deficit -/

| handed (d : Deficit)

/-- evidence showed it fits; the AI withdrew its own flag -/

| withdrawn

def standing (c : Context P) (m : Mismatch c) : Standing :=

match filledValue (resolution c m) with

| some r => .resolved r

| none =>

/-- One concrete action the gate offers for a mismatch: what it does, as the resolution it would

record, and what then happens. -/

structure Action where

resolution : Resolution

consequence : String

/-- **Your judgment**: the actions to offer for `m`, each concrete to this mismatch — the change

that would make it fit where one is evident, leaving it as it is and what then happens, not

using the result and what would take its place, and for an unclear owner the deficit each

supported claim would hand it to. Never a category title; the person may answer in their own

words instead. -/

axiom actions : (c : Context P) → Mismatch c → List Action

/-- **Your selection** of the open mismatch the gate presents next: one whose owner is unclear

first, then by severity, critical first. -/

axiom selectNext : (c : Context P) → Option (Mismatch c)

/-- How the person ends the run. -/

inductive Closing

/-- the run is finished; said while mismatches are still open, it reads as `stop` -/

| done

/-- stop here: the result stays as it is, and what is open stays unresolved -/

| stop

/-- go on to the protocol the person names -/

| route (target : String)

/-- **Your judgment**: the cited turn closes the run this way. Only the person's latest turn is

read here: a closing said before the latest round was presented was answered by that round. -/

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 record**, read from the context: the locator the carrier-creating write returned — the

one durable record every mismatch and its standing is written into; `none` where nothing was

ever written. -/

axiom carrier : Context P → Option String

/-- **Your record**: contrary grounds you showed before the person's resolutions — evidence that

a mismatch does not fit, beside a resolution that left it as it is, among them — attached to

the closure; empty when there were none. -/

axiom dissent : Context P → List String

/-- `ContextualizedExecution`: the context at closure, what the person is left with (`none` when a

withdrawal left nothing), the carrier's locator, and the dissent attached to the closure. -/

structure ApplicabilityVerdict (P : Type) where

context : Context P

target : Option Result

carrier : Option String

dissent : List String

inductive Outcome (P : Type)

/-- nothing open and the person closed: by the resolution in their latest turn, or by saying

the run is done -/

| done (v : ApplicabilityVerdict P)

/-- the person withdrew the result and the withdrawal landed; the replacement is carried with no

claim of fit -/

| discarded (v : ApplicabilityVerdict P)

/-- the person stopped; the result stays as it is and what was open stays unresolved -/

| stopped (v : ApplicabilityVerdict P)

/-- the person went on to a protocol they named -/

| routed (target : String) (v : ApplicabilityVerdict P)

| holding (c : Context P)

/-! ── 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 pass is the silent work. It first carries out what a person's resolution asked and the context

does not yet show done, and the write's result returns into the context. It then judges afresh:

the mismatches, whose each one is, what evidence alone settles, and how each stands. The pass's

record follows, then the carrier write. Either a closure fires, or `respond` presents the current

list and one gate. Each person utterance is fused, and the next pass reads it; after an adaptation

that pass judges the new result.

-/

/-- **Your action** for a pass, before anything is judged: where a person's resolution asks for an

adaptation or a withdrawal the context does not yet show carried out, the artifact write that

carries it out, returning what the write returned. -/

axiom perform : Context P → List (Evidence P)

/-- **Your record** of a pass, written once its writes have entered the context: what the pass

judged — the mismatches, their certificates, what evidence settled, their standing — and what

changed since the last pass. A record grounds nothing. -/

axiom passRecord : Context P → List (Response P)

/-- **Your action**: the carrier write — created the first time a mismatch is found, brought into

line on every later pass — returning its locator. -/

axiom persist : Context P → List (Evidence P)

def pass (c : Context P) : Context P :=

let c₁ := c ++ (perform c).map (·.val)

let c₂ := c₁ ++ (passRecord c₁).map (·.val)

c₂ ++ (persist c₂).map (·.val)

/-- The position of the latest turn the person sent. -/

def lastPerson (c : Context P) : Option Nat :=

((List.range c.length).filter fun i =>

match c[i]? with

| some t => decide (t.origin = .person)

| none => false).getLast?

/-- Where the person's resolution of `m` was said. -/

def resolvedAt {c : Context P} (m : Mismatch c) : Option Nat :=

match resolution c m with

| .filled _ src _ _ => some src.idx

| .open_ _ => none

def PersonClosed (c : Context P) : Prop :=

filledValue (closing c) = some .done ∨

def NothingOpen (c : Context P) : Prop := ∀ m ∈ mismatches c, standing c m ≠ .open_

def Closable (c : Context P) : Prop :=

filledValue (closing c) = some .stop ∨

(∃ t, filledValue (closing c) = some (.route t)) ∨

(NothingOpen c ∧ PersonClosed c)

open Classical in

def close (c : Context P) : Outcome P :=

match filledValue (closing c) with

| some .stop => .stopped ⟨c, some (target c), carrier c, dissent c⟩

| some (.route t) => .routed t ⟨c, some (target c), carrier c, dissent c⟩

| _ => .done ⟨c, some (target c), carrier c, dissent c⟩

open Classical in

/-- `respond` presents the round. First the current list: every mismatch found, each with what does

not fit, where, and how it stands, in plain words. Then what this turn changed: what the

person's turn resolved, what an adaptation changed in the result, what is newly found, what an

adaptation aimed at and did not repair, a flag evidence withdrew with that evidence, and a

handoff with its fit and the command only as a hint. Then one gate. For `selectNext`: what does

not fit, where in the result, the turn of the context it does not fit, how much it matters, and

evidence that it does not fit where evidence showed that; then `actions`, each with its

consequence. With nothing open, the list, how far the judgment reached, and whether the run is

done. -/

def contextualize (respond : Context P → Response P) :

Context P → List (Utterance P) → Outcome P

| c, [] => .holding c

| c, u :: us =>

let c₁ := pass (fuse c u)

if Closable c₁ then close c₁

else contextualize respond (c₁ ++ [(respond c₁).val]) us

open Classical in

def start (respond : Context P → Response P) (c : Context P)

(us : List (Utterance P)) : Outcome P :=

let c₁ := pass c

if Closable c₁ then close c₁

else contextualize respond (c₁ ++ [(respond c₁).val]) us

/-! ── LOOP ──

Transformative revalidation (NON-MONOTONE): an adaptation produces a new result, and the next pass

judges it, so an adaptation can breed mismatches that did not exist before, and can leave the one

it aimed at in place. Nothing counts down; every pass judges the whole result against the whole

context. The loop is dialogue: each round ends at a gate, and the person ends the run.

-/

/-!

Silence judges nothing and closes nothing.

theorem silence (respond : Context P → Response P) (c : Context P) :

contextualize respond c [] = .holding c

While no closure fires, an utterance leads to the next gate and closes nothing.

theorem unclosed_holds_gate (respond : Context P → Response P) (c : Context P) (u : Utterance P)

(us : List (Utterance P)) (h : ¬ Closable (pass (fuse c u))) :

contextualize respond c (u :: us) =

contextualize respond (pass (fuse c u) ++ [(respond (pass (fuse c u))).val]) us

A pass only adds to the context.

theorem pass_extends (c : Context P) : ∃ t, pass c = c ++ t

-/

/-! ── CONVERGENCE ──

Every closure is read where it fires and nowhere else. done: nothing open, and the person closed —

routed: the person named the next protocol. Fit is claimed only for the mismatches found, and fit

is not correctness, which was presupposed at entry and is not re-checked here. A mismatch left as

it is carries the person's reason and no claim that it does or does not stand.

Convergence evidence: one line per mismatch found — what did not fit, where, and how it stood at

the close: the person's resolution with the turn it came from, the certificate's handoff with its

-/

/-!

The person's resolution stands over anything evidence or the certificate read.

theorem person_first (c : Context P) (m : Mismatch c) (r : Resolution)

(h : filledValue (resolution c m) = some r) : standing c m = .resolved r

A resolution always rests on a turn the person sent.

theorem resolved_by_person (c : Context P) (m : Mismatch c) (r : Resolution)

(h : standing c m = .resolved r) :

∃ s : Cite c, s.src.val = .person ∧ (c[s.idx]'s.lt).origin = .person

Evidence never rests on the person's say-so.

theorem evidence_not_person {c : Context P} {m : Mismatch c} {s : Cite c}

(ok : (evidenceCoord m).admits s.src) : s.src.val ≠ .person

Only the person closes.

theorem closing_by_person {c : Context P} {s : Cite c}

(ok : (closeCoord (P := P)).admits s.src) : s.src.val = .person

A done run has nothing open, and the person closed it.

theorem done_closed_by_person (c : Context P) (v : ApplicabilityVerdict P) (hc : Closable c)

(h : close c = .done v) : NothingOpen c ∧ PersonClosed c

A mismatch never stands against the assistant's own turn.

theorem against_not_assistant {c : Context P} (m : Mismatch c) :

(c[m.against.idx]'m.against.lt).origin ≠ .assistant

-/

/-! ── TOOL GROUNDING ── -/

-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed

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

inductive Op | judge | certify | handoff | evidenceWithdraw | evidenceShow | gate | adapt

| discard | persist | readTurn | converge | seam

def grounding : Op → Annot × String

| .judge => (.sense, "Internal analysis: the whole result as it now stands against the whole context as it now stands, afresh every pass; it re-executes nothing and reads the completed result and the observable context, never the assistant's own words, as what the result must fit")

| .certify => (.sense, "Internal analysis: each mismatch's claim fitted against this contract's own claim and its route claims, reading nothing outside this contract; fail-closed, so evidence that supports no claim leaves it unclear")

| .handoff => (.extension, "TextPresent+Proceed: a mismatch the certificate alone hands to another deficit, named with its fit and the command only as a hint — a missing pre-execution fact (/inquire), undefined convention or dependency ownership (/bound); nothing is dispatched")

| .evidenceWithdraw => (.extension, "TextPresent+Proceed: where evidence alone shows a flagged place fits, withdraw the flag and say so with that evidence; a person's turn that disputes it puts it back")

| .evidenceShow => (.extension, "TextPresent+Proceed: where evidence alone shows a mismatch does not fit, show that evidence before the gate; the person still resolves it")

| .gate => (.constitution, "present: the current list and this turn's changes, then one mismatch — an unclear owner first — with concrete actions, each with its consequence and never a category title; with nothing open, whether the run is done")

| .adapt => (.transform, "artifact write: the person's adaptation applied to the result; the write's result returns into the context and the next pass judges it")

| .discard => (.transform, "artifact write: withdraw the result and put the replacement in its place, or remove it when nothing takes its place")

| .persist => (.track, "record, record update: the one carrier entry — created when a mismatch is first found, brought into line every pass, one line per mismatch with its standing and what it stood on; its locator is carried out on the verdict")

| .readTurn => (.sense, "Internal analysis: the latest turn read whole against the fused context — a resolution, a closing, something named as not fitting, a correction, a question — whatever form it takes")

| .converge => (.extension, "TextPresent+Proceed: the per-mismatch trace with who settled each line and what it stood on, the adaptations made and any that did not repair what they aimed at, the dissent attached to the closure, and what the verdict does not claim")

| .seam => (.extension, "TextPresent+Proceed: at a chain the person declared, naming the next protocol, proceed to it citing that turn; every Constitution gate inside Epharmoge and the next protocol fires unchanged")

/-! ── COMPOSITION ──

*: product — (D₁ × D₂) → (R₁ × R₂). Mismatch-domain resolution emergent via session context.

contextualize ∘ caller-loop: this protocol is built to run inside another loop. It keeps

collating the result against the accumulated context as the result changes; it does not

establish that the result is correct, and assigns no one else that duty — the verdict states

its own silence.

-/

end

end Epharmoge

```

## Core Principle

**Applicability over Correctness**: Surface evidence that a correct result does not fit its application context; contextual fitness is the question this protocol settles.

## Mode Activation

### Activation

Layer 1 activates whenever the user invokes `/contextualize`, including when nothing may turn out not to fit. Layer 2 may activate only after Aitesis operational evidence has established the recurring pattern “context gathered but application mismatched,” and only when the post-execution result satisfies the formal auto-activation guard. Prior-session recall indices may inform the judgment when available; they never settle the user's resolution.

## Protocol

The formal blocks define execution. This section fixes the user-facing rendering.

### The round

Open every round with the current list: each place the result does not fit, where it is, and how it stands now — waiting on you, what you decided, handed to another protocol, or withdrawn because evidence showed it fits. Follow it with what this turn changed: what your last answer settled, what an adaptation changed in the result, what is newly found, what an adaptation aimed at and did not repair, and any flag withdrawn with the evidence that withdrew it. Keep one carrier entry for the result, one line per mismatch with its standing and what it stood on.

Then ask about one mismatch. Before the question, show what does not fit, where in the result, the part of the context it does not fit (quoted with where it came from), how much it matters, and evidence that it does not fit where evidence showed that. Ask first about a mismatch whose owner is unclear.

The options are concrete actions for this mismatch, each with what then happens — never category titles. For a schedule that lands after working hours:

```

The report goes out at 18:00 Seoul time — after the team has left.

result `0 9 * * *` (server in UTC)

context "the team works in Seoul" (your message)

What should happen?

1. Send it at 09:00 Seoul time — `0 0 * * *`; this overlaps the 00:00–00:30 UTC backup window, so it is checked again

2. Leave the 18:00 arrival as it is — the report goes out unchanged

3. Stop using this cron — say what should replace it

```

The person may answer in their own words, and one answer may settle more than one mismatch. Leaving a mismatch as it is records the reason they gave and makes no claim that the mismatch does or does not stand. Where the owner is unclear, the options name the concrete split, for example "install mail in this image as part of this work" beside "hand it to whoever owns the image (/bound)".

## Rules

- **Non-circularity**: What the result must fit is the context the person and the environment supplied — never the assistant's own words, which a mismatch cannot cite.

- **Round composition**: Compose each round so the reader can act on it without reassembling it — everyday language rather than this file's formal vocabulary, the judgment set beside the evidence it rests on together with the differential implication that matters for the next move, and analytical context laid out before a gate rather than inside it, so the gate carries the question and each option's differential implication. Read `references/round-composition.md` before composing when a term's rendering has to hold across the session or wording has to be carried through unchanged, when some of what is in view belongs to a later round or a trace rather than this one, or when this protocol's own phases bear on where a sentence sits relative to a gate.

- **Recognition over categories**: Offer actions concrete to the mismatch in front of the person, each with its consequence. The person's own words settle what a category would have asked them to choose.

- **Verdict scope**: Present the per-mismatch trace before the verdict. Fit is claimed only for the mismatches found, and an adapted result claims fit, not correctness; a withdrawal claims neither for its replacement.

- **The person resolves and closes**: A mismatch is resolved only by the person's turn, whatever its form, and the person's resolution stands over anything evidence or the certificate read. Evidence alone may withdraw the AI's own flag, reported with that evidence, or show that a mismatch does not fit before the gate; a person's turn that disputes a withdrawal puts it back. Where nothing was found, or nothing was the person's to resolve, the run ends only when the person says it is done after seeing the list.

- **Significant requires demonstrable behavioral impact**: Severity = Significant requires that the mismatch produces a demonstrable behavioral consequence — downstream-decision impact, runtime divergence, gate-trajectory change. Structural-change extent (line count, file count, scope size) alone is insufficient grounds — categorize as Minor when behavioral impact is undemonstrated. This guards against false-positive gating arising from conflation of structural-change extent with applicability impact

- **Form feedback**: Silence about form is not evidence about form. Too dense fails quietly — the reader skims, answers past it, stops — while too plain fails out loud, so the complaints that arrive come from one side only. Density therefore does not carry over from the previous round: each round takes it from what this request asked for, while a statement about form does carry over until it is countermanded. Read an instruction about form for the parts of a round it reaches, not for what kind of reaction it is — a complaint, a request, a symptom report and a bare preference are one input here, and sorting them by kind yields nothing the reach reading does not already give while costing a clause per kind. Change the form rather than asking which form they want; naming one is the recall this discipline exists to remove. What such an instruction reaches is whatever the active protocol leaves open in how a round is composed — its density, its ordering, its length. What it does not reach is whatever is already fixed for this round elsewhere: content the protocol requires, wording carried verbatim, an order it presents in, a cadence it caps, a turn boundary it sets. Those stay in place, and the layer that fixed them is what states why. Say in one line what changed; where the instruction overlapped something that stays, say in one line that it stays and why — that second line is owed by the overlap, not by how the instruction was worded.