/ground

name: ground
description: "A framework, analogy, or earlier design is carried to a case, or an abstraction tested: the user can say what carries each conclusion, what would break it, and if it holds, is blocked, or is open."

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 rep