/contextualize

name: contextualize
description: "A result may not fit where it lands or may leave out what was asked: the user sees each misfit found, settled or withdrawn, and the fixes carried out and reread until nothing is open."

Epharmoge Protocol

Check a result against every place it lands and every intent it was meant to carry, show every place it does not fit on one sheet, and carry out the fixes the person settles. Type: `(ApplicationDecontextualized, AI, CONTEXTUALIZE, Result) → ContextualizedExecution`.

Definition

**Epharmoge** (ἐφαρμογή): A dialogical act of checking that a result fits the situation it is applied in — from Aristotle's notion of practical application — resolving the gap between technical correctness and contextual appropriateness. The result is any work product: this session's output, an analysis, a decision, a document, or an artifact another session or person produced. Two things run side by side. The person holds one coordinate per place the result does not fit — fix it this way, leave it for this reason, stop using it, or it is not this result's to fix — and only that coordinate waits on them. Orthogonal to it, the AI relays: it follows the result to everywhere it lands and every intent it was meant to carry, and carries out what is settled within what this run may write. Every place the result does not fit, an omission included, goes on one sheet with its consequence in the person's own situation, and the person answers the sheet in one turn. The run completes when a pass leaves nothing open, with no closing turn asked of them. Completion establishes fit for what was found within what was reached — not the correctness of the result.

/-!
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 ──
Epharmoge(X) → start(c) → contextualize(c, utterances), where c is the fused session context and
X, the result under review, is whatever the invocation names — this session's output or an
artifact from elsewhere:
  pass(c): observe; perform — the relay; observe again
  [nothing open]   completed — the closing sheet
  [otherwise]      holding — the sheet, with one question over every open mismatch
  next utterance u: c' := fuse(c, u), read whole →
    [u does not bear on this run]   the session answers it; the run stands as it was
    [otherwise]                     pass(c') → the same reading
  no utterance: the last outcome stands; a later utterance that bears on the run opens it again
-/

/-! ── MORPHISM ──
(X, context)
  → observe(reach)             -- every place X lands and every intent it answers to, without changing existing state; what could not be reached, named
  → judge(result, context)     -- where X as it now stands does not fit the context as it now stands; afresh on every pass
  → perform(settled)           -- the relay: every settled resolution within what this run may write, and what its own writes newly settle
  → surface(sheet, changes)    -- every mismatch at once, with concrete actions, what fits, what was not reached, and what changed
  → resolve(person's turn)     -- adapt, keep with their reason, stop using, not this result's — their words, a proposal they took, a grant of theirs
  → ContextualizedExecution
requires: mismatch_detected(X)   -- the AI-opened path only (Layer 2); an invocation declares the deficit and enters without it
deficit:  ApplicationDecontextualized
preserves: every turn of the context -- the context only grows (pass_extends); a write changes only what this run may write (perform)
invariant: Applicability over Correctness
invariant: the person holds each resolution; evidence settles one only where it chooses nothing that is the person's (SettledSupported)
invariant: transformative revalidation (NON-MONOTONE) -- a write changes what the next observation reads, so a run can have more open after a resolution than before it; every pass judges the whole X against the whole context
invariant: Focus never records -- the sheet, its order, and whether an utterance bears on the run are re-read every turn; only the person's turn, a grant of theirs, or evidence that fixes it moves a resolution onto the record
-/

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