ideate · diff
git:20260925.27d5e91 to git:20260926.252fa79
437 added, 246 removed. Audit A to A.
---
name: ideate
- description: "Widen an empty or prematurely converged idea field; reads only the invocation. Type: (CandidateFieldUnderexpanded, User, DIVERGE, IdeationRequest) → DiverseCandidateField"
+ description: "Widen an empty or prematurely converged idea field in width and depth; reads your words and what you name. Type: (CandidateFieldUnderexpanded, User, DIVERGE, IdeationRequest) → DiverseCandidateField"
---
# Heuresis Protocol
- Resolve an underexpanded candidate field through frame-parallel divergent generation, without ever eliminating, ranking, or selecting among the candidates it produces. Type: `(CandidateFieldUnderexpanded, User, DIVERGE, IdeationRequest) → DiverseCandidateField`.
+ Resolve an underexpanded candidate field through frame-parallel divergent generation, widening it in width and in depth, without ever eliminating, ranking, or selecting among the candidates it produces. Type: `(CandidateFieldUnderexpanded, User, DIVERGE, IdeationRequest) → DiverseCandidateField`.
## Definition
- **Heuresis** (εὕρεσις): the act of finding or discovering — a dialogical act of widening a candidate field that is empty or has prematurely converged, before any selection is made. Divergent and convergent thinking are distinct cognitive operations (Runco & Acar, 2012), and no protocol in this catalog carries a typed guarantee to generate the object-level alternative set itself — heuresis sits at the point where the candidate field itself is thin. On a blank entry, heuresis opens an abstract frame map before showing any concrete idea — early concrete examples measurably narrow independent generation (Wadinambiarachchi et al., 2024), and ideating before seeing material preserves ownership and diversity that seeing it first does not (Qin et al., 2025). Generation is frame-parallel and never eliminates, ranks, or scores: selection is a downstream act, out of this protocol's scope.
+ **Heuresis** (εὕρεσις): the act of finding or discovering — a dialogical act of widening a candidate field that is empty or has prematurely converged, before any selection is made. Divergent and convergent thinking are distinct cognitive operations (Runco & Acar, 2012), and no protocol in this catalog carries a typed guarantee to generate the object-level alternative set itself — heuresis sits at the point where the candidate field itself is thin. On a blank entry, heuresis opens an abstract frame map before showing any concrete idea — early concrete examples measurably narrow independent generation (Wadinambiarachchi et al., 2024), and ideating before seeing a model's ideas preserves ownership and yields ideas less similar to the model's own (Qin et al., 2025). Generation is frame-parallel and never eliminates, ranks, or scores: selection is a downstream act, out of this protocol's scope. The field grows two ways — a new frame widens it, a branch dug under an open frame or candidate deepens it — and every round redraws the whole field as one map, so where the person stops is a checkpoint a later run can resume from.
- ```
- ── FLOW ──
- Heuresis(U) → bind(U) → classify_entry(U) → Entry →
- [Entry = Blank] derive_frames(topic) → Qframes(frame_map) → Stop → FrameSelection →
- [FrameSelection = Open(F_selected)] generate(∥ F_selected) → Round₁
- [FrameSelection = Stop] → EarlyExit
- [Entry = Seeded(seeds)] derive_frames(seeds, topic) → generate(∥ frames; seeds fold in under their origin — utterance fragments as User) → Round₁
- present(Round) → Qround → Stop → D →
- [D = Continue(frames)] shape_frames(frames)? → generate(∥ frames) → Round → present → Qround (loop)
- [D = Stop] assemble(Λ) → DiverseCandidateField (Λ.candidates ≠ ∅) | EarlyExit (Λ.candidates = ∅)
- -- chain note: when U names a ChainRef (a prior protocol's output), its material folds in as seeds at classify_entry —
- -- origin preserved when already tagged (a chained DiverseCandidateField), origin=User when untagged (collection
- -- output, utterance fragments); a deliberate substrate-first choice the user made, documented as a trade-off (`Chain semantics`)
- -- park note: a deepen request at any Qround (wanting more on an already-open frame) parks into Λ.parked — it never
- -- re-opens a frame mid-loop; parked follow-ups are declared at either terminal for post-protocol chaining
- -- signal note: Phase 0 also extracts Signal(s) — concerns, weaknesses, or requirements present in the same bound
- -- utterance + named ChainRef material — tagged by source (Utterance or Chain); coverage (unaddressed(Λ)) is
- -- recomputed each round from Λ.candidates, never separately stored, and never a score, elimination reason, or
- -- ranking signal
+ ```lean
+ /-!
+ How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is
+ written for: you read it, and by inference over the context you settle each element it leaves
+ open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from
+ the material in front of you; its doc comment says what you judge there, and nothing in this
+ block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract. A
+ `theorem` line inside a doc comment states a consequence the contract already has; it is proved
+ outside this block and asks nothing further of you.
+ -/
- ── MORPHISM ──
+ /-! ── FLOW ──
+ Heuresis(U) → start(c) → ideate(c, utterances), where c is the fused session context:
+ start: a record outside the session the request names is read → the classification relay →
+ Blank: the frame map, abstract frames and no concrete candidate → gate
+ Seeded: a first pass → the map → gate
+ next utterance u: c' := fuse(c, u), then any record outside the session u names, read →
+ the person's closing, read from c' —
+ stop: candidates in c' → DiverseCandidateField | none → EarlyExit
+ withdraw → withdrawn · a protocol they name → routed
+ none: the frames the answer opens — some: a pass over them → the map → gate
+ none: the gate again
+ no utterance: the gate holds; nothing is assembled
+ -/
+
+ /-! ── MORPHISM ──
IdeationRequest
- → bind(utterance) -- read only the invocation utterance + any explicitly named chain reference
- → classify_entry(utterance) -- Blank | Seeded(seeds); zero entry questions — inferred, never asked; a named
- -- ChainRef's material folds in here as seeds (origin preserved when already
- -- tagged, origin=User otherwise), so a ChainRef-bearing
- -- entry classifies Seeded even on a bare-topic utterance
- → derive_frames(Entry) -- candidate GenerationFrames — the registry later rounds progressively open
- → select_frames(frames) -- Blank only: Cognitive Partnership Move (Constitution) — frame map BEFORE any concrete candidate
- → generate(∥ open frames) -- parallel candidate production; no elimination, no ranking, no scoring
- → present(Round) -- relay: candidates by frame + explored/unexplored declaration + unaddressed
- -- signals when any exist
- → continue_or_stop(Round) -- user constitutive judgment; Stop available at every round AND before the first one;
- -- a deepen request parks (relay) rather than continuing — the loop only widens
- → assemble(field) -- the surviving field entire under the bound topic: every candidate origin- and frame-tagged, parked
- -- follow-ups and unaddressed signals declared, nothing dropped
- → DiverseCandidateField -- happy-path terminal; the zero-candidate stop path exits as EarlyExit (FLOW)
- requires: candidate_field_underexpanded(U) -- runtime checkpoint (Phase 0); direct /ideate invocation satisfies it
+ → DiverseCandidateField -- the field the person bounded, every candidate under its frame or branch with its origin
+ requires: candidate_field_underexpanded(U) -- direct /ideate invocation satisfies it
deficit: CandidateFieldUnderexpanded -- activation precondition (Layer 1)
- preserves: seed_provenance(U) -- every seed keeps the origin it folded in with (User for the user's own
- -- fragments, an already-tagged chain origin as-is) through every later
- -- round; never relabeled
- invariant: Divergence over Selection -- generation never eliminates, ranks, or converges; selection is outside this protocol
+ preserves: seed_provenance(U) -- every seed and candidate keeps the origin of the material it came from; naming material is adoption, recorded apart; never relabeled
+ invariant: the person closes -- only their Stop, withdrawal, or a protocol they name ends the run; a pick among candidates, a judgment, or a correction does not
+ invariant: frame map first -- on a Blank entry no concrete candidate precedes the person's choice of frames
+ invariant: Divergence over Selection -- nothing is eliminated, ranked, scored, or chosen; selection is outside this protocol
+ invariant: width and depth both widen -- a new frame or a branch under an open frame or candidate; the map shows each branch's place
+ invariant: dissent rides the field -- unaddressed signals, unexplored frames, and your contrary grounds stand before every gate and in the result
+ -/
- ── TYPES ──
- U = IdeationRequest: the invocation utterance, read as-is — a natural-language topic, optional idea fragments, and an
- optional explicit reference to a prior collection protocol's output
- -- Input type: the morphism reads only the bound utterance plus an explicitly named prior-output reference — a
- -- bare invocation binds the immediately preceding user message AS the utterance (U-BINDING: a one-turn
- -- binding rule, still the user's own words); beyond that binding it never scans the wider session, codebase,
- -- or rules (Euporia's reverse-trace territory, not this protocol's)
- Entry = Blank -- utterance carries a topic only — no idea fragments, no named ChainRef
- | Seeded(Set(Seed)) -- utterance carries idea fragments and/or names a ChainRef; both sources
- -- fold in as seeds at classify_entry — utterance fragments as origin=User, chained material under its
- -- existing origin tag when it carries one (origin=User only when untagged)
- -- coproduct: Blank and Seeded take DIFFERENT phase paths (frame-first gate vs. expand-first) — behavioral
- -- branching per the structural convention (natural-language definitions are for uniform-processing inputs only)
- Seed = { content: String, origin ∈ {User, AI} } -- a pre-frame fragment; origin=User for utterance-borne fragments and
- -- untagged chained material, while chained material already carrying an origin tag keeps it (a chained
- -- DiverseCandidateField's candidates re-seed under their existing tags — an origin=AI candidate is never
- -- relabeled User by re-chaining). Carries no frame yet — frames do not exist until Phase 1 derives them
- -- (GenerationFrames are invocation-local, so a chained candidate's old frame is dropped, not preserved).
- -- Promoted to Candidate on the first generation pass, gaining the frame it lands under (origin travels unchanged)
- ExpansionWitness ∈ {Empty, NarrowAcrossFrames, PrematurelyConverged} ∪ Emergent(T)
- -- classification of WHY the candidate field is underexpanded; cited as Phase 0 relay basis. Sub-level to
- -- CandidateFieldUnderexpanded — NOT itself a top-level deficit, and never gates activation (User-initiated:
- -- direct /ideate invocation IS the activation)
- ChainRef = an explicit reference the utterance itself names to a prior collection protocol's output (e.g. "using what
- -- /inquire just gathered") -- the ONLY substrate-adjacent material this protocol reads; absent a named
- -- reference, no external material enters (Euporia boundary: no substrate scan, no reverse-traced coordinates)
- Signal = { content: String, source ∈ {Utterance, Chain} }
- -- a concern, weakness, or requirement present in the bound input only — extracted at Phase 0 alongside Entry,
- -- from the same bound utterance plus any explicitly named ChainRef material (never a wider scan); source
- -- records which of the two it came from. Never a quality score, elimination reason, or ranking signal
- -- (coverage — unaddressed(Λ), defined in CONVERGENCE — is a binary observation, not a judgment on any candidate)
- Candidate = { content: String, frame: Frame, origin ∈ {User, AI} }
- -- a generated idea item (raw material for divergence) — NOT a selection-ready alternative; carries no score,
- -- rank, or preference signal
- Frame = GenerationFrame { label: String, angle: String }
- -- a partition for parallel candidate production; distinct from an analytical
- -- lens — GenerationFrame carries no substrate_need, no per-perspective directive, no
- -- epistemic-perspective machinery. It organizes divergent generation only — derived at Phase 1, extended
- -- only for a user-named new angle, opened progressively across rounds (never re-derived by a bare
- -- continue) — and is never handed off as a framed inquiry object
- Round = { candidates: Set(Candidate) } -- one generation pass over F_open; F_open ∩ Λ.frames_open = ∅ is guaranteed at Phase 2,
- -- so each pass opens only not-yet-open frames (no mid-loop re-entry; a deepen wish parks instead)
- Qframes = frame-map presentation (Blank path only) — abstract frames, no concrete candidate yet [Tool: Constitution interaction]
- FrameSelection ∈ {Open(frames: Set(Frame)), Stop} -- Qframes answer type, Open/Stop differential-future rationale: read references/blank-entry.md
- Qround = per-round presentation: candidates by frame + explored/unexplored (direction contrast) + parked-so-far + unaddressed-signal declaration, then continuation ask, Continue always first and Stop always second [Tool: Constitution interaction]
- D = ContinuationAnswer ∈ {Continue(frames: Set(Frame)), Stop}
- -- Continue's frames are drawn from the declared unexplored set, or are user-named frames outside the declared
- -- set (free response — type-preserving materialization of Continue, not a new constructor). An already-open
- -- frame is NOT a Continue target: wanting more on it is a park request (→ ParkedFollowUp) — mid-loop
- -- deepening narrows the very field the loop exists to widen, so depth belongs to a later invocation chaining
- -- on the assembled field. A Continue naming no frames defaults to the declared unexplored set; when none
- -- remain, Continue has no default target — it materializes only with a user-named new angle (the gate's
- -- option text renders that state), and a Continue that materializes no target re-presents the round
- -- question rather than entering generation — an empty pass never runs. Stop is available at every Qround exactly as at
- -- Qframes — the user's stop is the constitutive act that bounds the field, not a pre-convergence abandonment
- ParkedFollowUp = { frame: Frame, note: Optional(String) }
- -- a mid-loop wish to go deeper on an already-open frame, captured as a typed follow-up instead of narrowing
- -- the live loop; held in Λ.parked and declared at either terminal — its durable externalization (a task
- -- record, an issue) is a host-side handoff after the protocol ends, so the loop itself stays side-effect-free
- DiverseCandidateField = {
- topic: String,
- candidates: Set(Candidate { content, frame, origin }),
- explored_frames: Set(Frame),
- unexplored_frames: Set(Frame),
- parked: Set(ParkedFollowUp),
- unaddressed_signals: Set(Signal)
- }
- -- "diverse" = frame-distributed, never scored/ranked/optimized; candidates ≠ ∅ always holds here (see EarlyExit
- -- for the empty case). unaddressed_signals holds only signals with no responding candidate at Stop — an
- -- addressed signal needs no field of its own: the candidates heuresis read as answering it are already in
- -- the field, and judging that fit is the consumer's own act at selection time.
- -- The field is the propagation contract: endpoint-neutral and complete for unfolding what it carries
- -- (an issue tracker, /preview, a chained /ideate) — topic carries the bound request; the one declared
- -- boundary is the full signal take/discard ledger, which stays in session text (see Known Limitations);
- -- endpoint-specific unfolding is downstream scope, not heuresis's
- EarlyExit = { frames_offered: Set(Frame), parked: Set(ParkedFollowUp), unaddressed_signals: Set(Signal) }
- -- the typed terminal for a stop (Qframes Stop, a Qround Stop after passes that produced nothing)
- -- that fires while no candidate exists — an empty
- -- field is never mislabeled DiverseCandidateField; frames_offered declares what was on the table even
- -- though nothing was generated, unaddressed_signals holds every signal extracted (none had a candidate to
- -- respond to it), and any parked follow-ups are declared alongside — nothing is silently dropped
+ namespace Heuresis
- ── U-BINDING ──
+ /-! ── GROUND ──
+ The session primitive this contract reads.
+ -/
+
+ inductive Origin | person | assistant | external | peer | injected | unknown
+ deriving DecidableEq
+
+ /-- A turn is who sent it and what it says. What the turn does — a statement, a request, an
+ instruction, a report of what was observed — is read from its content, never stored here. -/
+ structure Turn (P : Type) where
+ origin : Origin
+ content : P
+
+ abbrev Context (P : Type) := List (Turn P)
+
+ /-- An origin that may ground: the harness says who sent a turn, and that is all this admits on.
+ The assistant's own turns, injected text, and turns of unknown origin ground nothing. -/
+ def Grounding := {o : Origin // o ≠ .assistant ∧ o ≠ .injected ∧ o ≠ .unknown}
+
+ /-- Any turn a person sent, whatever it does. -/
+ def Utterance (P : Type) := {e : Turn P // e.origin = .person}
+ def Response (P : Type) := {e : Turn P // e.origin = .assistant}
+ /-- A turn from outside the conversation: what a tool or the environment returned, or a peer's
+ report. A person's account of what they observed is an utterance, read as such. -/
+ def Evidence (P : Type) := {e : Turn P // e.origin = .external ∨ e.origin = .peer}
+
+ def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]
+
+ /-- One turn of the context, with the origin it grounds on. -/
+ structure Cite {P : Type} (c : Context P) where
+ idx : Nat
+ lt : idx < c.length
+ src : Grounding
+ ok : (c[idx]'lt).origin = src.val
+
+ /-- `admits` reads only who sent the cited turn; `supports` is the model's reading of what that
+ turn says, including what it does — a statement, a request, a report of an observation. -/
+ structure Coord (P A : Type) where
+ admits : Grounding → Prop
+ supports : Context P → Turn P → A → Prop
+
+ /-- `open_` may carry a candidate citation whose support is still short. -/
+ inductive Occ {P A : Type} (q : Coord P A) (c : Context P)
+ | open_ (candidate : Option (Cite c))
+ | filled (a : A) (src : Cite c) (allowed : q.admits src.src)
+ (supported : q.supports c (c[src.idx]'src.lt) a)
+
+ /-!
+ theorem fuse_extends {P : Type} (c : Context P) (u : Utterance P) :
+ ∃ t, fuse c u = c ++ t
+
+ theorem cited_not_assistant {P : Type} {c : Context P} (s : Cite c) :
+ (c[s.idx]'s.lt).origin ≠ .assistant
+
+ theorem cited_not_injected {P : Type} {c : Context P} (s : Cite c) :
+ (c[s.idx]'s.lt).origin ≠ .injected
+ -/
+
+ /-- The same turn, cited from a longer context; what it supports is judged again against the
+ context that now stands. -/
+ def Cite.lift {P : Type} {c : Context P} (s : Cite c) (t : Context P) : Cite (c ++ t) :=
+ { idx := s.idx
+ lt := by have := s.lt; simp; omega
+ src := s.src
+ ok := by rw [List.getElem_append_left s.lt]; exact s.ok }
+
+ /-! ── TYPES ── -/
+
+ noncomputable section
+
+ variable {P : Type}
+
+ /-- `U`, `IdeationRequest`: the invocation utterance, read as it was said — a topic, optional idea
+ fragments, and optionally a chain reference that names material: a prior protocol's output in
+ the session, or a record outside it. A bare invocation binds the person's immediately
+ preceding message as the utterance. -/
+ abbrev IdeationRequest (P : Type) := Context P
+
+ /-- **Your reads**: when the latest of the person's turns — the bound request, or an answer at any
+ gate — names a record outside the session, such as an issue or a document, that record, read
+ by a tool. Nothing the person does not name is read, and nothing wider is scanned. Empty when
+ the turn names none. -/
+ axiom reference : Context P → List (Evidence P)
+
+ /-- **Your reading** of the bound request: its topic. -/
+ axiom topic : Context P → String
+
+ /-- A fragment the request brings before any frame holds it, and where it came from: `person` for
+ the person's own fragments. Material a named reference supplied keeps the origin it already
+ carries as a tag, or else the origin of the turn it was read from — `external` for a record a
+ tool read. Naming the reference is the person's adoption of that material; the adoption is
+ recorded apart from the origin and never written into it. -/
+ structure Seed where
+ content : String
+ origin : Origin
+
+ /-- `blank`: a topic only. `seeded`: idea fragments, named material, or both. The two take
+ different paths: the frame map first, or a first pass. -/
+ inductive Entry
+ | blank
+ | seeded (seeds : List Seed)
+
+ /-- **Your reading** of the bound request: which entry it is — inferred, never asked. The
+ classification relay states it with its basis, why the field reads thin, and the signals. -/
+ axiom entry : Context P → Entry
+
+ inductive SignalSource | utterance | chain
+
+ /-- A concern, weakness, or requirement the person holds, and whether it came from their words or
+ from named material. Never a quality score, an elimination reason, or a rank. -/
+ structure Signal where
+ content : String
+ source : SignalSource
+
+ /-- **Your reading**, from the context as it now stands: the concerns the bound request and named
+ material carry, and any the person voiced later in the run — a constraint added at a gate is a
+ signal from then on. Nothing is fixed at entry, and none is dropped while the person's words
+ still hold it. -/
+ axiom signals : Context P → List Signal
+
+ /-- A partition for parallel generation: a frame, or a branch dug under an open frame or under a
+ candidate, `parent` naming that frame's label or that candidate's content. It organizes
+ divergence only and is never handed off as a framed inquiry. -/
+ structure Frame where
+ label : String
+ angle : String
+ parent : Option String
+
+ /-- **Your record**, read from the context: the frames and branches registered — derived from the
+ entry, frames the person named at the frame map or at a round shaped into frames, and branches
+ under what the person asked to deepen. On Seeded, at least one, seed-anchored and novel, every
+ seed landing under one; on Blank, novel and abstract. When the request chains a field this
+ protocol assembled, that field's frames and branches carry over as it stood at its Stop.
+ Whether the person's words name a registered frame is read here. -/
+ axiom frames : Context P → List Frame
+
+ /-- **Your reading**: a pass has opened the frame. -/
+ axiom Opened : Context P → Frame → Bool
+
+ /-- The explored frames: the registered ones a pass opened, so none lies outside the register. -/
+ def explored (c : Context P) : List Frame := (frames c).filter (Opened c)
+
+ /-- A frame the person put out of scope, with the turn in which they did — its branches and
+ candidates go with it. -/
+ structure Exclusion (c : Context P) where
+ frame : Frame
+ request : Cite c
+ byPerson : request.src.val = .person
+
+ /-- **Your reading** of every exclusion in the person's turns, each citing the turn that made it.
+ A boundary the person states — "only this area" — reaches particular frames only once the
+ person takes that application; until then it stands in `proposedExclusions`. An excluded frame
+ is never deleted: it stays on the map marked out of scope with the turn quoted, and it is never
+ widened. -/
+ axiom excluded : (c : Context P) → List (Exclusion c)
+
+ /-- **Your reading**: frames you read as outside a boundary the person stated, shown on the map as
+ your proposal until the person takes it. -/
+ axiom proposedExclusions : Context P → List Frame
+
+ def Excluded (c : Context P) (f : Frame) : Prop := ∃ e ∈ excluded c, e.frame = f
+
+ def Unexplored (c : Context P) (f : Frame) : Prop :=
+ f ∈ frames c ∧ Opened c f = false ∧ ¬ Excluded c f
+
+ /-- A generated idea: raw material for divergence, not a selection-ready alternative. It carries
+ no score, rank, or preference. -/
+ structure Candidate where
+ content : String
+ frame : Frame
+ origin : Origin
+
+ /-- **Your record**: every candidate the passes produced, under the frame or branch it came from —
+ on a Seeded entry's first pass the seeds, each keeping its own origin, and every generated one
+ as `assistant`; a chained field's candidates under their own frames and origins; the items of
+ material the person names at a later turn under their frames, with their own origin —
+ `external` for a tool read — at the pass after they are read. Never removed, re-ranked, or
+ relabeled, an excluded frame's included. -/
+ axiom candidates : Context P → List Candidate
+
+ /-- **Your judgment**, remade at each presentation from the candidates and signals as they stand:
+ the candidate responds to the signal. Never stored as a mapping and never a score on the
+ candidate. Once the person stops, it stands as the presentation their Stop answered showed
+ it; no reading after the Stop changes what they closed on. -/
+ axiom Responds : Context P → Candidate → Signal → Prop
+
+ def Unaddressed (c : Context P) (s : Signal) : Prop :=
+ s ∈ signals c ∧ ¬ ∃ x ∈ candidates c, Responds c x s
+
+ /-- Something the person themselves set aside for later — a frame or branch they want to return
+ to after this run — with the turn in which they said so. -/
+ structure ParkedFollowUp (c : Context P) where
+ frame : Frame
+ note : Option String
+ request : Cite c
+ byPerson : request.src.val = .person
+
+ /-- **Your reading** of every deferral in the person's turns, each citing the turn that made it and
+ relayed with the request quoted. What the cited turn asks is your `supports` reading of it. A
+ request to deepen is not a deferral: it opens a branch. -/
+ axiom parked : (c : Context P) → List (ParkedFollowUp c)
+
+ /-- **Your judgment**: your grounds against stopping here or against the field as it stands — a
+ direction left unexplored that the topic points to, a signal no candidate answers, a branch
+ thinner than its siblings. Shown before every gate; never a recommendation to continue or to
+ stop, and never a rank on a candidate. -/
+ axiom dissent : Context P → List String
+
+ /-- **Your reading** of the latest answer: the frames the next pass opens — at the frame map, the
+ frames selected and any the person named, shaped into frames; at a round, the named unexplored
+ frames, a new angle shaped into frames, or a branch under an open frame or candidate the
+ person asked to deepen. An excluded frame is never among them. A continue that names nothing
+ takes every unexplored frame. On a
+ Seeded entry's first pass, how many derived frames to open is yours; the rest stay unexplored
+ and show as such. Empty when the answer opens nothing — a deferral alone, a question, a
+ correction, a pick among candidates, or a continue with nothing left to open. -/
+ axiom targets : Context P → List Frame
+
+ /-- How the person ends the run. -/
+ inductive Closing
+ /-- stop here: the field closes on what the map shows -/
+ | stop
+ /-- drop the ideation: nothing is assembled -/
+ | withdraw
+ /-- go on to the protocol the person names -/
+ | route (target : String)
+
+ /-- **Your judgment**: the cited turn closes the run this way, read against the context as it now
+ stands. A pick among candidates, a judgment on one, or a correction does not by itself take the
+ field; a stop is said of the field. -/
+ axiom ClosingSupported : Context P → Turn P → Closing → Prop
+
+ /-- Only the person closes. -/
+ def closeCoord : Coord P Closing :=
+ { admits := (·.val = .person), supports := ClosingSupported }
+
+ /-- **Your reading**: the person's closing; `open_` until one reaches it. -/
+ axiom closing : (c : Context P) → Occ (closeCoord (P := P)) c
+
+ def filledValue {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Option A
+ | .open_ _ => none
+ | .filled a .. => some a
+
+ /-- `DiverseCandidateField`, read from `context`: the topic, every candidate with its frame or
+ branch and its origin, the explored frames, the unexplored ones, the frames the person put out
+ of scope with their turns quoted, the parked follow-ups with their citations, the unaddressed
+ signals, and your contrary grounds (`dissent`).
+ Frame-distributed, never scored; complete for whatever unfolds it next, a later /ideate
+ resuming from it included. -/
+ structure DiverseCandidateField (P : Type) where
+ context : Context P
+ nonempty : (candidates context).isEmpty = false
+
+ /-- `EarlyExit`: a Stop while no candidate exists, read from `context` — the frames offered, those
+ the person put out of scope, the parked follow-ups, every signal, since no candidate answered
+ any, and your contrary grounds. -/
+ structure EarlyExit (P : Type) where
+ context : Context P
+ empty : (candidates context).isEmpty = true
+
+ inductive Outcome (P : Type)
+ | field (r : DiverseCandidateField P)
+ | early (r : EarlyExit P)
+ /-- the person dropped the ideation: nothing is assembled -/
+ | withdrawn (c : Context P)
+ /-- the person named another protocol: proceed to it, citing their words -/
+ | routed (target : String) (c : Context P)
+ | holding (c : Context P)
+
+ /-! ── U-BINDING ──
bind(U) = explicit_arg ∪ colocated_expr ∪ prev_user_turn ∪ chain_ref
Priority: explicit_arg > colocated_expr > prev_user_turn > chain_ref
- -- prev_user_turn binds only on a bare invocation: the immediately preceding user message BECOMES the utterance
- -- (one turn, the user's own words) — a binding rule for U, not a license to scan session history
- -- chain_ref, when named, folds its material in as seeds (origin preserved when tagged, User otherwise) — it never substitutes for the topic itself
+ /ideate "topic or fragments" → U = the argument
+ /ideate (alone) → U = the person's previous message; one turn, not a scan
+ "give me some ideas ... /ideate" → U = the text before the trigger
+ "using what /inquire just found, /ideate" → U also carries the named material; it folds in as
+ seeds under the origin it came with
+ "from issue ROO-12's comments, /ideate" → the named record is read by a tool and folds in the same way
+ A chain reference never stands in for the topic.
+ -/
- /ideate "topic or fragments" → U = "topic or fragments"
- /ideate (alone) → U = previous user message
- "give me some ideas ... /ideate" → U = text before trigger
- "using what /inquire just found, /ideate" → U also carries the named ChainRef; its material folds in as origin=User seeds (untagged collection output; a chained DiverseCandidateField would keep its candidates' own origin tags)
+ /-! ── MODE STATE ──
+ Λ is the fused context and nothing else; every reading above is taken from it. The map a round
+ draws is re-read from the context each time, never stored.
+ -/
- ── PHASE TRANSITIONS ──
- Phase 0: U → bind(U) → classify_entry(U) → Entry ⊗ ExpansionWitness; Λ.topic := topic(U); Λ.signals := extract_signals(U) -- silent; zero entry questions; topic(U) records the bound request in mode state, so assemble(Λ) has a formal source for the field's topic; extract_signals(U) reads the same bound utterance + named ChainRef only (`Euporia boundary — utterance-only input` boundary) and tags each Signal's source
- classify_relay(Entry, ExpansionWitness) → TextPresent+Proceed -- states the inferred entry + its basis + the extracted signals (source-tagged) before proceeding; relay, not a gate — every signal enters session text once, at extraction
- Phase 1: Entry → Λ.frames_candidate := derive_frames(Entry) -- registered into mode state at derivation, so the frames_open ⊆ frames_candidate invariant is checkable from the first pass
- [Entry = Blank] present(frame map) → Qframes → Stop → FrameSelection [Tool] -- read references/blank-entry.md
- [FrameSelection = Open(F_selected)] → Phase 2 with F_selected
- [FrameSelection = Stop] → EarlyExit(frames_offered := Λ.frames_candidate, parked := Λ.parked, unaddressed_signals := Λ.signals) -- stop before any candidate exists; Λ.parked is necessarily ∅ here (parks originate at Qround) — passed explicitly for uniform construction; every extracted signal is unaddressed since no candidate exists yet
- [Entry = Seeded(seeds)] → Phase 2 directly with Λ.frames_candidate (no gate — expand-first) -- read references/seeded-entry.md
- Phase 2: F_open → generate(∥ over F_open) → Round(candidates) -- no elimination, no ranking; on the first pass of a Seeded entry, seeds promote to Candidates under the frame each lands in, each keeping its seed origin (utterance fragments User); generated candidates carry origin=AI; F_open ∩ Λ.frames_open = ∅ (Phase 3 admits only unexplored or newly registered frames), so every pass opens genuinely new frames
- Λ.candidates := Λ.candidates ∪ Round.candidates, Λ.frames_open := Λ.frames_open ∪ F_open, Λ.rounds := append(Λ.rounds, Round) -- state absorbed BEFORE Phase 3 presents: every Qround guard (the Stop branches' Λ.candidates test) reads post-round state, never stale
- Phase 3: Round → present(Round: candidates by frame, explored_frames, unexplored_frames, parked so far, unaddressed(Λ)) → Qround → Stop → D [Tool]
- [park request — the response asks for more on an already-open frame] Λ.parked := Λ.parked ∪ {ParkedFollowUp(frame, note)} — relay the parking (extension); a response carrying only a park leaves the continuation question open, so Qround is re-presented with the park acknowledged
- [D = Continue(frames: F'), F' ≠ ∅, F' ⊆ frames_unexplored(Λ)] → Phase 2 with F' (open unexplored — no new derivation; an already-open frame is never a Continue target)
- [D = Continue(frames: F'), F' ⊄ Λ.frames_candidate] Fₙ := shape_frames(F' \ Λ.frames_candidate); Λ.frames_candidate := Λ.frames_candidate ∪ Fₙ → Phase 2 with (F' ∩ frames_unexplored(Λ)) ∪ Fₙ (user-named new angle — shape_frames shapes it into registered frames before generation, a distinct operation from Phase 1's derive_frames: its domain is Set(Frame), not Entry; type-preserving materialization of Continue; any already-open frame the response also named routes to the park branch, never back into F_open)
- -- a Continue naming no frames defaults F' := frames_unexplored(Λ); when none remain, Continue has no default target — it materializes only with a user-named new angle (the gate's option text renders that state), and a bare Continue never derives new frames
- [D = Continue(frames: ∅) — the default resolved to an empty set: no unexplored frame remains and no new angle was named] → re-present Qround with that state rendered — Continue materialized no target, so no generation pass runs (F' ≠ ∅ guards Phase 2 entry; an empty round never exists)
- [D = Stop, Λ.candidates ≠ ∅] → assemble(Λ) → DiverseCandidateField(topic := Λ.topic, candidates := Λ.candidates, explored_frames := Λ.frames_open, unexplored_frames := frames_unexplored(Λ), parked := Λ.parked, unaddressed_signals := unaddressed(Λ)) -- every field sourced from Λ; explored_frames is the chain-contract name of Λ.frames_open
- [D = Stop, Λ.candidates = ∅] → EarlyExit(frames_offered := Λ.frames_candidate, parked := Λ.parked, unaddressed_signals := Λ.signals) -- a completed pass can yield nothing; honest stop typing routes an empty field to EarlyExit, never DiverseCandidateField; with no candidates, every extracted signal is unaddressed
+ abbrev Mode (P : Type) := Context P
- ── LOOP ──
- Round cadence: Phase 2 (generate, ∥ over open frames) → Phase 3 (present + Qround). Before every Qround, heuresis
- evaluates four things: which signals remain unaddressed, how the explored and unexplored frames differ in direction
- (not just their labels), what continuing would cost to review, and what stopping would finalize and preserve — the
- evaluation is fixed every round, but what renders adapts to what carries decision-relevant content this round
- (empty or unchanged detail may compress), except unaddressed signals, which are always surfaced whenever any exist.
- A Continue answer triggers
- shape_frames only when the user names a wholly new angle (shaped into registered frames before generation); opening
- declared-unexplored frames returns directly to Phase 2 — then back to Phase 3. A deepen request never re-enters
- Phase 2 mid-loop: it parks (Λ.parked) for a later invocation chaining on the assembled field — depth is downstream,
- width is this loop's whole business.
- No fixed round count and no quota: heuresis tracks no target to converge toward; the loop continues until the user's own Stop.
- Novelty relay (optional, extension): at any Qround, heuresis MAY note as basis-cited context whether recent rounds read
- as producing candidates closer to earlier ones (novelty has not yet declined further, or has) — informational only,
- sits in the pre-gate text, describes state only, and never reorders the Continue/Stop options or blocks or discourages Stop.
- Continue until: DiverseCandidateField (user Stop with ≥1 candidate already generated) OR EarlyExit (Stop
- while no candidate exists — the Blank frame map declined, or a Stop
- after passes that produced nothing).
- Convergence evidence: at DiverseCandidateField, present the transformation trace — the bound topic, then for each
- opened frame, the candidates it produced with their origin tags, plus the declared unexplored frames, parked
- follow-ups, and unaddressed signals. At
- EarlyExit, present the frames that were derived and offered, none of which yielded a candidate, plus any parked
- follow-ups and unaddressed signals (every extracted signal, since none was addressed). Demonstrated, not asserted —
- and the trace materializes the full result type, nothing more, nothing less.
+ /-! ── PHASE TRANSITIONS ──
+ A round is one step of a structural recursion over the person's utterances. `relay` is the
+ classification relay: the entry, its basis, why the field reads thin, and the signals with their
+ sources. `generate` is one pass: candidates under each frame the pass opens (`targets`), in
+ parallel over the frames, with the seeds promoted on a Seeded entry's first pass, and no
+ elimination, ranking, or scoring. On Blank, `respond` first presents the frame map and the gate
+ before any pass.
+ -/
- ── CONVERGENCE ──
- resolved ≡ a Stop answer was returned at Qframes (FrameSelection = Stop; Blank path only) or at a Qround (D = Stop)
- -- an event predicate over the gate answers, not a field of Λ: the user's own Stop IS the completion predicate — not a separate judgment layered on
- top of an already-built object; this is what keeps termination-at-any-time from reading as pre-convergence abandonment
- unaddressed(Λ) = { s ∈ Λ.signals | no c ∈ Λ.candidates responds to s } -- derived, binary, source-traceable coverage
- observation, recomputed every round from current Λ.candidates — never a stored partition, and never a quality score,
- elimination reason, or ranking signal; a candidate "responding" to a signal is a semantic judgment heuresis makes at
- presentation time — a session-local reading remade from scratch each round (Λ.signals never shrinks, so a reading
- can reverse; nothing is sticky), never stored as a signal-to-candidate mapping, and never itself a score or rank on
- the candidate. The contract carries only the derived set as it stands at Stop — whether a candidate truly answers a
- signal is the consumer's own judgment at selection time, downstream of this protocol
- frames_unexplored(Λ) = Λ.frames_candidate \ Λ.frames_open -- derived each round; opening a frame removes it, so no frame is ever reported explored AND unexplored
- result equations:
- DiverseCandidateField ⇔ resolved ∧ Λ.candidates ≠ ∅
- EarlyExit ⇔ resolved ∧ Λ.candidates = ∅
- -- a typed terminal, never a DiverseCandidateField mislabeled empty; frames_offered and
- -- unaddressed_signals (every extracted signal, since none was addressed) declare what was
- -- on the table so nothing is silently dropped
- cleanup: not applicable — heuresis holds no side-effect state (no team spawned, no file artifact); the
- user_withdraw cleanup tier does not apply here — only Normal convergence (the user's own Stop) does.
- Parked follow-ups live in Λ and are declared at the terminal — their
- durable externalization (a task record, an issue) is a host-side handoff AFTER convergence, per the substrate
- boundary, so no cleanup obligation ever arises mid-loop
- framing readout: the surfaced state names the work in play (which frames are open, how many candidates so far, what
- remains unexplored, what is parked, what signals remain unaddressed) — never a completion tally against a target
- round count, since heuresis tracks no such target
+ def pass (generate respond : Context P → Response P) (c : Context P) : Context P :=
+ let c₁ := c ++ [(generate c).val]
+ c₁ ++ [(respond c₁).val]
- ── TOOL GROUNDING ──
+ /-- The person's Stop closes the field on the context as it then stands. -/
+ def assemble (c : Context P) : Outcome P :=
+ match h : (candidates c).isEmpty with
+ | true => .early ⟨c, h⟩
+ | false => .field ⟨c, h⟩
+
+ /-- The person's turn fused, then any record outside the session it names, read. -/
+ def receive (c : Context P) (u : Utterance P) : Context P :=
+ let c' := fuse c u
+ c' ++ (reference c').map (·.val)
+
+ /-- `respond` presents the map and ends at the gate. Every round, one map of the whole field: the
+ frames and the branches under them, the candidates under each with their origins, the
+ unexplored frames, the frames out of scope marked as such with the person's turn quoted, your
+ proposed exclusions marked as proposals, what is parked, every signal still unaddressed, and
+ your contrary grounds — with what this round added marked. The map is re-read from the context, never stored; when it
+ grows large it compresses to branches and counts while this round's additions show in full,
+ the density yours to judge. Then what continuing would cost to review and what stopping keeps,
+ and the gate: at a round, continue first and stop second; on a Blank entry's first
+ presentation, the frame map and its selector, before any candidate. -/
+ def ideate (generate respond : Context P → Response P) :
+ Context P → List (Utterance P) → Outcome P
+ | c, [] => .holding c
+ | c, u :: us =>
+ let c' := receive c u
+ match filledValue (closing c') with
+ | some .stop => assemble c'
+ | some .withdraw => .withdrawn c'
+ | some (.route t) => .routed t c'
+ | none =>
+ if (targets c').isEmpty then ideate generate respond (c' ++ [(respond c').val]) us
+ else ideate generate respond (pass generate respond c') us
+
+ def start (relay generate respond : Context P → Response P) (c : Context P)
+ (us : List (Utterance P)) : Outcome P :=
+ let c₀ := c ++ (reference c).map (·.val)
+ let c₁ := c₀ ++ [(relay c₀).val]
+ match entry c₁ with
+ | .blank => ideate generate respond (c₁ ++ [(respond c₁).val]) us
+ | .seeded _ => ideate generate respond (pass generate respond c₁) us
+
+ /-! ── LOOP ──
+ No fixed round count and no quota: nothing is tracked toward a target, and the loop goes on until
+ the person closes it. A basis-cited note on whether recent rounds read as closer to earlier ones
+ may sit before the gate; it describes state only and never reorders or discourages either answer.
+ -/
+
+ /-! ── CONVERGENCE ──
+ field: the person's Stop with candidates; early: their Stop with none; withdrawn: they dropped the
+ ideation; routed: they named the next protocol. Their Stop is the completion itself, not a judgment
+ layered on a built object, and it takes the field with the map's dissent in view.
+ Convergence evidence: at DiverseCandidateField, present the trace — the topic, then the map: every
+ registered frame and its branches, each marked explored or unexplored, with every candidate under
+ the frame it sits in and its origin, the frames out of scope marked as such with the person's
+ turn quoted, the parked follow-ups with the requests quoted, the unaddressed signals, and your
+ contrary grounds; at EarlyExit, the frames offered, those out of scope, the parked follow-ups,
+ every signal, and your contrary grounds.
+ Demonstrated, not asserted. Nothing is held beyond the context, so nothing needs cleanup; the
+ parked set's durable record is the host's after the protocol ends.
+ -/
+
+ /-! ── TOOL GROUNDING ── -/
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
- Phase 0 bind (sense) → Internal analysis (parse the invocation utterance + any explicitly named chain reference; no external tool, no substrate scan)
- Phase 0 classify_relay (extension) → TextPresent+Proceed (states the inferred Entry — Blank or Seeded — and its basis, quoting the utterance fragment, plus the extracted signals with their source tags; relay, not a gate — zero entry questions)
- Phase 0 extract_signals (sense) → Internal analysis (Signals — concerns, weaknesses, requirements — read from the same bound utterance + named ChainRef only, same `Euporia boundary — utterance-only input` boundary as bind; tagged Utterance or Chain by source; surfaced once via the classify_relay emission; feeds unaddressed(Λ) each round, never scored or ranked)
- Phase 1 derive_frames (sense) → Internal analysis (candidate GenerationFrames, registered as Λ.frames_candidate; seed-anchored + novel on Seeded, purely novel and abstract on Blank)
- Phase 3 shape_frames (sense) → Internal analysis (a user-named new angle shaped into registered GenerationFrames, extending Λ.frames_candidate — distinct from Phase 1's derive_frames: domain Set(Frame), not Entry)
- Phase 1 Qframes (constitution) → present (Blank path only; conditional: fires when Entry = Blank; multi-select frame map presented BEFORE any concrete candidate, plus the Stop path; read references/blank-entry.md before presenting — it carries the template and the Stop-branch rationale)
- Phase 2 generate (sense) → Internal generation (logical topology: parallel over open frames — no mandatory subagent dispatch; a host MAY realize this via isolated parallel agents when available, but heuresis's meaning is independent of that realization; no elimination, no ranking, no scoring)
- Phase 3 present (extension) → TextPresent+Proceed (round relay: candidates grouped by frame with origin tags, explored/unexplored frame declaration with direction contrast, unaddressed signals when any exist, plus the fixed four-part decision-delta evaluation; precedes the gate)
- Phase 3 Qround (constitution) → present (mandatory every round; fixed order Continue=1, Stop=2 at every presentation and re-presentation; Continue — open more unexplored or name a new frame — or Stop; a deepen request parks rather than continuing)
- Phase 3 park (extension) → Internal state update + TextPresent+Proceed (a request for more on an already-open frame parks as ParkedFollowUp — relay, basis: the user's own request quoted; declared at either terminal; durable externalization is a host-side handoff after the protocol ends)
- Λ (track) → Internal state update (topic records at Phase 0 bind; signals extracted at Phase 0 and fixed thereafter — never re-scanned, never removed; frames_candidate registers at Phase 1 and extends only on a user-named new angle; candidates, rounds, frames_open, parked accumulate; frames_unexplored(Λ) and unaddressed(Λ) are both derived — frames_candidate minus frames_open, and signals with no responding candidate, respectively — recomputed each round, never stored as a separate partition; a candidate is never removed or relabeled once tagged with origin)
- converge (extension) → TextPresent+Proceed (DiverseCandidateField: transformation trace — the bound topic + per opened frame, its candidates + declared unexplored frames + parked follow-ups + unaddressed signals; EarlyExit: the frames offered, none of which yielded a candidate, + parked follow-ups + unaddressed signals; either way the parked set's durable externalization hands off to the host after the trace)
- Seam transition to declared next protocol (extension) → TextPresent+Proceed (fires at deactivation, after converge, at either terminal — DiverseCandidateField or EarlyExit: a user-declared chain naming the next protocol settles the next move — proceed directly to it, citing that settling source. This protocol declares no wired outbound continuation edge — the field is endpoint-neutral by contract (an issue tracker, /preview, a chained /ideate), so the second trigger is vacuously absent. What crosses the seam is the assembled terminal whole, with every origin tag, parked follow-up, and unaddressed signal intact — the seam never selects, ranks, or trims among candidates (Divergence over Selection holds through the handoff; selection is the next protocol's act). The seam is the outbound counterpart of `Chain semantics`: a chained /ideate re-reads the field as a ChainRef under the inbound rule, and any other next protocol reads it as its own input. Parked follow-ups are NOT routed here — their durable externalization stays the host-side handoff `converge` declares, unless the user's chain names a later /ideate on them. Every Constitution gate inside this protocol and inside the next protocol fires unchanged — the seam exists only after the user's own Stop and never pre-empts it)
- ── MODE STATE ──
- Λ = { phase: Phase, entry: Option(Entry),
- topic: Option(String), -- the bound request, recorded at Phase 0; assemble(Λ) carries it into
- -- DiverseCandidateField so the chain contract needs no source outside Λ
- chain_ref: Option(ChainRef),
- signals: Set(Signal), -- extracted at Phase 0 from the same bound utterance + named ChainRef only;
- -- fixed thereafter — never re-scanned from a wider source, never removed; unaddressed(Λ)
- -- (defined in CONVERGENCE) derives from this set and Λ.candidates, not
- -- stored separately
- frames_candidate: Set(Frame),
- frames_open: Set(Frame), -- invariant: frames_open ⊆ frames_candidate — every opened frame is registered
- -- before generation (the Phase 3 new-angle branch registers Fₙ first);
- -- assembled as explored_frames in DiverseCandidateField
- candidates: Set(Candidate), -- accumulate-only across rounds; origin never relabeled once tagged
- rounds: List(Round),
- parked: Set(ParkedFollowUp), -- accumulate-only; deepen wishes captured mid-loop, declared at either terminal
- active: Bool, cause_tag: String }
- Phase ∈ {0, 1, 2, 3}
+ inductive Annot | sense | observe | track | transform | dispatch | constitution | extension
- ── COMPOSITION ──
+ inductive Op | bind | readReference | classify | extractSignals | classifyRelay | deriveFrames
+ | qframes | generate | present | qround | readAnswer | shapeFrames | park | converge
+ | seam
+
+ def grounding : Op → Annot × String
+ | .bind => (.sense, "Internal analysis: the invocation utterance and a chain reference it names; nothing unnamed is scanned")
+ | .readReference => (.observe, "Tool read, conditional: fires only when a turn of the person's — the bound request or an answer at any gate — names a record outside the session: that record and nothing else; what it returns enters with its external origin")
+ | .classify => (.sense, "Internal analysis: the entry, Blank or Seeded, inferred from the bound request; zero entry questions")
+ | .extractSignals => (.sense, "Internal analysis: signals — concerns, weaknesses, requirements — read from the bound request, named material, and what the person says later, each tagged by its source; never scored or ranked")
+ | .classifyRelay => (.extension, "TextPresent+Proceed: the inferred entry and its basis, quoting the utterance fragment, why the field reads thin, and the signals with their sources; relay, not a gate")
+ | .deriveFrames => (.sense, "Internal analysis: the generation frames — seed-anchored and novel on Seeded, novel and abstract on Blank; a chained field's frames and branches carry over")
+ | .qframes => (.constitution, "present: Blank only — the frame map, multi-select, before any concrete candidate, with the Stop path and room for a frame the person names; read references/blank-entry.md before presenting")
+ | .generate => (.sense, "Internal generation: parallel over the frames the pass opens; a host may realize it through isolated parallel agents, and the meaning does not depend on that; no elimination, ranking, or scoring")
+ | .present => (.extension, "TextPresent+Proceed: the map of the whole field with this round's additions marked, the unaddressed signals, your contrary grounds, what continuing would cost to review and what stopping keeps; precedes the gate")
+ | .qround => (.constitution, "present: every round, continue first and stop second at every presentation; continue opens unexplored frames, a new angle, or a branch under what the person asks to deepen; an answer that opens nothing presents the gate again")
+ | .readAnswer => (.sense, "Internal analysis: the latest utterance read whole with the context — the person's closing if any, the frames it opens, any new angle or branch, any deferral, any exclusion or taken proposal, any record it names, any new signal")
+ | .shapeFrames => (.sense, "Internal analysis: a new angle or a deepening the person named, shaped into frames or branches not already registered before the pass opens them")
+ | .park => (.extension, "TextPresent+Proceed: something the person set aside for later acknowledged as parked, quoting their request; declared at either terminal; its durable record is the host's after the protocol ends")
+ | .converge => (.extension, "TextPresent+Proceed: DiverseCandidateField — the topic and the map, every registered frame and branch marked explored, unexplored, or out of scope with every candidate under it and its origin, the parked follow-ups, the unaddressed signals, your contrary grounds; EarlyExit — the frames offered, those out of scope, the parked follow-ups, every signal, your contrary grounds")
+ | .seam => (.extension, "TextPresent+Proceed: after the person's Stop, at either terminal, a user-declared chain naming the next protocol settles the next move; proceed to it citing that source. A route the person names at a gate is the routed outcome itself. This protocol declares no wired outbound edge. The assembled terminal crosses whole, every origin, branch, park, signal, and contrary ground intact, and the seam never selects, ranks, or trims; every Constitution gate inside this protocol and the next fires unchanged")
+
+ /-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Candidate-field resolution emergent via session context.
+ -/
+
+ end
+
+ end Heuresis
```
## Mode Activation
- `/ideate` is user-initiated: an observation that a field looks narrow does not activate it. Selection and recommendation wait until the user's `Stop` produces `DiverseCandidateField` or `EarlyExit`.
+ `/ideate` is user-initiated: an observation that a field looks narrow does not activate it. Selection and recommendation wait until the person's Stop produces `DiverseCandidateField` or `EarlyExit`.
## Protocol
### User-facing realization
- Present the Phase 0 classification as a short basis-cited relay: the inferred entry, its witness, and source-tagged signals. For `Blank`, read `references/blank-entry.md` before presenting abstract frames and the pre-generation Stop path; for `Seeded`, read `references/seeded-entry.md` before the first expand-first pass. When a named `ChainRef` supplied seeds, also read `references/chain-reference.md` after classification and before promotion.
+ Present the classification as a short basis-cited relay: the inferred entry, why the field reads thin, and source-tagged signals. For `Blank`, read `references/blank-entry.md` before presenting abstract frames and the pre-generation Stop path; for `Seeded`, read `references/seeded-entry.md` before the first pass. When named material supplied seeds or a chained field, also read `references/chain-reference.md` after classification and before the first pass.
- Before every `Qround`, present candidates grouped by frame with origins, the directional contrast between explored and unexplored frames, parked follow-ups, and every signal still unaddressed. State the extra review load and what Stop will preserve. Then present `Continue` first and `Stop` second with symmetric specificity: Continue opens unexplored or user-named new frames; a no-target Continue re-presents the question; a request for depth on an open frame parks and leaves the question open. Render Stop as `DiverseCandidateField` only when candidates exist and otherwise as `EarlyExit`.
+ Before every gate, present one map of the whole field — frames and the branches dug under them, candidates with their origins, unexplored frames, parked follow-ups, every signal still unaddressed, and your contrary grounds — with this round's additions marked. State the extra review load and what Stop will keep. At the Blank frame map the gate is the frame selector `references/blank-entry.md` carries. At every round gate, present continue first and stop second with symmetric specificity: continue opens unexplored frames, a new angle, or a branch under whatever the person asks to deepen; an answer that opens nothing presents the question again. Render Stop as `DiverseCandidateField` only when candidates exist and otherwise as `EarlyExit`.
Read `references/round-composition.md` before composing when terminology must remain stable, wording must be carried unchanged, material belongs to another round or trace, or phase order determines placement around a gate.
## Known Limitations
- `unexplored_frames` covers derived frames, not every conceivable angle.
- - A `ChainRef` gives up the blank path's independent-ideation-first benefit; no mitigation is claimed.
- - Signal extraction is bounded to the entry input and is not exhaustive or session-long.
- - The result carries the final unaddressed snapshot, not the full signal take/discard ledger; that ledger remains recoverable only from the session presentation.
+ - A chain reference gives up the blank path's independent-ideation-first benefit; no mitigation is claimed.
+ - Signals are read from what the person said and the material they named; a concern never put into words is not among them.
+ - The rendered field carries the final unaddressed snapshot, not the full signal take/discard ledger; that ledger remains recoverable only from the round presentations the session context holds.
## Rules
- - **User-initiated, zero entry questions**: `/ideate` activates only on direct invocation (Layer 1); `Entry` (Blank vs. Seeded) is inferred from the utterance alone — never asked. Phase 0's `classify_entry` is Extension/relay, not a gate.
+ - **User-initiated, zero entry questions**: `/ideate` activates only on direct invocation (Layer 1); `Entry` (Blank vs. Seeded) is inferred from the request alone — never asked. The classification is a relay, not a gate.
- **Frame-first ownership**: On `Blank`, read `references/blank-entry.md` before presenting abstract frames or any concrete candidate. Preserve every candidate's origin thereafter.
- - **User-bounded field**: `Stop` remains available from the first gate onward; it returns `DiverseCandidateField` only with candidates and otherwise the fully declared `EarlyExit`.
- - **Euporia boundary — utterance-only input**: heuresis reads only what the invocation carries — the utterance itself, plus a prior protocol's output the user explicitly names (a chain reference). A bare invocation binds the immediately preceding user message as the utterance (a one-turn U-BINDING rule, not a session scan). Beyond the bound utterance it never scans the wider session, codebase, or rules, and it never reverse-traces hidden decision coordinates from externalized substrate — that is Euporia's territory (`/elicit`), not this protocol's.
- - **Chain semantics**: A named `ChainRef` folds material in as seeds, preserving existing origin tags and using `User` only for untagged material. Read `references/chain-reference.md` after classification and before first-pass promotion; the ownership trade-off remains declared under Known Limitations.
+ - **The person closes**: Stop, withdrawal, or a protocol the person names ends the run, and only the person's own turn does. A pick among candidates, a judgment on one, or a correction does not take the field; it is read for the frames it opens and the signals it adds, and the gate stays. Stop returns `DiverseCandidateField` only with candidates and otherwise the fully declared `EarlyExit`, and it closes on what the map it answered showed.
+ - **Out of scope, never erased**: A frame the person puts out of scope stays on the map with its branches and candidates, marked out of scope and citing their turn, and is never widened. Applying a boundary the person stated to particular frames is your proposal, shown as such, until the person takes it.
+ - **Named material only**: heuresis reads the request, material the person explicitly names at invocation or at any later turn — a prior protocol's output in the session, or a record outside it such as an issue or a document, read by a tool — and what the person says as the run goes on. A bare invocation binds the immediately preceding user message as the request (a one-turn U-BINDING rule, not a session scan). It never scans unnamed material — the wider session, codebase, or rules — and never reverse-traces hidden decision coordinates from externalized substrate; that is `/elicit`'s territory.
+ - **Chain semantics**: Named material folds in as seeds, each keeping the origin tag it carries or else the origin of the turn it was read from — `external` for a record a tool read; naming it is the person's adoption, recorded apart. A record named at a later turn is read then, and its items land under their frames with that origin at the next pass. A chained field this protocol assembled resumes: its frames, branches, and candidates carry over as the map stood at its Stop. Read `references/chain-reference.md` after classification and before the first pass; the ownership trade-off remains declared under Known Limitations.
- **Round composition**: Compose each round so the reader can act on it without reassembling it — everyday language rather than this file's formal vocabulary, the judgment set beside the evidence it rests on together with the differential implication that matters for the next move, and analytical context laid out before a gate rather than inside it, so the gate carries the question and each option's differential implication. Read `references/round-composition.md` before composing when a term's rendering has to hold across the session or wording has to be carried through unchanged, when some of what is in view belongs to a later round or a trace rather than this one, or when this protocol's own phases bear on where a sentence sits relative to a gate.
- - **Depth parks, width continues**: A request for more inside an already-open frame parks as a source-cited `ParkedFollowUp`, is declared at either terminal, and leaves `Qround` open; deepening chains from the assembled field later.
- - **Decision delta**: Before every `Qround`, surface unaddressed signals, the explored/unexplored directional contrast, continuing's review cost, and what stopping preserves. Continue names its widening target and Stop names its live terminal.
- - **Neutral option order**: Continue is always first and Stop second, with symmetric specificity. Any novelty or coverage observation stays basis-cited pre-gate state and does not recommend or reorder either answer.
+ - **Width and depth both widen**: A request for more on an open frame or on one candidate opens a branch under it, registered with its parent, and the next pass fills it; nothing is ranked or chosen. Only what the person themselves sets aside for later parks, citing their turn, and is declared at either terminal.
+ - **One map every round**: The whole field is redrawn from the context before each gate, this round's additions marked; a large map compresses to branches and counts while the additions show in full.
+ - **Decision delta**: Before every gate, surface unaddressed signals, your contrary grounds, the explored/unexplored directional contrast, continuing's review cost, and what stopping keeps. Continue names its widening target and Stop names its live terminal.
+ - **Neutral option order**: At every round gate, Continue is always first and Stop second, with symmetric specificity. Any novelty or coverage observation, and every contrary ground, stays basis-cited pre-gate state and does not recommend or reorder either answer.
- **Form feedback**: Derive each round's density from the current request; carry an explicit form instruction until countermanded. Change form directly. Content, wording, order, cadence, and turn boundaries fixed elsewhere remain fixed; state what changed and, where the instruction overlaps a fixed element, what stays and why.