\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,shapes.geometric}
\usepackage[margin=1in]{geometry}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}
\usepackage[numbers,sort&compress]{natbib}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{tabularx}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage{listings}
\usepackage{pdflscape}
\usepackage{url}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={Semantic Sharding and Distributed Query Planning},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{requirement}[theorem]{Requirement}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newtheorem{counterexample}[theorem]{Counterexample}

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\prior}{\textsc{supported by prior literature}}
\newcommand{\paperreasoned}{\textsc{paper reasoning}}
\newcommand{\acceptedpaper}{\textsc{accepted paper contract}}
\newcommand{\proposed}{\textsc{proposed}}
\newcommand{\openclaim}{\textsc{open}}
\newcommand{\obstructed}{\textsc{obstructed}}
\newcommand{\rejected}{\textsc{rejected}}
\newcommand{\nonclaim}{\textsc{nonclaim}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1.}\par}
\newcommand{\Ans}{\ensuremath{\mathsf{Ans}}}
\newcommand{\Admitted}{\ensuremath{\mathsf{Admitted}}}
\newcommand{\Deferred}{\ensuremath{\mathsf{Deferred}}}
\newcommand{\Rejected}{\ensuremath{\mathsf{Rejected}}}
\newcommand{\Unsupported}{\ensuremath{\mathsf{Unsupported}}}
\newcommand{\Exact}{\ensuremath{\mathsf{Exact}}}
\newcommand{\Conservative}{\ensuremath{\mathsf{ConservativeSuperset}}}
\newcommand{\Hint}{\ensuremath{\mathsf{SampledHint}}}
\newcommand{\Complete}{\ensuremath{\mathsf{Complete}}}
\newcommand{\Partial}{\ensuremath{\mathsf{ExplicitlyPartial}}}
\newcommand{\Unknown}{\ensuremath{\mathsf{Unknown}}}
\newcommand{\Ready}{\ensuremath{\mathsf{Ready}}}
\newcommand{\Invalid}{\ensuremath{\mathsf{Invalid}}}
\newcommand{\Digest}{\ensuremath{\mathsf{Digest}}}
\newcommand{\Route}{\ensuremath{\mathsf{Route}}}
\newcommand{\Coverage}{\ensuremath{\mathsf{Coverage}}}
\newcommand{\Selected}{\ensuremath{\mathsf{Selected}}}
\newcommand{\Placements}{\ensuremath{\mathsf{Placements}}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

\setlength{\emergencystretch}{4em}
\setlist{itemsep=0.25em,topsep=0.4em}
\raggedbottom
\lstset{
  basicstyle=\ttfamily\footnotesize,
  breaklines=true,
  breakatwhitespace=false,
  columns=fullflexible,
  frame=single,
  rulecolor=\color{black!20},
  showstringspaces=false,
  keepspaces=true,
  upquote=true
}

\definecolor{grokgray}{RGB}{110,110,110}
\definecolor{shardblue}{RGB}{226,238,250}
\definecolor{shardorange}{RGB}{252,237,216}
\definecolor{shardred}{RGB}{250,227,227}
\AddToHook{shipout/background}{%
  \ifnum\value{page}=1
    \begin{tikzpicture}[remember picture,overlay]
      \node[
        rotate=90,
        anchor=south,
        font=\Large\sffamily\bfseries\color{grokgray},
        inner sep=0pt
      ] at ([xshift=38pt,yshift=0.52\paperheight]current page.south west)
      {GrokRxiv:2026.07.catdb-semantic-sharding\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Semantic Sharding and Distributed Query Planning:\\
A Typed, Versioned Routing Contract for \CatDB{}}
\author{Matthew Long \\
\textit{The YonedaAI Collaboration} \\
\textit{YonedaAI Research Collective} \\
Chicago, IL \\
\texttt{matthew@yonedaai.com} $\cdot$ \url{https://yonedaai.com}}
\date{23 July 2026}

\begin{document}
\maketitle

\begin{center}
\fbox{\large Provisional research specification: \obstructed{}}
\end{center}

\begin{abstract}
Putting related records on the same machine can reduce communication, but
``related'' has several meanings in a semantic database.  Two records may
share a tenant, workspace, source, semantic object, provenance authority,
region, time interval, or physical key.  Those scopes can disagree.  A
low-latency replica may violate residency policy.  A path whose endpoints are
local may still depend on a remote edge.  A shard advertised as irrelevant
under one mapping may contain qualifying rows under another.

This paper gives a provisional placement and routing contract for \CatDB{}.
It separates logical partitions from physical placements, records exact or
conservative coverage predicates, binds every route to query, mapping,
snapshot, policy, consistency, and topology revisions, and carries explicit
obligations into distributed join, exchange, index, and materialization
alternatives.  A partition may be pruned for logical disjointness only when a
checkable certificate proves that its coverage and the rewritten query
predicate cannot overlap under the same semantics.  Policy exclusion and
snapshot incompatibility remain distinct outcomes.  Complete selection must
also preserve ordinary bag multiplicity after replica and intentional-overlap
handling.

The paper states twelve proposed invariants, supplies eighteen finite
counterexamples, and fixes fifteen claim anchors.  It compares the proposed
contract with established work on distributed query processing, workload and
graph partitioning, geographic and tenant placement, logical data skipping,
provenance, and materialized computation.  The possible \CatDB{} contribution
is narrow: a versioned contract that keeps semantic scopes and physical
obligations together, followed eventually by controlled ablation against
physical-only and communication-aware baselines.

This is not a sharding system or a distributed planner result.  The repository
contains no P12 routing runtime, exchange executor, distributed join planner,
pruning oracle, migration protocol, cross-shard benchmark, vector-locality
result, or full-text locality result.  Papers 2, 5, 10, and 11 are internally
accepted paper contracts, but the repository supplies no executable
interfaces or independent oracles that instantiate their query denotation,
source coverage, topology/migration, and observation-consistency boundaries.
CatDB-specific correctness, locality, performance, and scale claims therefore
remain \openclaim{}, \obstructed{}, or \rejected{}.
\end{abstract}

\tableofcontents

\section{Introduction}
\label{sec:introduction}

\subsection{One request, several boundaries}

Consider a tenant that has a published customer model, a private workspace
with an uncommitted mapping, orders in two regional PostgreSQL shards, a
rate-limited source of support cases, and a materialized revenue view.  An
analyst asks for customers whose June orders and support activity satisfy a
typed path.  The response must include complete lineage and obey a policy that
keeps raw support text in one region.

Several attractive shortcuts are wrong.  Routing by tenant alone can expose
the private workspace.  Routing by a semantic \code{Customer} label can
overload one hot shard.  Sending the whole query to the closest region can
violate residency or use a connector with different scalar semantics.
Reading the materialized view because its refresh timestamp is current can
cross a mapping revision.  Pruning a June shard because it was marked closed
can miss a late correction.  Replicating a small reference relation can
multiply an ordinary bag result if the replicas are treated as distinct
logical inputs.

These are not edge cases that a cost model can repair later.  They determine
which physical alternatives are admissible.  Cost-based selection belongs
after query meaning, coverage, policy, snapshot, replica, and migration
obligations have been made explicit.

\subsection{Research question}

The bounded question is:

\begin{quote}
Can a versioned semantic placement contract improve shard selection,
cross-shard plan enumeration, and plan explanation over a physical-statistics
baseline without changing query denotation, hiding incomplete coverage, or
erasing network and consistency costs?
\end{quote}

The strongest defensible target is a finite profile with a frozen relational
fragment, exact result-bag comparison, explicit source coverage, conventional
hash and range baselines, a fixed topology and consistency profile, and
feature-by-feature ablation.  No such implementation or evaluation exists
today.

\subsection{Contributions and boundaries}

This provisional manuscript contributes:

\begin{enumerate}
  \item a typed separation among partition coverage, physical placement,
  routing epochs, requests, decisions, and obligations;
  \item a partition-dimension analysis for workspace, tenant, semantic object,
  source, provenance domain, geography, time, and physical key;
  \item soundness and completeness conditions for correctness-preserving
  pruning under exact or conservative coverage;
  \item admissibility contracts for paths, distributed joins, query and data
  shipping, reference replicas, indexes, and materializations;
  \item twelve proposed invariants and eighteen finite counterexamples;
  \item a primary-source synthesis, fifteen claim anchors, and a falsifiable
  future evaluation contract.
\end{enumerate}

The paper does not claim a running router, a distributed executor, a benchmark
win, native pruning superiority, cross-shard performance, vector locality, or
full-text locality.  It does not call an alternative optimal.  P12 may
enumerate admissible alternatives; Paper 14 owns later cost-based choice.

\status{\proposed{} manuscript contract; implementation and evaluation
\obstructed{}.}

\section{Evidence Discipline and Dependency Boundary}
\label{sec:evidence}

\subsection{Status vocabulary}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.22\textwidth}Y}
\toprule
Label & Meaning in this paper \\
\midrule
\prior{} & A primary source establishes the cited result under its own
assumptions.  It is not CatDB evidence. \\
\paperreasoned{} & A finite argument or counterexample establishes the bounded
statement in this manuscript.  It does not verify a runtime. \\
\acceptedpaper{} & An internally accepted predecessor manuscript fixes a
paper-level boundary.  It is not an executable interface, oracle, or runtime
result. \\
\proposed{} & A typed contract is specified but not accepted or executed. \\
\openclaim{} & A claim has a defined evidence path but no accepted result. \\
\obstructed{} & A required upstream definition, implementation, or evidence
path is absent. \\
\rejected{} & A claim conflicts with prior work, a counterexample, or the
current repository cut. \\
\bottomrule
\end{tabularx}
\caption{Evidence labels.  No P12 claim is currently computational,
experimentally supported, machine checked, or an implemented guarantee.}
\label{tab:evidence-labels}
\end{table}

Evidence does not transfer automatically between layers.  A distributed join
paper does not implement \CatDB{}.  A typed path does not reveal a placement.
A coverage predicate does not prove that routing metadata is current.  A
locally sound prune does not prove a complete multi-source answer.  An
immutable replicated target does not make a mutable active pointer
consistent.  A query equivalence proof does not verify exchange code.

\subsection{Direct dependency blockers}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.08\textwidth}L{0.39\textwidth}L{0.15\textwidth}Y}
\toprule
Paper & Required paper boundary & Status & Consequence for P12 \\
\midrule
P2 & Query denotation, bag/null/scalar semantics, typed physical-plan boundary,
and result equivalence. & \acceptedpaper{} & No executable query oracle or
physical-plan interface exercises routing and join equivalence. \\
P5 & Source interpretation, coverage, capabilities, pushdown, source snapshots,
and partial-failure semantics. & \acceptedpaper{} & No executable coverage or
capability interface exercises source pruning and query shipping. \\
P10 & Operation envelope, topology epoch, membership, replica identity,
migration, and replay. & \acceptedpaper{} & No distribution runtime or history
oracle tests route stability and shard movement. \\
P11 & Snapshot, visibility, consistency, freshness, stale/tentative/error, and
active-reference profiles. & \acceptedpaper{} & No consistency runtime or
history oracle tests multi-placement reads and mutable references. \\
\bottomrule
\end{tabularx}
\caption{The four accepted predecessor contracts.  Their executable
instantiation and the P12 evidence that would consume it remain absent.}
\label{tab:dependencies}
\end{table}

P6, P9, and P13 also affect materialization, workspace isolation, and
provenance completeness.  Those secondary dependencies cannot replace the
four direct boundaries.  P12 must not treat accepted manuscript definitions
as implemented behavior or invent router-local substitutes for their missing
executable profiles.

\subsection{Current repository cut}

The current repository has no P12 partition descriptor, placement registry,
routing table, exchange operator, distributed join planner, pruning
certificate checker, topology-epoch implementation, migration protocol,
distributed materialization placement service, cross-shard fixture, Haskell
oracle, Lean P12 theorem, or benchmark result.  The source package accompanying
this manuscript therefore reproduces a LaTeX specification and citation
audit, not a system result.

\section{Typed Partition and Placement Contract}
\label{sec:partition-contract}

\subsection{Primitive identities}

The contract uses stable, version-bearing identities.  None implies locality.

\begin{lstlisting}[caption={Primitive P12 identities.},label={lst:ids}]
PartitionId           := stable logical-partition identity
ReplicaId             := stable physical-replica identity
PlacementId           := stable physical-placement record
RoutingEpochId        := immutable topology revision
TenantId              := authorization and billing domain
WorkspaceId           := immutable workspace or overlay identity
SemanticObjectId      := versioned canonical object or family
SourceId              := versioned physical-source identity
ProvenanceDomainId    := provenance authority or retention domain
RegionId              := geography or residency region
TimeDomainId          := valid, system, or source-frontier time
SnapshotId            := immutable source or catalog snapshot
ConsistencyProfileId  := immutable P11 profile identity
CapabilityProfileId   := immutable P5 capability identity
QueryProfileId        := immutable P2 query-semantics identity
MappingVersionId      := immutable mapping revision
PolicyVersionId       := immutable policy revision
MaterializationId     := immutable definition or instance
IndexId               := immutable index definition and build
Digest                := canonical-content digest
\end{lstlisting}

A \code{SemanticObjectId} names meaning under a revision.  A
\code{PartitionId} names logical coverage.  A \code{PlacementId} states where
that logical coverage is realized.  A \code{ReplicaId} names one physical
copy.  Conflating these identities is enough to create routing, multiplicity,
and migration errors.

\subsection{Partition dimensions}

\begin{lstlisting}[caption={Partition dimension sum type.},label={lst:dimensions}]
PartitionDimension :=
    Workspace
  | Tenant
  | SemanticObject
  | Source
  | ProvenanceDomain
  | Geography
  | Time
  | PhysicalKey
  | Composite(list<PartitionDimension>)
\end{lstlisting}

\code{PhysicalKey} remains explicit because semantic dimensions must be
compared and composed with hash, range, list, graph-derived, and
workload-derived placement.  Semantic dimensions do not replace ordinary
physical partition keys.

\subsection{Coverage predicate}

\begin{lstlisting}[caption={Versioned coverage predicate.},label={lst:coverage}]
CoveragePredicate := {
  language: PredicateLanguageId,
  expression: CanonicalPredicateIR,
  query_profile: QueryProfileId,
  mapping_scope:
      BoundTo(MappingVersionId)
    | MappingIndependent(MappingIndependenceWitness),
  exactness: Exact | ConservativeSuperset | SampledHint,
  authority: AuthorityRecord,
  valid_from: LogicalTime?,
  valid_to: LogicalTime?,
  recorded_at: SystemTime,
  digest: Digest
}
\end{lstlisting}

Only \Exact{} and \Conservative{} coverage may participate in
correctness-preserving exclusion.  A \Hint{} may affect estimates, probe
priority, or physical-plan ranking.  It cannot remove a partition from a
complete exact answer.

\code{mapping\_scope} has no omitted or default case.
\code{BoundTo(v)} may support pruning only when the request rewrite and
partition descriptor bind the same mapping version \(v\).
\code{MappingIndependent(w)} requires a checkable witness that the predicate
uses only source-native or raw fields whose denotation is independent of every
mapping admitted by the request.  A missing, unknown, or invalid mapping scope
fails closed: the partition remains a candidate, or the request is rejected,
but the partition is never excluded by logical disjointness.

\subsection{Partition descriptor}

\begin{lstlisting}[caption={Logical partition descriptor.},label={lst:partition}]
PartitionDescriptor := {
  partition_id: PartitionId,
  logical_relation: LogicalRelationRef,
  dimensions: nonempty list<PartitionDimension>,
  coverage: CoveragePredicate,
  partition_key: PhysicalPartitionKey?,
  logical_owner: AuthorityRecord,
  topology_epoch: RoutingEpochId,
  placements: nonempty list<PlacementId>,
  replica_policy: ReplicaPolicy,
  residency_policy: PolicyVersionId,
  consistency_profile: ConsistencyProfileId,
  source_snapshots: map<SourceId, SnapshotId>,
  mapping_versions: set<MappingVersionId>,
  workspace_scope: WorkspaceScope,
  tenant_scope: TenantScope,
  provenance_scope: ProvenanceScope,
  temporal_scope: TemporalScope,
  indexes: set<IndexId>,
  materializations: set<MaterializationId>,
  migration_state:
      Stable | Copying | DualReadable | Cutover | Retiring,
  digest: Digest
}
\end{lstlisting}

The descriptor separates logical coverage from placement.  Two physical
replicas of one partition do not create two logical copies.  Two overlapping
logical partitions can create duplicate logical coverage, so they require an
explicit overlap and multiplicity rule.

A row update is a cross-shard migration whenever it changes the effective
partition key, even if the topology epoch is otherwise unchanged.  This
includes updates to a region, semantic-object assignment, workspace scope, or
other semantic dimension used by the key.  The transition must bind one
read-snapshot or cut, old and new coverage predicates, write ownership for
each phase, and duplicate suppression keyed by stable row identity and
mutation identity.  During copying or dual readability, reads use the named
migration protocol.  The source coverage may exclude the row only after the
destination coverage is sound for the cut and the protocol has prevented loss
or double visibility.  Without those witnesses, the update is deferred or
rejected rather than treated as an in-place mutation.

\subsection{Placement descriptor}

\begin{lstlisting}[caption={Physical placement descriptor.},label={lst:placement}]
PlacementDescriptor := {
  placement_id: PlacementId,
  partition_id: PartitionId,
  replica_id: ReplicaId,
  source_id: SourceId,
  region: RegionId,
  endpoint: EndpointRef,
  capability_profile: CapabilityProfileId,
  observed_snapshot: SnapshotId,
  consistency_profile: ConsistencyProfileId,
  health: Healthy | Degraded | Unreachable | Unknown,
  lag: FreshnessObservation?,
  routing_epoch: RoutingEpochId,
  indexes: set<IndexId>,
  materializations: set<MaterializationId>,
  digest: Digest
}
\end{lstlisting}

Health and lag are observations with timestamps and authorities.  They are not
timeless facts, and they do not override policy or snapshot requirements.

\subsection{Routing epoch}

\begin{lstlisting}[caption={Versioned routing epoch.},label={lst:epoch}]
RoutingEpoch := {
  epoch_id: RoutingEpochId,
  parent: RoutingEpochId?,
  partitions: map<PartitionId, PartitionDescriptor>,
  placements: map<PlacementId, PlacementDescriptor>,
  effective_frontier: OperationFrontier,
  transition: Stable | FromParent(MigrationProtocolRef),
  consistency_profile: ConsistencyProfileId,
  created_by: AuthorityRecord,
  digest: Digest
}
\end{lstlisting}

A request must not silently combine unrelated epochs.  A migration read needs
a P10/P11 rule for old and new coverage, duplicate suppression, visibility,
and write ownership.

\section{Partition Dimensions and Their Failure Modes}
\label{sec:dimensions}

No one dimension is the semantic partitioning scheme.  One deployment may use
region, then tenant, then time ranges, with source-specific physical shards.
Another may partition object families and replicate a small immutable
reference version.  The contract retains the dimensions because flattening
them into one label hides conflicts among isolation, completeness, locality,
and policy.

\begin{landscape}
\begin{longtable}{L{0.13\linewidth}L{0.20\linewidth}L{0.22\linewidth}L{0.25\linewidth}}
\caption{Partition dimensions, possible uses, and correctness risks.}
\label{tab:dimension-analysis}\\
\toprule
Dimension & Candidate selector & Possible use & Main correctness risk \\
\midrule
\endfirsthead
\toprule
Dimension & Candidate selector & Possible use & Main correctness risk \\
\midrule
\endhead
Workspace & Base commit, overlay, branch, immutable commit & Isolate
experimental or uncommitted state while sharing immutable base data & One
workspace observes another overlay or a mixed base/overlay snapshot \\
Tenant & Tenant identity and policy scope & Isolation, quota accounting, and
tenant-local work & Cross-tenant leakage through references, caches, pooled
indexes, or shared materializations \\
Semantic object & Canonical object, relation, typed object family, or path
neighborhood & Co-locate bounded typed traversals & Semantic adjacency does
not predict frequency; a central object can become a hotspot, and reassignment
is a row migration \\
Source & Source identity and declared coverage & Source-native pushdown and
avoidance of irrelevant calls & Coverage may be partial or overlapping;
failure can be mistaken for emptiness \\
Provenance domain & Authority, retention, trust, source, or evidence class &
Local lineage retention and policy evaluation & Derivation crosses domains
and an incomplete explanation is labeled complete \\
Geography & Region, jurisdiction, or residency rule & Policy-admissible
placement, user locality, regional availability & Location, authority,
residency, network distance, and replica freshness disagree; region-key
changes are row migrations \\
Time & Valid time, system time, source frontier, or event range & Range
pruning, archival tiers, incremental refresh & Late data, corrections,
overlapping intervals, or the wrong temporal interpretation \\
Physical key & Hash, range, list, graph cut, or workload group & Balance,
parallelism, and conventional pruning & Skew, correlated hot keys, and
workload drift; mutable keys require cross-shard row migration \\
\bottomrule
\end{longtable}
\end{landscape}

\subsection{Workspace and tenant}

Workspace placement must distinguish immutable shared base state,
workspace-local overlay state, workspace-visible materializations, mutable
publication references, merge/rebase operations, and authority to read
another workspace.  A tenant may own several isolated workspaces.  A
workspace is not a tenant.

Tenant routing is security-sensitive.  A tenant key can be useful, but it
does not prove isolation.  Every tenant-derived exclusion must use
authenticated context and a versioned policy.  A missing tenant constraint is
a rejected request, not permission for a global scan.

\subsection{Semantic object and source}

A semantic-object partition may group a canonical entity with total
functional attributes, a bounded family traversed together, a path
neighborhood, or a schema module with declared crossing edges.  Such a
partition remains a placement hypothesis.  Cardinality, skew, update rate,
data size, workload frequency, and network topology remain physical inputs.

A source partition is interpreted through P5 coverage and capability
contracts.  It may be complete, partial, overlapping, stale, materialized, or
temporarily unavailable.  Source selection asks which sources may contribute
to a canonical query.  Shard selection asks which placements of their data
should be read.  The two decisions are related but not interchangeable.

\subsection{Provenance, geography, and time}

A provenance-domain partition can reduce unnecessary lineage scans or keep
regulated evidence in approved locations.  If a result crosses provenance
domains, the result contract must distinguish complete lineage, domain-scoped
lineage, accepted summaries, policy withholding, failure, and unknown
coverage.  Withheld evidence is not ``no lineage.''

Geographic routing separates legal residency, physical location, coordinator
location, failure domain, network distance, and authority jurisdiction.  A
nearby replica may be stale or unauthorized.  A distant replica may be the
only admissible source.

Temporal routing separates valid time, system time, source frontier,
materialization refresh time, and metadata observation time
\citep{P12S27JensenSnodgrass1999}.  A valid-time predicate cannot
automatically prune a system-time partition.  Late arrivals and corrections
can modify an older valid-time range.

\subsection{Composite, hierarchical, and overlapping coverage}

A composite selector may use
\[
C_s(x)=C_{\mathrm{tenant}}(x)\land
       C_{\mathrm{region}}(x)\land
       C_{\mathrm{time}}(x).
\]
The conjunction does not define precedence, overlap, fallback, replication,
or migration.

One candidate evaluation order is:

\begin{lstlisting}[caption={Proposed policy-first routing order.}]
request
  -> policy-admissible regions
  -> tenant and workspace scopes
  -> semantic and source coverage
  -> time and physical-key partitions
  -> healthy, version-compatible placements
  -> admissible distributed-plan alternatives
\end{lstlisting}

An implementation may reorder pure metadata checks if it preserves the same
admissible set and diagnostics.  The overlap class is explicit:

\begin{lstlisting}[caption={Logical overlap classes.},label={lst:overlap}]
OverlapClass :=
    DisjointLogicalCoverage
  | SameLogicalPartitionReplicas
  | IntentionalLogicalOverlap(DeduplicationRule)
  | TransitionalMigrationOverlap(MigrationProtocolRef)
  | UnknownOverlap
\end{lstlisting}

\code{UnknownOverlap} cannot support a complete exact bag result without an
accepted identity and multiplicity rule.

\section{Route Requests, Decisions, and Obligations}
\label{sec:routing}

\subsection{Route request}

\begin{lstlisting}[caption={Route request.},label={lst:request}]
RouteRequest := {
  request_id: RequestId,
  query: TypedQueryRef,
  query_profile: QueryProfileId,
  workspace: WorkspaceId?,
  tenant: TenantId,
  semantic_scope: set<SemanticObjectId>,
  allowed_sources: set<SourceId>?,
  required_provenance: ProvenanceRequirement,
  geography: GeographyRequirement,
  time_window: TemporalPredicate?,
  source_snapshots: map<SourceId, SnapshotRequirement>,
  consistency: ConsistencyProfileId,
  freshness: FreshnessRequirement,
  residency_policy: PolicyVersionId,
  mapping_versions: set<MappingVersionId>,
  topology_epoch: RoutingEpochId,
  max_fanout: nonnegative integer?,
  execution_budget: ExecutionBudget?,
  failure_policy: Strict | ExplicitPartial | DeclaredStale,
  trace_level: TraceLevel
}
\end{lstlisting}

Tenant is required because a request without an authorization domain is not
admissible.  Workspace is optional because a request may target a published
immutable commit.

\subsection{Route decision}

\begin{lstlisting}[caption={Typed routing outcome.},label={lst:decision}]
RouteDecision :=
  Admitted {
    selected_partitions: nonempty set<PartitionId>,
    selected_placements: nonempty set<PlacementId>,
    excluded_partitions:
        map<PartitionId, PruneCertificate>,
    alternatives:
        nonempty list<DistributedPlanAlternative>,
    obligations: set<RoutingObligation>,
    expected_completeness:
        Complete | ExplicitlyPartial | Unknown,
    topology_epoch: RoutingEpochId,
    decision_digest: Digest
  }
| Deferred {
    missing_metadata: set<MetadataRequirement>,
    retry_condition: RetryCondition
  }
| Rejected {
    code: RoutingDiagnosticCode,
    reasons: nonempty list<RoutingDiagnostic>,
    violated_requirements: set<RequirementRef>
  }
| Unsupported {
    code: RoutingDiagnosticCode,
    unsupported_features: nonempty set<FeatureRef>
  }
\end{lstlisting}

A \code{max\_fanout} limit cannot justify an incomplete ordinary answer.  If
a complete result exceeds the limit, routing must reject, defer, or return an
explicitly partial result under a profile that allows partiality.

\subsection{Routing obligations}

\begin{lstlisting}[caption={Obligations retained by admitted plans.},label={lst:obligations}]
RoutingObligation :=
    CoverageSound(PartitionId, CoveragePredicate)
  | PruningSound(PartitionId, PruneCertificate)
  | CompleteSelection(set<PartitionId>, CompletenessWitness)
  | TenantIsolation(TenantId, PolicyVersionId)
  | WorkspaceIsolation(WorkspaceId, SnapshotId)
  | ResidencyAllowed(PlacementId, PolicyVersionId)
  | CapabilitySatisfied(
        PlacementId, CapabilityProfileId, PlanFragment)
  | SnapshotCompatible(
        set<PlacementId>, ConsistencyProfileId)
  | MappingCompatible(set<MappingVersionId>)
  | ReplicaMultiplicityPreserved(ReplicaEquivalenceWitness)
  | JoinSemanticsPreserved(JoinEquivalenceWitness)
  | PathCoveragePreserved(PathRoutingWitness)
  | MaterializationValid(
        MaterializationId, DependencyWitness)
  | RoutingEpochCoherent(RoutingEpochId)
  | MigrationReadSafe(MigrationWitness)
  | ProvenanceSufficient(ProvenanceRequirement)
\end{lstlisting}

These are proof or validation requests, not explanatory decoration.  An
executor that discards them changes the admitted-plan contract.

\section{Sound Pruning and Complete Selection}
\label{sec:pruning}

\subsection{Coverage soundness}

Let \(I_s\) be the logical contents of partition \(s\) at the accepted
snapshot.  Let \(C_s(x)\) be its versioned coverage predicate and
\(\phi_q(x)\) the query predicate after accepted P2/P5 rewriting.  Coverage
soundness requires
\begin{equation}
  x\in I_s \Longrightarrow C_s(x).
  \label{eq:coverage}
\end{equation}

Logical-disjointness pruning is admissible only if
\begin{equation}
  C_s(x)\land\phi_q(x)
  \quad\text{is unsatisfiable}
  \label{eq:disjoint}
\end{equation}
under the same scalar, null, mapping, time, and policy semantics used by the
query.

\begin{proposition}[Conservative coverage permits false positives, not false
negatives]
\label{prop:conservative}
Assume \cref{eq:coverage} and that the decision procedure for
\cref{eq:disjoint} is sound under the frozen query semantics.  If \(C_s\) is
an exact predicate or a conservative superset, pruning \(s\) after a valid
unsatisfiability result removes no qualifying occurrence from \(I_s\).
\end{proposition}

\begin{proof}
Suppose a qualifying \(x\in I_s\) were removed.  By coverage soundness,
\(C_s(x)\).  Because \(x\) qualifies, \(\phi_q(x)\).  Their conjunction would
therefore be satisfiable, contradicting the valid unsatisfiability result.
The conservative superset may retain extra partitions, but it cannot justify
removing an actual qualifying occurrence.
\end{proof}

\status{\paperreasoned{} under explicit assumptions; P2/P5 instantiation,
decision procedure, metadata maintenance, and execution remain
\obstructed{}.}

\subsection{Prune certificate}

\begin{lstlisting}[caption={Prune certificate.},label={lst:prune}]
PruneCertificate := {
  partition_id: PartitionId,
  query_fragment: PredicateRef,
  coverage_predicate: CoveragePredicate,
  rewrite_trace: RewriteTrace,
  decision:
      Disjoint | PolicyExcluded | SnapshotIncompatible,
  decision_engine: DecisionEngineId,
  assumptions: set<AssumptionRef>,
  mapping_evidence:
      BoundMappings(nonempty set<MappingVersionId>)
    | MappingIndependent(MappingIndependenceWitness),
  policy_version: PolicyVersionId,
  topology_epoch: RoutingEpochId,
  checked_at: SystemTime,
  witness_or_core:
      UnsatWitness | PolicyDecision | CompatibilityFailure,
  digest: Digest
}
\end{lstlisting}

\code{PolicyExcluded} and \code{SnapshotIncompatible} do not establish that a
partition contains no matching data.  They establish that a complete answer
is not currently admissible from the placement.  The request may need a typed
rejection or an explicitly partial result.

\subsection{Safe and unsafe inputs}

Candidate correctness inputs include authenticated tenant and workspace
scope, exact canonical-object coverage, mapping and source-coverage
predicates, enumerated domains, exact equalities, temporal ranges, provenance
requirements, residency policy, materialization dependency scope, exact path
reachability summaries, and exact min/max or set summaries.

Embeddings, sampled histograms, stale statistics, learned source-selection
scores, observed affinity, semantic names, unverified mappings, best-effort
capabilities, health guesses, and natural-language policy labels are
cost inputs or hints.  They do not correctness-prune by themselves.  In
particular, this manuscript reports no vector or full-text pruning or locality
result.

\subsection{Complete selection}

For a request requiring a complete exact result:
\begin{equation}
  \Ans(q,I)
  =
  \Ans\left(q,
    \biguplus_{s\in S_{\mathrm{selected}}} I_s
  \right),
  \label{eq:complete-selection}
\end{equation}
after applying the declared replica and overlap quotient without changing
logical bag semantics.

Equation~\eqref{eq:complete-selection} is a target, not a current theorem.  It
depends on P2 query denotation and P5 source completeness.  A correct
per-shard prune can coexist with an incomplete global answer if a contributing
source or logical partition never entered the candidate cover.

\section{Cross-Shard Paths}
\label{sec:paths}

Let a typed path be
\[
p=f_1;f_2;\cdots;f_n.
\]
Typing establishes composability.  It does not establish placement, index
availability, replication, snapshot compatibility, source coverage, policy
admissibility, or remote-call count.

\begin{lstlisting}[caption={Path placement record.},label={lst:path}]
PathPlacement := {
  path_ref: TypedPathRef,
  edge_realizations: nonempty list<EdgePlacement>,
  endpoint_partitions: set<PartitionId>,
  required_indexes: set<IndexId>,
  source_fragments: list<SourcePlanFragment>,
  exchange_points: list<ExchangePoint>,
  snapshot_obligations: set<SnapshotObligation>,
  provenance_obligations: set<RoutingObligation>,
  topology_epoch: RoutingEpochId
}
\end{lstlisting}

P12 may enumerate local indexed navigation, a local join chain, source-native
query shipping, batched remote lookup, edge or endpoint replication, data
shipping, repartition on a path key, and reuse of a valid path
materialization.  Each alternative must preserve definedness, missing-value
behavior, multiplicity, endpoint identity, mapping and source revisions,
snapshot visibility, policy, and required provenance.  Co-locating endpoints
is insufficient when an intermediate edge or authority decision remains
remote.

\section{Distributed Joins and Exchanges}
\label{sec:joins}

Distributed query processing, semijoins, relation shipping, parallel
exchange, and split execution are established work
\citep{P12S02BernsteinEtAl1981,P12S03BernsteinChiu1981,
P12S04MackertLohman1986,P12S05DeWittGray1992,P12S06Graefe1994,
P12S07DeWittEtAl2013,P12S08ModiEtAl2022}.  P12's role is to enumerate
admissible alternatives without changing the P2/P5 logical join.

\begin{landscape}
\begin{longtable}{L{0.17\linewidth}L{0.20\linewidth}L{0.28\linewidth}L{0.24\linewidth}}
\caption{Distributed join alternatives.}
\label{tab:joins}\\
\toprule
Alternative & Shape & Preconditions & Main costs and risks \\
\midrule
\endfirsthead
\toprule
Alternative & Shape & Preconditions & Main costs and risks \\
\midrule
\endhead
Co-located local & Both inputs already partitioned compatibly & Exact
compatible keys, equality, mapping, and snapshot & Skew and hidden collation
or mapping mismatch \\
Source-native pushdown & Connector executes the join & Exact P5 capability
and source interpretation & Source load, dialect, failure, and returned bytes
\\
Coordinator & Ship one or both inputs to a coordinator & Residency permits
movement and coordinator preserves semantics & Bytes, memory, spill, and
single-site bottleneck \\
Broadcast & Copy a small side to all partitions & Size bound, pinned replica
version, bag and identity rule & Fanout, staleness, and write amplification \\
Repartition & Hash or range both sides by a join key & Compatible equality,
hash/range, null, and scalar semantics & Network, spill, skew, and partition
count \\
Semijoin & Send projected keys, filter remotely, return matches & Exact key
projection and equality & Extra rounds, duplicate keys, and large key sets \\
Bloom-assisted semijoin & Send probabilistic membership filter & False
positives allowed, false negatives forbidden & Build and transfer cost,
saturation, residual traffic \\
Remote lookup & Issue batched key probes & Remote index, bounded outer
cardinality, capability, and rate limits & Calls, throttling, and tail latency
\\
Materialized join & Read a precomputed result & Dependency, frontier,
snapshot, policy, and version validity & Freshness, storage, invalidation,
refresh \\
Replicated-reference join & Join local facts with a pinned small reference
replica & Exact version, digest, bag, equality, and snapshot & Active-pointer
staleness and replica maintenance \\
\bottomrule
\end{longtable}
\end{landscape}

\begin{lstlisting}[caption={Distributed join alternative.},label={lst:join}]
DistributedJoinAlternative := {
  join_ref: LogicalJoinRef,
  strategy: JoinStrategy,
  input_partitions: map<InputSide, set<PartitionId>>,
  execution_sites: set<PlacementId>,
  exchanges: list<Exchange>,
  required_capabilities: set<CapabilityRequirement>,
  required_indexes: set<IndexId>,
  snapshot_contract: SnapshotContract,
  equality_profile: EqualityProfileId,
  multiplicity_profile: MultiplicityProfileId,
  null_profile: NullProfileId,
  residency_check: PolicyDecision,
  provenance_plan: ProvenancePlan,
  obligations: set<RoutingObligation>,
  cost_inputs: CostInputBundle
}
\end{lstlisting}

A cheap join is inadmissible if it changes equality or null semantics, reads
incompatible snapshots, duplicates replicated rows, drops a contributing
source, crosses a residency boundary, cannot produce required provenance, or
uses a stale mapping or materialization.  Only admissible alternatives reach
the P14 cost model.

\subsection{Query shipping, data shipping, and split execution}

Query shipping sends executable work to the data.  Data shipping moves data or
intermediates to another execution site.  Split execution combines remote
fragments, local residuals, exchanges, and materialized stages.  They are plan
properties, not backend-wide labels.

\begin{lstlisting}[caption={Exchange contract.},label={lst:exchange}]
Exchange := {
  exchange_id: ExchangeId,
  mode:
      QueryShipping | DataShipping |
      KeyShipping | FilterShipping,
  from: PlacementId,
  to: PlacementId,
  schema: PhysicalSchemaRef,
  partitioning: ExchangePartitioning,
  ordering: OrderingProperty?,
  estimated_rows: Estimate?,
  estimated_bytes: Estimate?,
  compression: CompressionProfile?,
  encryption: EncryptionProfile?,
  retry_profile: RetryProfile,
  snapshot_token: SnapshotToken?,
  provenance_mode: ProvenanceTransferMode,
  residency_decision: PolicyDecision,
  materialization:
      Temporary | Durable(MaterializationId) | Streaming,
  cost_inputs: CostInputBundle
}
\end{lstlisting}

The planner first establishes whether code and data may cross a proposed
boundary.  It can then compare CPU, I/O, messages, bytes, serialization,
remote calls, throttling, spill, coordination, provenance capture, and
failure exposure.  Semantic metadata may change admissibility or improve an
estimate.  It cannot erase the transfer.

\section{Reference Replicas, Indexes, and Materializations}
\label{sec:stateful}

\subsection{Reference data}

Reference data includes schemas, mappings, code sets, taxonomies, policies,
dimension tables, and small entity dictionaries.  An immutable,
content-addressed version can support a local join only if the request pins
that version, the digest matches, policy permits the placement, equality and
bag semantics match, all dependencies exist, and result provenance records
the version.

A mutable active pointer such as \code{current\_mapping}, \code{main}, or
\code{approved\_policy} requires a P10/P11 observation contract.  A route must
name an exact active reference at an accepted linearization point, a causally
compatible reference, a bounded-stale reference with observed lag, an explicit
conflict or tentative state, or unavailability.  It may not label all of those
states ``current.''

Replicating one logical reference row to \(n\) placements must not multiply a
logical join result by \(n\).  A plan chooses one compatible replica per
logical partition or retains a replica-equivalence witness.

\subsection{Index placement}

\begin{lstlisting}[caption={Local index placement.},label={lst:index}]
IndexPlacement := {
  index_id: IndexId,
  logical_relation: LogicalRelationRef,
  covered_partition: PartitionId,
  placement: PlacementId,
  key_semantics: KeySemanticsId,
  predicate: PredicateRef?,
  ordering: OrderingProperty?,
  snapshot: SnapshotId,
  build_frontier: OperationFrontier,
  mapping_versions: set<MappingVersionId>,
  topology_epoch: RoutingEpochId,
  health: IndexHealth,
  digest: Digest
}
\end{lstlisting}

An index definition and an index build are distinct identities.  Candidate
patterns include tenant-leading composites, workspace-overlay indexes, typed
path edge indexes, source-native indexes, provenance-domain indexes, spatial
indexes within region partitions, temporal indexes, RDF permutations, and
materialization-specific exchange keys.  RDF-3X and Hexastore already
demonstrate rich RDF index permutations
\citep{P12S19NeumannWeikum2008,P12S20WeissEtAl2008}; the existence of such
indexes is not a P12 novelty claim.

A global secondary index is itself distributed, replicated, and
consistency-sensitive.  It may reduce fanout while adding write
amplification, index lag, migration, rebuild, residency, and a new snapshot
relation to base data.  No locality advantage is reported here.  Semantic
adjacency and path indexes remain hypotheses to be measured against equivalent
physical indexes.

Vector and full-text locality require separate physical baselines.  SPANN uses
balanced vector partitions, replicated closure assignments, and query-aware
machine selection for billion-scale approximate nearest-neighbor search
\citep{P12S35ChenEtAl2021}.  Earlybird hash-partitions documents across
servers and maintains concurrently readable, real-time inverted indexes
\citep{P12S36BuschEtAl2012}.  These systems establish baseline mechanisms and
metrics; they do not establish exact semantic pruning or a CatDB locality
result.

\subsection{Distributed materialization}

\begin{lstlisting}[caption={Distributed materialization descriptor.},label={lst:materialization}]
DistributedMaterialization := {
  materialization_id: MaterializationId,
  definition: TypedQueryRef,
  output_schema: LogicalRelationRef,
  partitioning: PartitioningContract,
  placements: nonempty set<PlacementId>,
  dependency_versions: set<ArtifactVersionRef>,
  source_frontiers: map<SourceId, OperationFrontier>,
  topology_epoch: RoutingEpochId,
  consistency_profile: ConsistencyProfileId,
  provenance_profile: ProvenanceRequirement,
  residency_policy: PolicyVersionId,
  refresh_mode: Full | Incremental | Lazy | OnDemand,
  visibility: PrivateWorkspace | Tenant | Published,
  freshness: FreshnessObservation,
  indexes: set<IndexId>,
  state: Building | Ready | Stale | Invalid | Failed | Retiring,
  digest: Digest
}
\end{lstlisting}

P12 may enumerate shard-local partial views, partition-aligned joins,
region-local replicas, a coordinator aggregate, replicated reference views,
source-local pushed views, workspace-private or tenant-shared views, and
partitioned dataflow state.  Reuse is admissible only when definition
coverage, schema and mapping versions, source frontiers, visibility, policy,
residency, provenance, partition overlap, ready state, and topology epoch all
match.

Partial aggregates require an admitted merge algebra.  \code{SUM} and
\code{COUNT} under fixed bag and numeric semantics differ from
\code{AVG}, distinct aggregates, order-sensitive aggregates, top-\(k\), and
nonassociative functions.  There is no generic ``materialize locally and
merge'' rule.

Incremental view maintenance and distributed dataflow are established areas
\citep{P12S30BlakeleyEtAl1986,P12S31McSherryEtAl2013,
P12S32GjengsetEtAl2018,P12S33BudiuEtAl2023}.  Refresh and movement also cross
P6, P10, and P11 boundaries.  Copy completion alone does not prove freshness
or safe cutover.

\section{Proposed Correctness Invariants}
\label{sec:invariants}

The following IDs are local to P12.  They are acceptance obligations, not
current system guarantees.

\begin{longtable}{L{0.11\textwidth}L{0.42\textwidth}L{0.10\textwidth}L{0.20\textwidth}}
\caption{Twelve proposed P12 invariants.}
\label{tab:invariants}\\
\toprule
ID & Proposed invariant & Deps & Status \\
\midrule
\endfirsthead
\toprule
ID & Proposed invariant & Deps & Status \\
\midrule
\endhead
\code{SHARD-01} & Every logical partition descriptor over-approximates its
actual contents at the named snapshot. & P2, P5 & \obstructed{} \\
\code{SHARD-02} & Every excluded partition has a valid disjointness, policy,
or compatibility certificate; only disjointness proves no matching tuple. &
P2, P5 & \obstructed{} \\
\code{SHARD-03} & Selected partitions cover every qualifying logical
occurrence for a complete request. & P2, P5 & \obstructed{} \\
\code{SHARD-04} & Replica selection and intentional overlap preserve logical
bag multiplicity. & P2, P10, P11 & \obstructed{} \\
\code{SHARD-05} & Every admitted local, broadcast, repartition, semijoin,
lookup, or materialized join equals the frozen logical join. & P2, P5 &
\obstructed{} \\
\code{SHARD-06} & Cross-shard path routing preserves endpoint results,
definedness, multiplicity, versions, and provenance. & P2, P5 &
\obstructed{} \\
\code{SHARD-07} & A route uses one coherent topology epoch or an accepted
migration-read protocol, including row-level effective shard-key changes. &
P10, P11 & \obstructed{} \\
\code{SHARD-08} & Every mutable-reference read satisfies the named P11 profile
or returns a typed stale, conflict, or unavailable result. & P10, P11 &
\obstructed{} \\
\code{SHARD-09} & Materialization reuse satisfies dependency, frontier,
policy, workspace, tenant, and topology conditions. & P6, P10, P11 &
\obstructed{} \\
\code{SHARD-10} & Residency and tenant/workspace isolation are checked before
cost-based route selection. & P5, P9, P11 & \openclaim{} design;
runtime \obstructed{} \\
\code{SHARD-11} & Routing explanations are deterministic for the same
versioned metadata and request. & P2, P5, P10, P11 & \openclaim{} \\
\code{SHARD-12} & Semantic-feature benefit is reported only when a named
ablation improves a preregistered endpoint after overhead. &
Bench.\newline harness & \openclaim{} \\
\bottomrule
\end{longtable}

\section{Counterexamples}
\label{sec:counterexamples}

Each counterexample is a required future fixture family.  The consequence is
\paperreasoned{} for the bounded history.  No \CatDB{} runtime is proved.

\begin{counterexample}[CE-01: semantic object creates a hotspot]
Partition all customer facts and edges by semantic object.  Ninety percent of
queries traverse \code{Customer}, and one enterprise customer owns forty
percent of orders.  The grouping is well typed but overloads one partition.
A hash or workload-derived subpartition can do better.
\end{counterexample}
\noindent\textit{Consequence.} Semantic coherence does not imply balance.

\begin{counterexample}[CE-02: mapping rewrite invalidates pruning]
Partition \(S_1\) advertises \code{region = US} under mapping \(m_1\).
Mapping \(m_2\) interprets source code \code{NA} as both US and Canada under a
reconciliation rule.  A Canadian query compiled with \(m_2\) is evaluated
against old \(m_1\) coverage and \(S_1\) is pruned.
\end{counterexample}
\noindent\textit{Consequence.} Coverage and query predicates must share
mapping semantics.

\begin{counterexample}[CE-03: tenant and workspace are conflated]
Tenant \(T\) owns workspaces \(W_1\) and \(W_2\).  \(W_1\) contains an
uncommitted mapping and overlay row.  Routing by tenant alone exposes the row
to a query in \(W_2\).
\end{counterexample}
\noindent\textit{Consequence.} Tenant routing does not establish workspace
isolation.

\begin{counterexample}[CE-04: mutable reference replicas diverge]
Two regions cache \code{active\_mapping}.  During a partition, one points to
\(m_7\) and one to \(m_8\).  A global query joins results compiled under both.
\end{counterexample}
\noindent\textit{Consequence.} Mutable reference replication requires a named
observation contract.

\begin{counterexample}[CE-05: local endpoints hide a remote path edge]
\code{Order} and \code{Country} endpoints are local, but the
\code{Order -> Customer -> Address -> Country} realization stores
\code{Address} in another region.
\end{counterexample}
\noindent\textit{Consequence.} Endpoint co-location does not prove path
locality.

\begin{counterexample}[CE-06: local uniqueness is not global uniqueness]
Two tenant shards each accept customer key \(42\) because uniqueness is
enforced locally.  A global identity query assumes one row.
\end{counterexample}
\noindent\textit{Consequence.} Local constraints do not imply global
constraints.

\begin{counterexample}[CE-07: late data defeats a closed time partition]
A June valid-time partition is marked closed on 1 July.  On 5 July a source
corrects a June event.  A router that trusts only the closed marker excludes
June from a history query.
\end{counterexample}
\noindent\textit{Consequence.} Valid time, system time, and source frontier
remain distinct.

\begin{counterexample}[CE-08: geography and residency disagree]
The lowest-latency replica is in region \(R_2\), but policy \(p_9\) permits
the tenant's raw records only in \(R_1\).  The planner ships data to \(R_2\).
\end{counterexample}
\noindent\textit{Consequence.} Cost does not override residency.

\begin{counterexample}[CE-09: shipping cost reverses with selectivity]
A coordinator expects a remote predicate to select \(0.1\%\) of a table and
ships the query.  The source cannot push the predicate exactly and returns the
whole table.  Key shipping would have transferred less.
\end{counterexample}
\noindent\textit{Consequence.} Capability and residual work are explicit cost
inputs.

\begin{counterexample}[CE-10: broadcast changes bag multiplicity]
A dimension row exists in three replicas.  The coordinator scans all three as
logical partitions and joins them with one fact row, returning three copies.
\end{counterexample}
\noindent\textit{Consequence.} Replica identity must be quotiented without
removing ordinary logical duplicates.

\begin{counterexample}[CE-11: stale materialization crosses mappings]
A revenue view is at source frontier \(100\) under
\code{gross-revenue@4}.  A query asks for frontier \(100\) under
\code{net-revenue@5}.  The router sees only the matching frontier and reuses
the view.
\end{counterexample}
\noindent\textit{Consequence.} Freshness without semantic dependency versions
is insufficient.

\begin{counterexample}[CE-12: routing-epoch cutover loses a read]
Range \([0,100)\) moves from shard \(A\) to shard \(B\).  The routing table
switches to \(B\) before the last copied delta is visible there.  A post-cutover
read misses a record.
\end{counterexample}
\noindent\textit{Consequence.} Cutover needs an accepted P10/P11 migration
protocol.

\begin{counterexample}[CE-13: provenance partition hides a derivation]
A result is stored in the \code{finance} provenance domain, but an input
mapping and reconciliation decision live in \code{identity}.  The router reads
only \code{finance} and labels the lineage complete.
\end{counterexample}
\noindent\textit{Consequence.} Provenance locality cannot redefine
completeness.

\begin{counterexample}[CE-14: graph cut fails under workload drift]
A graph partition minimizes crossing edges for workload \(W_0\).  A new query
family traverses a previously cold, high-degree relation, and nearly every
query crosses shards.
\end{counterexample}
\noindent\textit{Consequence.} Graph partition quality is workload-relative.

\begin{counterexample}[CE-15: local top-\(k\) is incomplete]
Each of ten shards returns its local top ten.  The global score uses a
cross-shard authority weight that local shards do not have.
\end{counterexample}
\noindent\textit{Consequence.} Local top-\(k\) merge needs explicit score and
bound assumptions.

\begin{counterexample}[CE-16: Bloom filter has a false negative]
An incorrectly resized Bloom filter drops a present join key and the remote
side removes its matching row.
\end{counterexample}
\noindent\textit{Consequence.} Bloom-assisted semijoins may admit false
positives, not false negatives.

\begin{counterexample}[CE-17: global index is ahead of base data]
A global index routes key \(k\) to shard \(B\) after a migration record is
published, but the base row is visible only on \(A\) at the requested
snapshot.
\end{counterexample}
\noindent\textit{Consequence.} An index route needs a snapshot relation to
base data.

\begin{counterexample}[CE-18: policy change leaves a reusable cache]
A tenant materialization was built under policy \(p_3\), which allowed a
sensitive field.  Policy \(p_4\) removes that authority.  The physically fresh
view remains in cache and is served.
\end{counterexample}
\noindent\textit{Consequence.} Policy revision participates in
materialization validity.

\section{Prior Art and the Narrow Candidate Delta}
\label{sec:related}

\subsection{Distributed planning and physical execution}

Cost-based access-path and join-order selection predates P12
\citep{P12S01Selinger1979}.  SDD-1 and semijoin work made communication part
of distributed query processing
\citep{P12S02BernsteinEtAl1981,P12S03BernsteinChiu1981}.  R* compared
estimated and actual messages, I/O, and CPU across relation shipping,
fetch-matches, semijoins, and Bloom joins
\citep{P12S04MackertLohman1986}.  Shared-nothing execution, exchange
operators, split execution, and modern exchange placement are also established
\citep{P12S05DeWittGray1992,P12S06Graefe1994,
P12S07DeWittEtAl2013,P12S08ModiEtAl2022}.

The consequence is direct: P12 cannot claim novelty for local, broadcast,
repartition, lookup, coordinator, semijoin, Bloom-assisted, query-shipping, or
data-shipping alternatives.  It must preserve and compare them.

\subsection{Partitioning, elasticity, tenancy, and geography}

Workload-driven placement, single-partition transaction design, deterministic
ordering, and elastic hot/cold movement are established
\citep{P12S09CurinoEtAl2010,P12S10KallmanEtAl2008,
P12S11ThomsonEtAl2012,P12S12TaftEtAl2014}.  Consistent hashing,
high-availability partitioning, global replication, range tablets,
tenant-guided distribution, and multi-tenant schema techniques likewise
precede P12
\citep{P12S13KargerEtAl1997,P12S14DeCandiaEtAl2007,
P12S15CorbettEtAl2012,P12S16ChangEtAl2008,
P12S17ShraerEtAl2018,P12S18AulbachEtAl2008}.

These systems show that keys, workload, geography, tenancy, replication, skew,
and transaction boundaries already guide placement.  Any P12 result must show
what versioned semantic metadata adds after those inputs receive an equal
baseline.

\subsection{Graph placement, logical skipping, and completeness}

RDF-3X, Hexastore, distributed RDF engines, graph partitioning, and graph-aware
query decomposition are close prior art for semantic-object and path claims
\citep{P12S19NeumannWeikum2008,P12S20WeissEtAl2008,
P12S21HuangEtAl2011,P12S22GurajadaEtAl2014,
P12S23KarypisKumar1998}.  Graph cuts can reduce communication for selected
workloads, but overlap, replication, skew, and drift remain.

Pando is a direct logical-partitioning and data-skipping baseline, while
completeness metadata constrains what source exclusion can mean
\citep{P12S24SudhirEtAl2023,P12S25Motro1986}.  R*-tree work and temporal data
management provide established geographic, multidimensional, and time
boundaries \citep{P12S26BeckmannEtAl1990,
P12S27JensenSnodgrass1999}.

\subsection{Provenance, materialization, and federation}

Provenance semirings and database-provenance surveys establish the
compositional and interpretive boundaries for lineage
\citep{P12S28GreenEtAl2007,P12S29CheneyEtAl2009}.  Classic view maintenance,
Differential Dataflow, Noria, and DBSP establish materialized and incremental
state \citep{P12S30BlakeleyEtAl1986,P12S31McSherryEtAl2013,
P12S32GjengsetEtAl2018,P12S33BudiuEtAl2023}.  BigDAWG illustrates
cross-engine islands and movement \citep{P12S34DugganEtAl2015}.

P12 therefore cannot claim novelty for provenance, materialization,
incremental maintenance, distributed dataflow, or polystore movement.

\subsection{Candidate delta}

The plausible CatDB contribution is a typed, versioned placement and routing
contract whose coverage predicates can name workspace, tenant, semantic
object, source, provenance domain, geography, time, and physical key; whose
logical exclusions carry checkable certificates; and whose alternatives
retain mapping, snapshot, authority, residency, provenance, consistency,
replica, routing-epoch, and materialization obligations.  Its added value
would have to survive feature ablation against conventional physical and
communication-aware baselines.

That contribution is \proposed{}.  It becomes a systems result only after
correctness checks, implementation, controlled evaluation, and independent
review.

\section{Claim Ledger}
\label{sec:claims}

The fifteen claim anchors are deliberately uneven.  \code{P12-C14} and
\code{P12-C15} are rejected, so their inclusion prevents later prose from
quietly reviving them.

\begin{landscape}
\small
\begin{longtable}{L{0.10\linewidth}L{0.43\linewidth}L{0.14\linewidth}L{0.23\linewidth}}
\caption{P12 claim anchors and promotion gates.}
\label{tab:claims}\\
\toprule
ID & Candidate claim & Current status & Required evidence \\
\midrule
\endfirsthead
\toprule
ID & Candidate claim & Current status & Required evidence \\
\midrule
\endhead
\code{P12-C01} & P12 can represent the seven requested semantic dimensions
plus physical keys in one typed descriptor. & \openclaim{} design;
implementation \obstructed{} & Accepted schema, fixtures, and cross-language
round trip \\
\code{P12-C02} & Versioned coverage predicates can support sound shard
pruning. & \obstructed{} & Executable P2 query oracle, P5 coverage evaluator,
and \code{SHARD-01/02} \\
\code{P12-C03} & Selected shards can be proved complete for the bounded
profile. & \obstructed{} & Executable P2/P5 denotation and completeness oracle
plus \code{SHARD-03} \\
\code{P12-C04} & Cross-shard paths can be decomposed without changing results.
& \obstructed{} & Executable P2 path oracle, P5 realizations, and
\code{SHARD-06} \\
\code{P12-C05} & P12 can enumerate the named distributed join alternatives
with explicit obligations. & \openclaim{} design; execution \obstructed{} &
Typed plan schema and correctness fixtures \\
\code{P12-C06} & Query and data shipping can respect capability, residency,
and provenance policy. & \obstructed{} & Executable P5/P11 profiles plus
policy fixtures \\
\code{P12-C07} & Version-pinned immutable reference replicas can support exact
local joins. & \openclaim{} & Digest, placement, equality, bag, and snapshot
tests \\
\code{P12-C08} & Mutable active references can be read without silent
consistency downgrade. & \obstructed{} & Executable P10/P11 profiles and
histories \\
\code{P12-C09} & Semantic-object, path, vector, or full-text indexes improve
locality. & \openclaim{} & Matched physical indexes, SPANN/Earlybird-style
baselines, retrieval-specific workloads, ablation, skew, and drift \\
\code{P12-C10} & Distributed materialization placement preserves validity. &
\obstructed{} & P6/P10/P11 frontiers, dependencies, recovery, and
\code{SHARD-09} \\
\code{P12-C11} & Routing-epoch migration preserves reads and writes under a
named profile. & \obstructed{} & P10/P11 migration model and fault histories
\\
\code{P12-C12} & Semantic metadata improves a preregistered routing or runtime
endpoint. & \openclaim{} & Baseline-controlled ablations including metadata
overhead \\
\code{P12-C13} & Routing explanations are deterministic and auditable. &
\openclaim{} & Canonical metadata, traces, and insertion-order tests \\
\code{P12-C14} & Semantic metadata eliminates network and consistency costs. &
\rejected{} & Conflicts with scope, prior work, and counterexamples \\
\code{P12-C15} & P12 currently has an executable implementation or benchmark.
& \rejected{} & Current repository audit \\
\bottomrule
\end{longtable}
\end{landscape}

\section{Evaluation Contract, Not Results}
\label{sec:evaluation}

\subsection{Safety gate}

No timing result may be interpreted until:

\begin{enumerate}
  \item query and result semantics are frozen;
  \item source coverage and failure semantics are accepted;
  \item every treatment returns the required result bag and provenance;
  \item bounded exhaustive and generated pruning fixtures observe no false
  negatives;
  \item tenant, workspace, residency, snapshot, and materialization gates pass;
  \item migration histories pass for the named epoch protocol.
\end{enumerate}

This manuscript executes none of those system checks and reports no benchmark.

\subsection{Baselines and treatments}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.24\textwidth}Y}
\toprule
Baseline & Comparison purpose \\
\midrule
Hash and range/time partitioning & Balance, fanout, conventional pruning, and
repartition joins \\
Physical statistics and capabilities only & Isolate the effect of semantic
metadata \\
R*-style communication alternatives & Messages, I/O, CPU, shipping,
fetch-matches, semijoin, and Bloom \\
Schism and E-Store style placement & Workload graph, balance, skew, movement,
and drift \\
Pando-style logical skipping & Metadata-rich logical predicate pruning \\
Distributed RDF and graph partitioning & Semantic-object and path workloads \\
SPANN-style distributed vector ANNS & Recall at \(k\), machine fanout,
partition balance, closure replication, memory/disk cost, and index build \\
Earlybird-style sharded inverted index & Term and posting placement, query
fanout, ingestion/indexing latency, concurrent updates, and freshness \\
PolyBase and exchange placement & Pushdown, split execution, and movement \\
Full recomputation plus IVM/dataflow & Distributed materialization \\
\bottomrule
\end{tabularx}
\caption{Minimum baseline families.  A reconstruction does not inherit the
original system's published performance.}
\label{tab:baselines}
\end{table}

Treatments add one feature at a time: tenant, workspace, semantic object/path,
source coverage, provenance domain, geography/residency, time/frontier, and
semantic materialization metadata.  The full treatment comes last.  Feature
order must be randomized or preregistered when interactions matter.

Vector workloads must pin dimension, distance, target recall, dataset size,
partition count, closure replication, update rate, and index-build resources.
Full-text workloads must pin corpus, tokenizer, term and document skew,
partitioning, posting replication, ingestion rate, freshness, top-\(k\)
semantics, and query fanout.  Neither workload may reuse relational
completeness language for an approximate retrieval result.

\subsection{Workloads and metrics}

The workload matrix varies partition and replica count, regions, tenants,
workspace depth and overlay fraction, semantic-object skew, source type and
overlap, provenance completeness, temporal width and late arrivals, join
selectivity and skew, path length, network behavior, snapshot compatibility,
routing-epoch phase, materialization validity, index state, and strict,
partial, or stale failure policy.

Correctness metrics include result-bag and provenance equality, pruning false
negatives and false positives, policy leaks, fractured reads, migration
loss/duplication, and invalid materialization reuse.  Planning metrics include
alternatives, metadata bytes, prediction error, certificate size, and
maintenance cost.  Execution metrics include first-row and total latency,
throughput, bytes, messages, calls, CPU, I/O, memory, spill, retries,
rejections, and movement.

\subsection{Falsifiers}

\begin{longtable}{L{0.34\textwidth}L{0.56\textwidth}}
\caption{Exact future falsifiers.}
\label{tab:falsifiers}\\
\toprule
Hypothesis & Falsifier \\
\midrule
\endfirsthead
\toprule
Hypothesis & Falsifier \\
\midrule
\endhead
Pruning is sound & Any qualifying occurrence on a disjointness-pruned
partition \\
Selection is complete & Any required occurrence absent from the selected
logical union \\
Replica handling preserves bags & Any multiplicity change caused by physical
replica count \\
Path routing preserves semantics & Any endpoint, missingness, multiplicity,
version, or provenance mismatch \\
A join alternative is exact & Any normalized result or provenance mismatch \\
Epoch migration is safe & Any lost, duplicated, fractured, or unauthorized
observation outside the accepted profile \\
Materialization reuse is valid & Reuse after an invalidating dependency,
policy, frontier, workspace, or topology change \\
Semantic metadata improves pruning & No benefit over physical metadata after
overhead, or the benefit vanishes under ablation \\
Semantic metadata improves planning & No preregistered reduction in cost error
or admissible execution cost \\
Semantic placement improves locality & No reduction in crossings, bytes, or
latency, or reversal under declared drift \\
\bottomrule
\end{longtable}

Future statistical reporting must pin source, compiler, connector, database,
topology, and protocol versions; preserve failures and rejected plans; use
repeated randomized schedules; separate cold and warm states; report
per-workload results; retain seeds and minimized counterexamples; count
metadata maintenance; and never substitute extrapolation for an unexecuted
scale.

\section{Formalization and Implementation Roadmap}
\label{sec:roadmap}

\subsection{Finite oracle and proof boundary}

A future independent finite oracle should enumerate typed partition covers,
evaluate frozen queries before and after partitioning, check disjointness
pruning, quotient replicas while preserving bags, compare join alternatives,
evaluate paths, check admitted aggregate algebras, and minimize false-negative
or mixed-epoch histories.

Proposed Lean targets are:

\begin{lstlisting}[caption={Proposed finite Lean target names.}]
Shard.coverage_sound
Shard.prune_sound
Shard.selection_complete
Shard.replica_quotient
Shard.local_join_equiv
Shard.semijoin_equiv
Shard.path_route_equiv
Shard.partial_aggregate_merge
Shard.epoch_coherence
\end{lstlisting}

Each theorem must state bag, null, scalar, mapping, completeness, and snapshot
assumptions.

Finite tests would not prove all sizes.  Lean query equivalence would not
verify a connector or router.  Semijoin equivalence would not make a semijoin
cheaper.  Coverage proof would not establish metadata currency.  Epoch
coherence would not establish liveness.

\subsection{Staged implementation}

\begin{enumerate}
  \item \textbf{R0, executable dependency profiles:} bind the accepted P2
  query, P5 source, P10 topology/migration, and P11 observation contracts to
  normalized executable interfaces and independent oracles.  Status:
  \obstructed{}.
  \item \textbf{R1, language-neutral schemas:} define canonical envelopes for
  descriptors, epochs, requests, decisions, certificates, exchanges, joins,
  indexes, materializations, and counterexamples.  Status: \openclaim{} after
  R0.
  \item \textbf{R2, independent finite oracle:} implement the bounded model
  without importing Rust decisions.  Status: \obstructed{}.
  \item \textbf{R3, Lean core:} prove only the frozen \code{SHARD-*} subset and
  publish axiom and coverage tables.  Status: \obstructed{}.
  \item \textbf{R4, metadata and routing layer:} implement descriptor,
  coverage, pruning, topology, route, explanation, and diagnostic modules.
  Status: \obstructed{}; no crate exists.
  \item \textbf{R5, physical alternatives:} add typed local, broadcast,
  repartition, semijoin/Bloom, lookup, shipping, and materialization
  alternatives.  Status: \obstructed{}.
  \item \textbf{R6, topology and fault simulator:} exercise skew, lag, source
  failure, epoch transition, late updates, and policy/mapping change.  Status:
  \obstructed{}.
  \item \textbf{R7, backend execution:} integrate only P5-conformant connectors
  and compare every distributed result with the independent oracle.  Status:
  \obstructed{}.
  \item \textbf{R8, benchmark harness:} implement the baseline, ablation,
  measurement, and falsification contract.  Status: \obstructed{}.
\end{enumerate}

\section{Exact Nonclaims and Limitations}
\label{sec:nonclaims}

For avoidance of doubt:

\begin{enumerate}
  \item \CatDB{} does not currently implement semantic sharding.
  \item \CatDB{} does not currently implement distributed query planning.
  \item No P12 route, join, pruning, materialization, or benchmark result has
  been measured.
  \item No semantic metadata feature has shown a performance benefit.
  \item No P12 pruning rule has been machine checked.
  \item A semantic object is not a physical partition.
  \item A typed path is not a placement map.
  \item A source partition is not necessarily complete or disjoint.
  \item A tenant key does not by itself prove isolation.
  \item A workspace is not a tenant.
  \item A provenance domain is not necessarily a complete derivation boundary.
  \item Geography, residency, authority, and network distance are distinct.
  \item Valid time, system time, source frontier, and refresh time are
  distinct.
  \item Replication does not imply freshness or authority.
  \item An active reference is not immutable because its targets are
  immutable.
  \item A global index is not free of replication and consistency cost.
  \item A materialization is not valid merely because its rows are present.
  \item Graph partitioning does not eliminate edge cuts.
  \item A semijoin or Bloom filter is not always cheaper than relation
  shipping.
  \item A distributed join is not correct because it is cheap.
  \item Semantic metadata does not eliminate network transfers.
  \item Semantic metadata does not eliminate consistency or coordination cost.
  \item Category theory does not change CAP, consensus, failure, or latency
  boundaries.
  \item P12 enumerates admissible alternatives; P14 owns cost-based choice.
  \item External system results do not establish CatDB behavior.
  \item This paper reports no vector-search locality result.
  \item This paper reports no full-text locality result.
  \item A row-level update is not local when it changes the effective shard
  key.
  \item An absent or unknown mapping binding does not establish
  mapping-independent coverage.
\end{enumerate}

\subsection{Open and obstructed questions}

Blocked questions include the exact P2 query denotation, P5 source-coverage
language and complete-answer rule, P10 epoch and migration operations, P11
snapshot cut and active-reference profiles, P6 materialization frontier, P9
workspace isolation, and P13 provenance completeness.

Open design questions include a practical predicate language for certificates,
maintenance of conservative coverage under mapping change, composite
hierarchies, high-degree object handling, exact path summaries, semijoin
crossover points, zero-false-negative Bloom implementations, index lag,
admitted partial aggregates, explicit incomplete results, metadata overhead,
workload drift, and useful operator explanations.

\section{Conclusion}
\label{sec:conclusion}

Semantic metadata can inform distributed placement, but it does not turn
meaning into locality.  The same object can span sources, regions,
workspaces, policies, mappings, and snapshots.  The contract in this paper
keeps those scopes separate, requires checkable exclusion certificates, and
retains physical and consistency obligations in every candidate plan.

The current result is a falsifiable specification.  It says what an eventual
router must prove, reject, expose, and measure.  It does not show that CatDB
routes a query, prunes a shard, executes a distributed join, preserves a
migration read, or improves locality.  Those claims remain blocked until the
accepted P2, P5, P10, and P11 boundaries are instantiated as executable
profiles and a bounded implementation passes correctness gates before
performance evaluation.

\appendix

\section{Disputed Claims}
\label{app:disputes}

\begin{longtable}{L{0.13\textwidth}L{0.50\textwidth}L{0.25\textwidth}}
\caption{Claims rejected by the specification.}
\label{tab:disputes}\\
\toprule
ID & Disputed claim & Reason for rejection \\
\midrule
\endfirsthead
\toprule
ID & Disputed claim & Reason for rejection \\
\midrule
\endhead
\code{P12-D01} & A typed path is physically local. & Typing has no placement
semantics. \\
\code{P12-D02} & Semantic-object partitions are naturally balanced. & CE-01
and workload/skew prior art. \\
\code{P12-D03} & Semantic metadata eliminates cross-shard joins. & Semantic
relations commonly cross partitions. \\
\code{P12-D04} & A replicated reference is current everywhere. & Mutable
references require P10/P11 guarantees. \\
\code{P12-D05} & A freshness timestamp proves materialization validity. &
Dependencies, mappings, policies, and frontiers also matter. \\
\code{P12-D06} & A Bloom join can safely lose positives. & False negatives
change the result. \\
\code{P12-D07} & Tenant partitioning proves isolation. & Caches, indexes,
references, and policy checks may cross tenants. \\
\code{P12-D08} & Region-local execution is policy-admissible. & Location,
authority, and residency are distinct. \\
\code{P12-D09} & Global indexes remove fanout without consistency cost. & The
index is a distributed replicated structure. \\
\code{P12-D10} & Local uniqueness implies global uniqueness. & CE-06. \\
\code{P12-D11} & Closed time partitions never change. & Late arrivals and
corrections. \\
\code{P12-D12} & Graph partitioning removes network communication. & Cuts,
overlap, skew, and workload drift remain. \\
\code{P12-D13} & Category theory changes CAP or consensus boundaries. & No
message or ordering mechanism follows from functoriality. \\
\code{P12-D14} & The route with minimum estimated bytes is admissible. &
Semantics, snapshots, residency, and provenance precede cost. \\
\code{P12-D15} & The current repository implements P12. & The local audit
found no P12 runtime surface. \\
\code{P12-D16} & A row-level shard-key update is an in-place local mutation. &
Changing the effective partition key is a cross-shard migration. \\
\code{P12-D17} & An omitted mapping version means coverage is
mapping-independent. & Mapping independence requires a checkable witness;
missing or invalid evidence fails closed. \\
\bottomrule
\end{longtable}

\section{Review and Reproduction Gate}
\label{app:review}

A future accepted manuscript must receive distributed-query, database-systems,
graph/RDF, consistency, security/residency, implementation, reproducibility,
and adversarial claim review.  Reviewers should ask whether:

\begin{enumerate}
  \item query semantics and source coverage are explicit;
  \item every excluded partition has the correct certificate class;
  \item the eight partition dimensions remain distinct;
  \item replicas, overlap, and bag duplicates remain distinct;
  \item all movement and snapshot obligations are visible;
  \item mutable references use a named P11 profile;
  \item migration histories cover loss, duplication, and fractured reads;
  \item policy checks precede cost;
  \item physical-only baselines receive the same ordinary statistics;
  \item semantic features are ablated individually;
  \item maintenance and planning overhead are included;
  \item failures, timeouts, partial answers, and stale answers are retained;
  \item correctness failure blocks performance interpretation;
  \item no sentence implies that network or consistency cost disappeared;
  \item row-level shard-key changes carry cross-shard migration obligations;
  \item mapping-independent pruning has a checkable independence witness;
  \item current evidence labels match actual artifacts.
\end{enumerate}

This correction draft follows an independent round-one review that requested
minor revisions.  It has not undergone terminal acceptance review.  Its
companion reproducibility record covers only the isolated LaTeX build,
citation closure, source hashes, and rendered-page inspection.

\bibliographystyle{plainnat}
\bibliography{references}

\end{document}
