/probe

name: probe
description: "Something feels off and the user cannot name what is stuck: the user can then say what it is — a shown candidate, their own words, or none shown — having seen what each rests on and what rules it out."
user_invocable: true

Probe Skill

Resolve a sense that something is off, before the person can name what is stuck, into a situation they recognize, through grounded candidates for what is stuck. Type: `(DeficitUnrecognized, AI, RECOGNIZE, UserSituation) → RecognizedSituation`.

Definition

**Probe** (ἐπίγνωσις, *epígnōsis*: knowing-upon, recognition of what was already there): A dialogical act of turning a person's sense that something is off into a situation they recognize. AI reads the present situation and the descriptions of the other installed skills, and shows the candidates the ground carries for what is stuck, at least two where it carries them — each a description of the situation resting on turns of it that it cites, with the condition that would rule it out, the installed skill that takes it where one does, and that skill's declared end where its description declares one. The person takes one shown candidate, puts the situation in their own words, or says none shown is theirs; that recognition is what the run yields, and no score, ranking, or reading of the AI's makes it. Where the ground carries only one, AI shows that one and says it carries no second rather than inventing one; where it carries none, AI says so. Taking a shown candidate whose line showed a skill takes that skill's invocation with it, unless the person declines the run.

/-!
How to read this block. It is core Lean 4 and elaborates as written, and you are the model it is
written for: you read it, and by inference over the context you settle each element it leaves
open. Every `axiom` is one of those judgments — a black box to the contract, yours to make from
the material in front of you; its doc comment says what you judge there, and nothing in this
block decides it for you. Every `def`, `inductive`, and `structure` is fixed by the contract.
-/

/-! ── FLOW ──
Probe(U) → start(catalog, c) → probe(catalog, c, utterances), where c is the fused session
context and catalog is as `Catalog` states, read once when the run starts:
  [no unrecognized deficit, and the person did not invoke this]  nothing is shown; not activated
  pass(c): what `gathered` reads enters the context; the situation is read against the catalog
  [the ground carries two or more candidates]  present them → Stop
  [it carries fewer]                           say so, with the one line it carries, if any,
                                               and what more of the situation would help → Stop
  next utterance u: c' := fuse(c, u) →
    [u is the person's own invocation of this probe]  this run holds where it stood; the
      invocation is `start`'s
    [u does not bear on this run]  as `Reaches` states; the session answers it
    [a turn of the person's is still owed]  no answer closes → pass(c') → a round that serves it
    [u takes a shown candidate, puts the situation in their own words, or says none shown is
     theirs]  close: recognized → the hand-off `invokedBy` names
    [otherwise] u is more of the situation — a narrower slice, a correction, a candidate set
      aside, a question, a read beyond the session admitted → pass(c') → the same reading
  no utterance: the round holds; nothing is recognized and nothing closes
-/

/-! ── MORPHISM ──
UserSituation
  → detect(deficit_unrecognized)   -- something is off and what is stuck goes unnamed; an invocation of the person's own activates on its own
  → read(catalog)                  -- as `Catalog` states, once at the start; the contract names no skill and no deficit
  → draw(candidates, situation)    -- descriptions of the situation, each resting on turns it cites, each with what would rule it out
  → present(candidates)            -- grounds, then the rules-out condition, then the skill and its declared end; contrary grounds; the turn yields
  → recognize(situation, person)   -- a shown candidate, the person's own words, or none shown: the person's observable act
  → emit(RecognizedSituation)      -- the answer, what the round showed, the contrary grounds closed over, and the recognizing turn, as session text
  → RecognizedSituation
requires: deficit_unrecognized(U) ∨ invoked(U)   -- runtime checkpoint, read by `start` before the first pass
deficit:  DeficitUnrecognized                    -- activation precondition
preserves: the catalog                           -- read, never written; the context only grows
invariant: Recognition over Resolution
-/

namespace Probe

/-! ── 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