From ambiguous utterances to governed reuse classes: canonicalization, quotient invariance, and conditional decidability

# From ambiguous utterances to governed reuse classes: canonicalization, quotient invariance, and conditional decidability1footnote 11footnote 1This note extracts and hardens the canonicalization layer of the working paper Certified Resolution: A Formal Theory of Governed Answer Spaces for Enterprise AI (Minerva CQ, 2026).
Source: [https://arxiv.org/html/2607.10069](https://arxiv.org/html/2607.10069)
Ray Garcia[ray@minervacq\.com](https://arxiv.org/html/2607.10069v1/mailto:[email protected])Minerva CQ \(Bourbaki Intelligent Systems, Inc\.\), Los Gatos, CA, USA

###### Abstract

Semantic caching defines answer reuse on embedding similarity: two utterances share a stored answer when a similarity score clears a threshold, with no notion of authorization, versioning, or of what makes two demands the*same*\. This note changes the object on which reuse is defined: in a governed domain, reuse should operate on a mathematically characterized quotient of resolved conversational demands, not on a similarity heuristic\. Three independently defined relations on resolved utterances—reading identity, resolution identity, and reuse identity—form a refinement chain, strict under realized nondegeneracy conditions checkable on deployment logs; the pipeline’s outputs are invariant along the chain, and reuse identity is exactly the kernel of the resolution map into the governed answer partition, so the reuse quotient is the utterance\-side object that partition induces, not a relabeling of it\. Reuse identity licenses the governed query key and its certified answer space; reuse of a particular answer requires resolution identity or an applicability certificate\. The supporting layer is stated at exactly the strength proved: exact\-denotation normal forms; join aggregation as a design operator, with closure\-stable cells characterizing no\-escape; total computability of the full pipeline relative to an untrusted proposal layer; policy admissibility for arbitrary proposers— and provably not factual grounding or intent fidelity; and elicitation terminating after finitely many informative replies, sound under target consistency\.

###### keywords:

formal semantics of questions , closure systems , canonical forms , Datalog , decidability , AI governance

††journal:Information Processing Letters## 1Problem

A governed conversational system—one whose answers must be licensed by a corpus of policies, regulations, and standard operating procedures—receives utterances, not questions\. “Tell me about Paris,” “can you do something about this fee?,” “what about last month?” are ambiguous along at least three axes: which question is being asked, whether the domain is competent to answer it at all, and whether enough material facts have been disclosed to single out one answer\. Retrieval pipelines dissolve the problem by ranking documents against the raw utterance; the cost is that the system has no representation of the question it is answering, hence no principled notion of when two utterances ask the*same*governed question—the property on which certified answer reuse depends\. Semantic caching substitutes a similarity threshold for that notion\[[7](https://arxiv.org/html/2607.10069#bib.bib7)\]; this note replaces the threshold with a quotient: the central object is the surjectionUres↠ℛcU\_\{\\mathrm\{res\}\}\\twoheadrightarrow\\mathcal\{R\}\_\{c\}, whereℛc:=Ures/≡reuse\\mathcal\{R\}\_\{c\}:=U\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{reuse\}\}is the*realized governed reuse space*—the quotient of resolved utterances by governed reuse identity \(abstentions are terminal outcomes, held outside the quotient\)—and the theorems below say when that map is well\-defined, what it is invariant under, and what it does and does not guarantee\. Figure[1](https://arxiv.org/html/2607.10069#S1.F1)is the whole paper in one picture: reading identity, resolution identity, and reuse identity form a chain of coarsening surjections, and certified reuse is defined on the rightmost quotient\.

UresU\_\{\\mathrm\{res\}\}resolved utterances\(abstentions exit viaAA\)Ures/≡readU\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{read\}\}same surviving readingsmod≡Φt\\equiv\_\{\\Phi\_\{t\}\}Ures/≡resU\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{res\}\}same resolvedpropositiona​\(u\)a\(u\)ℛc=Ures/≡reuse\\mathcal\{R\}\_\{c\}=U\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{reuse\}\}realized governed reuse space:same cell==reuse classRND1RND2invariant: fullresolved outcomeinvariant:Canon​\(a​\(u\)\)\\mathrm\{Canon\}\(a\(u\)\)certified answerinvariant:Canoncell​\(C\)\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\)reuse key

Figure 1:The quotient hierarchy of Theorem[1](https://arxiv.org/html/2607.10069#Thmtheorem1)\. Each arrow is a coarsening surjection; strictness holds under the realized nondegeneracy conditions RND1–RND2; abstentions are terminal outcomes under the mode mapAA, not classes of the quotient\. Certified reuse is defined on the rightmost quotient\.One clarification prevents the objection that this is a relabeling\. The governed answer partitionP​\(c\)P\(c\)lives on*worlds*; the reuse quotient lives on*utterances*\. The content of the construction is not the codomain but the factorization: the resolution mapres:Ures→P​\(c\)\\mathrm\{res\}:U\_\{\\mathrm\{res\}\}\\to P\(c\), assigning each resolved utterance its cell, factors throughℛc\\mathcal\{R\}\_\{c\}with≡reuse\\equiv\_\{\\mathrm\{reuse\}\}exactly its kernel \(Corollary[2](https://arxiv.org/html/2607.10069#Thmcorollary2)\)—and proving that this map is well\-defined on auditable pipeline artifacts, invariant under the finer identities, strict under realized conditions, and computable relative to an untrusted proposal layer is precisely what a similarity threshold cannot offer\. The quotient is moreover generally*smaller*than the partition: a cell with no realized utterance is a governed question no one has asked, soℛc\\mathcal\{R\}\_\{c\}measures realized demand, not corpus structure\.

We work in the governed\-answer\-space framework\[[1](https://arxiv.org/html/2607.10069#bib.bib1)\]\. Fix a contextccwith finite live\-world setWcW\_\{c\}, an admissibility closureclc\\mathrm\{cl\}\_\{c\}on℘​\(Wc\)\\wp\(W\_\{c\}\)\(extensive, monotone, idempotent\) induced by the governing corpusΦt\\Phi\_\{t\}in force at timett, the fiberL​\(c\)=Fix​\(clc\)L\(c\)=\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)of admissible propositions, an answer partitionP​\(c\)P\(c\)onWcW\_\{c\}in the sense of partition semantics\[[2](https://arxiv.org/html/2607.10069#bib.bib2)\], and a specificity thresholdσ​\(c\)\\sigma\(c\)read as partition fineness\. The order convention is fixed once: entailment is inclusion,X⊑Y⇔X⊆YX\\sqsubseteq Y\\iff X\\subseteq Yas sets of worlds, so a*more specific*proposition is*smaller*, anda⊑σ​\(c\)a\\sqsubseteq\\sigma\(c\)reads “aais at least as specific as the threshold”—specificity tightens downward in the lattice\. All results are relative to the snapshotL​\(c,t\)L\(c,t\); canonicity is theory\-relative, and a corpus revision re\-indexes the partition and the normal forms\.

Two disciplines are separated throughout\. The*proposal layer*—an untrusted language model—classifies discourse function and proposes candidate formal readings of the utterance\. The*verification layer*—the governed machinery—decides admissibility, specificity, and cell assignment\. The theorems live in the verification layer; the proposal layer enters only through an explicit computability assumption \(A1\), so the decidability claims are conditional and stated as such\.

## 2The pipeline, its gates, and its objects

Fix a finite relational signatureΣ\\Sigmaadequate forWcW\_\{c\}: each worldw∈Wcw\\in W\_\{c\}is an*effectively presented*finiteΣ\\Sigma\-structure and each is distinguished by a ground description, so satisfactionw⊧φw\\models\\varphiof closedΣ\\Sigma\-formulas is decidable and*every*set of worlds—in particular every cell ofP​\(c\)P\(c\)and every admissible proposition—is defined exactly by some closedΣ\\Sigma\-formula \(formula–cell adequacy, Condition FA below\)\. Propositions, cells, and the thresholdσ​\(c\)\\sigma\(c\)are represented asnn\-bit vectors overWcW\_\{c\}\(n=\|Wc\|n=\|W\_\{c\}\|\), so inclusion tests costO​\(n\)O\(n\)\. LetFm\\mathrm\{Fm\}be the closedΣ\\Sigma\-formulas under a fixed effective enumeration, and let≺\\precbe the induced length\-lexicographic total order—total, computable, and fixed once for the deployment\. Theory equivalence, writtenφ≡Φtψ\\varphi\\equiv\_\{\\Phi\_\{t\}\}\\psi, means⟦φ⟧=⟦ψ⟧\\llbracket\\varphi\\rrbracket=\\llbracket\\psi\\rrbracketoverWcW\_\{c\}; on a finite materialized fiber it is decidable\.

###### Assumption 1\(A1: proposal layer\)\.

There are total computable functionsC:U→\{0,1\}C:U\\to\\\{0,1\\\}\(discourse\-function classifier:C​\(u\)=1C\(u\)=1iffuuis a canonical inquiry—ignorant speaker, competent addressee, genuine gap\-filling\[[3](https://arxiv.org/html/2607.10069#bib.bib3)\]\) andDc:U→℘fin​\(Fm\)D\_\{c\}:U\\to\\wp\_\{\\mathrm\{fin\}\}\(\\mathrm\{Fm\}\)\(finite candidate reading set\)\. Nothing is assumed about their*correctness*; only totality and computability\.

The pipeline, givenuu:Gate 1\(canonicity\): ifC​\(u\)=0C\(u\)=0, route out of the certified pathway\.Gate 2\(admissibility\): retain the readingsφ∈Dc​\(u\)\\varphi\\in D\_\{c\}\(u\)with⟦φ⟧∈Fix\(clc\)\\llbracket\\varphi\\rrbracket\\in\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)\.Gate 3\(specificity\): retain those with⟦φ⟧⊑σ\(c\)\\llbracket\\varphi\\rrbracket\\sqsubseteq\\sigma\(c\)\. WriteDc∗​\(u\)D\_\{c\}^\{\\ast\}\(u\)for the survivors\.*IfDc∗​\(u\)=∅D\_\{c\}^\{\\ast\}\(u\)=\\emptyset, the pipeline routes to governed abstention before any aggregation*—the empty join would beclc​\(∅\)\\mathrm\{cl\}\_\{c\}\(\\emptyset\), and∅⊆C\\emptyset\\subseteq Cholds for every cell, so cell assignment over an empty survivor set is ill\-posed and is excluded by fiat\. Otherwise, if the surviving denotations lie in exactly one cell and their aggregation \(Definition[4](https://arxiv.org/html/2607.10069#Thmdefinition4)\) passes its domain check, the pipeline*resolves*; in all other cases it routes to governed abstention \(§[6](https://arxiv.org/html/2607.10069#S6)\)\. A reading can fail more than one gate \(an inadmissible reading may also be under\-specific\); the pipeline reports the*first*failing gate, yielding operationally distinguishable abstention modes—non\-canonical, inadmissible, under\-specific, cell\-ambiguous—and none is repaired by guessing\.

### 2\.1The question object and the two normal forms

Two conflations must be blocked at the level of definitions: a cell is not a question, and a formula denoting a subset of a proposition is not a normal form for it\.

###### Definition 1\(Cell\-indexed governed query\)\.

For a cellC∈P​\(c\)C\\in P\(c\), the governed queryQCQ\_\{C\}is the query whose admissible responses are exactly

Ans​\(QC\)=\{a∈Fix​\(clc\):a≠∅,a⊆C,a⊑σ​\(c\)\},\\mathrm\{Ans\}\(Q\_\{C\}\)\\;=\\;\\bigl\\\{\\,a\\in\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)\\;:\\;a\\neq\\emptyset,\\ a\\subseteq C,\\ a\\sqsubseteq\\sigma\(c\)\\,\\bigr\\\},the normatively answerable propositions whose denotation lies inCC\. We callCCthe*positive resolution region*ofQCQ\_\{C\}\.

###### Definition 2\(Cell normal form; the reuse key\)\.

ForC∈P​\(c\)C\\in P\(c\), letF\(C\)=\{φ∈Fm:⟦φ⟧=C\}F\(C\)=\\\{\\varphi\\in\\mathrm\{Fm\}:\\llbracket\\varphi\\rrbracket=C\\\}and

Canoncell​\(C\)=min≺⁡\(arg⁡minφ∈F​\(C\)⁡\|φ\|\)\.\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\)\\;=\\;\\min\\nolimits\_\{\\prec\}\\bigl\(\\arg\\min\_\{\\varphi\\in F\(C\)\}\|\\varphi\|\\bigr\)\.Canoncell​\(C\)\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\)is the canonical presentation of the positive resolution region ofQCQ\_\{C\}, and the reuse class of an utterance is keyed byCanoncell\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}of its resolved cell, not by any particular reading\.

###### Definition 3\(Proposition normal form, exact denotation\)\.

Let

Dom\(Canonc\)=\{a∈Fix\(clc\):\\displaystyle\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\)\\;=\\;\\bigl\\\{\\,a\\in\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)\\;:\\;\{\}a≠∅,a⊑σ​\(c\),\\displaystyle a\\neq\\emptyset,\\ a\\sqsubseteq\\sigma\(c\),∃C∈P\(c\)witha⊆C\}\.\\displaystyle\\exists\\,C\\in P\(c\)\\ \\text\{with\}\\ a\\subseteq C\\,\\bigr\\\}\.Nonemptiness is essential and does real work: sinceP​\(c\)P\(c\)is a partition, a*nonempty*aacontained in a cell is contained in*exactly one*cell, so “the cell ofaa” is well\-defined on the domain—whereas∅⊆C\\emptyset\\subseteq Cholds for every cell, and admitting∅\\emptysetwould make cell assignment ill\-posed\. The exclusion also closes a re\-entry route for contradiction: the⊥\\botthat exactness bars from the normal form \(Remark[2](https://arxiv.org/html/2607.10069#Thmremark2)\) is equally barred from the resolution domain\. Fora∈Dom​\(Canonc\)a\\in\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\), letF\(a\)=\{φ∈Fm:⟦φ⟧=a\}F\(a\)=\\\{\\varphi\\in\\mathrm\{Fm\}:\\llbracket\\varphi\\rrbracket=a\\\}—*exact*denotation, not containment—andCanon​\(a\)=min≺⁡\(arg⁡minφ∈F​\(a\)⁡\|φ\|\)\\mathrm\{Canon\}\(a\)=\\min\_\{\\prec\}\(\\arg\\min\_\{\\varphi\\in F\(a\)\}\|\\varphi\|\)\.

###### Lemma 1\(Well\-definedness and computability\)\.

On a finite fiber,Canoncell\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}is a single\-valued total computable function onP​\(c\)P\(c\), andCanon\\mathrm\{Canon\}is a single\-valued total computable function onDom​\(Canonc\)\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\)that is moreover injective:Canon​\(a\)=Canon​\(a′\)\\mathrm\{Canon\}\(a\)=\\mathrm\{Canon\}\(a^\{\\prime\}\)impliesa=a′a=a^\{\\prime\}\.

###### Proof\.

Non\-emptiness ofF​\(C\)F\(C\)andF​\(a\)F\(a\)is Condition FA: every world set is defined exactly by some closed formula \(a disjunction of ground world descriptions\)\. The set of minimum\-length candidates is finite and nonempty; the fixed total computable order≺\\prectherefore selects a unique least element\. Computability: enumerate formulas in≺\\prec\-order; each test⟦φ⟧=a\\llbracket\\varphi\\rrbracket=ais a finite denotation check against the materialized fiber; the first formula passing is the normal form\. Injectivity is Remark[2](https://arxiv.org/html/2607.10069#Thmremark2)\. ∎

### 2\.2Aggregation, and the compatibility conditions

###### Definition 4\(Resolution aggregation—a design operator\)\.

Given a*nonempty*Dc∗​\(u\)D\_\{c\}^\{\\ast\}\(u\)\(the empty case having been routed to abstention upstream\), the*resolved proposition*is the deterministic join

a\(u\)=⋁φ∈Dc∗​\(u\)⟦φ⟧=clc\(⋃φ∈Dc∗​\(u\)⟦φ⟧\),a\(u\)\\;=\\;\\bigvee\_\{\\varphi\\in D\_\{c\}^\{\\ast\}\(u\)\}\\llbracket\\varphi\\rrbracket\\;=\\;\\mathrm\{cl\}\_\{c\}\\Bigl\(\\bigcup\_\{\\varphi\\in D\_\{c\}^\{\\ast\}\(u\)\}\\llbracket\\varphi\\rrbracket\\Bigr\),and the pipeline resolves iffa​\(u\)∈Dom​\(Canonc\)a\(u\)\\in\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\): the join must itself be nonempty, cell\-contained, and clearσ​\(c\)\\sigma\(c\), re\-checked*after*aggregation\. In particulara​\(u\)=∅a\(u\)=\\emptyset\(e\.g\. whenclc​\(∅\)=∅\\mathrm\{cl\}\_\{c\}\(\\emptyset\)=\\emptysetand only empty\-denotation readings survive\) fails the domain check and routes to governed abstention\.

###### Condition 1\(FA: formula–cell adequacy\)\.

Every set of worlds over the finite baseWcW\_\{c\}is defined exactly by some closedΣ\\Sigma\-formula\. \(Assumed throughout; discharged by including ground world descriptions inΣ\\Sigma\.\)

###### Condition 2\(CP: closure–partition compatibility\)\.

Every cell ofP​\(c\)P\(c\)is admissible:C∈Fix​\(clc\)C\\in\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)for allC∈P​\(c\)C\\in P\(c\)\.

###### Lemma 2\(CP characterizes no\-escape\)\.

For a cellC∈P​\(c\)C\\in P\(c\), the following are equivalent: \(i\)clc​\(S\)⊆C\\mathrm\{cl\}\_\{c\}\(S\)\\subseteq Cfor everyS⊆CS\\subseteq C; \(ii\)clc​\(C\)=C\\mathrm\{cl\}\_\{c\}\(C\)=C\. Hence under CP, if every surviving denotation lies in one cellCC, thena​\(u\)⊆Ca\(u\)\\subseteq C: closure\-induced cross\-cell escape cannot occur, and the post\-aggregation domain check can fail only at theσ\\sigma\-threshold\. Without CP, escape is possible, and the domain check of Definition[4](https://arxiv.org/html/2607.10069#Thmdefinition4)detects it and routes to elicitation\.

###### Proof\.

\(ii\)⇒\\Rightarrow\(i\): monotonicity givesclc​\(S\)⊆clc​\(C\)=C\\mathrm\{cl\}\_\{c\}\(S\)\\subseteq\\mathrm\{cl\}\_\{c\}\(C\)=C\. \(i\)⇒\\Rightarrow\(ii\): takeS=CS=Cand use extensivity,C⊆clc​\(C\)⊆CC\\subseteq\\mathrm\{cl\}\_\{c\}\(C\)\\subseteq C\. The consequence is \(i\) applied toS=⋃φ∈Dc∗​\(u\)⟦φ⟧⊆CS=\\bigcup\_\{\\varphi\\in D\_\{c\}^\{\\ast\}\(u\)\}\\llbracket\\varphi\\rrbracket\\subseteq C\. ∎

###### Condition 3\(TC: threshold re\-check\)\.

Theσ\\sigma\-comparison is applied toa​\(u\)a\(u\)after aggregation, not only to readings individually \(built into Definition[4](https://arxiv.org/html/2607.10069#Thmdefinition4)\); per\-reading specificity does not imply joint specificity, since the join is coarser than each reading\.

###### Condition 4\(PC: proof\-producing closure\)\.

The materialization ofclc\\mathrm\{cl\}\_\{c\}records, for everya∈Fix​\(clc\)a\\in\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\), a derivation witnessCertc​\(a\)\\mathrm\{Cert\}\_\{c\}\(a\)—on a ground Horn fiber, the how\-provenance of the forward\-chaining derivation ofaa’s generators\. The mapCertc\\mathrm\{Cert\}\_\{c\}is total onFix​\(clc\)\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\)and computable from the materialization, and each witness is bound to the fiber data\(Σ,Φt,c,t\)\(\\Sigma,\\Phi\_\{t\},c,t\)\. For the proof\-producing Horn materializations considered here, PC can be implemented as a bookkeeping discipline by recording compact derivation provenance \(a derivation DAG, not a fully expanded proof object\) during forward chaining, without changing the asymptotic materialization bound; for closures given in other forms, PC is an assumption on the implementation, which is why it is stated as a condition; it is what makes “carries a certificate” a derived property rather than an assertion \(Proposition[2](https://arxiv.org/html/2607.10069#Thmproposition2)\)\.

The stored artifact is per cell: the pair⟨\\langlenatural\-language normal form ofCanoncell​\(C\)\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\), first\-order witness⟩\\rangle; the cell normal form is the reuse key, andCanon​\(a​\(u\)\)\\mathrm\{Canon\}\(a\(u\)\)is the certified representative of the emitted answer within it\.

###### Example 1\(Running example: fee waiver vs\. refund\)\.

Contextcc: consumer billing, jurisdiction requiring a documented hardship finding before any late\-fee waiver\. Ground atoms include𝑓𝑒𝑒𝐴𝑠𝑠𝑒𝑠𝑠𝑒𝑑\\mathit\{feeAssessed\},ℎ𝑎𝑟𝑑𝑠ℎ𝑖𝑝𝐷𝑜𝑐\\mathit\{hardshipDoc\},𝑐𝑎𝑛𝑐𝑒𝑙𝑊𝑖𝑛𝑑𝑜𝑤𝑂𝑝𝑒𝑛\\mathit\{cancelWindowOpen\};P​\(c\)P\(c\)contains \(among others\) the cellsCwaiveC\_\{\\mathrm\{waive\}\}\(late\-fee waiver eligibility\) andCrefundC\_\{\\mathrm\{refund\}\}\(refund eligibility\), both admissible \(CP holds\)\. Utteranceu=u=“can you do something about this fee?” The proposal layer returnsC​\(u\)=1C\(u\)=1andDc​\(u\)=\{φ1,φ2,φ3\}D\_\{c\}\(u\)=\\\{\\varphi\_\{1\},\\varphi\_\{2\},\\varphi\_\{3\}\\\}:φ1\\varphi\_\{1\}\(waiver eligibility givenℎ𝑎𝑟𝑑𝑠ℎ𝑖𝑝𝐷𝑜𝑐\\mathit\{hardshipDoc\}\),φ2\\varphi\_\{2\}\(a syntactic variant withφ2≡Φtφ1\\varphi\_\{2\}\\equiv\_\{\\Phi\_\{t\}\}\\varphi\_\{1\}\), andφ3\\varphi\_\{3\}\(refund eligibility\)\. Gates 2–3 retain all three \(φ3\\varphi\_\{3\}is admissible—refunds are a licensed topic\)\. The surviving denotations meet*two*cells, souuis cell\-ambiguous and routes to elicitation \(§[6](https://arxiv.org/html/2607.10069#S6)\): the cell\-decided predicate𝑐𝑎𝑛𝑐𝑒𝑙𝑊𝑖𝑛𝑑𝑜𝑤𝑂𝑝𝑒𝑛∈ℰc\\mathit\{cancelWindowOpen\}\\in\\mathcal\{E\}\_\{c\}is asked; the reply “the cancellation window has closed” contradictsCrefundC\_\{\\mathrm\{refund\}\}\. NowDc∗​\(u\)=\{φ1,φ2\}D\_\{c\}^\{\\ast\}\(u\)=\\\{\\varphi\_\{1\},\\varphi\_\{2\}\\\},a\(u\)=⟦φ1⟧∨⟦φ2⟧=⟦φ1⟧∈Dom\(Canonc\)a\(u\)=\\llbracket\\varphi\_\{1\}\\rrbracket\\vee\\llbracket\\varphi\_\{2\}\\rrbracket=\\llbracket\\varphi\_\{1\}\\rrbracket\\in\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\)\(by CP the join stays inCwaiveC\_\{\\mathrm\{waive\}\}\), the resolved cell isCwaiveC\_\{\\mathrm\{waive\}\}, and the emitted governed question isQCwaiveQ\_\{C\_\{\\mathrm\{waive\}\}\}presented byCanoncell​\(Cwaive\)\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\_\{\\mathrm\{waive\}\}\)—in normal\-form English, “underΦt\\Phi\_\{t\}, is this customer eligible for a late\-fee waiver?”—with certified answerCanon​\(a​\(u\)\)\\mathrm\{Canon\}\(a\(u\)\)and reuse keyed by the cell\. A later utterance “does the hardship rule let you drop the late charge?” whose surviving readings are theory\-equivalent toφ1\\varphi\_\{1\}is reading\-equivalent to the post\-elicitationuuand, by Theorem[1](https://arxiv.org/html/2607.10069#Thmtheorem1), hits the same reuse class with no regeneration\.

## 3The equivalence hierarchy

The relation that keys reuse must be defined*without reference to*the normal forms, else invariance is a quotient triviality—and it is not one relation but three, at increasing coarseness\. All are auditable artifacts of the pipeline, not properties of strings\. One structural choice precedes them: abstentions are terminal outcomes, not members of reuse classes\.

###### Definition 5\(Resolution split and mode map\)\.

LetU1=\{u∈U:C​\(u\)=1\}U\_\{1\}=\\\{u\\in U:C\(u\)=1\\\}and letUres⊆U1U\_\{\\mathrm\{res\}\}\\subseteq U\_\{1\}be the utterances the pipeline resolves\. The*mode map*A:U1∖Ures→MA:U\_\{1\}\\setminus U\_\{\\mathrm\{res\}\}\\to Massigns each non\-resolving utterance its abstention mode: inadmissible, under\-specific, empty survivor set, cell\-ambiguous, or aggregation failure \(the post\-aggregation domain check\)\. Non\-canonical is deliberately*not*inMM: Gate\-1 rejects haveC​\(u\)=0C\(u\)=0and never enterU1U\_\{1\}, so the mode map’s domain begins after canonicity\.

###### Definition 6\(Three equivalences\)\.

All three relations are defined onUresU\_\{\\mathrm\{res\}\}:

1. \(i\)u≡readu′u\\equiv\_\{\\mathrm\{read\}\}u^\{\\prime\}\(*same surviving readings*\) iffDc∗\(u\)/≡Φt=Dc∗\(u′\)/≡ΦtD\_\{c\}^\{\\ast\}\(u\)/\\\!\\equiv\_\{\\Phi\_\{t\}\}\\;=\\;D\_\{c\}^\{\\ast\}\(u^\{\\prime\}\)/\\\!\\equiv\_\{\\Phi\_\{t\}\};
2. \(ii\)u≡resu′u\\equiv\_\{\\mathrm\{res\}\}u^\{\\prime\}\(*same resolved proposition*\) iffa​\(u\)=a​\(u′\)a\(u\)=a\(u^\{\\prime\}\);
3. \(iii\)u≡reuseu′u\\equiv\_\{\\mathrm\{reuse\}\}u^\{\\prime\}\(*same governed question*\) iffuuandu′u^\{\\prime\}resolve in the same cell ofP​\(c\)P\(c\)\.

The central object isℛc:=Ures/≡reuse\\mathcal\{R\}\_\{c\}:=U\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{reuse\}\}, the*realized governed reuse space*: the partition of resolved conversational demands into governed reuse classes\.

###### Theorem 1\(Refinement hierarchy and invariance\)\.

OnUresU\_\{\\mathrm\{res\}\},≡read⁣⊆⁣≡res⁣⊆⁣≡reuse\{\\equiv\_\{\\mathrm\{read\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{res\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{reuse\}\}\}always\. Because the equivalences are relations on utterances, strictness depends on which reading sets the proposal layer actually realizes, not only on the fiber; it holds under the following*realized*nondegeneracy conditions, and may collapse when the realized image ofDcD\_\{c\}is too poor:

1. \(RND1\)there existu,u′∈Uu,u^\{\\prime\}\\in UwithC​\(u\)=C​\(u′\)=1C\(u\)=C\(u^\{\\prime\}\)=1, both resolving, such thatDc∗\(u\)/≡Φt≠Dc∗\(u′\)/≡ΦtD\_\{c\}^\{\\ast\}\(u\)/\\\!\\equiv\_\{\\Phi\_\{t\}\}\\neq D\_\{c\}^\{\\ast\}\(u^\{\\prime\}\)/\\\!\\equiv\_\{\\Phi\_\{t\}\}anda​\(u\)=a​\(u′\)a\(u\)=a\(u^\{\\prime\}\)\(then≡read⁣⊊⁣≡res\{\\equiv\_\{\\mathrm\{read\}\}\}\\subsetneq\{\\equiv\_\{\\mathrm\{res\}\}\}\);
2. \(RND2\)there existu,u′∈Uu,u^\{\\prime\}\\in Uboth resolving in the same cell witha​\(u\)≠a​\(u′\)a\(u\)\\neq a\(u^\{\\prime\}\)\(then≡res⁣⊊⁣≡reuse\{\\equiv\_\{\\mathrm\{res\}\}\}\\subsetneq\{\\equiv\_\{\\mathrm\{reuse\}\}\}\)\.

Moreover, onUresU\_\{\\mathrm\{res\}\}, the entire resolved outcome—\(cell,a​\(u\)a\(u\),Canoncell\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\},Canon​\(a​\(u\)\)\\mathrm\{Canon\}\(a\(u\)\)\)—is invariant under≡read\\equiv\_\{\\mathrm\{read\}\}; the resolved proposition and its certified representative are invariant under≡res\\equiv\_\{\\mathrm\{res\}\}; and the governed question, the cell normal form, and the reuse class are invariant under≡reuse\\equiv\_\{\\mathrm\{reuse\}\}\. \(Abstention modes are*not*claimed invariant under surviving\-reading identity; Remark[6](https://arxiv.org/html/2607.10069#Thmremark6)\.\) Certified reuse of the query key is defined onℛc\\mathcal\{R\}\_\{c\}\.

###### Proof\.

*Inclusions\.*OnUresU\_\{\\mathrm\{res\}\}, every pipeline decision from the survivor set onward is a function of the set of denotations\{⟦φ⟧:φ∈Dc∗\(u\)\}\\\{\\llbracket\\varphi\\rrbracket:\\varphi\\in D\_\{c\}^\{\\ast\}\(u\)\\\}: cell incidence, the joina​\(u\)a\(u\), and the post\-aggregation domain check are all denotational\. Theory\-equivalent readings have equal denotations, so≡read\\equiv\_\{\\mathrm\{read\}\}forces equal denotation sets, hencea​\(u\)=a​\(u′\)a\(u\)=a\(u^\{\\prime\}\), giving≡read⁣⊆⁣≡res\{\\equiv\_\{\\mathrm\{read\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{res\}\}\}\. Ifa​\(u\)=a​\(u′\)a\(u\)=a\(u^\{\\prime\}\), then sincea​\(u\)∈Dom​\(Canonc\)a\(u\)\\in\\mathrm\{Dom\}\(\\mathrm\{Canon\}\_\{c\}\)is nonempty, the cell containing the common proposition is unique \(Definition[3](https://arxiv.org/html/2607.10069#Thmdefinition3)\) and shared, giving≡res⁣⊆⁣≡reuse\{\\equiv\_\{\\mathrm\{res\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{reuse\}\}\}\.

*Strictness\.*The witnesses are supplied by the conditions themselves: under RND1 the pair\(u,u′\)\(u,u^\{\\prime\}\)is≡res\\equiv\_\{\\mathrm\{res\}\}\- but not≡read\\equiv\_\{\\mathrm\{read\}\}\-related; under RND2 it is≡reuse\\equiv\_\{\\mathrm\{reuse\}\}\- but not≡res\\equiv\_\{\\mathrm\{res\}\}\-related\. Nothing further is needed, which is the point of quantifying over realized utterances\.

*Invariances\.*Under≡read\\equiv\_\{\\mathrm\{read\}\}, all decisions coincide as above\. Under≡res\\equiv\_\{\\mathrm\{res\}\},Canon​\(a​\(u\)\)=Canon​\(a​\(u′\)\)\\mathrm\{Canon\}\(a\(u\)\)=\\mathrm\{Canon\}\(a\(u^\{\\prime\}\)\)by single\-valuedness \(Lemma[1](https://arxiv.org/html/2607.10069#Thmlemma1)\) applied to the common proposition, computed against the same fixed\(Σ,≺,Φt\)\(\\Sigma,\\prec,\\Phi\_\{t\}\)\. Under≡reuse\\equiv\_\{\\mathrm\{reuse\}\},Canoncell\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}of the common cell coincides, and the reuse key is by definition a function of the cell\. ∎

###### Corollary 1\(Quotient observation\)\.

By injectivity ofCanon\\mathrm\{Canon\}\(Lemma[1](https://arxiv.org/html/2607.10069#Thmlemma1)\),Canon​\(a​\(u\)\)=Canon​\(a​\(u′\)\)\\mathrm\{Canon\}\(a\(u\)\)=\\mathrm\{Canon\}\(a\(u^\{\\prime\}\)\)impliesa​\(u\)=a​\(u′\)a\(u\)=a\(u^\{\\prime\}\), henceu≡resu′u\\equiv\_\{\\mathrm\{res\}\}u^\{\\prime\}andu≡reuseu′u\\equiv\_\{\\mathrm\{reuse\}\}u^\{\\prime\}: the resolution and reuse assignments factor through the proposition normal form\. \(This direction was invalid under containment\-basedF​\(a\)F\(a\); Remark[2](https://arxiv.org/html/2607.10069#Thmremark2)\.\)

###### Corollary 2\(Factorization; the quotient is not a relabeling ofP​\(c\)P\(c\)\)\.

Letres:Ures→P​\(c\)\\mathrm\{res\}:U\_\{\\mathrm\{res\}\}\\to P\(c\)assign each resolved utterance the cell ofa​\(u\)a\(u\)\(well\-defined by nonemptiness, Definition[3](https://arxiv.org/html/2607.10069#Thmdefinition3)\)\. Then≡reuse\\equiv\_\{\\mathrm\{reuse\}\}is exactly the kernel ofres\\mathrm\{res\}, sores\\mathrm\{res\}factors as

Ures↠ℛc↪P​\(c\),U\_\{\\mathrm\{res\}\}\\;\\twoheadrightarrow\\;\\mathcal\{R\}\_\{c\}\\;\\hookrightarrow\\;P\(c\),with the induced map injective, and surjective iff every cell is realized by some resolved utterance\. Henceℛc\\mathcal\{R\}\_\{c\}is the utterance\-side object the partition induces: it coincides withP​\(c\)P\(c\)only when the deployment realizes every governed question, and in general it measures*realized demand*—whence its name— over the corpus structure—the object on which reuse economics \(hit rates over a query stream\) is actually defined\.

###### Proof\.

By Definition[6](https://arxiv.org/html/2607.10069#Thmdefinition6)\(iii\),u≡reuseu′u\\equiv\_\{\\mathrm\{reuse\}\}u^\{\\prime\}iffres​\(u\)=res​\(u′\)\\mathrm\{res\}\(u\)=\\mathrm\{res\}\(u^\{\\prime\}\), which is the definition of the kernel; the factorization and injectivity of the induced map are the universal property of quotients by a kernel, and surjectivity ontoP​\(c\)P\(c\)is by construction equivalent to every cell having a preimage\. ∎

## 4Decidability and complexity, by regime

###### Theorem 2\(Conditional decidability\)\.

Under Assumption A1 and a finite materialized fiber\(L​\(c\),P​\(c\),σ​\(c\)\)\(L\(c\),P\(c\),\\sigma\(c\)\), the full pipeline map

u⟼\{non\-canonical route\}⊎M⊎\{QC:C∈P​\(c\)\}u\\;\\longmapsto\\;\\\{\\textsf\{non\-canonical route\}\\\}\\;\\uplus\\;M\\;\\uplus\\;\\\{\\,Q\_\{C\}:C\\in P\(c\)\\,\\\}is total computable on all ofUU: Gate\-1 rejects \(C​\(u\)=0C\(u\)=0\) receive the routing outcome, utterances inU1∖UresU\_\{1\}\\setminus U\_\{\\mathrm\{res\}\}receive their modeA​\(u\)∈MA\(u\)\\in M, and resolved utterances receive their governed question\. All corpus\-side operations—fixpoint membership, theσ\\sigma\-comparison, cell incidence, the join aggregationa​\(u\)a\(u\), the CP check, and both normal forms—are decidable with no assumption on the proposal layer\.

###### Proof\.

CCis total computable by A1, so the Gate\-1 routing branch is decided for everyu∈Uu\\in U; onU1U\_\{1\},DcD\_\{c\}is total computable by A1, and each subsequent step is a finite check or computation against the materialization \(Gates 2–3, the mode assignment from the gate trace, cell incidence, the joina​\(u\)a\(u\)as one closure application, the post\-aggregation domain check, andclc​\(C\)=C\\mathrm\{cl\}\_\{c\}\(C\)=Cper cell for CP\) or is computable by Lemma[1](https://arxiv.org/html/2607.10069#Thmlemma1)\(Canoncell\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\},Canon\\mathrm\{Canon\}\)\. The three branches of the codomain are exhaustive and mutually exclusive by construction of the pipeline, and the composition of totally computable steps over finite data is totally computable\. ∎

###### Proposition 1\(Complexity, three regimes\)\.

Letn=\|Wc\|n=\|W\_\{c\}\|, letPcP\_\{c\}be the program generatingclc\\mathrm\{cl\}\_\{c\}, and letmmbe the number of literal occurrences in the grounding ofPcP\_\{c\}\.

1. \(i\)*Ground Horn tier\.*IfPcP\_\{c\}is a ground \(propositional\) Horn program, the closure of a fact set is computable in timeO​\(m\)O\(m\)by unit\-propagation\-style indexed forward chaining, in the manner of the linear\-time Horn satisfiability algorithms of Dowling and Gallier\[[4](https://arxiv.org/html/2607.10069#bib.bib4)\]\(the citation supports the propagation technique; the closure statement is the standard consequence under indexed representations\)\. WithL​\(c\)L\(c\),P​\(c\)P\(c\)materialized offline and propositions, cells, andσ​\(c\)\\sigma\(c\)held asnn\-bit vectors, Gate 2 is a lookup and Gate 3 a bit\-vector inclusion test inO​\(n\)O\(n\)\. Cell assignment is stated precisely: containment against a*given*candidate cell costsO​\(n\)O\(n\);*locating*the containing cell naïvely costsO​\(\|P​\(c\)\|​n\)O\(\|P\(c\)\|\\,n\)over the partition, reducible toO​\(n\)O\(n\)amortized under a precomputed world\-to\-cell index \(any world ofa​\(u\)a\(u\)names the candidate, leaving oneO​\(n\)O\(n\)containment check\)\. Each pipeline operation is polynomial inm\+nm\+n\. This is the regime of the production architecture\[[1](https://arxiv.org/html/2607.10069#bib.bib1),[6](https://arxiv.org/html/2607.10069#bib.bib6)\]\.
2. \(ii\)*Fixed\-program \(data\) complexity\.*For non\-ground Datalog withPcP\_\{c\}fixed, data complexity is measured in the sizeNNof the extensional input structure \(the EDB\), in which Datalog isPTime\-complete\[[5](https://arxiv.org/html/2607.10069#bib.bib5)\]\. In this architectureWcW\_\{c\}is*extensionally materialized*—the bit\-vector representation over the explicit world set is the input structure—son≤Nn\\leq Nand materialization and all gate checks are polynomial inNN\. Without that materialization assumption, polynomiality in the number of semantic worlds is not implied and is not claimed\.
3. \(iii\)*Combined complexity\.*With both program and data varying, Datalog isExpTime\-complete\[[5](https://arxiv.org/html/2607.10069#bib.bib5)\]; no polynomial claim is made in this regime, and none is needed: corpus compilation fixesPcP\_\{c\}offline, so query\-time operation is governed by \(i\)–\(ii\)\.

Both normal forms are computable \(Lemma[1](https://arxiv.org/html/2607.10069#Thmlemma1)\) but their naïve enumeration is not polynomial; in deploymentCanoncell​\(C\)\\mathrm\{Canon\}\_\{\\mathrm\{cell\}\}\(C\)is computed offline once per cell and cached, anda​\(u\)a\(u\)costs one closure application, so the query\-time cost of canonicalization is the cell assignment of \(i\)–\(ii\), not formula search\.

## 5Three orthogonal safety properties

The closure proves less than “safety” and the paper must say exactly what\. Three properties come apart\.

###### Definition 7\.

A pipeline run has:

1. \(a\)*policy admissibility*if every emitted proposition lies inFix​\(clc\)\\mathrm\{Fix\}\(\\mathrm\{cl\}\_\{c\}\), clearsσ​\(c\)\\sigma\(c\), is cell\-contained, and carries a certificate bound to its fiber—“can we say it?”;
2. \(b\)*factual grounding*if every premise on which the emitted proposition’s derivation rests is a verified fact of the live case—“is it supported?”;
3. \(c\)*intent fidelity*if the emitted answer resolves the question the speaker in fact intended—“is it what the user asked?”\.

###### Proposition 2\(Policy admissibility for arbitrary proposers\)\.

For every proposal layer satisfying A1—including an adversarial one—every run of the pipeline has policy admissibility: the emitted proposition is preciselya​\(u\)a\(u\)\(equivalently its certified representativeCanon​\(a​\(u\)\)\\mathrm\{Canon\}\(a\(u\)\), whose denotation isa​\(u\)a\(u\)by exactness\), which has passed the fixpoint, threshold, and cell\-containment checks*after*aggregation, computed by the verification layer against the materialized fiber, independently of how the proposals were produced; and by Condition PC the emission carriesCertc​\(a​\(u\)\)\\mathrm\{Cert\}\_\{c\}\(a\(u\)\), a derivation witness bound to the fiber data\(Σ,Φt,c,t\)\(\\Sigma,\\Phi\_\{t\},c,t\), so certificate possession is derived, not assumed\.

## 6Elicitation over cell\-decided predicates

Cell ambiguity and under\-specificity are resolved inside the fixed fiber by monotone accumulation: admissible facts grow, live cells are eliminated, until one cell remains or none can be separated\. The termination claim requires the elicitation vocabulary to interact with the partition cleanly, so that “indistinguishable” is a genuine equivalence\.

###### Assumption 2\(A2′: cell\-decided separability\)\.

The admissible elicitation vocabularyℰc\\mathcal\{E\}\_\{c\}consists of decidable predicates that are*cell\-decided*: eachf∈ℰcf\\in\\mathcal\{E\}\_\{c\}has a constant truth value on every cell ofP​\(c\)P\(c\)\(writef​\(C\)∈\{0,1\}f\(C\)\\in\\\{0,1\\\}\)\. This is natural whenℰc\\mathcal\{E\}\_\{c\}is drawn from the material atoms that generate the partition\. The*observational signature*of a cell issig​\(C\)=\(f​\(C\)\)f∈ℰc\\mathrm\{sig\}\(C\)=\(f\(C\)\)\_\{f\\in\\mathcal\{E\}\_\{c\}\};ff*separates*Ci,CjC\_\{i\},C\_\{j\}ifff​\(Ci\)≠f​\(Cj\)f\(C\_\{i\}\)\\neq f\(C\_\{j\}\); andCi∼ℰcCjC\_\{i\}\\sim\_\{\\mathcal\{E\}\_\{c\}\}C\_\{j\}iffsig​\(Ci\)=sig​\(Cj\)\\mathrm\{sig\}\(C\_\{i\}\)=\\mathrm\{sig\}\(C\_\{j\}\)—an equivalence relation by construction\. A live\-cell set satisfies A2′when its cells have pairwise distinct signatures\.

###### Assumption 3\(A3: responsiveness\)\.

Each reply to an askedf∈ℰcf\\in\\mathcal\{E\}\_\{c\}is an admissible ground fact that decidesff\(an*informative*reply\)\. Refusals, ambiguous replies, and non\-answers are permitted but do not count against the bound\.

###### Assumption 4\(A4: target consistency\)\.

There is a fixed intended cellC⋆∈P​\(c\)C^\{\\star\}\\in P\(c\)\(equivalently, a fixed intended worldw⋆∈Wcw^\{\\star\}\\in W\_\{c\}withC⋆C^\{\\star\}its cell\) such that every informative reply reports the value of the asked predicate at the target:r​\(f\)=f​\(C⋆\)r\(f\)=f\(C^\{\\star\}\)\. A3 alone constrains replies to be admissible and decisive; it does not make them truthful or mutually consistent, and soundness below is exactly what A4 adds\.

###### Theorem 3\(Termination and soundness of elicitation\)\.

Consider any policy that, while\|\{sig​\(C\):C∈Lk\}\|≥2\|\\\{\\mathrm\{sig\}\(C\):C\\in L\_\{k\}\\\}\|\\geq 2, selects live cellsCi,Cj∈LkC\_\{i\},C\_\{j\}\\in L\_\{k\}withsig​\(Ci\)≠sig​\(Cj\)\\mathrm\{sig\}\(C\_\{i\}\)\\neq\\mathrm\{sig\}\(C\_\{j\}\)and somef∈ℰcf\\in\\mathcal\{E\}\_\{c\}withf​\(Ci\)≠f​\(Cj\)f\(C\_\{i\}\)\\neq f\(C\_\{j\}\)\(which exists, since signatures determine separation\), asksff, and eliminates the cells whose signature the reply contradicts\. WriteLkL\_\{k\}for the live set afterkkinformative replies\. Then:

1. \(i\)*\(Termination, A2′–A3\.\)*The procedure halts after at most\|P​\(c\)\|−1\|P\(c\)\|\-1informative replies, in a singleton, in a set with a single shared signature \(case \(iii\)\), or in the empty set \(case \(iv\)\)\.
2. \(ii\)*\(Soundness, A2′–A4\.\)*C⋆∈LkC^\{\\star\}\\in L\_\{k\}for everykk: an informative reply eliminates only cells whose signature disagrees with the reported valuef​\(C⋆\)f\(C^\{\\star\}\), which never includesC⋆C^\{\\star\}\. Hence under A4 the live set can never become empty; and if the live signatures are pairwise distinct, the procedure halts inLk=\{C⋆\}L\_\{k\}=\\\{C^\{\\star\}\\\}—a sound resolution of the intended governed question\.
3. \(iii\)*\(Vocabulary limit\.\)*If the live set’s signatures are not pairwise distinct, the procedure halts as soon as the live set is contained in a single ambient∼ℰc\\sim\_\{\\mathcal\{E\}\_\{c\}\}\-class, and reports governed abstention naming*the ambient equivalence class containing the live set*\. The live set itself need not be a full class—earlier evidence may already have eliminated some of the class’s members—but the ambient class is a genuine equivalence class, since∼ℰc\\sim\_\{\\mathcal\{E\}\_\{c\}\}is an equivalence by construction, and the report is the diagnostic that the elicitation vocabulary, not the corpus, is the binding constraint\.
4. \(iv\)*\(Inconsistent evidence\.\)*Without A4, an empty live set is possible and must be reported as*no compatible cell*: the replies were individually admissible but jointly inconsistent with every cell \(or untruthful relative to any fixed target\)\. This outcome is distinguished from the*certified no\-match*of the corpus—asserting that no admissible cell answers the query requires evidence that is truthful and complete, which A3 alone does not supply\. Operationally, no\-compatible\-cell routes to human escalation, not to a certified negative\.
5. \(v\)*\(Non\-responsiveness\.\)*If A3 fails, no bound on wall\-clock rounds is claimed; the bound counts informative replies only, and accumulation appliesclc\\mathrm\{cl\}\_\{c\}to admissible facts, so every intermediate state is admissible regardless\.

###### Proof\.

\(i\) Because eachffis cell\-decided, an informative reply assigningffits value contradicts precisely the live cellsCCwithf​\(C\)f\(C\)opposite to the reply, of which there is at least one whenffseparates two live cells; the live count strictly decreases and is finite, so at most\|P​\(c\)\|−1\|P\(c\)\|\-1strict decreases reach a halting configuration\. \(ii\) By A4 the reported value isf​\(C⋆\)f\(C^\{\\star\}\), soC⋆C^\{\\star\}is never among the contradicted cells; induction givesC⋆∈LkC^\{\\star\}\\in L\_\{k\}for allkk, whenceLk≠∅L\_\{k\}\\neq\\emptyset, and when signatures are pairwise distinct the halting singleton must be\{C⋆\}\\\{C^\{\\star\}\\\}\. \(iii\) When all live cells share one signature, nof∈ℰcf\\in\\mathcal\{E\}\_\{c\}separates any pair \(signatures determine separation\), the policy’s guard fails, and the live set lies in the∼ℰc\\sim\_\{\\mathcal\{E\}\_\{c\}\}\-class of that shared signature; containment, not equality, is claimed\. \(iv\) Without the invariant of \(ii\), each reply removes a signature\-determined subset and the intersection of the surviving constraints can be empty; emptiness certifies only that no cell is consistent with all replies\. \(v\) Non\-informative replies leave the live set unchanged; admissibility is preserved sinceclc\\mathrm\{cl\}\_\{c\}is applied to admissible inputs andP​\(c\)P\(c\)partitionsWcW\_\{c\}\. ∎

The base/fiber composition of\[[1](https://arxiv.org/html/2607.10069#bib.bib1)\]is unchanged:*which*closure is in force narrows contravariantly with context refinement; elicitation runs monotonically inside that closure\. Ambiguity about the operative context is handled at the base \(rebindingcc\), ambiguity about the question in the fiber, and the two are never traded against each other\.

## 7Concluding remark

The central object of this note is the realized governed reuse spaceℛc=Ures/≡reuse\\mathcal\{R\}\_\{c\}=U\_\{\\mathrm\{res\}\}/\\\!\\equiv\_\{\\mathrm\{reuse\}\}, reached by the surjectionUres↠ℛcU\_\{\\mathrm\{res\}\}\\twoheadrightarrow\\mathcal\{R\}\_\{c\}: the partition of*resolved*conversational demands into governed reuse classes, with abstentions held apart as terminal outcomes of the mode map\. Its claims, stated at their honest strength: the cell normal form \(presenting the governed queryQCQ\_\{C\}, which is an operational object and deliberately not a partition\-semantics question\) and the proposition normal form \(defined by exact denotation, hence injective\) are single\-valued computable maps on explicit domains \(Lemma[1](https://arxiv.org/html/2607.10069#Thmlemma1)\); resolution aggregation is a conservative design operator whose one non\-obvious hazard—closure\-induced cross\-cell escape—is characterized exactly by the closure–partition compatibility condition and detected at the domain check where the condition fails \(Lemma[2](https://arxiv.org/html/2607.10069#Thmlemma2)\); the three equivalences≡read⁣⊆⁣≡res⁣⊆⁣≡reuse\{\\equiv\_\{\\mathrm\{read\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{res\}\}\}\\subseteq\{\\equiv\_\{\\mathrm\{reuse\}\}\}form a refinement chain, strict under*realized*nondegeneracy conditions—a joint property of corpus and proposal layer, checkable on deployment logs \(Figure[1](https://arxiv.org/html/2607.10069#S1.F1)\)—along which the pipeline’s outputs are invariant, so reuse equivalence is a provable coarsening of reading\-level equivalence, with abstention modes explicitly outside the invariance \(Theorem[1](https://arxiv.org/html/2607.10069#Thmtheorem1), Remark[6](https://arxiv.org/html/2607.10069#Thmremark6)\), and with query\-key reuse distinguished from particular\-answer reuse and≡reuse\\equiv\_\{\\mathrm\{reuse\}\}identified as the kernel of the resolution map—so the quotient measures realized demand, not a relabeling of the answer partition \(Corollary[2](https://arxiv.org/html/2607.10069#Thmcorollary2), Remark[8](https://arxiv.org/html/2607.10069#Thmremark8)\); the whole map is decidable conditional on a computable proposal layer—deliberately immediate, with the content in the placement of the assumptions—with polynomial checks in the ground and fixed\-program regimes only over bit\-vector representations \(Theorem[2](https://arxiv.org/html/2607.10069#Thmtheorem2), Proposition[1](https://arxiv.org/html/2607.10069#Thmproposition1)\); and of the three orthogonal safety properties—policy admissibility, factual grounding, intent fidelity—the closure proves exactly the first, for arbitrary proposers, with certificate possession derived from the proof\-producing closure rather than asserted \(Proposition[2](https://arxiv.org/html/2607.10069#Thmproposition2), Remark[12](https://arxiv.org/html/2607.10069#Thmremark12)\)\. Elicitation over cell\-decided predicates terminates, is sound under target consistency—the intended cell is an invariant of the live set—and reports its two failure modes honestly: a vocabulary limit as containment in an ambient observational equivalence class, and inconsistent evidence as no compatible cell, distinct from a certified no\-match \(Theorem[3](https://arxiv.org/html/2607.10069#Thmtheorem3)\)\. The order theory underneath is classical\[[8](https://arxiv.org/html/2607.10069#bib.bib8)\]; the contribution is the characterization of when two different conversational demands are legitimately the same reusable governed object—the question on which certified\-reuse economics ultimately rests\.

#### Disclosure

The authors are affiliated with Minerva CQ, which has commercial interests in AI\-governance tooling that builds on these results\.

## References

- \[1\]C\. Spera, R\. Garcia, Certified Resolution: a formal theory of governed answer spaces for enterprise AI, Minerva CQ working paper \(2026\)\.
- \[2\]J\. Groenendijk, M\. Stokhof, Studies on the Semantics of Questions and the Pragmatics of Answers, PhD thesis, Univ\. of Amsterdam \(1984\)\.
- \[3\]N\.D\. Belnap, T\.B\. Steel, The Logic of Questions and Answers, Yale University Press, 1976\.
- \[4\]W\.F\. Dowling, J\.H\. Gallier, Linear\-time algorithms for testing the satisfiability of propositional Horn formulae, J\. Logic Programming 1 \(1984\) 267–284\.
- \[5\]S\. Abiteboul, R\. Hull, V\. Vianu, Foundations of Databases, Addison\-Wesley, 1995\.
- \[6\]C\. Spera, Capability safety as Datalog: a foundational equivalence, arXiv:2603\.26725 \(2026\)\.
- \[7\]F\. Bang, GPTCache: an open\-source semantic cache for LLM applications, in: Proc\. EMNLP Industry Track, 2023, pp\. 212–218\.
- \[8\]A\. Tarski, A lattice\-theoretical fixpoint theorem and its applications, Pacific J\. Math\. 5 \(1955\) 285–309\.