Part VI

The theorems are stated. The specification is written. Part VI asks: does the machinery work?

Intended consistency is not proof of consistency. The question here also concerns explanatory power: does the specified operation make a problem and its possible outcomes more intelligible? Do the definitions earn their complexity? Do the constructions produce artifacts that a practitioner would recognize as useful?

The following constructed examples put the proposed operations under pressure. Their premises determine what can be established: an empty answer, a retained distinction, an admitted predicate or a refusal with work still outstanding. An illustrative receipt supplies no evidence that software performed the checks it names.

These constructed demonstrations exercise the formal machinery developed in the preceding parts. Vol I, Chapters 5–8 supply related institutional questions; the examples and proofs here are self-contained.

What This Part Demonstrates

Refusal (A27) demonstrates that a coherent system can say no — and explain why. Where a supported procedure establishes inconsistent constraints, its refusal carries the checked grounds. A core’s minimality needs a separate check; ordinary empty results need not have inconsistent constraints. The refusal obligation is not a limitation; it is a feature. A system that can refuse with explanation is structurally different from a system that produces plausible garbage when the answer is "no answer exists."

Sense gluing (A28) demonstrates the full pomegranate problem, formally. The sense predicate $s_U$ maps terms and contexts to senses. Restriction requires that senses agree on overlaps; transport carries senses along context equivalences; explicit forks handle cases where senses genuinely diverge. The exact function-sheaf case explains how compatible assignments assemble. It does not solve the assignment of meanings or make polysemy a contradiction.

Predicate acceptance (A29) demonstrates the full lifecycle of a new predicate: from Proposed through Provisional, Local, Promoted, Deprecated, to Retracted. Each state has entry conditions, usage constraints, and transition rules. The acceptance test suite — positive exemplars, negative exemplars, boundary cases, invariant checks, conservative extension verification — is the formal version of "does this predicate deserve citizenship?"

Scoped equivalence (A30) demonstrates that "same" is always relative to scope. The constructed sources give a term different uses. Context can also establish that different sources mean the same thing; a schema or mapping can preserve that evidence. The proof obligation is concrete: any substitution $x \to y$ must cite the witness for $x \sim_S y$ and confirm that the current context is contained in $S$.

N-ary event objects (A31) demonstrate that higher-arity events are meaning atoms. "Alice introduced Bob to Carol" is a single three-party event. The counterexample compares two collections of introductions with identical ungrouped role edges. A shared event key or equivalent grouping structure preserves what that projection loses; binary storage is not generally incapable of doing so.

The Third Mode (A32) gathers four design requirements. Appendix I supplies the ten-operation implementation contract, including correction across reuse. The demonstrations make those obligations inspectable; compliance requires evidence that an implementation supplies them.

Key Anchors

Anchor	Name	Status	Chapter
A27	Refusal Obligation	formal	Ch. 25
A28	Sense Gluing	formal	Ch. 26
A29	Predicate Acceptance	formal	Ch. 27
A30	Scoped Equivalence	formal	Ch. 28
A31	N-ary Event Object	formal	Ch. 29
A32	The Third Mode	formal	Ch. 30

What the Formalism Does Not Capture

Written demonstrations establish only the steps justified under their specified assumptions; an illustrative output is not evidence that software produced it. They supply no universal sufficiency result for binding, conditions, stakes, recourse and composition. Such a claim would first need a specified class of problems and a criterion of adequacy; this work has not supplied that theorem or a complete formulation of it.

The worked examples also inherit the limitation of every formal model: they are cleaner than reality. The pomegranate problem in a real product catalog comes with OCR errors, multilingual metadata, vendor-specific abbreviations, and a team of category managers who disagree about whether "pomegranate" is a color or a motif. Those differences can change which assignments and comparisons the model should contain. A worked gluing must leave the reader able to distinguish the assignments it assumed from the assembly it proved.

Part VI lets the reader assess whether the proposed artifacts—witnesses, transport certificates, unsat cores and lifecycle records—make the constructed decisions more intelligible. Their practical adequacy still depends on implementing the checks and supplying their grounds. The gap between "formally correct" and "practically adopted" is real, but it is a different gap than the one this work set out to close.