elicit · diff
git:20260902.c728ff3 to git:20260924.f30d1a0
371 added, 115 removed. Audit A to A.
---
name: elicit
description: "Reverse-trace decision coordinates for axis-undetermined intent. Type: (AbstractAporia, Hybrid, REVERSE-INDUCE-CYCLE, IntentSeed × ExternalizedSubstrate) → ResolvedEndpoint"
---
# Euporia Protocol
Resolve abstract aporia through Extended-Mind reverse induction. Type: `(AbstractAporia, Hybrid, REVERSE-INDUCE-CYCLE, IntentSeed × ExternalizedSubstrate) → ResolvedEndpoint`.
## Definition
**Euporia** (εὐπορία): A dialogical act of opening a way through abstract aporia, where AI reverse-traces decision coordinates from the user's externalized cognitive substrate (codebase, rules, past sessions, user environment), surfaces them as cycle-emergent dimension projections, and shapes the converging intent through user answers until the endpoint resolves.
- ```
- ── FLOW ──
- Euporia(I) → Detect(I, S) → aporia? →
- true: (I, S, ctx) → Substrate access → ReverseTrace(I, S, ctx) → D[] →
- filter_confidence(D[]) → (D_surfaced, Λ.deferred) -- concrete substrate basis retained; thin-basis projections held back
- resurface(Λ.parked) -- coordinates the user could not answer yet come back as themselves
- Qs(D_surfaced, Λ.parked, cycle_n) → Stop → A → integrate(A, I) → I' →
- loop until resolved(I') ∨ A = Dismiss
- false: surface scan result; route to axis-specific protocol (axis-determined) or invite user to articulate or withdraw (substrate empty)
+ ```lean
+ /-!
+ How to read this block. It is core Lean 4 and elaborates as written.
+ Every `opaque` declaration is a judgment that is 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` states a
+ consequence the contract already has; it asks nothing further of you.
+ -/
- ── MORPHISM ──
+ /-! ── FLOW ──
+ Euporia(I) → Detect(I, S) → aporia with an external substrate signal? →
+ true: elicit(c, utterances), where c is the fused session context:
+ cycle(c): Substrate access → ReverseTrace(c) → D[] → filter_confidence → (D_surfaced, deferred)
+ → resurface(parked) → Qs(D_surfaced, parked, cycle_n) → Stop
+ next utterance u: c' := fuse(c, u) → answer(c') →
+ Resolved: ResolvedEndpoint(c') (the user's resolution covers the values relayed)
+ Dismiss: ResolvedEndpoint(c') with unresolved axes delegated in its residual
+ Provide or Defer: cycle(c') (the re-trace reads the whole fused context)
+ no utterance: the gate holds
+ false: surface the scan result; route to an axis-specific protocol (axis-determined) or invite
+ the user to articulate or withdraw (no external substrate signal)
+ -/
+
+ /-! ── MORPHISM ──
IntentSeed
→ detect(aporia, axis_undetermined) -- verify abstract aporia exists
→ access(externalized_substrate) -- read external substrate channels (codebase / rules / sessions / environment)
- → observe(utterance_ambiguity) -- analyze I.utterance for in-text semantic ambiguity (Utterance channel; internal)
- → reverse_trace(coordinates) -- infer user's externalized decision coordinates → candidate DimensionProjections
- → filter_confidence(D[]) → D_surfaced -- retain projections whose substrate basis is concrete; hold thin-basis projections back in Λ.deferred
- → resurface(parked_coordinates) -- bring back coordinates the user deferred in an earlier cycle, as themselves rather than re-derived
- → surface(D_surfaced, parked, cycle_emergent) -- present this cycle's projections with substrate-cited basis, alongside anything brought back
- → integrate(answer, I) -- update intent per user answer; ADDS determination, never revises an accepted coordinate
- → resolve(intent) -- convergence when user judges resolved
+ → observe(utterance_ambiguity) -- analyze the utterance for in-text semantic ambiguity (internal)
+ → reverse_trace(coordinates) -- over the fused context: the user's externalized decision coordinates
+ → filter_confidence(D[]) → D_surfaced -- concrete substrate basis surfaces; thin basis is held back
+ → resurface(parked_coordinates) -- deferred coordinates come back as themselves
+ → surface(D_surfaced, parked, cycle_emergent)
+ → fuse(answer) -- the answer joins the context; it adds determinations
+ → resolve(intent) -- convergence when the user judges it resolved
→ ResolvedEndpoint
- requires: aporia(I) -- runtime checkpoint (Phase 0); sole activation precondition
- deficit: AbstractAporia -- activation precondition (Layer 1/2)
- preserves: utterance(I) -- I.utterance read-only; I' accumulates substrate trace
+ requires: aporia(I) -- runtime checkpoint (Phase 0); sole activation precondition
+ deficit: AbstractAporia -- activation precondition (Layer 1/2)
+ preserves: utterance(I) -- the seed utterance is read-only; the context only grows
invariant: Reverse Induction over Axis-Fixed Extraction
- invariant: Coordinate Monotonicity -- accepted coordinates are immutable (full statement: §Coordinate Monotonicity Invariant)
+ invariant: Coordinate Monotonicity -- an accepted coordinate is revised only by a person's utterance
+ -/
- ── TYPES ──
- I = IntentSeed { utterance: String, axis: Optional(Axis) }
- I' = Updated intent (substrate-traced + user-answered)
- S = ExternalizedSubstrate { codebase, rules, sessions, environment }
- -- read-only view of user's externalized cognition
- -- environment: machine-setup metadata (uname, pwd, tool versions, git config public fields)
- D[] = List(DimensionProjection) -- cycle-emergent; no fixed taxonomy
- DimensionProjection = { axis_inferred: String, coordinates: List(Coordinate) }
- Coordinate = { name: String, default: Optional(Value), question: String, basis: Evidence }
- Evidence = { source: SubstrateChannel, content: String }
- SubstrateChannel ∈ {Codebase, Rules, Session, Environment, Utterance}
- -- Codebase / Rules / Session / Environment: sourced from S (ExternalizedSubstrate fields)
- -- Utterance: sourced from I.utterance (not a field of S; in-text semantic ambiguity of the IntentSeed itself);
- -- citation MUST quote the actual utterance fragment, not paraphrase or attribute unstated mental models
- filter_confidence = D[] → (D_surfaced, deferred) -- partition on substrate-basis concreteness; deferred projections are re-tried on a later cycle's re-projection
- D_surfaced = List(DimensionProjection) -- this cycle's surfaceable projections (the ones Phase 2 presents)
- A = UserAnswer ∈ {Provide(values), Defer(coords), Dismiss} -- per-coordinate answer
- values = Map(Coordinate, Value)
- coords = Set(Coordinate) -- parked for a later cycle (covers ambiguous/partial/not-yet-answerable)
- R = ResolvedEndpoint { intent_resolved: I', residual: Set(Axis ⊎ DeferredResidual ⊎ Coordinate) }
- -- residual members are tagged: Axis = an unresolved axis delegated to a downstream protocol; DeferredResidual = a projection the confidence filter held back; Coordinate = a coordinate the user deferred. None is reduced to a bare axis label or silently dropped
- DeferredResidual = { projection: DimensionProjection, basis: Evidence }
- -- a projection still in Λ.deferred at convergence, surfaced as residual with its substrate basis
- cycle_n = Nat -- current cycle counter; surfaced at every Phase 2
- Phase ∈ {0, 1, 2, 3}
- Axis = String -- emergent label; examples: "intent", "goal", "form", "scope", "framework"
- Initiator ∈ {UserInvoked, AIDetected} -- bound at activation; informs Hybrid Phase 2 first-surface semantics
- Qs = Cycle-emergent surfacing interaction with D_surfaced + Λ.parked + cycle counter [Tool: Constitution interaction]
+ namespace Euporia
- ── A-BINDING ──
+ /-! ── GROUND ──
+ The session primitive this contract reads. A context is the list of turns the session has
+ accumulated; a turn carries where it came from and what form it takes. Only a person's
+ statement is an utterance; an AI turn, an injected turn, and a summary ground nothing.
+ -/
+
+ inductive Origin | person | assistant | external | peer | injected | unknown
+ inductive Form | statement | observation | request | reasoning | summary | instruction
+ inductive Basis | utterance | testimony | observation | report
+ deriving DecidableEq
+
+ structure Turn (P : Type) where
+ origin : Origin
+ form : Form
+ content : P
+
+ abbrev Context (P : Type) := List (Turn P)
+
+ /-- What a turn may ground directly: eligibility, not truth or instruction priority. -/
+ def Turn.basis {P : Type} (e : Turn P) : Option Basis :=
+ match e.origin, e.form with
+ | .person, .statement => some .utterance
+ | .person, .observation => some .testimony
+ | .external, .observation => some .observation
+ | .peer, .statement => some .report
+ | _, _ => none
+
+ def Utterance (P : Type) := {e : Turn P // e.basis = some .utterance}
+ def Response (P : Type) := {e : Turn P // e.origin = .assistant}
+ def Evidence (P : Type) := {e : Turn P //
+ e.basis = some .observation ∨ e.basis = some .report ∨ e.basis = some .testimony}
+
+ /-- Fusion appends one turn; the record only grows. -/
+ def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]
+
+ /-- A citation of one turn of `c`, with the basis that turn is eligible for. -/
+ structure Cite {P : Type} (c : Context P) where
+ idx : Nat
+ lt : idx < c.length
+ kind : Basis
+ ok : (c[idx]'lt).basis = some kind
+
+ /-- An open coordinate: which bases it admits, and whether a cited turn supports a value
+ (the support reading is the model's). -/
+ structure Coord (P A : Type) where
+ admits : Basis → Prop
+ supports : Context P → Turn P → A → Prop
+
+ /-- A coordinate is filled only by a citation it admits and that supports the value; `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.kind)
+ (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 := ⟨[u.val], rfl⟩
+
+ theorem ai_never_grounds {P : Type} (e : Turn P) (h : e.origin = .assistant) :
+ e.basis = none := by simp [Turn.basis, h]
+
+ /-- A citation into an earlier context still points at the same turn after later fusion;
+ what it supported there 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
+ kind := s.kind
+ ok := by rw [List.getElem_append_left s.lt]; exact s.ok }
+
+ /-! ── TYPES ── -/
+
+ variable {P : Type}
+
+ /-- `I`: the user's intent seed. The seed utterance is a turn of the context and is never
+ rewritten; `axis` is set when the seed already names one. -/
+ structure IntentSeed where
+ utterance : String
+ axis : Option String
+
+ /-- The channels a coordinate's basis is read from. Codebase, Rules, Session, and Environment
+ are the externalized substrate `S` — a read-only view of the user's externalized cognition;
+ Environment is machine-setup metadata only (uname, pwd, tool versions, public git config
+ fields). Utterance is the seed utterance itself: its citation quotes the actual fragment and
+ attributes no unstated mental model. -/
+ inductive SubstrateChannel | codebase | rules | session | environment | utterance
+
+ structure SubstrateBasis where
+ source : SubstrateChannel
+ content : String
+
+ abbrev Value := String
+
+ structure Coordinate where
+ name : String
+ default : Option Value
+ question : String
+ basis : SubstrateBasis
+
+ /-- Cycle-emergent; no fixed taxonomy. -/
+ structure DimensionProjection where
+ axisInferred : String
+ coordinates : List Coordinate
+
+ /-- **Your judgment**: the decision coordinates the user's externalized substrate implies for
+ the intent, read from the whole fused context — the seed, every answer since, and what
+ the substrate reads returned. -/
+ opaque reverseTrace : Context P → List DimensionProjection
+
+ /-- **Your judgment**: the projection's substrate basis is concrete enough to surface. -/
+ opaque concreteBasis : DimensionProjection → Bool
+
+ /-- `filter_confidence`: projections with concrete basis surface this cycle; the rest are held
+ back and tried again on a later re-trace. -/
+ def surfaced (c : Context P) : List DimensionProjection := (reverseTrace c).filter concreteBasis
+ def deferred (c : Context P) : List DimensionProjection :=
+ (reverseTrace c).filter (fun d => !concreteBasis d)
+
+ /-- `A`, the reading of the user's latest utterance. Coordinate values and deferrals are read
+ from every utterance in the context (`provided`, `parked`); the constructor fixes the path
+ that follows. -/
+ inductive Answer
+ /-- values for surfaced or parked coordinates -/
+ | provide (values : List (Coordinate × Value))
+ /-- coordinates parked for a later cycle: ambiguous, partial, or not yet answerable -/
+ | defer (coords : List Coordinate)
+ /-- stop here, delegating the unresolved axes; on an AI-detected first surface, a decline -/
+ | dismiss
+ /-- the user judges the endpoint resolved; this utterance is the closing citation -/
+ | resolved
+ deriving Inhabited -- elab: lets `answer` be declared `opaque`
+
+ /-- **Your judgment** on the latest utterance read with the context. -/
+ opaque answer : Context P → Answer
+
+ /-- **Your judgment**: the value this person's utterance gives coordinate `x`, read with the
+ context before it; `none` when it gives none. -/
+ opaque provided : Context P → Turn P → Coordinate → Option Value
+
+ /-- The accepted value of `x`: the latest value a person's utterance gave it. Only utterances
+ are read, so no other turn can set or revise it. -/
+ def acceptedAux (x : Coordinate) : Context P → Context P → Option Value → Option Value
+ | _, [], acc => acc
+ | pre, t :: ts, acc =>
+ acceptedAux x (pre ++ [t]) ts
+ (if t.basis = some .utterance then
+ match provided pre t x with
+ | some v => some v
+ | none => acc
+ else acc)
+
+ def accepted (c : Context P) (x : Coordinate) : Option Value := acceptedAux x [] c none
+
+ /-- **Your judgment**: the coordinates the user deferred and has not since given a value, each
+ returning as itself — the same question with the same basis. -/
+ opaque parked : Context P → List Coordinate
+
+ /-- A coordinate is either still waiting on the user or already answered, never both. -/
+ def Leftover (c : Context P) : Prop := ∀ x ∈ parked c, accepted c x = none
+
+ /-- **Your judgment**: the axes still unresolved when the user dismisses. -/
+ opaque unresolvedAxes : Context P → List String
+
+ /-- **Your count**, read from the record: which cycle this is. -/
+ opaque cycleOf : Context P → Nat
+
+ inductive Initiator | userInvoked | aiDetected
+ deriving Inhabited -- elab: lets `initiatorOf` be declared `opaque`
+
+ /-- **Your reading** of how this activation began. On an AI-detected activation the first
+ surface is an implicit confirm-or-decline. -/
+ opaque initiatorOf : Context P → Initiator
+
+ /-- A residual member keeps its kind; none is reduced to a bare axis label or dropped. -/
+ inductive ResidualItem
+ /-- an unresolved axis delegated downstream -/
+ | axis (label : String)
+ /-- a projection the confidence filter still held back -/
+ | projection (d : DimensionProjection)
+ /-- a coordinate the user deferred -/
+ | coordinate (x : Coordinate)
+
+ /-- **Your judgment**: the intent as resolved — every coordinate with its accepted value, and
+ every value relayed as the single dominant one, which the resolving utterance covers. -/
+ opaque resolvedIntent : Context P → List (Coordinate × Value)
+
+ structure ResolvedEndpoint (P : Type) where
+ context : Context P
+ intent : List (Coordinate × Value)
+ residual : List ResidualItem
+
+ /-- Every termination folds what the filter still holds back and every parked coordinate;
+ a dismissal also delegates the unresolved axes. -/
+ def residualAt (c : Context P) (dismissed : Bool) : List ResidualItem :=
+ (deferred c).map .projection ++ (parked c).map .coordinate ++
+ (if dismissed then (unresolvedAxes c).map .axis else [])
+
+ def endpoint (c : Context P) (dismissed : Bool) : ResolvedEndpoint P :=
+ { context := c, intent := resolvedIntent c, residual := residualAt c dismissed }
+
+ inductive Outcome (P : Type)
+ | resolved (r : ResolvedEndpoint P)
+ /-- the gate is held; nothing is answered on the user's behalf -/
+ | holding (c : Context P)
+
+ /-- **Your judgments** at Phase 0: the intent's axis is undetermined; the signal comes from
+ the external substrate — the utterance alone cannot activate. -/
+ opaque Aporia : Context P → Prop
+ opaque ExternalSignal : Context P → Prop
+
+ def activates (c : Context P) : Prop := Aporia c ∧ ExternalSignal c
+
+ /-! ── A-BINDING ──
bind(I) = explicit_arg ∪ recent_intent_seed ∪ surfaced_aporia
Priority: explicit_arg > recent_intent_seed > surfaced_aporia
+ /elicit "intent" → I = IntentSeed with that utterance
+ /elicit (alone) → I = the most recent intent seed in the session
+ "I want to..." → I = the utterance under discussion
+ When `activates` fails, Phase 0 surfaces the scan result instead of opening a cycle: a fully
+ axis-determined intent routes to the matching axis-specific protocol; with no external
+ substrate signal it invites the user to articulate further or withdraw.
+ -/
- /elicit "intent" → I = IntentSeed with utterance
- /elicit (alone) → I = most recent intent seed in session
- "I want to..." → I = utterance under discussion
+ /-! ── MODE STATE ──
+ Λ is the fused context and nothing else. The traced projections, what surfaces and what is held
+ back, the accepted values, the parked coordinates, the cycle count, the initiator, and the
+ residual are read from it when needed; none is stored beside it.
+ -/
- If no aporia signal is detectable, Phase 0 detection surfaces the scan result instead of
- proceeding to Phase 1: when the intent is fully axis-determined it routes to the matching
- axis-specific protocol; when the substrate is empty it invites the user to articulate
- further or withdraw.
+ abbrev Mode (P : Type) := Context P
- ── PHASE TRANSITIONS ──
- Phase 0: I → Detect(I, S) → aporia? -- detection checkpoint; aporia=true → silent proceed to Phase 1; aporia=false → surface scan result (axis-determined → routing recommendation; substrate empty → invite articulate-or-withdraw), no activation
- Phase 1: (I, S, ctx) → Substrate access [Tool] → ReverseTrace [Internal] → D[] (candidate projections)
- → filter_confidence(D[]) → (D_surfaced, Λ.deferred)
- → resurface(Λ.parked) -- coordinates the user deferred earlier are brought back as themselves, not re-derived
- → (D_surfaced, Λ.parked)
- Phase 2: (D_surfaced, Λ.parked, cycle_n, initiator) → Qs(D_surfaced, Λ.parked, cycle_n) → Stop → A -- Constitution; cycle counter visible
- -- Hybrid contract: cycle_n=1 ∧ initiator=AIDetected → first surfacing = implicit confirm-or-decline
- Phase 3: A → integrate(A, I) → I' -- track, residual identification; integrate ADDS only
+ /-! ── PHASE TRANSITIONS ──
+ Each cycle is one step of a structural recursion over the user's utterances. The run starts
+ from the context in which Phase 0 found `activates` and the first cycle surfaced. After each
+ utterance that continues, `respond` is the next cycle's surface: `surfaced` and `parked`
+ beside the cycle count (`cycleOf`) and, from the second cycle, a one-sentence readback of the
+ intent. Where `initiatorOf` reads an AI-detected activation, the first surface is an implicit
+ confirm-or-decline, and a decline reads as `dismiss`.
+ -/
- Phase 0 → Phase 1: aporia(I) = true -- aporia confirmed → silent re-projection loop opens
- Phase 0 → deactivate: aporia(I) = false -- no aporia signal → surface scan result (axis-determined routing recommendation OR articulate-or-withdraw), no activation
- Phase 1 → Phase 2: always -- every cycle hands the turn to the user, including one whose trace surfaced nothing new
- Phase 2 → Phase 3: A received -- per-coordinate answer accepted
- Phase 3 → Phase 1: ¬user_judges_resolved(I') ∧ A ≠ Dismiss → cycle_n += 1 -- re-projection: re-trace the substrate with accumulated I'; accepted coordinates carried forward unchanged, parked coordinates re-surfaced as themselves
- Phase 3 → converge: user_judges_resolved(I') -- user constitutive judgment → ResolvedEndpoint + per-cycle coordinate trace; residual folded per LOOP
- Phase 3 → converge (residual): A = Dismiss -- ResolvedEndpoint with residual annotated for downstream delegation (unresolved axes; residual folded per LOOP; it may be empty)
+ def elicit (respond : Context P → Response P) : Context P → List (Utterance P) → Outcome P
+ | c, [] => .holding c
+ | c, u :: us =>
+ let c' := fuse c u
+ match answer c' with
+ | .resolved => .resolved (endpoint c' false)
+ | .dismiss => .resolved (endpoint c' true)
+ | _ => elicit respond (c' ++ [(respond c').val]) us
- ── LOOP ──
- Every termination below folds the same two leftovers into residual before returning: each projection still in Λ.deferred (as a DeferredResidual) and each coordinate still in Λ.parked (as itself). Neither is ever silently dropped.
- If user_judges_resolved(I'): terminate, return ResolvedEndpoint.
- If A = Dismiss: terminate with ResolvedEndpoint (residual annotated; it may be empty).
- Else: cycle_n += 1, return to Phase 1 (re-project: re-trace the substrate with accumulated I'; accepted coordinates carried forward unchanged; parked coordinates re-surfaced as themselves).
- No fixed cycle cap.
- Convergence presentation (relay, extension-classified; at termination):
- (a) Intent readback — plain single-sentence form of resolved I' assembled from coordinate values, in user-facing language;
- (b) Per-cycle coordinate trace — for each cycle, show (D_surfaced → A → I').
- Convergence is demonstrated, not asserted; the readback materializes I' as a recognizable target without adding a separate constitutive gate.
- Mid-cycle scope: Intent readback (a) also surfaces in Phase 2 from cycle_n ≥ 2 (see Phase 2 surfacing format); the per-cycle coordinate trace (b) is termination-only.
+ /-! ── LOOP ──
+ Every termination folds the same two leftovers into the residual — each projection the filter
+ still holds back and each parked coordinate as itself — and a dismissal adds the unresolved
+ axes. No fixed cycle cap. Convergence presentation, relayed at termination: (a) a plain
+ one-sentence readback of the resolved intent, in the user's language; (b) the per-cycle trace
+ (surfaced → answer → intent). The readback also appears in Phase 2 from the second cycle, as
+ the recognizable target a resolving answer points at; the trace is termination-only.
+ Convergence is demonstrated, not asserted.
+ -/
- ── CONVERGENCE ──
- resolved(I') = user_judges_resolved(I') -- residual folded per LOOP
+ theorem acceptedAux_skip (x : Coordinate) (pre ts : Context P) (acc : Option Value)
+ (h : ∀ t ∈ ts, t.basis ≠ some .utterance) :
+ acceptedAux x pre ts acc = acc := by
+ induction ts generalizing pre acc with
+ | nil => rfl
+ | cons t ts ih =>
+ have hn : ¬ (t.basis = some .utterance) := h t (by simp)
+ simp only [acceptedAux, hn, ↓reduceIte]
+ exact ih _ _ (fun t' ht' => h t' (by simp [ht']))
- ── TOOL GROUNDING ──
+ theorem acceptedAux_append (x : Coordinate) (pre c e : Context P) (acc : Option Value) :
+ acceptedAux x pre (c ++ e) acc = acceptedAux x (pre ++ c) e (acceptedAux x pre c acc) := by
+ induction c generalizing pre acc with
+ | nil => simp [acceptedAux]
+ | cons t ts ih =>
+ simp only [List.cons_append, acceptedAux]
+ rw [ih]
+ simp
+
+ /-- Coordinate Monotonicity: turns that are not a person's utterance — a re-trace, a substrate
+ read, an AI response — leave every accepted value as it was. -/
+ theorem accepted_revised_only_by_utterance (c e : Context P) (x : Coordinate)
+ (h : ∀ t ∈ e, t.basis ≠ some .utterance) : accepted (c ++ e) x = accepted c x := by
+ simp only [accepted]
+ rw [acceptedAux_append]
+ exact acceptedAux_skip x _ e _ h
+
+ theorem silence (respond : Context P → Response P) (c : Context P) :
+ elicit respond c [] = .holding c := rfl
+
+ /-! ── CONVERGENCE ──
+ resolved(c) = the user's latest utterance judges the endpoint resolved; the residual is folded
+ per LOOP.
+ -/
+
+ theorem resolved_here (respond : Context P → Response P) (c : Context P) (u : Utterance P)
+ (us : List (Utterance P)) (h : answer (fuse c u) = .resolved) :
+ elicit respond c (u :: us) = .resolved (endpoint (fuse c u) false) := by
+ simp [elicit, h]
+
+ /-- Nothing parked is dropped at termination. -/
+ theorem parked_in_residual (c : Context P) (d : Bool) (x : Coordinate) (hx : x ∈ parked c) :
+ ResidualItem.coordinate x ∈ residualAt c d := by
+ simp only [residualAt, List.mem_append, List.mem_map]
+ exact .inl (.inr ⟨x, hx, rfl⟩)
+
+ /-- An endpoint always follows a person's utterance. -/
+ theorem endpoint_ends_in_utterance (respond : Context P → Response P) (c : Context P)
+ (us : List (Utterance P)) (r : ResolvedEndpoint P) (h : elicit respond c us = .resolved r) :
+ ∃ (c₀ : Context P) (u : Utterance P), r.context = fuse c₀ u := by
+ induction us generalizing c with
+ | nil => simp [elicit] at h
+ | cons u us ih =>
+ simp only [elicit] at h
+ split at h
+ · cases h; exact ⟨c, u, rfl⟩
+ · cases h; exact ⟨c, u, rfl⟩
+ · exact ih _ h
+
+ /-! ── TOOL GROUNDING ── -/
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
- Phase 0 Detect (sense) → Internal analysis (no external tool)
- Phase 0 Surface (extension) → TextPresent+Proceed (aporia=false: surface scan result; routing recommendation when axis-determined, or invite articulate-or-withdraw when substrate empty; no activation, no constitutive gate)
- Phase 1 Substrate (observe) → artifact read, artifact search, environment run (read-only substrate access — codebase / rules / session history / Environment queries: machine-setup metadata only — uname, pwd, version probes, git config public fields). Immutable read: substrate is never mutated
- Phase 1 Utterance (sense) → Internal analysis of I.utterance for in-text semantic ambiguity (citation quotes actual utterance fragments only)
- Phase 1 ReverseTrace (sense) → Internal analysis (axis inference + coordinate construction → candidate DimensionProjections)
- Phase 1 filter_confidence (track) → Internal state update (extension — retain projections whose substrate basis is concrete in Λ.D_surfaced; hold thin-basis projections back in Λ.deferred for a later cycle. Relay: the partition is grounded in whether a citable substrate basis exists, never a user gate)
- Phase 1 resurface (track) → Internal state update (extension — bring each coordinate in Λ.parked back into this cycle's surfacing as itself, carrying the question and basis it was parked with. Relay: the user already asked for it to come back, so there is nothing to gate)
- Phase 2 Qs (constitution) → present (mandatory; cycle-emergent dimension options from D_surfaced + any re-surfaced parked coordinates + substrate-cited basis + cycle counter)
- Phase 3 (track) → Internal state update (integrate ADDS coordinate determination to I'; accepted coordinates never revised; Defer moves coordinates into Λ.parked, Provide removes them)
- converge (extension) → TextPresent+Proceed (intent readback + per-cycle coordinate trace; proceed with ResolvedEndpoint)
- Seam transition to declared next protocol (extension) → TextPresent+Proceed (fires at deactivation/handoff: 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, so the second trigger is vacuously absent. Every Constitution gate inside this protocol and inside the next protocol fires unchanged)
- ── MODE STATE ──
- Λ = { phase: Phase, I: IntentSeed, I': IntentSeed, S: ExternalizedSubstrate,
- cycle_n: Nat,
- D_surfaced: List<DimensionProjection>, -- this cycle's surfaceable projections (the only ones presented at Phase 2)
- deferred: Set(DimensionProjection), -- projections held back by the confidence filter for lack of a concrete substrate basis; re-tried on a later cycle's Phase 3 → Phase 1 re-projection; surfaced as residual at every termination
- parked: Set(Coordinate), -- coordinates the user answered Defer on. Entered by Defer(coords), left only when that coordinate is later answered with Provide. Re-surfaced as itself at every subsequent Phase 2 — not re-derived, because the user already saw the question and said not yet. Folded into residual as itself at every termination. Kept apart from deferred above: different reason (the user could not answer vs. the substrate could not ground it) and different return path (comes back every cycle as itself vs. re-derived on a later re-projection)
- accepted_coords: Set(Coordinate), -- monotone accumulator — once a coordinate is answered (Provide), it enters here and is NEVER removed or revised
- initiator: Initiator,
- residual: Set(Axis ⊎ DeferredResidual ⊎ Coordinate), -- Axis members = delegated unresolved axes; DeferredResidual members = projections the confidence filter held back; Coordinate members = user-deferred coordinates. All three folded in at every termination
- active: Bool, cause_tag: String }
- -- Monotonicity invariant: accepted_coords is accumulate-only across cycles — integrate(A, I) may ADD to accepted_coords, never remove or overwrite an entry (full statement in §Coordinate Monotonicity Invariant)
- -- Leftover invariant: parked ∩ accepted_coords = ∅ — a coordinate is either still waiting on the user or already answered, never both. Provide moves it across; nothing moves it back
+ inductive Annot | sense | observe | track | transform | dispatch | constitution | extension
- ── COMPOSITION ──
+ inductive Op | detect | scanSurface | substrate | utteranceRead | reverseTrace
+ | filterConfidence | resurface | qs | readAnswer | converge | seam
+
+ def grounding : Op → Annot × String
+ | .detect => (.sense, "Internal analysis: axis-undetermined intent with an external substrate signal")
+ | .scanSurface => (.extension, "TextPresent+Proceed: when Phase 0 does not activate, the scan result with a routing recommendation, or an invitation to articulate or withdraw; no constitutive gate")
+ | .substrate => (.observe, "artifact read, artifact search, environment run: read-only substrate access — codebase, rules, session history, and machine-setup metadata only; the substrate is never mutated")
+ | .utteranceRead => (.sense, "Internal analysis of the seed utterance for in-text semantic ambiguity; citations quote actual fragments")
+ | .reverseTrace => (.sense, "Internal analysis: axis inference and coordinate construction over the fused context")
+ | .filterConfidence => (.sense, "Internal analysis: concrete substrate basis surfaces, thin basis is held back; a relay grounded in whether a citable basis exists, never a user gate")
+ | .resurface => (.sense, "Internal analysis: each parked coordinate returns as itself, with the question and basis it was parked with")
+ | .qs => (.constitution, "present: this cycle's projections with their cited basis and defaults, the returning parked coordinates, the cycle count, and per-coordinate provide-or-defer slots beside Dismiss and Resolved")
+ | .readAnswer => (.sense, "Internal analysis: the handling the latest utterance carries and the values it gives")
+ | .converge => (.extension, "TextPresent+Proceed: intent readback and per-cycle coordinate trace; proceed with ResolvedEndpoint")
+ | .seam => (.extension, "TextPresent+Proceed: at a user-declared chain naming the next protocol, proceed directly to it citing that source; this protocol declares no wired outbound edge, and every Constitution gate fires unchanged")
+
+ /-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Substrate channel resolution emergent via session context.
+ -/
+
+ end Euporia
```
## Scope Boundary
Euporia surfaces grounded decision coordinates without adjudicating which sibling protocol owns them. A coordinate that exposes a missing fact, undefined boundary, or unrecognizable direction remains a coordinate with its substrate basis; the user decides what to reach for next.
## Coordinate Monotonicity Invariant
- An accepted coordinate is immutable. `integrate` only adds determinations to `I'`; a later contradiction is surfaced as a frame change requiring the user to reopen that coordinate through a fresh constitutive act.
+ An accepted coordinate is revised only by a person's utterance. An answer joins the context and adds determinations; a later re-trace, a substrate read, or an AI turn is not ground for revising a value the user gave. When the re-trace finds a contradiction with an accepted value, surface it as such and leave the value standing until the user's own words change it.
## Mode Activation
`/elicit` remains directly invocable. AI-guided activation requires an axis-undetermined intent backed by an external substrate signal from Codebase, Rules, Session, or Environment. Utterance evidence may ground a projection after activation, but cannot activate Euporia by itself.
On the AI-guided path, the immutable Phase 1 scan may precede confirmation; the first Phase 2 response confirms or declines the run. Skip AI-guided activation when the user explicitly asks to proceed without surfacing, or when the same utterance and substrate slice was resolved or dismissed in this session.
## Protocol
### Phase 2 surfacing format
- At Phase 2, render the cycle counter and, from cycle 2 onward, a plain one-sentence readback of current `I'`. For each surfaced projection, show its inferred axis, coordinate questions, cited substrate basis, and any substrate-derived default. Mark each parked coordinate as returning in the same wording and with the same basis. Let the listed coordinates establish what is currently in play without a derived count or resolved/total tally, then present per-coordinate provide-or-defer slots plus Dismiss-with-residual and yield the turn.
+ At Phase 2, render the cycle counter and, from cycle 2 onward, a plain one-sentence readback of current `I'`. For each surfaced projection, show its inferred axis, coordinate questions, cited substrate basis, and any substrate-derived default. Mark each parked coordinate as returning in the same wording and with the same basis. Let the listed coordinates establish what is currently in play without a derived count or resolved/total tally, then present per-coordinate provide-or-defer slots, a way to say the intent is resolved as read back, and Dismiss-with-residual, and yield the turn. An answer beyond the slots — a value for an unlisted coordinate, a dimension the surface excluded, a changed framing — joins the context whole, and the next re-trace reads it.
Utterance evidence quotes the user's actual fragment; it does not attribute an unstated mental model. Only projections with concrete substrate basis reach the surface. Read `references/round-composition.md` before composing when a term must remain stable across the session, wording must travel unchanged, material belongs to another round or trace, or phase order determines whether text belongs before or inside the gate.
### Intensity
| Level | When | Format |
|-------|------|--------|
| Light | One grounded dimension | Brief surface and per-coordinate slots |
| Medium | Several dimensions or partial evidence | Full surface at coordinate granularity |
| Heavy | Multi-axis, weak-basis, multi-cycle prospect | Full surface with per-coordinate evidence and explicit residuals |
## Rules
- **Recognition over Recall**: Present structured dimension projections with anticipatable post-answer states.
- **Round composition**: Use everyday language, keep each judgment beside its nearest evidence and next-move implication, and place analytical context before the answer slots.
- - **Option-set relay test**: Present a single dominant coordinate value as Extension. Keep the answer slot constitutive when different user value weightings sustain multiple values.
- - **Parked-coordinate identity**: A deferred coordinate returns each cycle as the same question with the same basis, marked as returning; it leaves `Λ.parked` only through Provide or termination residual folding.
+ - **Option-set relay test**: Present a single dominant coordinate value as Extension; it becomes part of the resolved intent only through the user's resolving answer, which covers it. Keep the answer slot constitutive when different user value weightings sustain multiple values.
+ - **Parked-coordinate identity**: A deferred coordinate returns each cycle as the same question with the same basis, marked as returning; it stops being parked only through a value the user gives it or termination residual folding.
+ - **Re-trace over the whole context**: Each re-trace reads the fused context — the seed, every answer, and every substrate read — not a summary of the values provided, so a dimension the user named in their own words is traced like any other.
- **Form feedback**: Derive each round's density from the current request and carry an explicit form instruction until countermanded. Change the 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.