/inquire

name: inquire
description: "A task rests on missing context or unchecked assumptions: the user can then recognize what was settled and from where, what rests on weak or unreached ground, and what only they decide."

Aitesis Protocol

Collect every piece of context the AI can reach on its own, then hand back what it cannot reach as the user's own unknown. Type: `(ContextInsufficient, AI, INQUIRE, Prospect) → SufficientContext`.

Definition

**Aitesis** (αἴτησις): A dialogical act of collecting context to the limit of the AI's own reach before the person is asked for anything. The AI infers what the prospect leaves uncertain, pushes each uncertainty through every source it can read or run on its own until none is left, and writes down for each what that reached — a fact that settles it, a finding whose ground it declares short, or nothing — with the sources it tried and those it could not reach named, beside any finding that answers no uncertainty raised. Once everything reachable is reached, what remains open is handed back as the person's own unknown, shown so they can recognize it: where collected material conflicts, the AI names what conflicts with what; where a decision blocks further collection, it names which collection waits on it. Which open uncertainty is the person's is the AI's reading, shown for their recognition and correction; a decision the work rests on that the person holds stays open until their own turn gives it, as the record rule `Settles` states. The beneficiary is the person's epistemic state; the AI's collection is the instrument, and what it spares the person is recalling everything the work rests on. Only a cited source or the person's own words moves a value into the record. The run completes when collection ends; what is still open does not block completion and is not settled by it. The run keeps reading later utterances — one that bears on it opens collection again and a new completion — and silence leaves the last completion standing. Stopping in the middle of a collection is the harness's interrupt, not an outcome of this contract. Completion establishes the collected context the work ahead reads, with what is still open named — not the factual correctness of its parts, and not the readiness of work that rests on what is open.

/-!
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 ──
Aitesis(X) → start(c) → inquire(c, utterances), where c is the fused session context:
  collect(c): every source you can read or run on your own, to the limit of your reach, for every
    live uncertainty and every one collection exposes; what it returns joins the context
  after every collection: SufficientContext — the relay hands back what is open, naming what
    conflicts with what and which collection waits on which decision, and the turn is not held;
    what is open does not block completion
  next utterance u: c' := fuse(c, u), read whole against the prospect and c' →
    [the utterance does not bear on this run]  the session answers it; no collection of this
                                               run; the last completion stands
    [otherwise]                                → collect(c') → after every collection …
  no utterance: the last completion stands — silence settles nothing, what is open stays open
  after completion: the next move the `seam` entry names
  mid-collection stop: the harness's interrupt — a delegation point, not an outcome
-/

/-! ── MORPHISM ──
Prospect
  → scan(prospect, context)      -- the live inventory: what the prospect rests on that the context leaves uncertain; open dimensions, no fixed taxonomy (focus)
  → collect(uncertainties)       -- every source the AI can read or run on its own, to the limit of its reach; what it returns joins the context before anything is recorded
  → read(uncertainty)            -- how each stands: settled with a citation, ground short with its candidate, or unreached; the sources tried and those not reached, by name
  → relay(open)                  -- hand what is open back as the person's own unknown, each with its reach — naming what conflicts with what and which collection waits on which decision — and each settled value with its provenance; proceed
  → fuse(answer)                 -- an answer, when it comes, joins the context whole; if it bears on the run, collection runs again
  → SufficientContext
requires: insufficient(X)        -- declared by invoking /inquire, never judged; judged only on the AI-guided path, where not starting leaves no outcome
deficit:  ContextInsufficient    -- activation precondition (Layer 1/2)
preserves: task_identity(X)      -- the prospect is never rewritten; the context only grows, provided the session is not cleared, compacted, or rewound between invocation and convergence — a harness event this contract does not govern, named here as its delegation point
invariant: Evidence over Inference over Detection
invariant: Focus never records   -- the inventory, the relay, and whether an utterance bears on the run are re-read every turn; only a cited source or the person's turn moves a value into the record
-/

namespace Aitesis

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