/ideate

name: ideate
description: "The idea field is empty, narrowed too early, or thin: the user can then see one map from their words and what they name — frames, branches, idea origins, the unexplored — and take it, nothing chosen."

Heuresis Protocol

Resolve an underexpanded candidate field through frame-parallel divergent generation, widening it in width and in depth, without ever eliminating, ranking, or selecting among the candidates it produces. Type: `(CandidateFieldUnderexpanded, User, DIVERGE, IdeationRequest) → DiverseCandidateField`.

Definition

**Heuresis** (εὕρεσις): the act of finding or discovering — a dialogical act of widening a candidate field that is empty or has prematurely converged, before any selection is made. Divergent and convergent thinking are distinct operations (reviewed in Runco & Acar, 2012), and heuresis sits at the point where the candidate field itself is thin. While the field holds no candidate, heuresis shows an abstract frame map before any concrete idea — AI generation support amplifies fixation on the example already in view (Wadinambiarachchi et al., 2024), an instruction to avoid common examples reduced fixation when the examples were stated abstractly rather than concretely (Ezzat et al., 2020) — carried here, as a transfer, to showing abstract frames first — and ideating before seeing a model's ideas preserves ownership and yields ideas less similar to the model's own (Qin et al., 2025). Generation is frame-parallel and never eliminates, ranks, or scores: selection is a downstream act, out of this protocol's scope. The field grows two ways — a new frame widens it, a branch dug under an open frame or candidate deepens it; both routes reach original ideas and can be taken in sequence (Nijstad et al., 2010) — and every round redraws the whole field as one map. The person takes the field when it serves them; until then the run holds, and a later invocation can resume the field whether or not it was taken.

/-!
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: the records `reference` names, read → the classification relay →
    Blank: a pass over the frames the request names, if any → the map
    Seeded: a first pass → the map
    Resumed: a pass over the frames the request opens, if any → the earlier field's map
    whether the map is the frame map or a round is "The map"'s
  next utterance u: c' := fuse(c, u) →
    u takes the field, with candidates in it → DiverseCandidateField; nothing u names is read
    the person's own invocation of this protocol → this run's reading ends, holding; the run it
      starts reads u
    a turn that does not bear on the run → the session answers it; no map; the run holds
    otherwise the records `reference` names, read →
      the frames the answer opens — some: a pass over them → the map
                                    none: the map
  no utterance: nothing is taken; the run holds
-/

/-! ── 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 takes the field         -- only their taking closes; a pick, a judgment, a correction, an ending, or other work does not
invariant: frame map first                    -- at a frame map, until the person has chosen frames, no candidate of yours is shown
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 doubts stand on every map and in the field
-/

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 o