/induce

name: induce
description: "Cases at hand seem to share what no one named yet, or what a name in use no longer says: the user can then name it, say which cases it takes in and leaves out, and recognize it as serving their goal."

Periagoge Protocol

Name what several concrete cases share by crossing a working candidate with the goal it serves and with every live reading of the cases, until the user recognizes the abstraction as serving their goal. Type: `(AbstractionInProcess, AI, INDUCE, A) → CrystallizedAbstraction`.

Definition

**Periagoge** (περιαγωγή): a turning-around — a dialogical act for the moment when several concrete cases seem to share something no one has named yet, or that a name in use no longer says. From the first sheet the AI states the goal the abstraction serves and a working candidate — a name and a rule, with the ground it stands on and, where that ground is short, what is short beside it —, and crosses every live reading of what the cases share with that goal: which cases each reading takes in and which it leaves out. The user answers in their own words: they move the goal or the candidate, take what the AI showed, set a reading aside, or recognize the abstraction; they can stop at any time, and the run stays as it stood. Once it has run, the user can name what their cases share, say which cases it takes in and which it leaves out, and recognize it as serving their goal — their settlement for that goal, not proof that the reading is correct (the Greek dialectical vocabulary supplies the source terms).

/-!
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 ──
Periagoge(A) → start(c) → induce(c, utterances), where c is the fused session context:
  start: what bears on the cases is collected into c; then your reading, on it, that this is not
    this protocol's case (`notActivated`) → not activated — on an invocation, your reading with its
    basis; AI-guided activation stays silent; otherwise → sheet
  next utterance u, read on fuse(c, u):
    [does not bear on this run]                                the session answers it; that answer
                                                               stays in c; the run stays as it stands
    [the person recognizes the goal and the candidate]         what is collected now enters c; where
                                                               c is `Overturned` → the sheet again;
                                                               otherwise → crystallized
    [otherwise]                                                what is collected now enters c → the sheet again
  no utterance: nothing comes to stand; the run holds
  after a crystallization, or not activating on an invocation: the next move the `seam` entry names
-/

/-! ── MORPHISM ──
A
  → CrystallizedAbstraction
requires: in_process(A)                     -- read before activation (`notActivated`)
deficit:  AbstractionInProcess              -- activation precondition
preserves: instance_set(A)                  -- the cases are read, never rewritten: they stay as read, whatever carried work changes in their artifacts; a case you found is yours
invariant: Goal Crossed with Readings through Examples, with Alternatives Maintained, over Single-Candidate Steering
invariant: setting a reading aside, taking a value you showed, an open item's words, and every closing are the person's; your readings make none of them
-/

namespace Periagoge

/-! ── GROUND ──
The session primitive this contract reads.
-/

inductive Origin | person | assistant | external | peer | injected | unknown
  deriving DecidableEq

/-- A turn is who sent it and what it says. What the turn does — a statement, a request, an
    instruction, a report of what was observed — is read from its content, never stored here. -/
structure Turn (P : Type) where
  origin  : Origin
  content : P

abbrev Context (P : Type) := List (Turn P)

/-- An origin that may ground: the harness says who sent a turn, and that is all this admits on.
    The assistant's own turns, injected text, and turns of unknown origin ground nothing. -/
def Grounding := {o : Origin // o ≠ .assistant ∧ o ≠ .injected ∧ o ≠ .unknown}

/-- Any turn a person sent, whatever it does. -/
def Utterance (P : Type) := {e : Turn P // e.origin = .person}
def Response (P : Type) := {e : Turn P // e.origin = .assistant}
/-- A turn from outside the conversation: what a tool or the environment returned, or a peer's
    report. A person's account of what they observed is an utterance, read as such. -/
def Evidence (P : Type) := {e : Turn P // e.origin = .external ∨ e.origin = .peer}

def fuse {P : Type} (c : Context P) (u : Utterance P) : Context P := c ++ [u.val]

/-- One turn of the context, with the origin it grounds on. -/
structure Cite {P : Type} (c : Context P) where
  idx : Nat
  lt  : idx < c.length
  src : Grounding
  ok  : (c[idx]'lt).origin = src.val

/-- `admits` reads only who sent the cited turn; `supports` is the model's reading of what that
    turn says, including what it does — a statement, a request, a report of an observation. -/
structure Coord (P A : Type) where
  admits   : Grounding → Prop
  supports : Context P → Turn P → A → Prop

/-- `open_` may carry a candidate citation whose support is still short. -/
inductive Occ {P A : Type} (q : Coord P A) (c : Context P)
  | open_  (candidate : Option (Cite c))
  | filled (a : A) (src : Cite c) (allowed : q.admits src.src)
      (supported : q.supports c (c[src.idx]'src.lt) a)

/-- The same turn, cited from a longer conte