Heuresis Protocol

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

namespace Heuresis

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

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

abbrev Mode (P : Type) := Context P

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

def pass (generate respond : Context P → Response P) (c : Context P) : Context P :=
  let c₁ := c ++ [(generate c).val]
  c₁ ++ [(respond c₁).val]

/-- 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 ──
What each operation of this contract does. An interaction with the person is one of two kinds,
and its kind fixes how it continues once its text is presented.
-/

inductive Interaction | constitution | extension

inductive Continuation | stop | proceed

inductive Annot | sense | observe | track | transform | dispatch | interaction (kind : Interaction)

/-- Every interaction presents its text; a Constitution then stops for the person's turn, and an
    Extension proceeds. -/
def Interaction.realization : Interaction → Continuation
  | .constitution => .stop
  | .extension    => .proceed

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  => (.interaction .extension, "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        => (.interaction .constitution, "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        => (.interaction .extension, "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         => (.interaction .constitution, "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           => (.interaction .extension, "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       => (.interaction .extension, "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           => (.interaction .extension, "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