Analogia Protocol
Audit what a mapping licenses: on the question the person's own words set, or your draft of it while they leave it open, collect to the limit of your reach over what the mapping rests on, construct the correspondences between the source structure and the target, warrant each fit claim from evidence the protocol can cite, and report for each conclusion at stake whether it holds, is blocked, or stays undetermined. Type: (MappingUncertain, AI, GROUND, R) → MappingAssessment.
Definition
Analogia (ἀναλογία): A dialogical act of auditing analogical inference. A mapping — a framework, an analogy, an earlier design, an abstraction — is being relied on, and what it licenses about the target is unclear: the feeling that it fits does not tell which conclusions it supports. The person's own words set the question: what the comparison is for, the conclusions at stake, and which source and which target where that choice is open. While their words leave it open, the AI may draft it and carry the audit forward on its draft; only the person's turn makes the question stand, and an assessment says which it rests on. The AI then collects to the limit of its own reach over what the mapping rests on — the source's relations and their counterparts in the target, reading any account it can reach itself — names the places it reached and those it could not, constructs the correspondences, warrants each fit claim against evidence with what would defeat it, and reports for each conclusion the source relation, or chain of relations, that carries it, what was checked and found, what difference would break it, and whether it holds and how far, is blocked, or stays undetermined with what is missing and who can reach it. What remains open is shown as the person's own unknown. The person's utterance supplies grounds and records what they adopt; it never promotes a claim to warranted, because assent is not evidence about the world. An assessment establishes no correctness beyond the evidence it cites, and a blocked conclusion is not thereby false.
/-!
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 ──
Analogia(R) → start(c) → ground(c, utterances), where c is the fused session context:
pass(c):
[nothing to audit] TOOL GROUNDING `questionDraft`; nothing is collected
[otherwise] collect(c): to the limit of your reach over what the mapping rests on — the
source's relations and their target counterparts, and the checks on the claims bearing
on K, the conclusions of the question that stands or of your draft; every place looked
joins the context, a null result included →
[the collected context leaves nothing to audit] `questionDraft`
[otherwise] assessment: each conclusion Licensed with its limits, Blocked, or Undetermined
with what is missing and who can reach it, on the question that stands or on your draft,
named which — a draft shown as `questionDraft` states; present it and proceed — no
verdict is asked
next requested move: as TOOL GROUNDING `seam` states
next utterance u: c' := fuse(c, u), read whole against R and c' →
[u bears on the audit] pass(c') (a changed purpose, conclusion, pair, or ground is read there)
[otherwise — adopting or setting aside a conclusion, a question the current grounds answer
entirely, other work, turning away from an open question] the session answers it; no
pass opens; the last outcome stands — an open question stays open
no utterance: the last outcome stands — silence settles nothing
mid-pass stop: the harness's interrupt — a delegation point, not an outcome
-/
/-! ── MORPHISM ──
R
→ question(R, context) → Q -- purpose, conclusions at stake (K), and an open pair; standing only on the person's turn, otherwise your draft
→ collect(Q, context) -- to the limit of reach over what the mapping rests on, constructing the claims it needs and running their reachable checks; results join the context; reached and unreached named
→ construct(mapping, context) -- correspondences and their fit claims; each placement is a claim
→ check(claims bearing on K) -- per bearing claim, what target-side fact within its scope would change it, and who can reach it; the reachable ones run within collection
→ warrant(claims, checks) -- read off evidence, never assent
→ judge(K) -- Licensed with limits, Blocked, or Undetermined with what is missing
→ surface(assessment) -- present and proceed; what is open is the person's own unknown
→ MappingAssessment
requires: uncertain(licenses(mapping)) -- declared by invoking /ground; judged only on the AI-guided path
deficit: MappingUncertain -- activation precondition
preserves: content_identity(R) -- output content invariant; the assessment is carried beside R
invariant: Warrant tracks cited evidence, never assent
invariant: The question stands only on the person's turn
-/
namespace Analogia
/-! ── 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}
/-- `R`: text carrying a source structure — a framework, an analogy, an earlier design, an
abstraction — and the target it is applied to: AI output, user analysis, or an external
reference. The morphism processes it uniformly; it is bound by R-BINDING and read from the
context, as the positions of its turns. -/
abbrev Text (c : Context P) := List (Fin c.length)
/-- A part of the source or the target structure; where an abstraction is tested against its own
cases, a target component's name says which case it belongs to. -/
structure Component where
name : String
structure_ : String
/-- A source component and its target counterpart, related by `relation`: the source relation the
correspondence carries — one relation, or a composite of relations read as one from its first
term to its last. -/
structure Correspondence where
/-- the source side -/
abstract : Component
/-- the target side -/
concrete : Component
relation : String
/-- One conclusion the mapping is being asked to license about the target: a prediction, a
permission, a limit, an expected behavior. -/
structure Inference where
claim : String
/-- Who first put the question forward: you, as a draft read from the context and shown with its
grounds, or the person. -/
inductive Proposer | draft | person
/-- What the person's turn that made the question stand did: set it in its own words, or took a
draft put forward before, as it was or corrected. -/
inductive Standing | set | adopted
/-- What a question asks: what the comparison is for, the conclusions at stake (`K`), and the
source and target — carried only where `R` and the context leave a materially different choice
of either open, `none` where they fix it. A question concerns one source–target pair. -/
structure Draft where
purpose : String
conclusions : List Inference
pair : Option (String × String)
/-- The question an audit answers: what it asks, with who first put it forward and how it came to
stand. -/
structure Question extends Draft where
proposer : Proposer
standing : Standing
/-- **Your judgment**: the cited turn establishes question `q` in `c`, in the whole scope that turn
asks — a turn asking about A and B supports no question narrowed to A — with conclusions to
audit. Where the purpose is to carry a structure over — a port, a migration, a sibling's shape
— and the turn asks nothing narrower, the conclusion is that the structure is preserved in the
target; the relations under it are what collection finds, never a list fixed here. A narrower
question the turn asks — whether the retries will match, say — is that turn's whole scope.
Where a located abstraction is tested against its own cases (the abstraction the source, its
cases the target), the conclusion for each case asked about is that it instantiates the
abstraction, and a collective relation asked of the cases together is one more conclusion, never
replaced by the per-case ones.
Articulating what a stated purpose entails is reading it; choosing among materially different
purposes, conclusions, or source–target pairs is not, and a pair `R` or a fact fixes is read,
not asked.
How the source reads is none of these choices, and the question is not left open on it. Once a
person's turn names which reading they mean, that turn fixes the sense of their question's
conclusions.
The question stands only on the person's turn that sets it in their own words
(`set`) or takes a draft you put forward, as it was or corrected (`adopted`); a draft counts
only where it was visible as yours, with its grounds, before that turn. A draft alone is a
proposal, and an instruction to do the next task takes none. Several drafts a turn takes
establish a question only where their whole scope is one pair's, without your choosing,
dropping, or conflating pairs; otherwise the question stays open. -/
axiom QuestionSupported : Context P → Turn P → Question → Prop
/-- The question stands only on a person's turn: this audit closes on evidence, so no later turn of
theirs would cover a question you chose. -/
def questionCoord : Coord P Question :=
{ admits := (·.val = .person), supports := QuestionSupported }
/-- **Your judgment**: how the question stands in `c`, read again against the context as it now
stands. -/
axiom question : (c : Context P) → Occ (questionCoord (P := P)) c
/-- **Your judgment**: the question you carry the audit forward on while the person's turns leave
it open — its purpose, conclusions, and pair read from the context as `QuestionSupported` reads
a turn's question, the whole scope asked, per-case and collective conclusions; `none` where you
carry none forward. -/
axiom draft : Context P → Option Draft
/-- `K`: the conclusions of the question that stands, or, while it is open, of your draft. -/
def inferences (c : Context P) : List Inference :=
match question c with
| .filled q .. => q.conclusions
| .open_ _ => match draft c with
| some d => d.conclusions
| none => []
/-- The question stands: it is filled on a person's turn. -/
def QuestionStands (c : Context P) : Prop :=
match question c with
| .filled .. => True
| .open_ _ => False
/-- There are conclusions to audit, on the question that stands or on your draft. -/
def ToAudit (c : Context P) : Prop := inferences c ≠ []
inductive FitLabel
/-- the target structure preserves the source relation -/
| preserved
/-- a correspondence exists, but some of its structural dimensions lack evidence -/
| «partial»
/-- the source relation adds constraints the target does not support -/
| overextended
/-- What fit assessment asserts; every placement, `preserved` included, is a claim that can be
warranted or defeated. -/
inductive FitClaim
| fit (c : Correspondence) (l : FitLabel)
/-- a source component with no evidenced correspondent in the target; where an abstraction is
tested against its own cases, `inCase` names the case it is missing in, and is `none`
otherwise -/
| missing (x : Component) (inCase : Option String)
/-- **Your judgment**: the fit claims over the correspondences constructed from what collection
found, each distinct claim once — each correspondence in exactly one cell, and every source
component with no evidenced correspondent missing — where an abstraction is tested against its
own cases, missing in each case that has none, that case named. They cover the composite of
every chain of source relations a conclusion of `K` rests on; under the preservation conclusion,
the chains the source itself runs as one or asserts equal to another path. A step whose
endpoints have counterparts but whose relation has none is that step's correspondence placed
`overextended`, reported as a step with no counterpart. -/
axiom fitClaims : Context P → List FitClaim
/-- **Your judgment**: whether `x` bears on `k` — its verdict would change if `x` changed, under any
of the source's materially different readings (`references/judgments.md` §collection) where it
has several. A source feature the target lacks bears on `k` only where `k` needs that feature;
under the preservation conclusion every source relation is needed, and a missing counterpart is
reported as missing. Whether an absence was meant is the person's to say — their turn can narrow
the conclusion — never yours to infer. Where `k` is that a case instantiates an abstraction,
what bears is what the abstraction actually requires of that case: a feature it leaves optional,
absent there, is no misfit. Direction: `references/judgments.md` §BearsOn. -/
axiom BearsOn : Context P → FitClaim → Inference → Prop
/-- A fit claim a conclusion of the question audited turns on. -/
def Relevant (c : Context P) (x : FitClaim) : Prop := ∃ k ∈ inferences c, BearsOn c x k
/-- Who can carry a check out. `userHeld` is context only the user holds; it is met by what the
user reports observing, and otherwise it is shown as their own unknown. -/
inductive Reach
| aiReachable (action : String)
| userHeld (question : String)
inductive Bearing | supports | defeats
/-- **Your judgment**: the cited turn establishes, within `scope`, that it supports or defeats
`x`. A citation's stated bearing is read against its source and scope. Where the evidence
would fit a materially different explanation as well, read it against that explanation too:
evidence as expected under either explanation supports neither. A turn of any admitted origin
bears only through what it reports observing or the source content it carries — a result run, a
source read — read against the claim and scope; assent, agreement, or bare endorsement
establishes nothing here, whatever its form or origin. -/
axiom CheckSupported : FitClaim → String → Context P → Turn P → Bearing → Prop
def checkCoord (x : FitClaim) (scope : String) : Coord P Bearing :=
{ admits := fun _ => True, supports := CheckSupported x scope }
/-- The check on fit claim `x`. -/
structure Check (c : Context P) (x : FitClaim) where
scope : String
/-- a target-side fact or observable result that, within `scope`, would require the claim to
change -/
wouldChangeIt : String
/-- `none`: reachable by neither party now; say what is missing -/
reach : Option Reach
state : Occ (checkCoord x scope) c
/-- further cited grounds beside the one that fills the state -/
more : List (Cite c)
/-- **Your judgment**: the one check on a fit claim bearing on `K`, its state read off the grounds
the context now holds; a claim that bears on nothing asked has none. Direction:
`references/judgments.md` §checks. -/
axiom check : (c : Context P) → (x : FitClaim) → Relevant c x → Check c x
open Classical in
/-- Every check of a pass: exactly one per fit claim bearing on `K`, none for any other. -/
def checks (c : Context P) : List (Σ x : FitClaim, Check c x) :=
(fitClaims c).filterMap fun x => if h : Relevant c x then some ⟨x, check c x h⟩ else none
inductive Warrant | open_ (missing : String) | supported | defeated
def Check.warrant {c : Context P} {x : FitClaim} (ch : Check c x) : Warrant :=
match ch.state with
| .open_ _ => .open_ ch.wouldChangeIt
| .filled .supports _ _ _ => .supported
| .filled .defeats _ _ _ => .defeated
/-- The grounds a verdict cites, each read as evidence — a person's report of what they observed
among them, never their assent (`CheckSupported`). -/
def Grounds (c : Context P) :=
{g : List (Cite c) // g ≠ []}
inductive Verdict (c : Context P)
/-- grounds support the whole conclusion at its asked scope, with a met check for every fit
claim bearing on it; `limits` is that supported reach -/
| licensed (g : Grounds c) (limits : String)
/-- a decisive ground against this route to the conclusion; it does not make the conclusion
false -/
| blocked (g : Grounds c)
/-- what is missing and who can reach it; never a check this session can reach and has not
run -/
| undetermined (missing : String)
/-- **Your judgment** per conclusion, reading the grounds' bearing on `k` rather than a
label-to-verdict polarity. Where the verdict on `k` turns on which of the source's materially
different readings holds, `k` is Undetermined, its `missing` naming the reading as the person's
to say, with each reading's verdict and grounds shown side by side; where the readings reach the
same verdict, judge it plainly. Direction: `references/judgments.md` §judge. -/
axiom judge : (c : Context P) → Inference → Verdict c
inductive Pref | adopted | setAside
/-- **Your judgment**: the cited turn of the person's adopts or sets aside conclusion `k` — takes it
into, or leaves it out of, what they carry over. An instruction to do the next task adopts
nothing; where their turns conflict, it stays open. -/
axiom PrefSupported : Inference → Context P → Turn P → Pref → Prop
/-- What the reader takes up. It never moves a warrant or a verdict; a conclusion adopted over a
Blocked or Undetermined verdict stands as accepted and evidentially disputed. -/
def prefCoord (k : Inference) : Coord P Pref :=
{ admits := (·.val = .person), supports := PrefSupported k }
/-- **Your judgment**: how the person's adoption of `k` stands in `c`. -/
axiom preference : (c : Context P) → (k : Inference) → Occ (prefCoord k) c
/-- **Your collection** from `c`, to the limit of your own reach, over what the mapping rests on:
the source's relations and their counterparts in the target, the checks on the fit claims
bearing on `K`, and every one collection exposes; where to look is yours to judge, and no list
of sources bounds it. A source or target account you can reach, you read yourself, and what you
say you read, you read whole. Each place you look returns an evidence turn, a null result
included, so the places looked stay in the context by name. Where collected material conflicts,
name what conflicts with what and show it, not only as a check's grounds. What the context
already holds from a source is not fetched again unless an utterance, evidence, or your own work
since says it changed. Read and run without changing existing state; what you create only to
look you remove afterwards. An observation that needs to change existing state, someone's
permission, or another's authority is not made and leaves no evidence turn: name it, with what
it needs, in what you present, and leave it open. Where a claim turns on what an artifact does,
exercise it over the case that separates the explanations. Collection includes trying the
construction it needs: a reachable check that constructing the correspondences over what was
collected exposes is run within collection as well. What is still open once collection ends is
shown as the person's own unknown. Direction: `references/judgments.md` §collection. -/
axiom observe : Context P → List (Evidence P)
def collect (c : Context P) : Context P := c ++ (observe c).map (·.val)
/-- **Your judgment**: the latest utterance, read whole against `R` and the fused context, bears on
this audit — a purpose, a conclusion, a source or target, a fact, a source to read, a
counterexample, a result from running something. One that bears on none of it leaves the audit
as it stands: the session answers it, that answer stays in the context, and no pass opens.
Adopting or setting aside a conclusion alone opens no pass: it moves no warrant or verdict,
and the session acknowledges it — reading `preference` for that conclusion and showing the
adoption apart from its verdict; an adoption over a Blocked or Undetermined verdict is shown as
accepted and evidentially disputed, with those grounds visible. Taking a drafted question, or
setting the question in the person's own words, makes it stand and opens a pass. A turn that
brings this audit a relevant new ground — a fact, a source, a counterexample, a result — bears
on it whatever its grammatical form, a question included; a question about this audit opens a
pass unless the current grounds answer it entirely; a question about other work is the
session's. -/
axiom BearsOnRun : Context P → Prop
/-- What an assessment carries, read off the contract's own readings over the collected context:
each conclusion of `K` with its verdict, and every check. Adopting or setting aside a
conclusion stays where `preference` reads it. -/
structure Assessed (c : Context P) where
verdicts : List (Inference × Verdict c)
checks : List (Σ x : FitClaim, Check c x)
def assessed (c : Context P) : Assessed c :=
{ verdicts := (inferences c).map fun k => (k, judge c k)
checks := checks c }
/-- Where the audit stands. Each carries the context it was reached on and the relay that
presents it. -/
inductive Outcome (P : Type)
/-- nothing to audit. A run status, not a closure. -/
| holding (c : Context P) (relay : Response P)
/-- Once it has run, the person can say, for each conclusion they expect a framework, analogy,
earlier design, or abstraction to carry to the target: the source relation, or chain of
relations, that carries it; what was checked in the target and found, and where — on the
composite, for a chain; what difference would break it; and whether it holds and how far,
is blocked, or stays undetermined, with what is missing and who can reach it.
`MappingAssessment` over the collected context `c`, on the question that stands on the
person's turn or on your draft, and which of the two: every
conclusion's verdict with its grounds and limits, every check with its warrant, scope,
defeater and reach, the places reached and those not, and what is open as the person's own
unknown. Not an endorsement of the mapping. -/
| assessment (c : Context P) (toAudit : ToAudit c) (record : Assessed c)
(relay : Response P)
/-- The context once the outcome's relay is presented. -/
def Outcome.context : Outcome P → Context P
| .holding c r => c ++ [r.val]
| .assessment c _ _ r => c ++ [r.val]
/-! ── R-BINDING ──
bind(R) = explicit_arg ∪ current_output ∪ most_recent_output
Priority: explicit_arg > current_output > most_recent_output
/ground "text" → R = "text"
/ground (alone) → R = the most recent relevant output in the session, the AI's or the user's
"ground this..." → R = the text currently under discussion
"does this abstraction hold across its cases?" → R = a candidate abstraction and the
instances it claims to subsume → self-grounding
With no relevant text, the first pass asks for the material to audit; it invents no candidate.
-/
/-! ── MODE STATE ──
Λ is the fused context and nothing else; every reading above is taken from it.
-/
/-! ── PHASE TRANSITIONS ──
A step is one arm of a structural recursion over the person's utterances, carrying the context as
it stands and the last outcome. `respond` is your relay for what a pass presents — the question
or the assessment; `session` is the session's own answer to an utterance that does not bear on the audit, which stays in the context without
opening a pass.
-/
open Classical in
/-- One pass. With nothing to audit, that is presented and nothing is collected. Otherwise
collection runs; where the collected context leaves nothing to audit, that is presented;
otherwise the assessment is. -/
def pass (respond : Context P → Response P) (c : Context P) : Outcome P :=
if ¬ ToAudit c then .holding c (respond c)
else
let c₂ := collect c
if h : ToAudit c₂ then .assessment c₂ h (assessed c₂) (respond c₂)
else .holding c₂ (respond c₂)
open Classical in
/-- One utterance, read whole, each answered once: a turn bearing on the audit opens a pass; any
other turn — one turning away from an open question included — is the session's, kept in
the context, and the last outcome stands. -/
def step (respond session : Context P → Response P) (c : Context P) (o : Outcome P)
(u : Utterance P) : Context P × Outcome P :=
let c' := fuse c u
if BearsOnRun c' then
let o' := pass respond c'
(o'.context, o')
else (c' ++ [(session c').val], o)
def ground (respond session : Context P → Response P) :
Context P → Outcome P → List (Utterance P) → Outcome P
| _, o, [] => o
| c, o, u :: us =>
let r := step respond session c o u
ground respond session r.1 r.2 us
/-- The audit opens on a pass. -/
def start (respond session : Context P → Response P) (c : Context P)
(us : List (Utterance P)) : Outcome P :=
let o := pass respond c
ground respond session o.context o us
/-! ── LOOP ──
Every utterance is read whole against the context as it now stands: nothing counts passes or
reconstructions, and no earlier reading is held apart from what later turns say. A changed
purpose, conclusion, source or target, or a new ground is simply the context the next pass reads;
evidence already gathered stays in the context, and every verdict is judged again over the
question now audited. Silence takes nothing: the last outcome stands, and an open question stays
open. Adoption changes no warrant or verdict. Stopping in the middle of a pass is the
harness's interrupt.
-/
/-! ── CONVERGENCE ──
assessed: a pass over the question that stands on the person's turn or over your draft, named
which, in which collection reached what it could, and every
conclusion in K carries a verdict — Licensed with its limits, Blocked, or Undetermined naming
what is missing and who can reach it. Undetermined does not block the
assessment and is not settled by it; a check this session can reach and has not run is run, not
reported Undetermined. Convergence evidence: the question with the person's turn it stands on,
who first put it forward, and whether that turn set it or took a draft, or your draft with its
grounds where the question is open — the purpose, K, and the source and target audited, with
the turn or fact that fixed them, or the person's answer or your draft where the choice was
open; the reading the person named, with the turn that named it, where a conclusion's
sense was fixed that way; for each k in K, one line
(MappingUncertain(k) → verdict(k)) showing the source relation, or chain of relations, that
carries it, the correspondences it rode on, the likenesses, the differences in both directions,
and the unknowns; where an abstraction is tested against its own cases, for a Licensed verdict
that a case, or the cases together, instantiate the abstraction, its level of abstraction and
consequence concrete enough to fail, and the contrast that makes its fit diagnostic or that none
was reachable;
for each checked fit claim, its label, warrant (`Check.warrant`), and scope beside the grounds,
the stated defeater, the reach or its absence, whether the check was unmet, survived, or
failed, and any materially different explanation the evidence fits as well; correspondences
outside the checked scope named as outside it; the places collection
reached and those it did not, by name; where collected material conflicts, what conflicts with
what; what is still open, as the person's own unknown. An unmet
check is reported as unmet, never as a pass; a claim whose warrant is open is named open rather
than weakly supported. Adoption is reported apart from warrant and never as a reason; a
conclusion adopted over a Blocked or Undetermined verdict is shown as accepted and evidentially
disputed. Carry any change to the question, distinguishing conclusions removed from scope from
conclusions answered. 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 | questionRead | questionDraft | questionReadback | collect | construct | checkRead
| warrantRead | judge | surface | converge | readAnswer | seam
def grounding : Op → Annot × String
| .questionRead => (.sense, "Internal analysis: how the question stands on the person's turns — the purpose, the conclusions at stake in the whole scope asked, and whether R and the context leave a materially different choice of source or target open")
| .questionDraft => (.interaction .extension, "where the person's turns leave the question open: with material in the context to draft from, the question drafted from it — the purpose, the conclusions, and the source–target pair where open — with its grounds, and where materially divergent questions are open, each candidate with its grounds and what it would audit, shown whether or not one is carried forward, for the person to take, correct, or replace in their own words; with no referent to draft from, ask for the material to audit, inventing no candidate")
| .questionReadback => (.interaction .extension, "when the question stands, relay it as the user-facing realization reads it back; no approval required")
| .collect => (.observe, "artifact read, artifact search, record read, external fetch, environment run: collection as `observe` states")
| .construct => (.sense, "Internal analysis: the correspondences over what collection found and their fit claims")
| .checkRead => (.sense, "Internal analysis: one check per fit claim bearing on K, each with its scope, target-side defeater, and reach")
| .warrantRead => (.sense, "Internal analysis: each claim's warrant read off its check")
| .judge => (.sense, "Internal analysis: per conclusion, Licensed with limits, Blocked, or Undetermined with what is missing and who can reach it")
| .surface => (.interaction .extension, "the assessment with its trace, the places reached and not, what is open as the person's own unknown, and what a later turn would change; no verdict answer is required")
| .converge => (.interaction .extension, "the convergence evidence CONVERGENCE names; proceed with the assessment")
| .readAnswer => (.sense, "Internal analysis: the latest utterance read whole against R and the fused context as it now stands — whether it bears on the audit")
| .seam => (.interaction .extension, "the next move the person declared, citing that turn")
/-! ── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). Dimension resolution emergent via session context.
-/
end
end Analogia
Mode Activation
/ground remains directly invocable, and invoking it declares the deficit; it is not judged away. During AI-guided activation, loaded safety boundaries, capability restrictions, and explicit user instructions continue to bind.
Activation heuristics and exceptions
Activate where a mapping is being relied on and what it licenses about a case is open: an abstract framework applied to a concrete case, a structure carried over from an earlier design or a sibling, a possible structural mismatch, or a located abstraction tested against its own cases. Prior-session recall indices may seed where to look; they do not settle a constitutive judgment.
A source or target account this session can reach — code, documents, a repository, a published source — is read as evidence inside the audit, whether or not the reader already holds it; the audit never waits for the reader to bring an account first, and never asks them to judge a correspondence. Where what the reader wants is only to come to hold an account, with no mapping being relied on, that is explanation rather than this audit, and the AI-guided path does not activate. Absence of evidence that a mapping is being relied on establishes neither eligibility nor its lack; where the accumulated context does not settle it, say which reading is being used and continue.
Skip AI-guided activation when what the mapping licenses is already settled in context, or no mapping is being relied on. Forming an abstraction from cases, or reconsidering one from its cases, to fit what the person means is a different deficit. Framework selection, factual context insufficiency, and whether an already-produced result applies in its actual context remain their own primary deficits.
Evidence loading
Collect to the limit of your own reach over what the mapping rests on: read code, configuration, documentation, and other available artifacts where either structure is recorded there, and where the source or target structure lives primarily in external APIs, standards, scholarship, or industry material, fetch it and keep its source address visible in the trace. Name the places reached and those that could not be.
Where a claim turns on what an artifact does rather than on what it says about itself, exercise it over the case that separates the explanations and cite the result.
Protocol
User-facing realization
Before assessing, read back the question that stands — what the comparison is for, the conclusions at stake, and the source and target being audited — citing the person's turn it stands on — whether they set it or took your draft — and the turn or fact that fixed the source and target where R or the context did. Where their words leave any of it open, show the question you draft from the context as yours (TOOL GROUNDING questionDraft); where you carry the audit forward on it, the assessment says it rests on your draft. An instruction to do the next task takes no draft. A source and target that R or a fact fixes are read, not asked. When the question changes, show what was added, removed or reformulated and why; a removed conclusion is outside the revised question, not resolved.
Present the whole assessment in everyday language: the question; for each conclusion, the source relation, or chain of relations, that carries it, every correspondence it rides on with its fit claim, one concrete scenario, and what actually warrants that claim, the likenesses and the differences in both directions, and what is still unknown; and whether each conclusion holds, is blocked, or is undetermined, with how far it reaches. A source feature the target lacks counts against a conclusion only where that conclusion needs it; under the preservation conclusion, a missing counterpart is reported as missing, and whether an absence was meant is the reader's to say. Where a conclusion's verdict turns on which materially different reading of the source holds, show each reading with its verdict and grounds side by side, and name the reading they mean as the reader's to say.
Beside each claim that matters, state the scope its grounds were checked within, the target-side fact or observable result that would change it, any materially different explanation its evidence fits as well, and who can reach that evidence or why neither party currently can. Carry out the checks this session can reach before presenting, and name the places collection reached and those it could not; where collected material conflicts, name what conflicts with what. What is still open is shown as the person's own unknown, as the question it is. An unmet check is reported as unmet. A claim with nothing behind it is named as having nothing behind it rather than described as tentative.
Then state what a later turn would change, and proceed without asking for a verdict; next work the person requests follows TOOL GROUNDING seam. A later turn is read whole: one that bears on the audit — a changed purpose, conclusion, source or target, a fact, a source, a counterexample, a result from running something — is the context the next pass reads, and a question about this audit the current grounds answer entirely is answered without a new pass; evidence already gathered stays, and verdicts are judged again over the question now audited. Saying the mapping looks right moves nothing, and saying so is not a failing on the reader's part — it is what this surface is built not to need. Adoption is the reader's own turn taking a conclusion into, or setting it aside from, what they carry over; it opens no pass, and an instruction to do the next task adopts nothing. Adopting and setting aside are recorded as the reader's, kept apart from what the evidence shows, and never given as a reason a verdict came out the way it did; a conclusion adopted over a blocked or undetermined verdict stands as accepted and evidentially disputed, with its grounds shown. While the question is open, a turn that turns to other work is simply answered; the question stays open.
Read references/round-composition.md before composing when terminology must remain stable, wording must be carried unchanged, or material belongs to another round or trace.
Intensity
| Level | When | Format | |-------|------|--------| | Light | One conclusion, one obvious correspondence | Compact rendering of the same required assessment trace | | Medium | Several conclusions or partial correspondences | Required assessment trace grouped by conclusion and bearing claim | | Heavy | Complex transfer or structural mismatch | Required assessment trace with expanded presentation of evidence and instantiations |
Rules
- Warrant tracks evidence, never assent: Read each fit claim's warrant off the grounds actually cited for it. Agreement does not promote a claim and disagreement does not defeat one without a ground; what the user reports having observed is evidence like any other observation. Evidence that would fit a materially different explanation as well is read against that explanation too. Record what the reader adopts, report it apart from the evidence, and never offer it as a reason a verdict came out as it did.
- The question stands on the person's turn: Read the purpose, the conclusions at stake in the whole scope asked, and the source and target where that choice is open off the person's own words. Where they leave it open, the AI may draft the question, but its draft settles none of it — not the purpose, not conclusions narrower than the cited turn asks, not a choice between materially different sources or targets — because this audit closes on evidence and no later utterance of the user's would cover a question the AI made stand.
- Collect to the limit of reach: Collect over what the mapping rests on until nothing reachable is left; name the places reached and those that could not be; show what remains open as the person's own unknown, never as a stall. Where the purpose is to carry a structure over and the person's turn asks nothing narrower, audit whether the whole structure is preserved, with its relations found by collection.
- Judgment is over conclusions, not correspondences: Judge each conclusion on its own. A peripheral correspondence may stay open without holding the audit open, and no disposition of correspondences completes it. An undetermined conclusion completes the assessment; a reachable check left unrun does not.
- A chain is checked as a chain: A conclusion carried by a chain of source relations is licensed only with a met check on the composite. Evidence that defeats preservation through the composite blocks that route, never the conclusion's truth. A Licensed preservation verdict names in its limits the relations and composites checked.
- A reading the source leaves open is shown, not chosen: Where a conclusion's verdict turns on which materially different reading of the source holds, it stays Undetermined with each reading's verdict and grounds shown side by side; the person's turn naming the reading they mean fixes the sense of the conclusions, and they are judged again on it.
- Self-grounding judges each case: Where an abstraction is tested against its own cases, each case asked about gets its own verdict and a collective relation asked of them is judged on its own; a Licensed verdict that a case, or the cases together, instantiate the abstraction names the level of abstraction its fit is claimed at and a consequence concrete enough to fail, shows the contrast that makes the fit diagnostic, and where none was reachable its limits say the fit was not shown to be diagnostic.
- Every bearing claim carries its own defeater: For each fit claim a conclusion turns on, state what target-side fact or observable result, within that claim's own scope, would require it to change, and who can reach that evidence. The builder and the checker being the same process is not the defect; a claim with no stated way to be wrong is. A check nobody ran is reported unmet.
- Round composition: Keep each correspondence beside its nearest evidence, scenario, warrant, and next-move implication. Which turn opens a pass is
BearsOnRun's reading; the reader is never asked to classify their own turn. - Structural evidence: Cite the specific source and target structures supporting each correspondence, and include a concrete target-domain instantiation. Where a claim turns on an artifact's behavior, exercise the artifact and cite what it did; its own account of that behavior evidences the claim made, not the behavior.
- Bounded reach: State the limits supported by the cited grounds and their checked scopes in the same breath as every Licensed verdict. A mapping presented without its breaking point produces confident wrong inference, which is the failure this protocol exists to catch.
- Form feedback: Derive each round's density from the current request and carry an explicit form instruction until countermanded. Change the form directly. Elements fixed elsewhere remain fixed; state what changed and, where the instruction overlaps a fixed element, what stays and why.