Merismos 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 ──
Merismos(G) → start(c) → apportion(c, utterances), where c is the fused session context:
  start: ground the goal's navigation block where one is in scope →
    [the handoff unreadable: relay → report]
  pass(c): read what the goal needs — its obligations, the host's standing contract subtracted,
    the out-of-scope ones set apart, seam evidence, the authority the run will reach — then judge
    the whole plan afresh against the context as it now stands: whether the request is one goal,
    the units, each unit's fit and seam, each unit's conditions, the whole-goal conditions, the
    acceptance question, the authority, and how each value came to stand → record
  [nothing could be read from the goal's scope: relay(too thin) → report]
  present the whole plan on one sheet, your doubts beside what each bears on, and the focus with
    concrete actions → Stop
  next utterance u, fused into c →
    [it does not bear on this run, or it stops here]     the session answers it; the run holds
  otherwise c₁ := pass(fuse(c, u)) →
    [the person takes the plan ∧ it is closable]         emit → park the carrier → record the
      block → [the block records the carrier: hand off as `.handoff` names → apportioned | the
       write came back incomplete: the sheet again, saying what `.recordHandoff` names; nothing
       closed → Stop]
    [the person takes the plan ∧ it is not closable]     the sheet again, saying the taking did
      not close and what stands in the way → Stop
    [otherwise] the sheet again → Stop
  no utterance: the sheet holds; nothing is taken, and nothing is emitted
  after the handoff: this protocol holds nothing of the autonomous run.
-/

/-! ── MORPHISM ──
AutonomousGoal × ExecutionHorizon
  → probe(goal)                        -- the stated autonomous goal whose unit plan is uncompiled; a bundle bound only by the host's standing procedural contract is the question of which goal this apportionment takes, on the first sheet
  → read_obligations(goal) → O_G       -- the goal's obligations with the host's standing contract subtracted — an ambient invariant every unit inherits — and what was subtracted shown on the sheet
  → filter(velocity) → oos             -- an obligation guardable only by pre-action interception is set out of scope with the substrate that must catch it
  → cut(O_G \ oos, horizon) → units    -- the irreducible core, part one: coarse units, each fitting one execution horizon, together a partition of what is in scope; each cut declares its seam and its fit
  → derive(unit) → certificate         -- the irreducible core, part two: per obligation a verifiable predicate, a residual left unguarded, or a reservation naming the ground that settles it
  → derive_plan(goal, units) → P       -- conditions whose subject is the whole goal, never distributed across units, none naming an order
  → authority(goal, units)             -- what the unattended run will reach that needs the person's authority, by kind, target, and limit
  → sheet(plan, dissent, focus)        -- the whole plan on every turn that bears on the run, your doubts, and the focus
  → take(person)                       -- the person takes the plan with everything it holds in view; that taking adopts what the draft proposed, the authority shown included, and accepts the residuals shown
  → emit(goal_entries) → package → park_carrier → record_handoff → handoff(run)
  → ConditionBearingUnitPlan
requires: user_initiated(G)            -- the person declares autonomous execution intent via /apportion
requires: single_goal(G)               -- read, not enforced: ONE stated outcome, the host's standing procedural contract being no shared goal; a bundle is the person's to settle on the sheet, and a taking over it takes the bundle as one goal with your reading attached as a doubt
deficit:  GoalPlanUncompiled           -- activation precondition (Layer 1)
preserves: G                           -- compile-time only; the context only grows (pass_extends), and no execution state is touched
invariant: Apportion over Order        -- Merismos cuts the units and conditions them; it does not sequence or arrange them
invariant: Whole Plan over Serial Cut  -- nothing is taken before the plan it belongs to has been shown whole
invariant: Coverage over Convenience   -- every goal obligation belongs to some unit or is visibly set out of scope
invariant: Fit over Ambition           -- every unit fits one execution horizon, or the person took it over its verdict (unfit_needs_person)
invariant: Declared Seam over Asserted Joint  -- every cut declares its seam: the evidence it cites, or heuristic
invariant: the person takes and closes; your judgments stand as proposals and contrary grounds
invariant: Handoff carries its obligations  -- every taken plan carries `handoffObligations`
-/

namespace Merismos

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

/-- `G`, `AutonomousGoal`: the one stated outcome and everything the context carries about it —
    the utterance, a prior protocol's output, the session. Nothing here rewrites it. -/
abbrev AutonomousGoal (P : Type) := Context P

/-- **Your reading** of `H`, the `ExecutionHorizon`: the budget one autonomous run is expected to
    fit, read from the context as it now stands, with its cue cited. -/
axiom horizon : Context P → String

/-- A cited piece of material: where it is and what it says. -/
structure Cited where
  source  : String
  content : String

/-- `Obligation`: a stated or inferred requirement the goal must satisfy — the unit of coverage —
    citing its evidence in the goal. -/
structure Obligation where
  statement : String
  evidence  : String
  deriving DecidableEq  -- elab: membership over obligation lists

/-- **Your reading** of the requirements the goal states or implies, before the subtraction, read
    afresh on every pass: a later turn can add one, narrow one, or take one back. -/
axiom candidates : Context P → List Obligation

/-- **Your judgment** (`host_standing_contract(G, o)`): `o` is goal-independent in the host the
    work is carried out in — the host's standing procedural contract attaches it to every change
    it accepts (its version or manifest discipline, its verification command, its branch,
    worktree, or review path, its merge authority) — and `o` is not itself the outcome the goal
    states. Read against the context as it now stands; a person's turn that says otherwise moves
    it. -/
axiom HostStanding : Context P → Obligation → Bool

/-- `O_G`: the candidates with the host's standing contract subtracted. What is subtracted is never
    cut, derived, or counted by coverage: every emitted unit inherits it. -/
def obligations (c : Context P) : List Obligation :=
  (candidates c).filter (fun o => !HostStanding c o)

/-- What the subtraction removed. It stands on the sheet and in the plan, so a misjudged
    subtraction is correctable. -/
def subtracted (c : Context P) : List Obligation := (candidates c).filter (HostStanding c)

/-- `OOSDeclaration`: an obligation whose violation must be caught before an action runs, and the
    substrate that must catch it. A reserved item names no substrate and is never written here. -/
structure OOSDeclaration where
  obligation : Obligation
  substrate  : String
  basis      : Cited

/-- **Your judgment** (`VelocityFilter`): the obligations of `O_G` guardable only by pre-action
    interception, each with its substrate — judged afresh on every pass, since a changed context
    can change what only interception can guard. -/
axiom oos : Context P → List OOSDeclaration

inductive SpanFit | fits | overflows | indeterminate
  deriving DecidableEq  -- elab: the fit check compares verdicts

/-- `Seam`: `grounded` cites the seam the goal evidences — a dependency, deliverable,
    verification, or ownership seam, or another the goal actually evidences; `heuristic` is
    declared where the goal carries none. -/
inductive Seam
  | grounded (evidence : Cited)
  | heuristic

/-- A unit of the plan: what it is about, the obligations it owns — never none — its horizon fit,
    its declared seam, and what carrying it out requires. Capability requirements and feasibility
    notes are functional descriptions read from the goal's stated needs, never a concrete
    executor, model, runtime, or tool. A unit carries no identity across turns: whether a unit on
    this sheet is one on an earlier sheet is your reading of the context. -/
structure PlanUnit where
  subject      : String
  obligations  : List Obligation
  nonempty     : obligations ≠ []
  fit          : SpanFit
  seam         : Seam
  capabilities : List String
  feasibility  : List String

/-- **Your judgment**, made afresh on every pass: the units the plan holds as the context now
    stands — what a person's turn set, on the scope their words reach, and your draft for the rest.
    Together they partition `O_G` less the out-of-scope obligations: each obligation in exactly one
    unit. Where a region admits more than one workable cut, draw one; a second cut that the goal's
    evidence backs as well is a contrary ground you show, never a second unit. -/
axiom units : Context P → List PlanUnit

/-- An obligation some unit holds or some out-of-scope declaration names. -/
def covered (c : Context P) (o : Obligation) : Bool :=
  (units c).any (fun u => u.obligations.contains o) || (oos c).any (fun d => d.obligation == o)

/-- What of `O_G` no unit holds and nothing sets out of scope: a hole in the plan, shown on the
    sheet, and a plan with one is not taken. -/
def residual (c : Context P) : List Obligation := (obligations c).filter (fun o => !covered c o)

/-- `coverage_complete`. -/
def coverageComplete (c : Context P) : Bool := (obligations c).all (covered c)

/-- The units and the out-of-scope declarations partition what they hold: no obligation sits in two
    units, or in a unit and out of scope, and nothing they hold lies outside `O_G`. -/
def partitioned (c : Context P) : Bool :=
  decide (((units c).flatMap (·.obligations) ++ (oos c).map (·.obligation)).Nodup) &&
    (units c).all (fun u => u.obligations.all (obligations c).contains) &&
    (oos c).all (fun d => (obligations c).contains d.obligation)

/-- What the person's turn took a unit with, over a fit verdict that is not `fits`: the reason, and
    for an `indeterminate` verdict the uncertainty named. -/
abbrev Override := String

/-- **Your judgment**: the cited turn takes `u` over its fit verdict. A turn that takes the whole
    plan covers it where the verdict and your contrary ground were in view on the sheet it
    answered; an `indeterminate` verdict is covered only by words that name the uncertainty. -/
axiom OverrideSupported : PlanUnit → Context P → Turn P → Override → Prop

/-- A unit that does not fit is taken only by the person's turn. -/
def overrideCoord (u : PlanUnit) : Coord P Override :=
  { admits := (·.val = .person), supports := OverrideSupported u }

/-- **Your reading**: the person's taking of `u` over its fit; `open_` until one reaches it. -/
axiom override : (c : Context P) → (u : PlanUnit) → Occ (overrideCoord (P := P) u) c

def isFilled {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Bool
  | .open_ _   => false
  | .filled .. => true

def filledValue {A : Type} {q : Coord P A} {c : Context P} : Occ q c → Option A
  | .open_ _     => none
  | .filled a .. => some a

/-- Every unit fits, or the person took it over its verdict. -/
def fitSettled (c : Context P) : Bool :=
  (units c).all (fun u => u.fit == .fits || isFilled (override c u))

inductive PredicateKind | completion | invariant
  deriving DecidableEq  -- elab: the certificate filters on kind

/-- `κ`: a verifiable predicate — an executable check with a determinate pass/fail outcome — for
    one obligation of its unit; a completion predicate says when the unit is done, an invariant a
    boundary the interval preserves while completing. A check the run itself could change so that
    it passes says so in its condition, on the sheet and to the run. -/
structure Compiled where
  obligation : Obligation
  kind       : PredicateKind
  condition  : String

/-- `ρ`: an obligation of its unit with no verifiable predicate, left unguarded. A taking of the
    plan with it shown accepts it as uncovered. -/
structure Residual where
  obligation : Obligation
  kind       : PredicateKind

/-- `σ`: an obligation of its unit that a judgment settles — made against the context accumulated
    by the moment the question comes live and what the person has actually said by then, so no
    compile-time artifact stands in for it. Leaving it open is the correct disposition, not a
    shortfall; `ground` names what settles it. It is neither a residual nor an out-of-scope
    delegation. -/
structure Reservation where
  obligation : Obligation
  kind       : PredicateKind
  ground     : String
  basis      : Cited

/-- What one unit's derivation holds. -/
structure Derivation where
  compiled  : List Compiled
  residuals : List Residual
  reserved  : List Reservation

/-- Every record names an obligation of its own unit. -/
def Derivation.Bound (u : PlanUnit) (d : Derivation) : Prop :=
  (∀ k ∈ d.compiled, k.obligation ∈ u.obligations) ∧
  (∀ r ∈ d.residuals, r.obligation ∈ u.obligations) ∧
  (∀ s ∈ d.reserved, s.obligation ∈ u.obligations)

/-- **Your judgment** for `u`, made afresh on every pass: per obligation a verifiable predicate — a
    completion or an invariant — a residual, or a reservation; every obligation of `u` lands in at
    least one, and `Derivation.Bound u`. A check that covers only part of an obligation leaves the
    rest as a residual or a reservation beside it. Where an obligation could become a check once
    sharpened, the sharpened check is your proposal and derives that obligation alone, with no
    residual beside it, so it reads apart from a partial check; it is shown as the draft's beside
    the obligation it sharpens, a taking adopts it, and where the person declines it the obligation
    is a residual again. A condition a person's turn set stands on the scope their words reach;
    where a change upstream leaves that scope unclear, the sheet names it and it stays open. -/
axiom derivation : Context P → PlanUnit → Derivation

def Derivation.derives (d : Derivation) (o : Obligation) : Bool :=
  d.compiled.any (·.obligation == o) || d.residuals.any (·.obligation == o) ||
    d.reserved.any (·.obligation == o)

/-- `obligations_derived`. -/
def obligationsDerived (c : Context P) : Bool :=
  (units c).all (fun u => u.obligations.all ((derivation c u).derives))

/-- Every record of every unit's derivation names an obligation of that unit — `Derivation.Bound`,
    read over the plan. -/
def derivationsBound (c : Context P) : Bool :=
  (units c).all (fun u =>
    let d := derivation c u
    d.compiled.all (fun k => u.obligations.contains k.obligation) &&
      d.residuals.all (fun r => u.obligations.contains r.obligation) &&
      d.reserved.all (fun s => u.obligations.contains s.obligation))

structure LeafConjunct where
  condition : String
  kind      : PredicateKind

/-- The unit's certificate: every compiled check, every gap accepted as uncovered, and every
    reservation with the ground that settles it, completion and invariant alike, together. A
    passing check never stands for the unit's done while a reserved judgment is still open, and a
    reservation never hides an accepted gap. -/
structure Certificate where
  checks   : List LeafConjunct
  accepted : List Residual
  reserved : List Reservation

def certificate (d : Derivation) : Certificate :=
  { checks := d.compiled.map (fun k => ⟨k.condition, k.kind⟩)
    accepted := d.residuals
    reserved := d.reserved }

/-- The certificate says when the unit is done: some completion check, accepted completion gap, or
    completion reservation stands. -/
def Certificate.terminates (k : Certificate) : Bool :=
  k.checks.any (·.kind == .completion) || k.accepted.any (·.kind == .completion) ||
    k.reserved.any (·.kind == .completion)

/-- `termination_covered`. -/
def terminationCovered (c : Context P) : Bool :=
  (units c).all (fun u => (certificate (derivation c u)).terminates)

inductive PlanScope | finalIntegration | globalNonRegression | wholeGoalAcceptance
  | emergent (name : String)
  deriving DecidableEq  -- elab: binding reads the scope

/-- The predicate of a `PlanStateRequirement`. -/
inductive Requirement
  /-- a condition over a candidate plan, as derived -/
  | stated (check : String)
  /-- `plan_terminal(n)`: the candidate plan has exactly `n` unit certificates and each holds —
      every check passes, and every accepted gap and reservation is carried in the plan -/
  | planTerminal (units : Nat)

/-- `PlanStateRequirement`: never without the evidence it rests on. Whether that evidence still
    tracks what it asserts is not certified here. -/
structure PlanStateRequirement where
  predicate : Requirement
  basis     : {l : List Cited // l ≠ []}

/-- `PlanCondition`: a condition whose subject is the whole goal. -/
structure PlanCondition where
  scope             : PlanScope
  kind              : PredicateKind
  condition         : String
  dischargeableWhen : PlanStateRequirement

/-- **Your judgment**, made afresh on every pass: the conditions whose subject is the whole goal —
    final integration, global non-regression, a whole-goal invariant, or another scope the goal
    carries — never distributed across units, and none naming a unit identity, a move, a region,
    or an order position; a condition you read as naming one is a contrary ground on the sheet.
    The whole-goal acceptance criterion is not among them: it is the acceptance question below. -/
axiom planConditions : Context P → List PlanCondition

/-- How the whole-goal acceptance question is settled. -/
inductive Acceptance
  /-- a completion criterion for the whole goal -/
  | defined (criterion : String)
  /-- constitutively open: its right answer varies with the context accumulated by the moment the
      goal is judged accepted and with what the person has said by then -/
  | reserved
  /-- a criterion the plan should have carried is waived -/
  | waived

/-- **Your judgment**: the cited turn settles the acceptance question this way — a criterion the
    person stated, in the goal itself or later; the draft's criterion taken, which a taking of the
    whole plan with it shown does; a reservation; or a waiver. Read against the context as it now
    stands: a later settling replaces an earlier one, so one value stands. -/
axiom AcceptanceSupported : Context P → Turn P → Acceptance → Prop

/-- Only a person's turn settles the acceptance question. -/
def acceptanceCoord : Coord P Acceptance :=
  { admits := (·.val = .person), supports := AcceptanceSupported }

/-- **Your reading**: the person's settling of the acceptance question; `open_` until one reaches
    it. -/
axiom acceptance : (c : Context P) → Occ (acceptanceCoord (P := P)) c

/-- **Your draft** of a whole-goal acceptance criterion, shown on the sheet as the draft's until
    the person settles the question; `none` where the goal gives you none to propose. -/
axiom draftCriterion : Context P → Option String

/-- `plan_terminal(n)`, whole: its predicate and the evidence it rests on, both over `n`. -/
def planTerminal (n : Nat) : PlanStateRequirement :=
  let src : Cited := ⟨"the current plan's unit certificates",
    "expected unit certificate count = " ++ toString n⟩
  ⟨.planTerminal n, ⟨[src], List.cons_ne_nil src []⟩⟩

/-- Every whole-goal acceptance requirement is bound to plan-terminal over the current unit
    count, so a plan that drops a unit cannot satisfy it vacuously. -/
def bindPlan (c : Context P) (p : PlanCondition) : PlanCondition :=
  if p.scope == .wholeGoalAcceptance then { p with dischargeableWhen := planTerminal (units c).length }
  else p

/-- The defined criterion as a completion condition over the whole goal. -/
def acceptanceCondition (c : Context P) : Option PlanCondition :=
  match filledValue (acceptance c) with
  | some (.defined d) =>
    let src : Cited := ⟨"the turn that settled the whole-goal acceptance criterion", d⟩
    some ⟨.wholeGoalAcceptance, .completion, d, ⟨.stated d, ⟨[src], List.cons_ne_nil src []⟩⟩⟩
  | _ => none

/-- `P`, bound. -/
def planOf (c : Context P) : List PlanCondition :=
  ((planConditions c) ++ (acceptanceCondition c).toList).map (bindPlan c)

/-- **Your reading**: what the run will reach, while the person is away, that needs their
    authority — each named by its kind, its target, and its limit, read from the goal, the units,
    and the context as it now stands. It is shown on the sheet before the person leaves, since
    what it will meet forms only at runtime; the exact act is the run's to meet. It stands as the
    person set it or as their taking adopted it, like any line of the sheet. -/
axiom authority : Context P → List String

/-- What the sheet shows about the plan's shape. -/
structure Status where
  coverageComplete       : Bool
  partitioned            : Bool
  fitSettled             : Bool
  obligationsDerived     : Bool
  derivationsBound       : Bool
  terminationCovered     : Bool
  oosSubstrateNamed      : Bool
  reservationGroundNamed : Bool
  acceptanceSettled      : Bool
  planNonempty           : Bool

def status (c : Context P) : Status :=
  { coverageComplete := coverageComplete c
    partitioned := partitioned c
    fitSettled := fitSettled c
    obligationsDerived := obligationsDerived c
    derivationsBound := derivationsBound c
    terminationCovered := terminationCovered c
    oosSubstrateNamed := (oos c).all (fun d => d.substrate != "")
    reservationGroundNamed := (units c).all (fun u => (derivation c u).reserved.all (·.ground != ""))
    acceptanceSettled := isFilled (acceptance c)
    planNonempty := !(units c).isEmpty || !(oos c).isEmpty }

/-- What a taking needs from the plan's structure; a plan with nothing in it is never taken. A
    reading of yours over content — that a condition names an order, that a unit will not fit —
    is not among them: it stands as a contrary ground. -/
def Structural (c : Context P) : Bool :=
  let s := status c
  s.coverageComplete && s.partitioned && s.fitSettled && s.obligationsDerived &&
    s.derivationsBound && s.terminationCovered && s.oosSubstrateNamed &&
    s.reservationGroundNamed && s.acceptanceSettled && s.planNonempty

/-- **Your judgment**, the adoption condition: every value the taking would take was shown on a
    sheet the person answered — who proposed it and how it came to stand, its ground, and your
    contrary grounds; a value the taking turn itself sets counts where its consequences were in
    view. Where anything would be taken unseen, the sheet is drawn again. -/
axiom Covered : Context P → Prop

/-- A line of the sheet, named as the sheet shows it — the goal, a unit, a condition, a plan
    condition, the acceptance criterion, an authority line, a subtraction, an out-of-scope
    declaration. -/
abbrev Entry := String

/-- **Your reading**: the lines the sheet shows as the context now stands — every line on every
    sheet, unchanged ones included. -/
axiom entries : Context P → List Entry

/-- Who first put a value forward. Kept apart from how the value came to stand: a unit the draft
    proposed and the person kept while moving another was proposed by the draft and set by the
    person. -/
inductive Proposer | draft | person

/-- **Your reading**: the position of the turn that first put forward what `e` holds now. -/
axiom introducedAt : Context P → Entry → Nat

def proposer (c : Context P) (e : Entry) : Proposer :=
  match c[introducedAt c e]? with
  | some ⟨.person, _⟩ => .person
  | _                 => .draft

/-- How a value came to stand: a person's turn set it, or the taking adopted the draft's. -/
inductive Standing | set | adopted

/-- **Your reading**: a person's turn set what `e` holds now — named it, edited it, or chose it —
    on the scope their words reach. -/
axiom setByPerson : Context P → Entry → Bool

def standing (c : Context P) (e : Entry) : Standing := if setByPerson c e then .set else .adopted

structure Provenance where
  entry    : Entry
  proposer : Proposer
  standing : Standing

def provenance (c : Context P) : List Provenance :=
  (entries c).map (fun e => ⟨e, proposer c e, standing c e⟩)

/-- One concrete action for a focus: what it would change, and what then happens. -/
structure Action where
  edit        : String
  consequence : String

/-- An open point the sheet asks about. -/
structure Focus where
  item    : String
  actions : List Action

/-- **Your selection** of the focus: the open points the sheet asks about; empty where nothing is
    open and the question is whether to take the plan. -/
axiom focus : Context P → List Focus

/-- **Your judgment**: the ground clearly separates action `i` of `f` from the others — not that it
    is somewhat better. -/
axiom Separates : Context P → Focus → Nat → Prop

/-- **Your recommendation** for `f`: an action the ground clearly separates, carried with that
    judgment; `none` where the actions are comparable, and then each stands beside its consequence
    alone. -/
axiom recommend : (c : Context P) → (f : Focus) → Option {i : Nat // Separates c f i}

/-- **Your record**: the doubts you hold about the plan, each naming what it bears on — a unit, a
    condition, the authority, the whole plan — and what it rests on, read from the context as it
    now stands; empty when you hold none. Each is shown beside what it bears on, before the
    person's turn it bears on, and refuses no taking. A taking over one keeps it attached to the
    plan — taken, and evidentially disputed — naming at emission the unit by the ref it is emitted
    under. -/
axiom dissent : Context P → List String

/-- **Your judgment**: the cited turn takes the plan as the latest sheet showed it, read against
    the context as it now stands; whatever the same turn changes is read with it. A turn before
    the latest sheet takes nothing on it, an answer to the focus takes nothing, a turn after the
    person stopped this run takes nothing unless their words return to this plan, and your own
    reading that the plan is ready takes nothing. -/
axiom ResolutionSupported : Context P → Turn P → Unit → Prop

/-- Only the person takes the plan. -/
def resolutionCoord : Coord P Unit :=
  { admits := (·.val = .person), supports := ResolutionSupported }

/-- **Your reading**: the person's taking of the plan; `open_` until one reaches it. -/
axiom resolution : (c : Context P) → Occ (resolutionCoord (P := P)) c

/-- **Your judgment**: the latest utterance bears on this run — an edit, an answer to the focus, a
    settling of the acceptance question, a change to the authority, a taking. An utterance about other work, or one
    that stops here, leaves the run as it stands: the session answers it, that answer stays in the
    context, the sheet is not drawn again, and the run holds. -/
axiom Reaches : Context P → Prop

/-- The plan may be taken: its structure holds and everything it takes was shown. -/
def Closable (c : Context P) : Prop := Structural c = true ∧ Covered c

/-- `UnitRef`: assigned at emission, one per unit, never shared. -/
abbrev UnitRef := Nat

/-- `JudgmentReservation` as emitted. -/
inductive ReservedSubject
  | obligation (o : Obligation)
  /-- the whole-goal acceptance criterion itself, which names no obligation -/
  | acceptance

def ReservedSubject.isAcceptance : ReservedSubject → Bool
  | .acceptance   => true
  | .obligation _ => false

structure JudgmentReservation where
  subject : ReservedSubject
  unit    : Option UnitRef
  kind    : PredicateKind
  ground  : String
  basis   : Cited

/-- The reserved acceptance criterion: its ground is the same in every plan that reserves it. -/
def acceptanceReservation : JudgmentReservation :=
  { subject := .acceptance, unit := none, kind := .completion,
    ground := "the context accumulated by the moment the goal is judged accepted, together with what the person has actually said by then",
    basis := ⟨"the person's reservation of the whole-goal acceptance criterion",
      "the criterion's right answer varies with that ground, so fixing it now would settle a live question where the person is not present"⟩ }

structure UnitEntry where
  ref          : UnitRef
  subject      : String
  obligations  : List Obligation
  fit          : SpanFit
  seam         : Seam
  certificate  : Certificate
  capabilities : List String
  feasibility  : List String

structure AcceptedResidualEntry where
  obligation : Obligation
  unit       : UnitRef
  kind       : PredicateKind

/-- The envelope: the accepted gaps, the reservations, the out-of-scope set, the subtraction, and
    the waiver kept apart from the reserved criterion, so a reader of the plan alone tells a
    waived criterion from one correctly left open. -/
structure Envelope where
  acceptedResiduals : List AcceptedResidualEntry
  reserved          : List JudgmentReservation
  oos               : List OOSDeclaration
  subtracted        : List Obligation
  waived            : Bool

/-- `E`: one entry per unit, one per plan condition, and exactly one envelope. -/
structure Emission where
  units          : List UnitEntry
  planConditions : List PlanCondition
  envelope       : Envelope

def numbered {α : Type} (l : List α) : List (Nat × α) := (List.range l.length).zip l

def entry (i : UnitRef) (u : PlanUnit) (k : Certificate) : UnitEntry :=
  ⟨i, u.subject, u.obligations, u.fit, u.seam, k, u.capabilities, u.feasibility⟩

def envelope (c : Context P) : Envelope :=
  let a := filledValue (acceptance c)
  { acceptedResiduals := (numbered (units c)).flatMap (fun (i, u) =>
      (derivation c u).residuals.map (fun r => ⟨r.obligation, i, r.kind⟩))
    reserved := (numbered (units c)).flatMap (fun (i, u) => (derivation c u).reserved.map (fun s =>
        ⟨.obligation s.obligation, some i, s.kind, s.ground, s.basis⟩)) ++
      (match a with | some .reserved => [acceptanceReservation] | _ => [])
    oos := oos c
    subtracted := subtracted c
    waived := match a with | some .waived => true | _ => false }

/-- `Emit`. -/
def emit (c : Context P) : Emission :=
  { units := (numbered (units c)).map (fun (i, u) => entry i u (certificate (derivation c u)))
    planConditions := planOf c
    envelope := envelope c }

/-- What every run of a taken plan carries, wherever and whenever it is started. This text is the
    statement; the Rule "Handoff carries its obligations" names it. -/
def handoffObligations : String :=
  "The run does what does not rest on the person without waiting for them and, when the plan has run, returns to them once with every unit's result; what rests on the person — a step that cannot be undone, where a doubt the plan carries, or one execution brings evidence for, bears on it, among them — comes back in that return with what did not proceed because of it, and nothing is decided for them."

/-- Once it has run, the person can say: this goal runs in these units, each with its checks, the
    gaps I accepted, and the judgments held open with what settles them; what only I decide and
    what the run may not do without me, I saw on one sheet; I settled before leaving what had to
    be settled, and the rest comes back to me once at the end with what did not proceed because of
    it; I took this plan as mine.
    `ConditionBearingUnitPlan`, with the authority the run will reach, the doubts the taking
    carried, how each value came to stand, and the obligations every run of it carries. -/
structure ConditionBearingUnitPlan where
  units             : List UnitEntry
  planConditions    : List PlanCondition
  acceptedResiduals : List AcceptedResidualEntry
  reserved          : List JudgmentReservation
  oos               : List OOSDeclaration
  subtracted        : List Obligation
  waived            : Bool
  authority         : List String
  dissent           : List String
  provenance        : List Provenance
  runObligations    : String

/-- `package`: the returned plan read back from what was emitted, never derived beside it. -/
def package (e : Emission) (au : List String) (ds : List String) (pv : List Provenance) :
    ConditionBearingUnitPlan :=
  { units := e.units, planConditions := e.planConditions,
    acceptedResiduals := e.envelope.acceptedResiduals, reserved := e.envelope.reserved,
    oos := e.envelope.oos, subtracted := e.envelope.subtracted, waived := e.envelope.waived,
    authority := au, dissent := ds, provenance := pv, runObligations := handoffObligations }

/-- Where the carrier is: its record identity, and the session that identity is scoped to. -/
structure HandoffLocator where
  record  : String
  session : String

/-- `N`, `NavigationBlock`: the fixed cross-session shape — a pointer, never a copied record. -/
structure NavigationBlock where
  purposeFrame           : String
  canonicalLocator       : HandoffLocator
  dereferenceInstruction : String
  snapshotAnchor         : Option String
  groundingInstruction   : String

/-- **Your reading**: the navigation block the context supplies — a prior `/apportion` block over
    the goal, or another protocol's; `none` otherwise. -/
axiom pointer : Context P → Option NavigationBlock

/-- **Your reading** at activation: follow the block's dereference instruction at its locator and
    run its grounding instruction; what the carrier returns enters the context. Nothing when there
    is no pointer. -/
axiom groundPointer : Context P → List (Evidence P)

def bindPointer (c : Context P) : Context P := c ++ (groundPointer c).map (·.val)

/-- **Your judgment**: the pointer's locator does not reach its carrier, or compiling this goal
    needs a premise its record does not support. An unsupported downstream judgment the
    compilation can leave open is not this: it stays reserved. False without a pointer. -/
axiom PointerUnreadable : Context P → Prop

/-- **Your record**: the identity this taking's carrier-creating write returned; empty where none
    returned. -/
axiom carrierRecord : Context P → String

/-- **Your reading** of what the writes returned: the emission was recorded and the carrier
    `carrierRecord` names holds the whole packaged plan — not only an identity allocated for it. -/
axiom CarrierComplete : Context P → Prop

/-- **Your record**: the session the plan was taken in — the source session, within which the
    carrier record is found. Where the environment carries more than one session id, which one
    reaches that session is yours to read. -/
axiom sessionId : Context P → String

/-- **Your reading**: what a receiving session needs to know the plan is for. -/
axiom purposeFrame : Context P → String

/-- **Your reading**: a snapshot anchor, only where exact-state determinacy is needed. -/
axiom snapshotAnchor : Context P → Option String

/-- `GroundingInstruction`: the receiving procedure the block carries. -/
def receivingProcedure : String :=
  "Dereference the carrier and its source session, using /inquire where available or an equivalent grounding pass; the authority the plan carries does not widen through reassignment."

/-- `record_handoff`: the block over the carrier — entry points only, never a re-authored plan. -/
def navigation (c : Context P) : NavigationBlock :=
  { purposeFrame := purposeFrame c
    canonicalLocator := ⟨carrierRecord c, sessionId c⟩
    dereferenceInstruction := "read the carrier record at the canonical locator's record identity, within the session it names; one read yields the whole plan"
    snapshotAnchor := snapshotAnchor c
    groundingInstruction := receivingProcedure }

/-- `handoff_recorded`, its structural half: the block's locator reaches the carrier the write
    returned — its record identity present, within the session it names — and the block states
    its purpose. That it was presented is the text itself. -/
def HandoffRecorded (n : NavigationBlock) (c : Context P) : Prop :=
  n.purposeFrame ≠ "" ∧ n.canonicalLocator = ⟨carrierRecord c, sessionId c⟩ ∧
    n.canonicalLocator.record ≠ ""

/-- The writes landed: the carrier holds the plan, and the block locates it. -/
def Recorded (n : NavigationBlock) (c : Context P) : Prop := CarrierComplete c ∧ HandoffRecorded n c

/-- Why the run ends without a plan, on evidence rather than the person's turn: the incoming
    handoff could not be read, or nothing could be read from the goal's scope. -/
inductive RelayKind
  | handoffUnreadable
  /-- nothing could be read from the goal's scope -/
  | tooThin

/-- The emitted result: the context after the writes, what was emitted, the plan read back from
    it, and the navigation block over its carrier. It is handed off by `.handoff` in the same
    turn. -/
structure Apportioned (P : Type) where
  context    : Context P
  emission   : Emission
  plan       : ConditionBearingUnitPlan
  navigation : NavigationBlock

inductive Outcome (P : Type)
  | relayed     (kind : RelayKind) (c : Context P)
  /-- the person took the plan, the navigation block records its carrier, and the plan is handed
      off as `.handoff` names -/
  | apportioned (a : Apportioned P)
  /-- no taking closed: the sheet holds, whether the person is silent, stopped, or turned to other
      work; nothing is handed off, and after a carrier write that came back incomplete the sheet
      that said what `.recordHandoff` names stays in the context -/
  | holding     (c : Context P)

/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it. Coverage
partition: the units' obligations, the out-of-scope obligations, and the holes together are
`O_G` — the holes by construction, and no obligation in two cells nor outside `O_G` wherever a
taking is read, as `partitioned` checks. The host's standing contract is subtracted before `O_G`
exists, and a reservation stays in the unit it belongs to, so neither is a fourth cell. Nothing persists
into the execution interval.
-/

abbrev Mode (P : Type) := Context P

/-! ── PHASE TRANSITIONS ──
A step is one arm of a structural recursion over the person's utterances. A pass is the silent
work: the reads the plan needs enter the context, then the pass's record — the plan judged afresh,
each value with how it came to stand. `respond` presents the sheet; a taking over a closable plan
writes the emission and the carrier instead; `session` is the session's own answer to an utterance
about other work, or one that stops here, which stays in the context without drawing the sheet.
-/

/-- **Your reads** for a pass: the goal's cited material, and seam evidence over its substrate. -/
axiom collect : Context P → List (Evidence P)

/-- **Your record** of a pass, once its reads have entered the context: the plan as judged —
    whether the request bundles several stated outcomes, units, conditions, plan conditions, the
    acceptance question, the authority, subtraction and out-of-scope classification, provenance,
    your doubts, and the focus. A record grounds nothing. -/
axiom passRecord : Context P → List (Response P)

def pass (c : Context P) : Context P :=
  let c₁ := c ++ (collect c).map (·.val)
  c₁ ++ (passRecord c₁).map (·.val)

/-- **Your action** on a taking: the Emit record write of `emit c`, then the write of the packaged
    plan into one new carrier record; each returns what it wrote and its identity. -/
axiom persist : Context P → List (Evidence P)

def close (c : Context P) : Apportioned P :=
  let c₃ := c ++ (persist c).map (·.val)
  { context := c₃, emission := emit c,
    plan := package (emit c) (authority c) (dissent c) (provenance c),
    navigation := navigation c₃ }

def tooThin (c : Context P) : Bool := (obligations c).isEmpty

open Classical in
def relayAt (c : Context P) : Option RelayKind :=
  if PointerUnreadable c then some .handoffUnreadable
  else none

open Classical in
/-- `respond` presents the sheet. First the whole plan: every unit with its obligations, fit, seam
    with its citation or heuristic declaration, capabilities and feasibility, and its certificate —
    checks, residuals, reservations with their grounds — a unit whose done rests only on accepted
    residuals shown as one the run cannot tell is done; the plan conditions with the requirement
    that makes each safe to discharge; the acceptance question — the person's settling, or the
    draft's criterion marked as the draft's; the authority the run will reach, by kind, target, and
    limit; the out-of-scope obligations with their substrates; what was subtracted as the host's
    standing contract; any hole; where the request bundles several stated outcomes, each stated
    outcome and their bond in the host's standing procedural contract, as the question of which
    goal this apportionment takes; each field labelled by the question it answers, in the person's
    everyday words; each value marked the person's or the draft's. Then your doubts, each beside
    what it bears on, with what it rests on. Then the focus with its actions, each with its consequence, an action marked recommended
    only as `recommend` carries it; with nothing open, whether to take the plan and what a taking
    would not yet satisfy; wherever a taking would close the run, that it hands the plan off in the
    same turn as `.handoff` names, unless the person keeps the start for themselves. After a taking
    that did not close — the structure did not allow it, or something it would take had not been
    shown — the sheet says so and what stands in the way. After a carrier write that came back
    incomplete, the sheet says what `.recordHandoff` names. Where the context
    holds an earlier taken plan for this goal, the sheet names it as the plan this one replaces.
    Wherever a person's earlier turn is read as setting a value, the sheet says which turn and what
    was taken from it, quoting their words. -/
def apportion (respond session : Context P → Response P) :
    Context P → List (Utterance P) → Outcome P
  | c, []      => .holding c
  | c, u :: us =>
    let c₀ := fuse c u
    if ¬ Reaches c₀ then apportion respond session (c₀ ++ [(session c₀).val]) us
    else
      let c₁ := pass c₀
      if isFilled (resolution c₁) = true then
        if Closable c₁ then
          if Recorded (close c₁).navigation (close c₁).context then .apportioned (close c₁)
          else apportion respond session ((close c₁).context ++ [(respond (close c₁).context).val]) us
        else apportion respond session (c₁ ++ [(respond c₁).val]) us
      else apportion respond session (c₁ ++ [(respond c₁).val]) us

def start (respond session : Context P → Response P) (c : Context P)
    (us : List (Utterance P)) : Outcome P :=
  let c₁ := bindPointer c
  match relayAt c₁ with
  | some k => .relayed k c₁
  | none =>
    let c₂ := pass c₁
    if tooThin c₂ then .relayed .tooThin c₂
    else apportion respond session (c₂ ++ [(respond c₂).val]) us

/-! ── LOOP ──
An utterance about other work, or one that stops here, is the session's to answer and leaves the
run holding. Every sheet re-judges the whole plan against the whole context: nothing counts down, no stage is
entered, and no answer is held for a later gate. A person's edit reaches what their words reach —
one unit, a region, a condition, the acceptance question — and the draft re-fills what depends on
it. A cut sent back, a
unit reopened, a condition adjusted are all edits of the same kind; re-reading rewrites no value a
person's turn made stand beyond the reach their later words give. The loop is dialogue: each
sheet ends at the focus, and only the person's taking closes the run. The run holds no state into
the execution interval.
-/

/-! ── CONVERGENCE ──
apportioned(G): the person took the plan with everything it holds in view, its structure held —
never an empty plan — the carrier holding the whole plan, the navigation block over it presented
(`Recorded`), and the plan handed off in the same turn as `.handoff` names — to the run, or by the
navigation block alone where no run was started, the turn saying which.
The taking adopted what the draft proposed, the authority shown included, and accepted every
residual shown; it established nothing about whether a check is the right one, and a doubt it was
taken over rides the plan attached to what it bears on.
Convergence evidence, at emission: (a) the goal restated as its units, one plain sentence each;
(b) per unit, the obligations, the seam with its citation or heuristic declaration, the fit or the
person's taking over it with their words, the certificate — every check, every accepted gap, every
reservation with its ground — and the capability requirements and feasibility notes; (c) the plan
conditions with the requirement that makes each safe to discharge; (d) every out-of-scope
obligation with its substrate, and what was subtracted as the host's standing contract; (e) the
acceptance question as settled — the criterion and whose it was, the reservation stated as left
open on purpose, or the waiver — never two of these; (f) the authority the run will reach, as it
stands; (g) how each value came to stand — who proposed it, set or adopted — and the turns
read as setting values, quoted; (h) the doubts the plan carries, each with what it bears on.
Demonstrated, not asserted.
-/

/-! ── 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. A Constitution settles a judgment
through the person's turn. An Extension settles none for the person: it passes on a result its
cited ground fixes, or carries reversible work forward on a judgment the AI states, which stays
the AI's proposal until the person takes it. Beyond the Constitution operations a contract
annotates, whether work goes forward this way or waits for the person's answer is the AI's
judgment in the situation, and work that cannot be undone waits for the authorization it needs.
Work carried forward, on a grant or a stated judgment or as clear work, returns with an account
of how the request was read, what was judged on what basis — naming an alternative set aside
where it may be preferred — and how far the work went.
-/

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 | probe | relay | collect | judge | record | sheet | readTurn | emit | package
             | parkCarrier | recordHandoff | converge | handoff

def grounding : Op → Annot × String
  | .probe         => (.observe, "record read, artifact read: the goal and whether its plan is uncompiled, cue cited. A navigation block in scope is dereferenced — the one carrier at its locator, within the session it names — and its grounding instruction run once; the plan read back from that carrier enters the context, and where it already carries its conditions the first sheet draws from it with that reading as a contrary ground")
  | .relay         => (.interaction .extension, "an unreadable handoff, which never falls through to fresh compilation, or nothing read from the goal's scope. No activation")
  | .collect       => (.observe, "record read, artifact read, artifact search: the goal's cited material and seam evidence over its substrate; read-only")
  | .judge         => (.sense, "Internal analysis: the whole plan afresh against the whole context — whether the request bundles several stated outcomes, obligations with the host's standing contract subtracted, the out-of-scope set, the units as a partition with each fit and seam, each unit's conditions, the plan conditions, the acceptance question, the authority the run will reach, how each value came to stand, and your doubts with what each bears on; a person's value stands on the scope their words reach")
  | .record        => (.track, "record: the pass's record of the plan as judged, and the focus")
  | .sheet         => (.interaction .constitution, "the whole plan on one sheet, as `respond` composes it. Silence holds and takes nothing")
  | .readTurn      => (.sense, "Internal analysis: the new turn, and every earlier turn of the person's it bears on, read whole against the fused context as it now stands — whether it bears on this run at all, and there an edit and its scope, an answer to the focus, a settling of the acceptance question, a change to the authority, a taking over a fit, a taking of the plan — whatever form it takes")
  | .emit          => (.track, "record: on a taking over a closable plan, one entry per unit with its ref and its whole certificate, one per plan condition, and exactly one envelope — accepted gaps, reservations, the out-of-scope set, the subtraction, and the waiver apart from the reserved criterion")
  | .package       => (.sense, "Internal analysis: the returned plan read back from the emitted entries, with the authority, the doubts the taking carried, and the obligations every run of it carries, and each value's provenance")
  | .parkCarrier   => (.track, "record: the packaged plan written into one new carrier record, whose write returns its identity")
  | .recordHandoff => (.interaction .extension, "the navigation block over the carrier — purpose, a locator that reaches the carrier, dereference instruction, snapshot anchor only where needed, and the receiving procedure; entry points only. A write that returned no identity or left the plan incomplete in the carrier, or a block whose locator does not reach the carrier, closes nothing and presents no block: the sheet says what was written and where (each identity the writes returned), what is missing, and that the plan is therefore not yet handed off")
  | .converge      => (.interaction .extension, "the apportionment trace after the navigation block: the convergence evidence CONVERGENCE names")
  | .handoff       => (.dispatch, "delegate: after the trace, in the same turn, the plan handed to the autonomous run through the navigation block, whose plan carries `handoffObligations` — where the plan holds no unit, nothing is started and the block alone is the handoff — a substrate that runs one unit per stretch and evaluates each unit's checks; where the session can start none, the start fails, or the person's taking keeps the start for themselves, the block is the handoff and the person starts the run, and the same turn says which of these happened — a failed start with what it returned; then this run ends")

/-- The operation an outcome hands off through: a taken plan goes to the run by `.handoff`, after
    the trace; a relay or a holding hands nothing off. -/
def handedOffBy : Outcome P → Option Op
  | .apportioned _ => some .handoff
  | _              => none

/-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Dimension resolution emergent via session context.
The plan leaves as session text and a navigation block over its carrier; what reads it next is the
person's and the session's to settle. The block carries the grounding instruction; the emission
supplies no answer to a reserved judgment.
-/

end

end Merismos