Epharmoge Protocol

/-!
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]      the sheet, then one gate over every open mismatch → Stop
  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  : 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}

/-- `X`, the result under review: any work product — this session's output, an analysis, a
    decision, a document, or an artifact another session or person produced. The morphism treats
    every kind alike. -/
abbrev Result := String

/-- **Your reading**: X as the person is now left with it, every write that has landed applied —
    each write returns its result into the context; after a discard, the replacement or `none`,
    whether or not the discarded artifact still exists elsewhere. Correctness is presupposed at
    entry and never re-checked here. -/
axiom target : Context P → Option Result

/-- **Your observation** of the reach, to the limit of what you can read or run without changing
    existing state: every place X lands — what reads or consumes it, its copies and neighbours,
    the people who will read it, the environment it runs in — and every intent in the context it
    was meant to carry. Where to look is yours to judge, and no list of places bounds it. What you
    say you read, you read whole; what the context already holds is read again where a write, an
    utterance, or evidence says it moved; what you create only to look — a scratch copy, a temp
    file — you remove afterwards. A place that needs a change to existing state, someone's
    permission, or another's authority is not reached on your own: it goes into `reach` with what
    it needs. Each return is an evidence turn. -/
axiom observe : Context P → List (Evidence P)

/-- One place X does not fit: what does not fit, in plain words; where in X, or where it lands;
    the turn of the context it does not fit, which is never the assistant's own (`Cite`), so the
    comparison stays non-circular. -/
structure Mismatch (c : Context P) where
  what     : String
  inResult : String
  against  : Cite c

/-- **Your judgment**, made afresh on every pass: where X as it now stands does not fit the context
    as it now stands. The context is the application context — the person's account of their
    situation and the intents they stated along the way, every earlier answer, the conventions
    and environment X meets, and what observation returned from every place X lands. An intent X
    was meant to carry and does not is a mismatch, an omission. 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 place of an X that nothing relies on any more — the person
    discarded it — is not a mismatch. -/
axiom mismatches : (c : Context P) → List (Mismatch c)

/-- What settles one mismatch, read the same way wherever it stands — by the person's turn or by
    evidence. There is no verdict beside it: whether the mismatch "really" stands is not asked,
    and nothing here asserts it either way. `adapt` and `discard` ask for a write and leave their
    mismatch open while it is still found: before the write lands, or after a write that did not
    repair it. A write that repairs it takes it out of what is found, and the sheet says so.
    `keep` and `elsewhere` close it as they stand. -/
inductive Resolution
  /-- change X this way -/
  | adapt (direction : String)
  /-- leave X as it is here, with the reason given where one was given -/
  | keep (reason : Option String)
  /-- stop relying on X; the replacement, or `none`, is what the person is now left with. Within
      what this run may write, the write removes X or puts the replacement in its place; outside
      it, the write is your turn recording that X is no longer relied on, and it counts as carried
      out -/
  | discard (replacement : Option Result)
  /-- not this result's to fix: whose it is — a system, a team, a scope — as named; nothing is
      dispatched -/
  | elsewhere (owner : String)

/-- How a resolution the person's turn carries came to stand: in their own words; by taking an
    action you proposed; or by your choice inside a grant of theirs. -/
inductive How | set | adopted | granted

/-- **Your judgment**: the cited turn of the person resolves `m`, as it now stands, this way — read
    against the context that now stands, the order of its turns included, and not tied to their
    latest turn; the `Resolution` reads as its constructor says. `set`: their own words.
    `adopted`: they took an action you proposed, and only where that action was visible as yours,
    with its consequence and your contrary grounds where there were any, before that turn.
    `granted`: the cited turn entrusts the choice to you, and only inside what it covers; the
    resolution is then your choice under it, recorded as yours. A question, a request to look, a
    deferral, or a bare mention settles nothing. Their answer is read whole: one turn may resolve
    several mismatches, or settle a class of them by a criterion; where it asks for dispositions
    of one result that conflict — a discard beside an adaptation of the same result — it resolves
    neither: only a turn of theirs after the combined consequence has been shown resolves them,
    and the earlier conflicting turn never takes effect on its own. -/
axiom ResolutionSupported : {c : Context P} → Mismatch c → Context P → Turn P → Resolution × How → Prop

/-- A mismatch is resolved on the person's record only by the person's turn, whatever form that
    turn takes. -/
def resolutionCoord {c : Context P} (m : Mismatch c) : Coord P (Resolution × How) :=
  { 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 settles about a mismatch. -/
inductive Settled
  /-- it fits after all: you withdraw your own flag, reported with that evidence -/
  | withdraw
  /-- the evidence settles the resolution: relayed, recorded as yours with that ground -/
  | resolves (r : Resolution)

/-- **Your judgment**: the cited evidence, read against X and the whole context as they now
    stand, admits this reading of `m` alone and fixes all of it; the `Resolution` reads as its
    constructor says. Evidence settles a resolution only where it selects no judgment that is the
    person's. Whether to leave a misfit as it is, to stop using X, or whose it is, is the person's:
    evidence settles those only where something the person already constituted — a decision
    they recorded — settles it. The direction of a change that makes X fit is something
    evidence can fix. Which grounds do this is your reading each time. Where the evidence admits
    more than one reading, it settles nothing; where several sources fix it together, the sheet
    shows them together. A person's turn that disputes it leaves it unsettled. -/
axiom SettledSupported : {c : Context P} → Mismatch c → Context P → Turn P → Settled → Prop

/-- Evidence stands on what was observed or recorded, never on the person's say-so, which is a
    resolution. -/
def evidenceCoord {c : Context P} (m : Mismatch c) : Coord P Settled :=
  { admits := (·.val ≠ .person), supports := SettledSupported 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 — nothing settled it, or what settled it asks for a write that has not
      repaired it; the sheet tells the two apart -/
  | open_
  /-- the person's turn resolved it, and how that resolution came to stand -/
  | resolved (r : Resolution) (how : How)
  /-- evidence alone fixed its resolution: yours, with that evidence -/
  | relayed (r : Resolution)
  /-- evidence showed it fits; you withdrew your own flag -/
  | withdrawn

/-- `adapt` and `discard` ask for a write; `keep` and `elsewhere` do not. -/
def Resolution.asksWrite : Resolution → Bool
  | .adapt _   => true
  | .discard _ => true
  | _          => false

/-- The person's resolution first, whatever evidence read; otherwise what evidence alone settled;
    otherwise it waits on the person. A mismatch still found whose resolution asks for a write
    stays open. -/
def standing (c : Context P) (m : Mismatch c) : Standing :=
  match filledValue (resolution c m) with
  | some (r, h) => if r.asksWrite then .open_ else .resolved r h
  | none =>
    match filledValue (byEvidence c m) with
    | some .withdraw     => .withdrawn
    | some (.resolves r) => if r.asksWrite then .open_ else .relayed r
    | none               => .open_

/-- **Your record** of the reach, read from the context as it now stands: where the judgment looked
    and what it found fits; each place it could not reach, and each write it did not carry out,
    with what it needs — a change outside what this run may write, a permission, another's
    authority — named so the person can point at one you missed. -/
axiom reach : Context P → String

/-- **Your judgment**: the latest utterance, read whole against the context as it now stands,
    bears on this run — it resolves, corrects, disputes, grants, names something that does not
    fit, points at a place to look, asks about the sheet, or changes X or the evidence — even
    where it looks like other work. An utterance that bears on none of it leaves the run as it
    stands: the session answers it, that answer stays in the context, no pass runs, and the last
    outcome stands. -/
axiom Reaches : Context P → Prop

/-- **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, a doubt about a grant's
    reach, 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
    removal left nothing), the reach, and the dissent attached to the closure. -/
structure ApplicabilityVerdict (P : Type) where
  context : Context P
  target  : Option Result
  reach   : String
  dissent : List String

inductive Outcome (P : Type)
  /-- a pass left nothing open -/
  | completed (v : ApplicabilityVerdict P)
  /-- the gate stands over the open mismatches; only the person's turn answers it -/
  | holding (c : Context P)

def Outcome.context : Outcome P → Context P
  | .completed v => v.context
  | .holding c   => c

/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it.
-/

/-! ── PHASE TRANSITIONS ──
A pass is silent and orthogonal to the person's coordinate: observe the reach, `perform` the
relay, observe again; every return enters the context, and how each mismatch stands is then read
from it. `respond` presents the sheet — the closing sheet on completion. `session` answers an
utterance that does not bear on this run.
-/

/-- A turn a write returns: your own, stating a revised result or recording a discard, or what an
    artifact write returned. Never the person's, never a peer's. -/
def Write (P : Type) := {e : Turn P // e.origin = .assistant ∨ e.origin = .external}

/-- **Your action**, the relay: carry out every adaptation and every discard a resolution settles —
    the person's, one under their grant, one evidence relays — that the context does not yet show
    carried out, the person's whole answer read and its combined consequence weighed first, and
    what your own writes newly settle, until nothing newly settled is left; where a write brings
    back a place an earlier write in this run repaired, stop there and leave both for the person.
    A write follows where X lives: an artifact is written where it lies; a result that lives in
    the conversation — an answer, an analysis — is adapted by your stating the revised result in
    your own turn. What this run may write is what the work in front of the person covers and
    they hold authority over: their own resolution turn authorizes a write to anything they hold,
    an artifact another session of theirs produced included; another person's artifact, or a
    scope they do not hold, needs that person or a permission. A write outside that, or one whose
    effect cannot be undone — a removal or overwrite with no way back, a deploy, a send outside —
    is not carried out, even where evidence fixes its direction: it goes into `reach` with what it
    needs, and its mismatch waits on the person; once their turn authorizes it, it is carried out.
    A discard there is the exception: its write is your turn recording that X is no longer relied
    on. Returns what the writes returned. -/
axiom perform : Context P → List (Write P)

def pass (c : Context P) : Context P :=
  let c₁ := c ++ (observe c).map (·.val)
  let c₂ := c₁ ++ (perform c₁).map (·.val)
  c₂ ++ (observe c₂).map (·.val)

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

def verdict (c : Context P) (t : Context P) : ApplicabilityVerdict P :=
  ⟨t, target c, reach c, dissent c⟩

open Classical in
/-- `respond` presents the round, read on the context the pass left, in this order. An overview:
    how many places do not fit, how many wait on the person's choice, and how many are settled
    and still to be carried out. Every mismatch found, the ones
    that matter most first: what does not fit, where, the part of the context it does not fit
    (quoted with where it came from), how much it matters — significant only with a demonstrable
    behavioral consequence (a downstream decision, a runtime divergence, a changed gate
    trajectory), structural extent alone minor — and how it stands: waiting on the person; the
    person's resolution with their turn quoted, the intent taken from it, and whether they said
    it, took a proposed action, or entrusted the choice; a relayed resolution with the evidence
    that fixed it; a withdrawn flag with that evidence; one whose write landed without repairing
    it, said to be unrepaired; one whose write was held, with what it needs. For each open one,
    concrete actions, each with its consequence and your contrary grounds where you have them,
    never a category title — the person may answer in their own words — and for one held, the
    resolutions that unblock it: the change carried out once they authorize it, the change they
    make themselves, handing it to its owner (nothing is sent), or leaving it. Mismatches that bear
    on each other grouped, with their combined consequence. Then `reach`: what fits and what was
    not reached. Then what changed since the last sheet: each line added, removed, or changed
    names what moved — a write, a new observation, a person's turn, or a reading of yours
    corrected on unchanged ground, said to be a correction; a line that left says why. Then one
    question over every open mismatch; take them one at a time only where one answer changes what
    a later choice means or the person asks for it. What the utterance asked outside this run is
    answered here; a step that rests on X and cannot be undone waits while something is open,
    and the open places are shown before it. Re-present the whole sheet where it changed or the
    person asked for it; a question about the sheet is answered with the gate said to stand. On
    completion, the closing sheet is CONVERGENCE's convergence evidence. Where the run may be cut off before it
    completes, keep the current sheet in a durable record the person can find. -/
def settle (respond : Context P → Response P) (c : Context P) : Outcome P :=
  let t := c ++ [(respond c).val]
  if NothingOpen c then .completed (verdict c t) else .holding t

open Classical in
def contextualize (respond session : Context P → Response P) :
    Context P → Outcome P → List (Utterance P) → Outcome P
  | _, o, []      => o
  | c, o, u :: us =>
    let c' := fuse c u
    if ¬ Reaches c' then contextualize respond session (c' ++ [(session c').val]) o us
    else
      let o' := settle respond (pass c')
      contextualize respond session o'.context o' us

def start (respond session : Context P → Response P) (c : Context P)
    (us : List (Utterance P)) : Outcome P :=
  let o := settle respond (pass c)
  contextualize respond session o.context o us

/-! ── CONVERGENCE ──
Every closure is read where it fires and nowhere else. completed: `NothingOpen`, whether or not
the person decided anything in this run; the closing sheet carries the ground. Fit is claimed
only for the mismatches found within the reach, and fit is not correctness, which was presupposed
at entry and is not re-checked here; a replacement this run wrote is judged by the next
observation like the result it replaced. A mismatch left as it is carries the reason given 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,
quoted, the intent taken from it, and how it came to stand; a grant with what it covered; a
relayed resolution or a withdrawn flag with its evidence — beside the writes made with what each
changed in X, any that did not repair what they aimed at, the lines that left and why, what was
checked and fits, what was not reached with what it needs, the dissent attached to the closure,
and what the verdict does not claim. 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 | observe | judge | evidence | gate | adapt | discard | readTurn | record | converge
             | seam

def grounding : Op → Annot × String
  | .observe   => (.observe, "artifact read, artifact search, record read, and a run that changes no existing state — no send, nothing left behind: every place the result lands and every intent it answers to; each return enters the context as an evidence turn; a place that needs a change to existing state, a permission, or another's authority is named with what it needs and left unreached")
  | .judge     => (.sense, "Internal analysis: the whole result as it now stands against the whole context as it now stands, afresh every pass — never the assistant's own words as what the result must fit; how each mismatch stands; what fits and what was not reached")
  | .evidence  => (.interaction .extension, "where evidence alone settles a mismatch as SettledSupported says, withdraw your own flag or record the relayed resolution as yours, with that evidence; a person's turn that disputes it leaves it open")
  | .gate      => (.interaction .constitution, "the sheet: every mismatch found with how it stands, concrete actions for each open one with their consequences and your contrary grounds where you have them, never a category title, what fits, what was not reached, and what changed since the last sheet — then one question over every open mismatch")
  | .adapt     => (.transform, "artifact write, or the revised result stated in your own turn where the result lives in the conversation: an adaptation a settled resolution asks, within what this run may write; what it returns enters the context and the next observation reads it")
  | .discard   => (.transform, "within what this run may write, an artifact write that withdraws the result and puts the replacement in its place, or removes it when nothing takes its place; outside it, your turn recording that the result is no longer relied on")
  | .readTurn  => (.sense, "Internal analysis: the new turn, and every earlier turn of the person's it bears on, read whole against the fused context as it now stands — whether it bears on the run, and what it does there: resolves, corrects, disputes, grants, names something that does not fit, points at a place to look, asks about the sheet")
  | .record    => (.track, "record: the current sheet kept in a durable record the person can find, where the run may be cut off before it completes")
  | .converge  => (.interaction .extension, "the closing sheet: the convergence evidence CONVERGENCE names")
  | .seam      => (.interaction .extension, "after completion, proceed to the next move the person declared, 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

Two places do not fit; both wait on you.

1. The report goes out at 18:00 Seoul time — after the team has left. Matters: nobody reads it the day it is sent.
   result   `0 9 * * *` (server in UTC)
   context  "the team works in Seoul" (your message)
   a. Send it at 09:00 Seoul time — `0 0 * * *`; this overlaps the 00:00–00:30 UTC backup window, so it is checked again
   b. Leave the 18:00 arrival — the report goes out unchanged

2. The report is mailed to ops@, but you asked for it in #daily-report. Matters: the forward from ops@ drops the attachment, so the team gets the report without its numbers.
   result   `MAILTO=ops@…`
   context  "put it in #daily-report" (your message)
   a. Post to #daily-report through the webhook the repo already uses
   b. Keep mail — say why, and it is recorded; against it: the team keeps getting it without the numbers

Fits: the script, its log path, the mail relay.
Not reached: whether the webhook token is valid in production — reaching it needs a live send.

Which way for each? Your own words are fine — for example "1a, 2a".