conduct · diff
git:20261004.2323a31 to git:20261006.9d9c00e
94 added, 121 removed. Audit A to A.
---
name: conduct
description: "The work needs several lines of thinking, and their order, independence, combination, stopping point, or where results go is not obvious: settle the method before starting."
---
# Hyphegesis Protocol
Conduct how a session's epistemic work will be carried out — the lines of work, their order, independence, combination, stopping point, and where their results go — when that method is underdetermined while the goal is clear. The morphism is **design THEN hand off**: Hyphegesis drafts the whole method as one map, the person recognizes or corrects it and keeps the coordinates only they can fill, and the method is handed off with what it carries; then Hyphegesis stops, and the substrate executes. Type: `(MethodUnderdetermined, Hybrid, CONDUCT, WorkProspect) → ConductedMethod`.
## Definition
- **Hyphegesis** (ὑφήγησις: a leading-the-way, guiding from just ahead): A dialogical act of conducting a session's epistemic work when the goal is clear but how to run it is not. The protocol's lexical verb is `/conduct`. Once it has run, the person can say: this work proceeds this way — these lines run in this order or side by side, they combine like this, they stop here, and their results go there; I recognize what I entrusted and what I kept, and I took this method as mine; what cannot be decided yet is marked to come back to me where it binds. The whole map and its execution start as your judgment — which lines of work, how they relate, who runs each and where, and how precisely the map is worth drawing for the time it takes to reach the goal. The person keeps only what is theirs: when to stop, how lines combine, where results go, the constraints in force, and the authority they entrust with its limits, given as a broad direction. Every person turn is read again against the context as it now stands. The method is taken on the person's word once what it takes was shown with its evidence and your contrary grounds, or relayed at the start where the person's own words already settle it; it is handed off carrying the person's coordinates, the deferred decisions, its lifetime, and the capabilities it needs — a way back to the person among them — and the run ends there.
+ **Hyphegesis** (ὑφήγησις: a leading-the-way, guiding from just ahead): A dialogical act of conducting a session's epistemic work when the goal is clear but how to run it is not. The protocol's lexical verb is `/conduct`. Once it has run, the person can say: this work proceeds this way — these lines run in this order or side by side, they combine like this, they stop here, and their results go there; I recognize what I entrusted and what I kept, and I took this method as mine; what rests on me goes no further without me and comes back to me at the end, while the rest runs on. The whole map and its execution start as your judgment — which lines of work, how they relate, who runs each and where, and how precisely the map is worth drawing for the time it takes to reach the goal. The person keeps only what is theirs: when to stop, how lines combine, where results go, the constraints in force, and the authority they entrust with its limits, given as a broad direction. Every person turn is read again against the context as it now stands. The method is taken on the person's word, or relayed at the start where the person's own words already settle it; the turn that closes presents the map as a relay — after a taking, once more, with what that turn changed on its ledger — and hands it off in the same turn without waiting, carrying what that map showed: the person's coordinates, the deferred decisions, its lifetime, and the capabilities it needs; and the run ends there.
```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 ──
Hyphegesis(WP) → start(c) → conduct(c, utterances), where c is the fused session context:
start: observe(c) — what the pointer's record returns and the loaded inventory enter the
- context → [the person's words already settle the method: relay] → the conduct trace →
+ context → [the person's words already settle the method: relay] → the map, relayed →
handoff | otherwise → the map → Stop
next utterance u, fused into c:
[the utterance does not bear on this run] the session answers it; the gate holds
[the person withdraws] → what stands and what is open; nothing handed off
otherwise c' := observe(fuse(c, u)), every reading below taken afresh on c' →
- [the person takes the method ∧ Covered(c')] → the conduct trace → handoff → ConductedMethod
+ [the person takes the method] → the map, relayed → handoff, in the same turn → ConductedMethod
[otherwise] → the map again, drawn from c', with a ledger
no utterance: the gate holds; nothing is taken
- after handoff: the run has ended. The substrate executes the method and returns to the person as
- the Rule "Handoff carries its obligations" names; re-entry is as the Rule "Re-entry" says.
+ after handoff: the run has ended; the substrate executes the method as the Rule "Handoff carries
+ its obligations" names, and re-entry is as the Rule "Re-entry" says.
-/
/-! ── MORPHISM ──
WorkProspect
→ observe(pointer, inventory) -- what the pointer's record returns and the loaded inventory enter the context first
→ draft(map) -- the whole method, your judgment, drawn only as precisely as reaching the goal is worth (focus)
→ place(substrate) -- who runs each line, where, and whether the person is present: your inference, shown on the map
→ present(map) -- the map with your contrary grounds; after an answer, a ledger of what it changed
→ fuse(answer) -- the answer joins the context whole
→ stand -- a person's turn makes a coordinate stand, under the record rule (`StandingSupported`)
- → take -- the person takes the method as shown; before any map, their words may already settle it (relay)
- → handoff(ConductedMethod) -- the method with what it carries; then stop
+ → take -- the person takes the method, as shown or with what the same turn changes; before any map, their words may already settle it (relay)
+ → handoff(ConductedMethod) -- the map relayed in the closing turn, then the method with what it showed, without waiting; then stop
→ ConductedMethod
requires: method_underdetermined(WP) -- declared by invoking /conduct; judged only on the AI-guided path
deficit: MethodUnderdetermined -- activation precondition (Layer 1/2)
preserves: WP -- the context only grows; the prospect is never rewritten
invariant: Conduction over Substrate -- the method is designed and handed off; the substrate runs it
invariant: Focus never records -- the map is re-read every turn; only the person's words move a value into the record
-/
namespace Hyphegesis
/-! ── 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}
/-- `WP`, `WorkProspect`: the work or goal facing object-level cognition, its method not yet
determined. Read from the context; an amendment the person makes is part of it. -/
abbrev WorkProspect (P : Type) := Context P
structure HandoffLocator where
record : String
session : String
/-- `N`, `NavigationBlock`: the fixed cross-session shape — a pointer, never a copied record. -/
structure NavigationBlock where
purposeFrame : String
canonicalLocator : HandoffLocator
dereferenceInstruction : String
snapshotAnchor : Option String
groundingInstruction : String
/-- **Your reading**: the navigation block the context supplies over the record the work was
parked in, a sibling protocol's emitted block included; `none` otherwise. It is carried
unchanged, and nothing it names is copied into this protocol's output. -/
axiom pointer : Context P → Option NavigationBlock
/-- **Your reading** while a pointer is held: follow the block's dereference instruction at its
locator and run its grounding instruction; what the record returns enters the context as
- observation. Nothing when there is no pointer. A pointer that does not resolve, or a record
- that does not support a premise the method needs, is a finding the map shows; it closes
- nothing. -/
+ observation. Nothing when there is no pointer. A pointer that does not resolve, or a record that
+ does not support a premise the method needs, is a finding the map shows, with what
+ was tried; it closes nothing. -/
axiom groundPointer : Context P → List (Evidence P)
/-- **Your observation**: what the loaded environment returns when you read it for the method the
map now holds — the agents, skills, sessions, and tools it actually answers with — before the
- map that shows it. -/
+ presentation that shows it. -/
axiom inventory : Context P → List (Evidence P)
/-- What is observed enters the context before the presentation it informs. -/
def observe (c : Context P) : Context P :=
let c₁ := c ++ (groundPointer c).map (·.val)
c₁ ++ (inventory c₁).map (·.val)
/-- The method as the map shows it, in the map's own words. Its shape is yours; nothing here fixes
one. -/
abbrev Method := String
/-- **Your draft**: the whole method, from the whole context, drawn again after every utterance so
a change upstream re-fills what depends on it. What a method settles are open questions for
you to answer from the work, never slots to fill: which lines of work there are and what each
does; in what order they run or whether side by side; whether they see each other before their
results combine; how separately produced results combine; when each stops; where each result
goes; and what the method leaves uncovered. Draw the map only as precisely as reaching the
goal is worth: where trying is cheap and can be undone, a coarse map run once and checked
against its use may be the method, and more precision spends the time it was meant to save.
Every line of work lands somewhere on the map — that the map is complete is your judgment, and
the person checks it. A protocol the person declared next stands as a line of the method placed
after the lines whose results it takes, recorded as their `constraint` coordinate — or, where it
receives the end results, as their `destination`. A value the person set stays theirs on the
- reach their words gave it, and the map marks it as theirs. -/
+ reach their words gave it. -/
axiom draft : Context P → Method
/-- **Your inference**: who runs each line of work, where, and whether the person will be present
while it runs — read from the tools the running harness describes and from the accumulated
context, never from a fixed list, since another harness describes its tools differently. It is
shown on the map as the draft's inference; the person points only the broad direction, and
where their words fix part of it — a direction, whether they will be present — that part stands
as their `constraint` coordinate and this inference follows it. That coordinate's reach is read
again on the context as it now stands, like any of theirs, and this inference follows what it
still reaches. A tool description is material for this proposal and for which observations to
attempt; it grounds no verdict, grants nothing, and shows no act reachable. -/
axiom placement : Context P → String
/-- **Your reading**: what the method needs from its substrate to run as drawn — an act, a tool, a
- session, a record to write to where a result's destination is a later session; and, where the
- substrate does not share this session, a way back to the person for every return to them, and a
- way to read the person's turns that govern its grants and coordinates. -/
+ session, a record to write to where a result's destination is a later session. -/
axiom required : Context P → List String
/-- **Your judgment**: the cited observation shows whether the substrate can provide `k`. -/
axiom FeasibilitySupported : String → Context P → Turn P → Bool → Prop
/-- Whether a capability is there is read from an observation: a turn the environment returned.
Text injected into the session, a tool description among it, grounds no verdict. -/
def feasibilityCoord (k : String) : Coord P Bool :=
{ admits := (·.val = .external), supports := FeasibilitySupported k }
/-- **Your reading** for `k`: filled with whether the substrate provides it, citing the
- observation; open where nothing observed it, and the map and the trace say it is unconfirmed. -/
+ observation; open where nothing observed it, and the map says it is unconfirmed. -/
axiom feasibility : (c : Context P) → (k : String) → Occ (feasibilityCoord (P := P) k) c
/-- The coordinates only the person fills. -/
inductive Held
/-- when a line of work, or the whole method, stops -/
| stop
/-- how the lines' results are combined -/
| combine
/-- where a result goes beyond the method -/
| destination
/-- a constraint in force on the work — a direction the person gave for the substrate, whether
they will be present, or a horizon among it -/
| constraint
/-- the authority the person entrusts and its limits, given as a broad direction -/
| grant
/-- One coordinate the person holds: its kind, and its reach — what it settles and the line or
lines it binds, or the whole method, in the map's words. Two decisions of one kind on the same
lines are two coordinates. -/
structure Coordinate where
kind : Held
reach : String
/-- **Your judgment**, the live inventory of the person's coordinates: every coordinate the method
turns on that this run has raised and the person's words have not since retired, read over the
whole fused context — the map, every answer, and what the person said outside the map: a
grant, a direction for the substrate, whether they will be present, a horizon. A value the
draft fills for a kind the person holds raises that coordinate, so it is recorded or left open,
never carried out as settled. -/
axiom coordinates : Context P → List Coordinate
/-- Who first put a value forward: you, or the person. -/
inductive Proposer | draft | person
/-- What the turn that made a value stand did: gave it in its own words, took a value put forward
before, or gave a grant that reaches your choice. -/
inductive Standing | set | adopted | granted
/-- What stands on a coordinate: the value, in the words of the turn that set it or of the
proposal as it was shown, who first put it forward, and how it came to stand. -/
structure Determination where
value : String
proposer : Proposer
standing : Standing
/-- **Your judgment**, the record rule: the cited turn makes coordinate `x` stand as `d`, read
against the context as it now stands, on the reach the turn's words give it. The proposer is
whoever first put the value forward in the context; the standing is what the cited turn itself
did: gave the value in its own words (`set`), took a value put forward before (`adopted`) —
- where you put it forward, only if it was visible as yours, with what decides it and your
- contrary grounds, before this turn — or gave a grant whose words reach your choice
- (`granted`). A grant never reaches the authority coordinate itself: the authority and its
- limits stand only as the person set or adopted them. Whether an act falls inside a grant is
- read the same way; an act the method needs that falls outside it, or whose place inside it is
- unclear, the person sees before the act — on the map, or after handoff as the Rule "Handoff
- carries its obligations" names. A question, a deferral, or a bare mention makes nothing
+ where you put it forward, only if it was shown on a map before this turn — or gave a grant
+ whose words reach your choice (`granted`). A grant never reaches the authority coordinate
+ itself: the authority and its limits stand only as the person set or adopted them. Whether an
+ act falls inside a grant is read the same way, and the Rule "Person's coordinates" says where
+ the person sees one that does not. A question, a deferral, or a bare mention makes nothing
stand. -/
axiom StandingSupported : Coordinate → Context P → Turn P → Determination → Prop
/-- Only a person's turn makes a value stand on a coordinate the person holds, and no grant makes
a value stand on the grant coordinate itself. -/
def heldCoord (x : Coordinate) : Coord P Determination :=
{ admits := (·.val = .person),
supports := fun c t d => StandingSupported x c t d ∧ (d.standing = .granted → x.kind ≠ .grant) }
/-- **Your reading**: how coordinate `x` stands in `c` — filled by the person's latest turn that
makes it stand; open where none does. A value a person's turn made stand changes only by their
later words, or returns open past the lifetime their words or the map they took gave it; a
value standing under their grant (`granted`) changes only within that grant's reach, and the
ledger flags the change as it flags a taken value. A map that left whether their decision still
reaches a coordinate unclear leaves that coordinate open, never adopted. -/
axiom operative : (c : Context P) → (x : Coordinate) → Occ (heldCoord (P := P) x) c
def isFilled {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Bool
| .open_ _ => false
| .filled .. => true
/-- One recorded value: the coordinate, what stands on it, and the person's turn it stands on,
with that turn's support. -/
structure Recorded (c : Context P) where
coord : Coordinate
det : Determination
src : Cite c
byPerson : src.src.val = .person
supported : StandingSupported coord c (c[src.idx]'src.lt) det
notSelfGrant : det.standing = .granted → coord.kind ≠ .grant
def recordOf {c : Context P} (x : Coordinate) :
Occ (heldCoord (P := P) x) c → List (Recorded c)
| .open_ _ => []
| .filled d s allowed supported => [⟨x, d, s, allowed, supported.1, supported.2⟩]
/-- The record: every filled occurrence over the live inventory. A proposal of yours the person
has not taken lives only in the map. -/
def record (c : Context P) : List (Recorded c) :=
(coordinates c).flatMap (fun x => recordOf x (operative c x))
/-- What is still open: every live coordinate whose occurrence is open. None closes by default. -/
def residual (c : Context P) : List Coordinate :=
(coordinates c).filter (fun x => !isFilled (operative c x))
/-- A decision or a supply the method leaves open, where it binds, and whether it returns to the
person; one that does not names in `what` the recorded grant whose reach covers it. -/
structure Deferred where
what : String
binds : String
toPerson : Bool
- /-- **Your reading**: what the method leaves open, each read along two questions that may both
- hold: does its deciding evidence arrive only later, and can only the person supply or settle
- it? One whose evidence arrives later is decided by the substrate only where a recorded grant's
- reach covers it, shown on the map as covered by that grant; where the grant is open or its reach
- unclear, and wherever only the person can supply or settle it, it returns to them (`toPerson`)
- before the work it binds, once its deciding evidence is in where that arrives later — a secret
- or credential to set, a runtime error the substrate cannot resolve, a deployment handed to
- runtime, a fusion whose shape only the person can choose. -/
+ /-- **Your reading**: what the method leaves open, each read along two questions that may both hold:
+ does its deciding evidence arrive only later, and can only the person supply or settle it? One
+ whose evidence arrives later is decided by the substrate only where a recorded grant's reach
+ covers it, shown on the map as covered by that grant; where the grant is open or its reach
+ unclear, and wherever only the person can supply or settle it, it returns to them (`toPerson`) —
+ a secret or credential to set, a runtime error the substrate cannot resolve, a deployment handed
+ to runtime, a fusion whose shape only the person can choose. -/
axiom deferred : Context P → List Deferred
/-- **Your reading**: how long the method's grants and readings hold — following a horizon the
person gave, which stands as their `constraint` coordinate, and your reading of the work
otherwise; past it, what rested on them returns open, as `operative` reads it. -/
axiom lifetime : Context P → String
- /-- **Your record**: the contrary grounds you presented before the utterance that closes — a
- value you would set otherwise, the draft's weakest assumption, a line you doubt, that the work
- may need no conducting, a capability you expect the substrate cannot provide, a pointer that
- did not resolve — attached to the closure; empty when there were none, as on a relay, which
- stands only where you hold none. -/
+ /-- **Your record**: the contrary grounds you hold at the closure — a value you would set otherwise,
+ the draft's weakest assumption, a line you doubt, that the work may need no conducting, a
+ capability you expect the substrate cannot provide, a pointer that did not resolve — shown on
+ the map, or in a withdrawal's record, and attached to the closure; empty when there are
+ none. -/
axiom dissent : Context P → List String
- /-- **Your judgment**, the adoption condition: everything the method would take was shown on the
- map the taking turn answered — each value with who proposed it and whether it is theirs,
- granted, or the draft's, its ground, whether each thing it needs was observed — unconfirmed
- where nothing did — and your contrary grounds. A value the taking turn itself sets is the
- person's own and is not taken unseen. Nothing observed after the taking turn changes what it
- took; where it does, or anything would be taken unseen, the map is drawn again. -/
- axiom Covered : Context P → Prop
-
/-- **Your judgment**: the cited turn takes the method as the map showed it, read against the
- context as it now stands; whatever the same turn settles is read with it. A turn before the
- latest map, or from an earlier run, takes nothing on it. Your own reading that the method is
- ready closes nothing. -/
+ context as it now stands; whatever the same turn settles or changes is read with it, and is
+ carried on the relayed map's ledger rather than drawn into a map that waits. A turn before the latest
+ map, or from an earlier run, takes nothing on it. Your own reading that the method is ready
+ closes nothing. -/
axiom ResolutionSupported : Context P → Turn P → Unit → Prop
/-- Only the person takes the method. -/
def resolutionCoord : Coord P Unit :=
{ admits := (·.val = .person), supports := ResolutionSupported }
/-- **Your reading**: the person's taking of the method; `open_` until one reaches it. -/
axiom resolution : (c : Context P) → Occ (resolutionCoord (P := P)) c
- /-- **Your judgment**, read only where the run opens, before any map: the person's own words,
- read against the context as it now stands, already settle every person-held judgment the
- method needs — what deferred decisions remain is said explicitly, and where they give a grant,
- its horizon — so no value of yours on a coordinate the person holds would be taken unseen. It
- stands only where you hold no contrary ground, and, where the person will not be present, the
- way back to them is not unconfirmed; otherwise the map is drawn, so a contrary ground meets a
- turn of theirs. The placement, the lifetime past what the person fixed, and what the method
- needs are your inference, not among these: the relay presentation and the trace show them,
- each need observed or unconfirmed. Words from an earlier run settle nothing here, and a run
- you opened does not relay: nothing said before its first map settles it. Where an observation
- found something missing — something the method needs, or the record an incoming pointer
- names — the person sees that on a map first. Once a map has been shown, words that settle the
- method are a taking. Your reading that the work needs no conducting is not this: it is a
- contrary ground on the map, and the person decides. -/
+ /-- **Your judgment**, read only where the run opens, before any map: the person's own words, read
+ against the context as it now stands, already settle every person-held judgment the method needs
+ — what deferred decisions remain is said explicitly, and where they give a grant, its horizon —
+ so no value of yours on a coordinate the person holds would be taken unseen. Your contrary
+ grounds do not hold it back — they ride the relayed map. The placement, the lifetime past what
+ the person fixed, and what the method needs are your inference, not among these: the relayed
+ map shows them, each need observed or unconfirmed. Words from an earlier run settle nothing
+ here, and a run you opened does not relay: nothing said before its first map settles it. Once a
+ map has been shown, words that settle the method are a taking. Your reading that the work needs
+ no conducting settles nothing here: it is a contrary ground like any other. -/
axiom RelaySupported : Context P → Turn P → Unit → Prop
/-- Only the person's words settle a method without a map. -/
def relayCoord : Coord P Unit :=
{ admits := (·.val = .person), supports := RelaySupported }
/-- **Your reading**: the person's words that settle the method; `open_` until they do. -/
axiom relay : (c : Context P) → Occ (relayCoord (P := P)) c
/-- **Your judgment**: the cited turn withdraws — the person stops here without taking a method —
read against the context as it now stands. A turn before the latest map, or from an earlier
run, withdraws nothing from this one, and your own reading that the run should end closes
nothing. -/
axiom WithdrawalSupported : Context P → Turn P → Unit → Prop
/-- Only the person withdraws. -/
def withdrawalCoord : Coord P Unit :=
{ admits := (·.val = .person), supports := WithdrawalSupported }
/-- **Your reading**: the person's withdrawal; `open_` until one reaches it. -/
axiom withdrawal : (c : Context P) → Occ (withdrawalCoord (P := P)) c
/-- **Your judgment**: the latest utterance bears on this run — an answer to the map, a value, a
grant, a direction, a question about the map, a withdrawal, a taking. An utterance about other
work leaves the run as it stands: the session answers it, that answer stays in the context, and
no gate of this run is raised. -/
axiom Reaches : Context P → Prop
/-- The record a withdrawal carries: the context, what stands with who proposed each value and
how it stood, what is still open, the deferred decisions, and the dissent. Nothing in it is
handed off, and the draft does not become the next move. -/
structure Closed (P : Type) where
context : Context P
record : List (Recorded context)
residual : List Coordinate
deferred : List Deferred
dissent : List String
def closed (c : Context P) : Closed P :=
{ context := c, record := record c, residual := residual c, deferred := deferred c,
dissent := dissent c }
/-- **Your record**: the navigation block over the record where the person's turns behind this
run's recorded values and grants can be read — the session record, or the record the run
writes to — produced by this run; `none` where no record outside this session can be
addressed. -/
axiom source : Context P → Option NavigationBlock
- /-- `ConductedMethod`: the method handed off and what it carries. `plan` is the method as the map
- the closing turn answered showed it, with what that turn itself set — on a relay, the person's
- words for what they settled and your draft for the rest — and where its text and a recorded
- value differ, the recorded value governs. The substrate executes it and returns to the person
- as the Rule "Handoff carries its obligations" names — one consolidated summary of every line's
- results when it has run, and the returns that Rule lists mid-run, where silence holds.
- Independent lines are handed off so they do not see each other's results before those results
- combine. Every navigation block this method leaves for a reader outside this session —
- `source`, and the one over the record a later-session result is written to — is supplied by
- its producer from that record's own identity, source session, and purpose; its grounding
- instruction directs the recipient to run `/inquire` or equivalent
- grounding over the record and its cited sources, recover the retained and entrusted judgments
- from the governing utterances, and keep an unsupported decision open while independent work
- may continue. `pointer` is the incoming block, carried unchanged. `required` names what the
- substrate must provide; naming it is not evidence that it is there, which `feasibility` reads.
- `c` is the session context its citations resolve in, and is not part of what the handoff
- dispatches; `source` is how a substrate outside it reaches what they cite. -/
+ /-- `ConductedMethod`: the method handed off and what it carries — each field as the relayed map
+ showed it, `source` aside, which its producer supplies; the substrate reads what is uncertain against this record. `plan` is the method
+ as the map the closing turn answered showed it, with what changed since that map, as the relayed
+ map showed it — on a relay, the person's words for what they settled and your draft for the
+ rest — and where its text and a recorded value differ, the recorded value governs. The substrate
+ executes it as the Rule "Handoff carries its obligations" names. Independent lines are handed
+ off so they do not see each other's results before those results combine. Every navigation block
+ this method leaves for a reader outside this session — `source`, and the one over the record a
+ later-session result is written to — is supplied by its producer from that record's own
+ identity, source session, and purpose; its grounding instruction directs the recipient to run
+ `/inquire` or equivalent grounding over the record and its cited sources, recover the retained
+ and entrusted judgments from the governing utterances, and keep an unsupported decision open
+ while independent work may continue. `pointer` is the incoming block, carried unchanged.
+ `required` names what the substrate must provide; naming it is not evidence that it is there,
+ which `feasibility` reads. `c` is the session context its citations resolve in, and is not part
+ of what the handoff dispatches; `source` is how a substrate outside it reaches what they cite.
+ -/
structure ConductedMethod (P : Type) (c : Context P) where
plan : Method
placement : String
record : List (Recorded c)
residual : List Coordinate
deferred : List Deferred
required : List String
feasibility : (k : String) → Occ (feasibilityCoord (P := P) k) c
lifetime : String
pointer : Option NavigationBlock
source : Option NavigationBlock
dissent : List String
- /-- The method the closing turn took, with everything it carries. -/
+ /-- The method the closing turn took, with everything it carries, read on the same context the
+ relayed map is drawn from. -/
def emitted (c : Context P) : ConductedMethod P c :=
{ plan := draft c
placement := placement c
record := record c
residual := residual c
deferred := deferred c
required := required c
feasibility := feasibility c
lifetime := lifetime c
pointer := pointer c
source := source c
dissent := dissent c }
- /-- `conducted c trace`: the person took the method shown in `c`, covered; `relayed c trace`: at
- the run's start, the person's words in `c` already settled it. `trace` is the conduct trace
- presented before the dispatch, and the method handed off is `emitted c`. -/
+ /-- `conducted c map`: the person took the method shown in `c`; `relayed c map`: at the run's
+ start, the person's words in `c` already settled it. `map` is the map relayed before the
+ dispatch in the same turn, and the method handed off is `emitted c`, carrying what that map
+ showed. -/
inductive Outcome (P : Type)
- | conducted (c : Context P) (trace : Response P)
- | relayed (c : Context P) (trace : Response P)
+ | conducted (c : Context P) (map : Response P)
+ | relayed (c : Context P) (map : Response P)
/-- the partial record; nothing is handed off -/
| withdrawn (r : Closed P)
| holding (c : Context P)
/-! ── WP-BINDING ──
bind(WP) = explicit_arg ∪ colocated_expr ∪ prev_user_turn ∪ ai_identified_prospect
Priority: explicit_arg > colocated_expr > prev_user_turn > ai_identified_prospect
/conduct "text" → WP = "text"
/conduct (alone) → WP = the work prospect under discussion
"how should I approach..." → WP = the work named before the trigger
AI-detected trigger → WP = the multi-move prospect AI identified (Hybrid: the person
reads it as the map's first line and corrects it there)
`pointer` is read alongside WP: a navigation block the context holds, a sibling protocol's
emitted block included. A prospect is what someone states; a pointer is what the session holds.
-/
/-! ── 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. Each utterance is
fused; one that bears on the run and does not withdraw is then observed (`.groundPointer`,
`.inventory`): what the pointer's record returns and the loaded inventory enter the context before
the presentation they inform, and an utterance about other work, or a withdrawal, triggers no
reading. `respond` is the next map (`.map`, then `.mapGate`), or, when the run closes on a taking
- — or, at `start`, on a relay — the conduct trace presented before `emitted` is handed off
- (`.relay` where it relays, `.converge`, then `.handoff`); a withdrawal is reported by `.withdraw`
+ — or, at `start`, on a relay — the map relayed before `emitted` is handed off in the same turn
+ (`.relay`, then `.handoff`); a taking closes whatever the same turn changed, which the relayed
+ map's ledger shows; a withdrawal is reported by `.withdraw`
and hands nothing off; `session` is the session's own answer to an utterance about other work,
which stays in the context without being a gate of this run.
-/
open Classical in
def conduct (respond session : Context P → Response P) :
Context P → List (Utterance P) → Outcome P
| c, [] => .holding c
| c, u :: us =>
let c₀ := fuse c u
if ¬ Reaches c₀ then conduct respond session (c₀ ++ [(session c₀).val]) us
else if isFilled (withdrawal c₀) = true then .withdrawn (closed c₀)
else
let c' := observe c₀
- if isFilled (resolution c') = true ∧ Covered c' then .conducted c' (respond c')
+ if isFilled (resolution c') = true then .conducted c' (respond c')
else conduct respond session (c' ++ [(respond c').val]) us
/-- The run opens on its first map, unless the person's words already settle the method. -/
def start (respond session : Context P → Response P) (c : Context P)
(us : List (Utterance P)) : Outcome P :=
let c₁ := observe c
if isFilled (relay c₁) = true then .relayed c₁ (respond c₁)
else conduct respond session (c₁ ++ [(respond c₁).val]) us
/-! ── LOOP ──
Every map re-reads the whole context; nothing counts rounds, and no earlier answer is held apart
from what later ones say. Each map is what `.map` names. No round cap: each map is dialogue.
After a handoff, re-entry is as the Rule "Re-entry" says.
-/
/-! ── CONVERGENCE ──
- conducted(WP): the method handed off on the person's covered taking, or relayed at the start on
- their words, after the conduct trace reached them. Convergence evidence, before the dispatch: what
- the closing turn itself changed, as a ledger — none on a relay at the start; the method as it
- will be handed off; each coordinate the person holds — a direction, presence, or horizon they
- fixed among them → what stands on it, in the words of the turn that set it or of the proposal as
- it was shown → who proposed it and how it stood, beside the coordinates still open; the
- substrate placement and the lifetime, marked as your inference where the person's coordinates
- leave them open; the deferred decisions, each marked as returning to the person or as covered by
- the recorded grant it names; what the method needs, each observed or unconfirmed; the
- navigation block `source` carries, or that there is none; and the dissent attached to the
- closure. Withdrawal keeps its partial record and hands nothing off. Demonstrated, not asserted.
+ conducted(WP): the method handed off on the person's taking, or relayed at the start on their words.
+ The convergence evidence is the map as it will be handed off, read on the context as it now stands
+ and presented once more as a relay in the closing turn — with the change ledger since the map the
+ person answered, where there was one, and any tally derived from the rows actually shown — then the
+ handoff in the same turn without waiting; the handoff carries what that map showed. Withdrawal
+ keeps its partial record and hands nothing off. 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 | groundPointer | inventory | readAnswer | draft | place | map | mapGate | withdraw
| relay | converge | handoff
def grounding : Op → Annot × String
- | .groundPointer => (.observe, "record read, artifact read: while the context holds a navigation block, follow its dereference instruction at its locator — the record it names, within the session it names — and run its grounding instruction; what the record returns enters the context before the map it informs, and nothing read here is copied onto the method; a pointer that does not resolve is named on the map with what was tried")
- | .inventory => (.observe, "artifact read, environment run: what the loaded environment actually answers with — its agents, skills, sessions, and tools — observed for what the method needs, before the map that shows it")
+ | .groundPointer => (.observe, "record read, artifact read: while the context holds a navigation block, follow its dereference instruction at its locator — the record it names, within the session it names — and run its grounding instruction; what the record returns enters the context before the presentation it informs, and nothing read here is copied onto the method; a pointer that does not resolve is named on the map with what was tried")
+ | .inventory => (.observe, "artifact read, environment run: what the loaded environment actually answers with — its agents, skills, sessions, and tools — observed for what the method needs, before the presentation that shows it")
| .readAnswer => (.sense, "Internal analysis: whether the latest utterance bears on this run, and what it does there — the coordinates it makes stand, a grant or a direction given outside the map, a taking, a withdrawal — read whole against the fused context as it now stands, whatever form it takes")
| .draft => (.sense, "Internal analysis: the whole method drafted from the context, as precisely as reaching the goal is worth — the lines of work and how they order, see each other, combine, stop, and where their results go — around every value the person set, with the deferred decisions, what the method needs, and its lifetime")
| .place => (.sense, "Internal analysis: who runs each line, where, and whether the person will be present, inferred from the tools the running harness describes and the accumulated context, bounded by any direction the person gave")
- | .map => (.interaction .extension, "the whole map on one sheet, which is the full state taking it as is would take: the lines of work as a graph the host can render, each line a node with its id and short everyday name in place, order and joins as its edges — an indented outline naming what each line follows only where no graph renders — each line's id and its order in the graph's source held from turn to turn, the drawn layout being the renderer's, so the change ledger is what lets the person check a change; what the method leaves uncovered; the substrate placement marked as your inference, following any direction or presence the person fixed, which shows among their coordinates; each coordinate the person holds, marked theirs, granted (a value of yours standing under their grant), or the draft's, a draft value with its ground and the alternative that most changes the plan; what the method needs, each observed or unconfirmed, and each act it needs that falls outside the grant or whose place inside it is unclear; the lifetime of its grants and readings, the draft's, following any horizon the person gave, which shows among their coordinates; the deferred decisions, each marked as returning to the person or as covered by the recorded grant it names; where the person will not be present, the authority the method would need, presented before they leave, with what must be decided before they leave set apart from what can wait; your contrary grounds; after an answer, the change ledger — the person's edits first, then each value re-filled because of them, pointing to the edit that caused it and marked a necessary consequence or your proposal, then what changed for any other reason — a new observation, your own re-draft — a removed line or replaced value kept with what it was, a value the person took before, or a granted value, that a change now alters flagged, and a person's value whose reach a change left unclear named with what it may reach and left open")
- | .mapGate => (.interaction .constitution, "what the map got wrong, anywhere on it — or take the method as shown, or withdraw; silence holds and takes nothing")
+ | .map => (.interaction .extension, "the whole map on one sheet, which is the full state taking it as is would take: the lines of work as a graph the host can render, each line a node with its id and short everyday name in place, order and joins as its edges — an indented outline naming what each line follows only where no graph renders — each line's id and its order in the graph's source held from turn to turn, the drawn layout being the renderer's, so the change ledger is what lets the person check a change; what the method leaves uncovered; the substrate placement marked as your inference, following any direction or presence the person fixed; what the method needs, each observed or unconfirmed, and each act it needs that falls outside the grant or whose place inside it is unclear; the lifetime of its grants and readings, the draft's, following any horizon the person gave; the deferred decisions, each marked as returning to the person or as covered by the recorded grant it names; where the person will not be present, the authority the method would need, presented before they leave, with what must be decided before they leave set apart from what can come back at the end; your contrary grounds; after an answer, the change ledger — the person's edits first, then each value re-filled because of them, then what changed for any other reason — a new observation, your own re-draft — a removed line or replaced value kept with what it was, a value the person took before, or a granted value, that a change now alters flagged, and a person's value whose reach a change left unclear named with what it may reach and left open")
+ | .mapGate => (.interaction .constitution, "what the map got wrong, anywhere on it — or take the method, as shown or with what the same words change; silence holds and takes nothing")
| .withdraw => (.interaction .extension, "at the person's word: what you took as withdrawn, and the partial record — the values that stand with who proposed each and how it stood, what is open, the deferred decisions, and your contrary grounds; nothing is handed off")
- | .relay => (.interaction .extension, "at the run's start, where the person's words already settle the method: the method — their words for what they settled, citing them, and your draft for the rest; then the conduct trace")
- | .converge => (.interaction .extension, "the convergence evidence CONVERGENCE names, before the dispatch")
- | .handoff => (.dispatch, "delegate: after the conduct trace, the ConductedMethod handed to the substrate, which executes it — its fields, never the session context its citations resolve in; the substrate returns to the person as the Rule \"Handoff carries its obligations\" names; an incoming pointer rides the method unchanged while the record it names stays where its locator names; then this run ends")
+ | .relay | .converge => (.interaction .extension, "the map, presented as a relay where the person's words settle the method — at the start, or by a taking — before the dispatch in the same turn")
+ | .handoff => (.dispatch, "delegate: after the relayed map, in the same turn, the ConductedMethod handed to the substrate, which executes it; the record an incoming pointer names stays where its locator names; then this run ends")
/-- The operation an outcome hands off through: a conducted or relayed run hands `emitted` to the
- substrate by `.handoff`, after the conduct trace; a withdrawal or a holding hands nothing off. -/
+ substrate by `.handoff`, after the relayed map; a withdrawal or a holding hands nothing off. -/
def handedOffBy : Outcome P → Option Op
| .conducted _ _ => some .handoff
| .relayed _ _ => some .handoff
| _ => none
/-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Dimension resolution emergent via session context.
-/
end
end Hyphegesis
```
## Mode Activation
- `/conduct` is directly invocable: the invocation declares the deficit, and the first map shows the method as drafted — the person may take it at once — unless the invocation's own words already settle it as the Rule "Conduction warrant" says, where it relays. AI-guided activation requires work with several lines of thinking whose order, independence, combination, stopping point, or destination is not obvious; scale and budget alone do not warrant it. Conduct the method before beginning its object-level work, while retaining loaded safety boundaries, capability restrictions, and explicit user instructions.
+ `/conduct` is directly invocable: the invocation declares the deficit, and the first map shows the method as drafted — the person may take it at once — unless the invocation's own words already settle it as `RelaySupported` reads them, where it relays. AI-guided activation requires work with several lines of thinking whose order, independence, combination, stopping point, or destination is not obvious; scale and budget alone do not warrant it. Conduct the method before beginning its object-level work, while retaining loaded safety boundaries, capability restrictions, and explicit user instructions.
When `/ground` reads an abstraction against its own instances and summarizes that reading as a split into rival groups — a summary of its reading, not a verdict it computes — read `references/decompose-recovery.md` before conducting the per-group work.
## Protocol
### User-facing realization
- Present the map as TOOL GROUNDING's `.map` entry names it, then `.mapGate`, and yield the turn. The map's first line says what the work is for and what it hands off. Prior-session recall indices may seed the lines but never settle them. Keep labels short, since display width is not character count and a column padded by counting characters breaks.
+ The map's first line says what the work is for and what it hands off. Prior-session recall indices may seed the lines but never settle them. Keep labels short, since display width is not character count and a column padded by counting characters breaks.
## Rules
- - **Conduction warrant**: Invoking `/conduct` declares the deficit; do not judge it away. Where you read that the work needs no conducting, show it on the map as a contrary ground; the person decides. Relay only at the start, where the person's own words already settle the method — their grant's horizon included where they give a grant — and you hold no contrary ground, and, for a person who will not be present, the way back to them is not unconfirmed; never on a run you opened, before its first map. Otherwise draw the map; once a map is shown, the method closes on a taking. Hyphegesis never conducts itself.
- - **Recognition over Recall**: Present the whole method on one map with differential futures and yield at every Constitution interaction, so the person recognizes the method instead of composing it.
- - **Round composition**: Use everyday language, place each judgment beside its evidence and next-move implication, and keep analytical context before the gate. Read `references/round-composition.md` when terminology or wording must persist, content belongs to another turn or trace, or placement relative to the gate is in question.
- - **Map precision**: Draw the map only as precisely as reaching the goal is worth; where trying is cheap and can be undone, a coarse map run once and checked against its use may be the method.
- - **Substrate placement is inferred**: Infer who runs each line, where, and whether the person will be present from the tools the running harness describes and the accumulated context; show it as your inference and keep the person's involvement to the broad direction; where their words fix a direction, whether they will be present, or a horizon, that stands as their constraint, and placement and lifetime follow it. A tool description grounds no verdict about what is reachable. Where the person will not be present, present before they leave the authority the method would need, and separate what must be decided before they leave from what can wait.
- - **Person's coordinates**: When to stop, how lines combine, where results go, the constraints in force, and the authority entrusted with its limits stand only by the person's words, read again against the context as it now stands. Read authority as a broad direction; where an act falls outside it or its place inside it is unclear, the person sees it before the act — as a contrary ground on the map, or after handoff as the Rule "Handoff carries its obligations" names.
- - **Map as a graph**: Draw the lines of work as a graph the host can render, each line's id and order held in its source; an indented outline only where no graph renders.
- - **Map change shown**: After every answer, show what changed as a ledger under the current map — the person's edits first, then each re-drafted value pointing to the edit that caused it, marked necessary consequence or proposal, then what changed for any other reason, a removed line or replaced value kept with what it was — flag a previously taken or granted value the change alters, and name a person's value whose reach the change left unclear, leaving it open.
- - **Adoption covered**: Take the method only on the person's taking over a map that showed everything taken with who proposed it and whether it is theirs, granted, or the draft's, its ground, whether each thing it needs was observed — unconfirmed where nothing did — and your contrary grounds. Nothing observed after the taking turn changes what it took; where it does, draw the map again. An open coordinate stays open; it is never adopted by default.
- - **Handoff carries its obligations**: Hand off the method with what `ConductedMethod` carries, then stop: independent lines kept apart until they combine, and every navigation block left for another session supplied by its producer with its grounding instruction. The substrate returns to the person with one consolidated summary of every line's results when the method has run. Mid-run, the returns this method originates are: a deferred decision marked for them; a coordinate left open, whose draft value in the plan is not acted on; authority for an act outside the grant, or whose place inside it the recorded value leaves unclear and the person's governing turns — in this session or through `source` — cannot settle, or that the lifetime no longer covers; a finding beyond the direction the person gave; what only the person can supply where nothing anticipated it — a secret or credential, a runtime error it cannot resolve, a deployment handed to runtime; and a contrary ground of the dissent, raised again where execution brings evidence for it before a dependent step that cannot be undone, which waits for the person. Each names what it needs, before the work it binds. A line that runs another protocol keeps that protocol's own gates, which return to the person as its contract says. Silence at any return holds; nothing is selected for the person.
- - **Re-entry**: After a handoff, a later utterance that changes the method's direction opens a new run over the accumulated context, where what stood is read again, and that run's plan names the method it replaces; stopping what still runs is the substrate's. A question about status reopens nothing; an answer at a return the substrate made goes to that return. A withdrawn run is not reopened this way: a person who wants it again invokes `/conduct`, and the draft is drawn from the accumulated context.
- - **`/apportion` seam**: Treat an incoming plan as a checked navigation pointer, not an import: dereference it, run the grounding instruction it carries against the current work, and carry the block unchanged.
- - **Convergence evidence**: Before dispatch, demonstrate what CONVERGENCE names; derive any tally from the rows actually shown.
+ - **Conduction warrant**: Hyphegesis never conducts itself.
+ - **Round composition**: Use everyday language, place each judgment beside its evidence and next-move implication, and keep analytical context before the gate. Read `references/round-composition.md` when terminology or wording must persist, content belongs to another turn, or placement relative to the gate is in question.
+ - **Person's coordinates**: Read the authority the person entrusts as a broad direction; where an act falls outside it or its place inside it is unclear, the person sees it as a contrary ground before the handoff, on the map; after the handoff, it comes back as the Rule "Handoff carries its obligations" names.
+ - **Handoff carries its obligations**: The substrate runs what does not rest on the person without waiting for them and, when the method has run, returns to them once with every line's results; what rests on the person — a step that cannot be undone, where a contrary ground the relayed map carried, or one execution brings evidence for, bears on it, among them — comes back in that return with what did not proceed because of it, and nothing is decided for them.
+ - **Re-entry**: After a handoff, a later utterance that changes the method's direction opens a new run over the accumulated context, where what stood is read again, and that run's plan names the method it replaces; stopping what still runs is the substrate's. A question about status reopens nothing; an answer to what came back goes to it. A withdrawn run is not reopened this way: a person who wants it again invokes `/conduct`, and the draft is drawn from the accumulated context.
- **Form feedback**: Derive each round's density from the current request and carry an explicit form instruction until countermanded. Change the form directly; preserve content, wording, order, cadence, and turn boundaries fixed elsewhere, stating what changed and any overlapping constraint that remains.
## Adversarial Guards
- **object-control-conflation**: Decompose transforms abstractions; the conduct method owns its ordering, focus, lifetime, state, and recursion.
- **cross-span-absorption**: A result crossing into a later session declares its record and externalization only; portability auditing and the later session's cognition stay with the receiving session.