% !TEX program = pdflatex
%=====================================================================
% I.tex
%
% Self-contained, scope-restricted manuscript source.
%
% Build:
%   pdflatex -interaction=nonstopmode -halt-on-error I.tex
%   pdflatex -interaction=nonstopmode -halt-on-error I.tex
% Repeat if cross-reference warnings remain.
%
% No external graphics, bibliography database, or shell escape required.
%
% Revision notes:
% - The primitive characterization and later implementation interfaces
%   are kept logically separate.
% - All quantum spectators are explicitly consumed or returned.
% - The path-map lemma permits higher-order internal syntax but has a
%   first-order quantum/classical input-output interface.
% - Record equations compare classical observations, not complete
%   residual instruments.
% - The direction of the Psy02-B process-equality implication is corrected.
% - A self-contained equal-record/different-residual example is included.
% - Coherent recording, destructive Enter, and represented nondestructive
%   measurement are distinguished explicitly.
% - Stability budgets include auxiliary record registers and intermediate
%   whole-register tests.
% - Global live-qubit budgets are distinguished from scheduled laboratory
%   peak bounds.
% - Companion citations use supplied manuscript identifiers and versions;
%   they are not represented as independently verified journal articles.
% - Unavailable companion figures are not claimed to have been recovered.
%
% Verification status:
% This source has not been compiled in the present interface.
% No mechanized proof, verified page count, or compiler certificate is
% claimed. Bibliographic status was checked on 10 October 2026.
%=====================================================================

\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1.05in]{geometry}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem}
\usepackage{array,booktabs,tabularx}
\usepackage{xcolor}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,calc}
\usepackage[font=small,labelfont=bf]{caption}
\usepackage[hidelinks]{hyperref}

\hypersetup{
  pdftitle={Born--Luders as the unique measurement strategy of the Enter calculus},
  pdfauthor={Ngo Cheung},
  pdfsubject={Finite operational characterization of destructive quantum measurement}
}

\setlength{\emergencystretch}{3em}
\setlength{\parskip}{2pt}
\setlist{itemsep=3pt,topsep=5pt}
\allowdisplaybreaks
\numberwithin{equation}{section}
\setcounter{secnumdepth}{2}
\setcounter{tocdepth}{1}
\urlstyle{same}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\newtheorem{example}[theorem]{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\Unit}{\mathbf 1}
\newcommand{\Bit}{\mathsf{Bit}}
\newcommand{\Q}{\mathsf Q}
\newcommand{\lto}{\multimap}
\newcommand{\New}{\mathsf{new}}
\newcommand{\Enter}{\mathsf{Enter}}
\newcommand{\lett}{\mathsf{let}}
\newcommand{\inn}{\mathsf{in}}
\newcommand{\CNOT}{\mathsf{CNOT}}
\newcommand{\copyBit}{\mathsf{copyBit}}
\newcommand{\dropBit}{\mathsf{dropBit}}
\newcommand{\EC}{\mathsf{EC}}
\newcommand{\ECB}{\mathsf{EC}_{\mathrm{Born}}}
\newcommand{\Theory}{\mathsf T}
\newcommand{\Strategy}{\mathsf S}
\newcommand{\BornStrategy}{\mathsf B}
\newcommand{\Prob}{\mathsf P}
\newcommand{\Update}{\mathsf U}
\newcommand{\Born}{\mathsf{Born}}
\newcommand{\Cstar}{(\mathrm C)^\star}
\newcommand{\NSstar}{(\mathrm{NS})^\star}
\newcommand{\Nstar}{(\mathrm N)^\star}
\newcommand{\Kstar}{(\mathrm K)^\star}
\newcommand{\Rstar}{(\mathrm R)^\star}
\newcommand{\redD}{\longrightarrow_{\mathrm d}}
\newcommand{\redB}{\longrightarrow_{\mathrm B}}
\newcommand{\redS}{\longrightarrow_{\Strategy}}
\newcommand{\TV}{d_{\mathrm{TV}}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\ket}[1]{\lvert #1\rangle}
\newcommand{\bra}[1]{\langle #1\rvert}
\newcommand{\ketbra}[2]{\lvert #1\rangle\!\langle #2\rvert}
\newcommand{\braket}[2]{\langle #1\mid #2\rangle}
\newcommand{\norm}[1]{\left\lVert #1\right\rVert}
\newcommand{\abs}[1]{\left\lvert #1\right\rvert}
\newcommand{\ifte}[3]{%
  \mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
\newcommand{\infrule}[2]{\dfrac{\;#1\;}{\;#2\;}}
\newcommand{\doi}[1]{%
  \href{https://doi.org/#1}{\nolinkurl{#1}}}
\newcommand{\SourceLabel}[1]{\texttt{\detokenize{#1}}}

\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\marg}{marg}
\DeclareMathOperator{\own}{own}
\DeclareMathOperator{\Obs}{Obs}
\DeclareMathOperator{\Defer}{defer}
\DeclareMathOperator{\supp}{supp}

\newcommand{\scopebox}[2]{%
  \par\medskip\noindent
  \fbox{\begin{minipage}{%
    \dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
  \textbf{#1}\par\smallskip #2
  \end{minipage}}
  \par\medskip
}

\tikzset{
  proofbox/.style={
    draw,rounded corners,align=center,font=\small,
    minimum height=1.0cm,inner sep=5pt
  },
  proofarrow/.style={-{Stealth[length=2mm]},thick}
}

\title{\textbf{Born--L\"uders as the unique measurement strategy\\
of a strictly linear quantum \(\lambda\)-calculus}\\[3pt]
\large A self-contained finite characterization in the Enter calculus}
\author{Ngo Cheung}
\date{}

\begin{document}
\maketitle

\begin{abstract}
We characterize the destructive computational-basis measurement
primitive of a fixed strictly linear quantum lambda calculus.
The admissible strategies are state sufficient, have normalized
outcome laws, and assign pure conditional residuals to
positive-probability branches. The argument separates two logical
layers. First, Born probabilities and destructive projective update
define a concrete calculus with type safety, a syntactic linear step
bound, observational confluence, circuit adequacy, semantic
no-cloning, and internal no-signaling. Second, only the measurement
transition is left unknown. Composability, no-signaling, nullity,
continuity, and a typed record equation are satisfied by the Born
strategy and uniquely determine it within the stated class.
Two independent finite constructions establish diagonal anchoring
without the record equation. Whole-register records then determine
coherent outcome laws, composability determines partial readout,
and branch-specific continuation tests determine residual rays.
We also prove resource-budgeted stability estimates and derive
mixed-state, adaptive, and finite-instrument consequences.
A static appendix constructs positive non-Born marginal assignments
and exhibits their failure of operational nullity.
Later record, decoder, instrument, and cutoff interfaces are kept
separate from the premises of primitive uniqueness.
\end{abstract}

\scopebox{Scope}{%
The result is conditional on the structural class stated below.
It is not a reconstruction of qubit kinematics, an independence
theorem for the five requirements, or a proof of record-free
uniqueness. It is not a physical Frauchiger--Renner no-go theorem.
No field-theoretic instrument, infinite apparatus, microscopic
evaporation channel, horizon construction, characteristic quantum
coefficient, or energy-uniform channel approximation is derived.}

\tableofcontents

%=====================================================================
\section{Introduction and logical scope}
\label{sec:introduction}
%=====================================================================

Fix a quantum programming language: its types, allocation,
tensor composition, coherent gates, and classical control.
Leave only the outcome law and conditional update of a destructive
measurement primitive unspecified. Which strategies interpret that
primitive while satisfying specified equations between experiments?

The primitive considered here is \(\Enter\), destructive
computational-basis readout of a finite qubit register.
A configuration contains one global pure state. Runtime qubit names
are access rights to its tensor factors; they are not individual
pure-state assignments. Readout consumes the measured names,
returns classical bits, and leaves a state on the surviving factors.

This manuscript gives a self-contained, scope-restricted
presentation of the finite Enter-calculus characterization
of Cheung~\cite{EnterCalculus}.
The central result is Theorem~\ref{thm:main}.
Here ``Born--L\"uders'' means projective conditioning followed by
removal of the measured factors, not retention of those factors.
The distinction between outcome probabilities and state change is
essential; the historical projective update is discussed in
L\"uders' work and its English translation~\cite{LudersTranslation}.

\subsection{Two logical layers}

\paragraph{Layer I: specified semantics.}
The concrete calculus \(\ECB\) has Born probabilities and destructive
projective update by definition. Safety, termination, confluence,
adequacy, and no-signaling are theorems about that already specified
semantics.

\paragraph{Layer II: unknown measurement.}
A strategy \(\Strategy=(\Prob,\Update)\) replaces only the measurement
transition. The structural class fixes the domain of the
characterization. The five requirements
\[
\Cstar,\qquad \NSstar,\qquad \Nstar,\qquad
\Kstar,\qquad \Rstar
\]
are conditions on the unknown strategy.

The two directions are
\[
\BornStrategy\models\Theory,
\qquad
\Strategy\models\Theory
\Longrightarrow \Strategy=\BornStrategy.
\]
The first establishes inhabitation; the second establishes
uniqueness within the declared class. A concrete Born calculation
is not available for an unknown strategy merely because both
strategies interpret the same syntax.

\subsection{Assumption ledger}

\begin{center}
\small
\begin{tabularx}{\linewidth}{@{}p{.22\linewidth}X@{}}
\toprule
Declared, not derived &
Finite-dimensional qubit kinematics, ordinary tensor composition,
global pure states, coherent gates, state sufficiency, normalized
outcome laws, pure positive-branch residuals, the structural
conditions of Assumption~\ref{ass:strategy-class}, and the five
requirements of Definition~\ref{def:requirements}.\\
\addlinespace
Checked syntactically &
The record transformation is definable and well typed using
allocation and CNOT. Every quantum spectator is consumed or returned.\\
\addlinespace
Derived &
The metatheory of the specified calculus; diagonal anchoring from
the first four requirements; and, using records, Born laws and
destructive projective residual rays for every admissible strategy.\\
\bottomrule
\end{tabularx}
\end{center}

No silent quantum deletion is added to the language.
Algebraic partial traces used in proofs are not term-level
weakening operations.

\subsection{Relation to other approaches}

Quantum lambda calculi with classical control already provide
well-developed operational and typing frameworks; the affine
calculus of Selinger and Valiron is a representative
example~\cite{SelingerValiron}.
The present language uses strict, branch-wise linear ownership.
Its characterization question concerns a variable measurement
transition in a fixed language, rather than type safety alone.

Gleason's theorem concerns measures on Hilbert-space subspaces
subject to a different assumption package~\cite{Gleason}.
The present proof does not begin with probabilities for all effects
or projectors. It characterizes one fixed-basis primitive; other
measurements are represented later by programs.

The uniform-correlation argument uses a system/environment
permutation mechanism related to envariance
arguments~\cite{ZurekEnvariance}.
Its premises are stated explicitly as operational requirements.
The importance of distinguishing such premises from derived
probabilities is emphasized in the analysis of Schlosshauer and
Fine~\cite{SchlosshauerFine}.
Neither envariance nor a separate noncontextuality axiom is imported
as an additional premise.

Finally, the companion manuscripts discussed in
Section~\ref{sec:interfaces} concern implementation and observational
boundaries. They are not premises of Theorem~\ref{thm:main}.

%=====================================================================
\section{Language, typing, and ownership}
\label{sec:syntax}
%=====================================================================

\subsection{Types and terms}

Types are
\[
A,B::=\Unit\mid\Bit\mid\Q\mid A\lto B\mid A\otimes B.
\]
Tensor powers are right nested:
\(A^{\otimes0}=\Unit\) and \(A^{\otimes1}=A\).
The empty tuple is \(*\). Linear pairing and elimination implement
the usual associativity and unit isomorphisms.
Tuple notation suppresses these administrative maps, not resource
uses.

Terms are
\[
\begin{aligned}
t,u::={}&x\mid q\mid *\mid0\mid1
\mid\lambda x{:}A.\,t
\mid t\,u
\mid\langle t,u\rangle\\
&\mid\lett\,\langle x,y\rangle=t\ \inn\ u
\mid\lett\,*=t\ \inn\ u
\mid\ifte{t}{u}{u'}\\
&\mid\New\mid V(t)\mid\Enter(t).
\end{aligned}
\]
Source variables are \(x,y,\ldots\).
Runtime names \(q,r,\ldots\) are introduced by allocation.
Source programs contain no runtime names.
Every finite-register unitary is available as a gate; a dense-gate
variant is given in Corollary~\ref{cor:dense}.

We abbreviate
\((\lambda x{:}A.\,u)t\) by
\(\lett\,x=t\ \inn\ u\).
Tuple-pattern binders abbreviate iterated linear tuple elimination.

\subsection{Typing}

Contexts assign types to distinct source variables and runtime names.
Contexts separated in a multiplicative rule are disjoint.
There is no structural weakening or contraction.
\[
\infrule{}{x{:}A\vdash x:A}
\qquad
\infrule{}{q{:}\Q\vdash q:\Q}
\qquad
\infrule{}{\vdash *:\Unit}
\qquad
\infrule{}{\vdash0:\Bit}
\qquad
\infrule{}{\vdash1:\Bit}
\]
\[
\infrule{\Gamma,x{:}A\vdash t:B}
{\Gamma\vdash\lambda x{:}A.\,t:A\lto B}
\qquad
\infrule{\Gamma\vdash t:A\lto B\quad\Delta\vdash u:A}
{\Gamma,\Delta\vdash t\,u:B}
\]
\[
\infrule{\Gamma\vdash t:A\quad\Delta\vdash u:B}
{\Gamma,\Delta\vdash\langle t,u\rangle:A\otimes B}
\]
\[
\infrule{\Gamma\vdash t:A\otimes B\quad
\Delta,x{:}A,y{:}B\vdash u:C}
{\Gamma,\Delta\vdash
\lett\,\langle x,y\rangle=t\ \inn\ u:C}
\]
\[
\infrule{\Gamma\vdash t:\Unit\quad\Delta\vdash u:C}
{\Gamma,\Delta\vdash\lett\,*=t\ \inn\ u:C}
\]
\[
\infrule{\Gamma\vdash b:\Bit\quad
\Delta\vdash u:A\quad\Delta\vdash u':A}
{\Gamma,\Delta\vdash\ifte{b}{u}{u'}:A}
\]
\[
\infrule{}{\vdash\New:\Q}
\qquad
\infrule{\Gamma\vdash t:\Q^{\otimes n}}
{\Gamma\vdash V(t):\Q^{\otimes n}}
\qquad
\infrule{\Gamma\vdash t:\Q^{\otimes n}}
{\Gamma\vdash\Enter(t):\Bit^{\otimes n}}.
\]
The conditional is additive: its alternatives use the same context,
but only one alternative executes.
The bit \(1\) selects the then-branch and \(0\) the else-branch.

\subsection{Branch-wise linearity}

\begin{definition}[Occurrence selection and ownership]
An occurrence selection retains the guard of each conditional and
exactly one of its alternatives, recursively.
It is a selection in the syntax tree, not a reduction.
The set \(\own(t)\) consists of the free runtime names of \(t\).
\end{definition}

\begin{lemma}[Branch-wise linearity]
\label{lem:branchwise}
If \(\Gamma\vdash t:A\), every resource in \(\Gamma\) has exactly one
free occurrence in every occurrence selection.
The free runtime names of \(t\) are exactly the runtime names in
\(\Gamma\), and the two alternatives of a conditional have identical
free-runtime-name sets.
\end{lemma}

\begin{proof}
Induct on typing. Multiplicative rules partition contexts.
Abstraction removes its bound variable from the free context.
For a conditional, the guard uses its own context, and either
selected alternative uses the shared alternative context once.
The same induction proves equality of the alternatives' name sets.
\end{proof}

A resource may therefore appear in both unexecuted alternatives
without being duplicated during execution.

Classical copying and deletion are definable:
\[
\begin{aligned}
\copyBit
&=\lambda b{:}\Bit.\,
\ifte{b}{\langle1,1\rangle}{\langle0,0\rangle},\\
\dropBit
&=\lambda b{:}\Bit.\,\ifte{b}{*}{*}.
\end{aligned}
\]
Their types are
\(\Bit\lto\Bit\otimes\Bit\) and \(\Bit\lto\Unit\).
Finite classical functions are definable by finite case analysis.

\begin{remark}[Ownership is not semantic no-cloning]
The type \(\Q\lto\Q\otimes\Q\) is inhabited:
\[
\lambda q{:}\Q.\,\langle q,\New\rangle
\]
has that type.
Typing prohibits duplicate ownership, not all terms with a possible
cloning type. Universal cloning is excluded semantically in
Theorem~\ref{thm:nocloning}.
Quantum consumption by an explicit measurement followed by classical
deletion is also different from structural quantum weakening.
\end{remark}

%=====================================================================
\section{Configurations and specified Born semantics}
\label{sec:concrete}
%=====================================================================

\subsection{One global state}

For a finite live-name set \(L\), write
\[
\mathcal H_L=\bigotimes_{q\in L}\mathbb C^2.
\]
An ordering is chosen for matrices and bit strings.
Changing the ordering simultaneously permutes names and tensor
factors.

For \(S\subseteq L\), let \(\overline S=L\setminus S\), and define
\[
P^S_\kappa
=\ketbra{\kappa}{\kappa}_S\otimes I_{\overline S},
\qquad
M^S_\kappa
=\bra{\kappa}_S\otimes I_{\overline S}.
\]
The projector acts on \(\mathcal H_L\), whereas
\[
M^S_\kappa:\mathcal H_L\longrightarrow\mathcal H_{\overline S}
\]
removes the measured factors.
It satisfies
\[
(M^S_\kappa)^\dagger M^S_\kappa=P^S_\kappa.
\]

\begin{definition}[Configuration]
A configuration is \([\psi,t]\), where \(\psi\) is a unit vector
in \(\mathcal H_L\), modulo global phase, and \(\own(t)=L\).
It is well typed at \(A\) if
\[
(q{:}\Q)_{q\in L}\vdash t:A.
\]
Allocation extends the name-to-factor ordering by a fresh name;
destructive readout restricts it to surviving names.
\end{definition}

An entangled name is not assigned an individual pure state.
All live names refer to factors of the same vector.

\subsection{Values and evaluation}

Values are
\[
v::=*\mid0\mid1\mid q\mid\lambda x{:}A.\,t
\mid\langle v_1,v_2\rangle.
\]
Left-to-right call-by-value contexts are
\[
\begin{aligned}
E::={}&[\,]\mid E\,t\mid v\,E
\mid\langle E,t\rangle\mid\langle v,E\rangle\\
&\mid\lett\,\langle x,y\rangle=E\ \inn\ t
\mid\lett\,*=E\ \inn\ t\\
&\mid\ifte{E}{u}{u'}\mid V(E)\mid\Enter(E).
\end{aligned}
\]
They do not enter abstraction bodies, let-bodies, or conditional
alternatives.

Administrative root reductions are
\[
\begin{aligned}
(\lambda x{:}A.\,t)v&\longrightarrow t[v/x],\\
\lett\,\langle x,y\rangle=\langle v,w\rangle\ \inn\ t
&\longrightarrow t[v/x,w/y],\\
\lett\,*=*\ \inn\ t&\longrightarrow t,\\
\ifte{1}{u}{u'}&\longrightarrow u,\\
\ifte{0}{u}{u'}&\longrightarrow u'.
\end{aligned}
\]
They preserve the state and are closed under \(E\).
Together with allocation and gates,
\[
[\psi,E[\New]]
\redD[\psi\otimes\ket0_r,E[r]]
\quad(r\text{ fresh}),
\]
\[
[\psi,E[V(\vec q_S)]]
\redD[V_S\psi,E[\vec q_S]],
\]
they form the deterministic transitions.

The specified Born measurement transition is
\begin{equation}
\boxed{
[\psi,E[\Enter(\vec q_S)]]
\redB
\left[
\frac{M^S_\kappa\psi}{\sqrt{b_\kappa}},
E[\vec\kappa]
\right]
\quad\text{with probability}\quad
b_\kappa=\norm{M^S_\kappa\psi}^2>0.
}
\label{eq:born-rule}
\end{equation}
There is no transition on a zero-weight branch.
Measured names are removed.
For \(S=\varnothing\), the outcome is \(*\) and the state is unchanged.
A zero-qubit gate changes only an irrelevant phase.

The calculus with these transitions is \(\ECB\).
Equation~\eqref{eq:born-rule} is a definition in Layer I.

\subsection{Safety}

\begin{lemma}[Substitution and canonical forms]
\label{lem:substitution}
If
\[
\Gamma,x{:}A\vdash t:B,\qquad \Delta\vdash v:A
\]
with disjoint contexts, then
\[
\Gamma,\Delta\vdash t[v/x]:B.
\]
In a context consisting only of runtime names, values of types
\(\Q,\Bit,\Unit\), tensor, and function are respectively names,
bits, \(*\), pairs, and abstractions.
\end{lemma}

\begin{proof}
Induct on the typing derivation for substitution.
A multiplicative rule places \(x\) in one premise.
In a conditional, \(x\) occurs either in the guard context or in
the shared alternative context.
In the latter case substitute in both alternatives and reuse the
same inserted context \(\Delta\) in the additive rule.
Canonical forms follow from the value grammar and possible final
typing rules.
\end{proof}

\begin{theorem}[Preservation and progress]
\label{thm:safety}
Every deterministic or positive-probability Born transition preserves
the type of a well-typed configuration.
Every nonvalue well-typed configuration has an enabled transition.
\end{theorem}

\begin{proof}
Administrative preservation follows from substitution.
Conditional selection retains the shared alternative resources by
Lemma~\ref{lem:branchwise}.
Allocation adds one name and one factor.
A gate changes neither ownership nor type.
Readout removes precisely its argument names and returns a bit
tuple of the required type.

For progress, follow the call-by-value typing decomposition until
a root operation is reached.
Canonical forms supply the required value shape.
Gate and readout arguments are tuples of distinct runtime names,
or \(*\) at arity zero.
Finally,
\[
\sum_\kappa\norm{M^S_\kappa\psi}^2=1
\]
provides at least one positive measurement branch.
\end{proof}

\subsection{A syntactic linear step bound}

Define
\[
m(x)=m(q)=m(*)=m(0)=m(1)=0,\qquad
m(\lambda x.\,t)=m(t),
\]
\[
m(\langle t,u\rangle)=m(t)+m(u),\qquad
m(\New)=1,
\]
\[
m(V(t))=m(\Enter(t))=1+m(t),
\]
and
\[
\begin{aligned}
m(tu)&=1+m(t)+m(u),\\
m(\lett\,\langle x,y\rangle=t\ \inn\ u)&=1+m(t)+m(u),\\
m(\lett\,*=t\ \inn\ u)&=1+m(t)+m(u),\\
m(\ifte{b}{u}{u'})
&=1+m(b)+\max\{m(u),m(u')\}.
\end{aligned}
\]

\begin{lemma}[Typed substitution bound]
\label{lem:measure}
Under the hypotheses of Lemma~\ref{lem:substitution},
\[
m(t[v/x])\le m(t)+m(v).
\]
Simultaneous substitutions for disjoint linear resources increase
\(m\) by at most the sum of the inserted measures.
\end{lemma}

\begin{proof}
Induct on typing, simultaneously proving the multiple-substitution
statement.
Multiplicative premises receive disjoint substitutions.
If substitutions of total measure \(a\) enter the shared alternative
context, then
\[
\max\{m(u[\cdot]),m(u'[\cdot])\}
\le \max\{m(u),m(u')\}+a.
\]
Substitutions in the guard are disjoint from these.
This proves the conditional case; the other cases are additive.
\end{proof}

\begin{theorem}[Strong normalization and step bound]
\label{thm:termination}
Every reduction sequence from a well-typed configuration
\([\psi,t]\) has length at most \(m(t)\).
\end{theorem}

\begin{proof}
Every root transition decreases \(m\) by at least one.
Beta reduction and tuple elimination use
Lemma~\ref{lem:measure}; conditional selection uses the maximum.
Other transitions remove one counted operation.
Along an evaluation-context hole the measure is additive, since
the hole is never inside a body or unselected alternative.
The same decrease therefore holds contextually.
\end{proof}

The bound counts primitive syntax operations.
A unitary is one node regardless of its matrix dimension or
synthesis cost.
Since \(m(t)\) is bounded by the number of written operation nodes,
this is a syntactically linear bound, not a physical complexity
claim.

\begin{definition}[Terminal observation]
\label{def:observation}
For an output of type
\(\Bit^{\otimes m}\otimes\Q^{\otimes k}\),
\(\Obs[\psi,t]\) is the terminal law of the classical tuple.
The quantum tuple remains returned and owned; this observation does
not test its state.
Purely classical output is included using the unit isomorphism.
\end{definition}

Termination, finite branching, and normalized transitions make these
laws well defined.

%=====================================================================
\section{Metatheory of the specified calculus}
\label{sec:metatheory}
%=====================================================================

\subsection{Liberal scheduling and observational confluence}

Liberal contexts permit independent argument evaluation:
\[
\begin{aligned}
L::={}&[\,]\mid L\,t\mid t\,L
\mid\langle L,t\rangle\mid\langle t,L\rangle\\
&\mid\lett\,\langle x,y\rangle=L\ \inn\ u
\mid\lett\,*=L\ \inn\ u\\
&\mid\ifte{L}{u}{u'}\mid V(L)\mid\Enter(L).
\end{aligned}
\]
They still do not enter bodies or alternatives.
A scheduler chooses an enabled redex at every nonterminal
configuration.
Configurations are identified up to consistent live-name
renaming, tensor permutation, and global phase.

\begin{lemma}[Concrete diamond]
\label{lem:diamond}
Distinct enabled liberal redexes occupy nonnested positions and own
disjoint runtime-name sets.
Firing either and then the residual of the other gives equal joint
weights and equivalent resulting configurations.
\end{lemma}

\begin{proof}
An enabled root redex has no enabled accessible redex inside it:
its required arguments are values, and bodies and alternatives are
inaccessible.
Distinct redexes are therefore nonnested.
Their positions are separated by context-splitting rules.
Shared additive contexts occur only in inaccessible alternatives.

Disjoint administrative transitions commute.
Allocations commute up to fresh-name renaming and commute with
operations on existing factors.
Disjoint gates commute.
A gate commutes with destructive readout on disjoint factors, with
the canonical identification of the surviving output space.

For disjoint readouts,
\[
M^T_\lambda M^S_\kappa
=M^{S\cup T}_{\kappa\lambda}
=M^S_\kappa M^T_\lambda.
\]
Both orders have joint weight
\[
\norm{M^{S\cup T}_{\kappa\lambda}\psi}^2
\]
and, on a positive joint branch, the same normalized residual.
Zero joint weights contribute zero in both orders.
\end{proof}

\begin{theorem}[Observational confluence]
\label{thm:confluence}
All liberal schedulers yield the same terminal observation law for
a well-typed \(\ECB\) configuration.
\end{theorem}

\begin{proof}
The termination measure also decreases in liberal contexts.
Induct on \(m(t)\).
If two first choices differ, refine each successor by firing the
residual of the other redex.
Lemma~\ref{lem:diamond} matches the resulting configurations with
equal weights.
The induction hypothesis identifies their terminal laws.
If the first choices agree, apply induction to their successors.
\end{proof}

\begin{lemma}[Concrete composability]
\label{lem:concrete-C}
Joint readout of disjoint \(S,T\) and successive readout in either
order have the same ordered joint law, with all other names returned.
\end{lemma}

\begin{proof}
Every joint weight equals
\(\norm{M^{S\cup T}_{\kappa\lambda}\psi}^2\).
\end{proof}

Confluence compares evaluations of one program.
Composability compares distinct programs.

\subsection{Path maps and circuit adequacy}

A \emph{first-order interface} has only finite classical and quantum
data at input and output.
Internal higher-order terms are allowed.
For a fixed classical input, the quantum input and output spaces are
fixed by the interface.

\begin{lemma}[Finite path semantics]
\label{lem:path}
For a fixed well-typed program with a first-order interface, every
complete classical history \(h\) determines a linear map \(K_h\)
from its quantum input space to its returned quantum output space.
It is a composition of allocation isometries, gates, wiring
permutations, and destructive readout maps.
For a pure input \(\psi\),
\[
\Pr(h)=\norm{K_h\psi}^2,\qquad
\psi_h=\frac{K_h\psi}{\norm{K_h\psi}}
\quad\text{when }\Pr(h)>0,
\]
and
\[
\sum_hK_h^\dagger K_h=I.
\]
\end{lemma}

\begin{proof}
A complete history fixes all classical choices.
Administrative reductions determine syntax and wiring but do not
inspect the quantum vector.
Multiplying the quantum maps along the history gives \(K_h\).
The successive conditional normalizations cancel in the product of
branch probabilities, leaving \(\norm{K_h\psi}^2\).

For completeness use the finite formal outcome tree, including
branches whose weight is zero on a particular input.
At a readout,
\[
\sum_\kappa(M^S_\kappa)^\dagger M^S_\kappa=I.
\]
Allocation is isometric and gates are unitary.
Backward induction on the tree proves completeness.
All paths have the same output Hilbert space after the canonical
identification by the returned tuple.
\end{proof}

\begin{theorem}[Finite-circuit adequacy]
\label{thm:adequacy}
Every well-typed program with a first-order interface denotes a
finite quantum instrument.
Conversely, every finite circuit built from the available gates,
zero-state allocation, destructive computational-basis readout,
and finite classical control has a well-typed implementation with
the same instrument.
\end{theorem}

\begin{proof}
For reported output \(y\), define
\[
\Phi_y(\rho)
=\sum_{h:\,\operatorname{out}(h)=y}K_h\rho K_h^\dagger.
\]
The maps are completely positive and their sum is trace preserving
by Lemma~\ref{lem:path}.
Unrolling the finite formal evaluation tree gives a finite adaptive
circuit.

Conversely, input wires are linear arguments.
Fresh wires use \(\New\), routing uses pairing and tuple elimination,
and operations use gates or \(\Enter\).
Finite control uses conditionals, \(\copyBit\), and \(\dropBit\).
Every quantum wire is passed to exactly one next operation,
explicitly consumed, or returned.
Induction through the circuit identifies its path maps.
\end{proof}

The CP-map language here is the standard finite-dimensional
instrument language; its operator-sum and dilation background is
provided by Choi and Stinespring~\cite{Choi,Stinespring}.
The adequacy proof itself is included above.

\begin{theorem}[Semantic no-cloning]
\label{thm:nocloning}
No closed term \(c:\Q\lto\Q\otimes\Q\) returns two copies of every
pure qubit input.
\end{theorem}

\begin{proof}
By Lemma~\ref{lem:path}, its averaged output map \(\Phi\) is linear on
density operators.
A universal cloner would satisfy
\[
\Phi(\ketbra{\varphi}{\varphi})
=\ketbra{\varphi}{\varphi}^{\otimes2}.
\]
But
\[
I/2
=\tfrac12(\ketbra0{0}+\ketbra1{1})
=\tfrac12(\ketbra+{+}+\ketbra-{-}).
\]
Linearity gives two expressions for \(\Phi(I/2)\).
Their diagonal entries at \(\ket{01}\) are respectively \(0\) and
\(1/4\), a contradiction.
\end{proof}

This is a calculus-level application of semantic no-cloning,
rather than an inference from the absence of contraction;
compare Wootters and Zurek~\cite{WoottersZurek}.

\subsection{Internal no-signaling}

A bipartite experiment has a state on \(A\sqcup B\) and two local
programs owning disjoint initial name sets.
They may allocate locally but exchange neither names nor messages.
An admissible interleaving retains each local program's
left-to-right order.

\begin{theorem}[Internal no-signaling of \(\ECB\)]
\label{thm:internal-ns}
Alice's terminal classical law is independent of Bob's local program
and of the admissible interleaving.
\end{theorem}

\begin{proof}
Let \(K_a\) and \(L_b\) be their local path maps, including allocations
and returned outputs.
Disjoint maps commute with the canonical output identifications.
The joint history weight is
\(\norm{(K_a\otimes L_b)\psi}^2\).
Consequently
\[
\begin{aligned}
\Pr(a)
&=\sum_b
\bra\psi K_a^\dagger K_a\otimes L_b^\dagger L_b\ket\psi\\
&=\bra\psi K_a^\dagger K_a\otimes I\ket\psi\\
&=\tr(K_a^\dagger K_a\,\rho_A),
\end{aligned}
\]
where the second line uses local completeness.
Summing histories with the same reported output proves the claim.
The calculation is independent of the interleaving.
\end{proof}

This concerns unconditioned local records.
Conditional dependence on a reported remote outcome is not excluded.

%=====================================================================
\section{Typed records and experiment interfaces}
\label{sec:records}
%=====================================================================

\subsection{The record transformation}

For \(k\) source and \(k\) target qubits, let \(C_k\) be the grouped
CNOT unitary
\[
C_k(\ket z_S\ket w_R)=\ket z_S\ket{w\oplus z}_R.
\]
It is a tensor product of CNOTs together with the required linear
regrouping maps.
At \(k=0\), it is the identity.

\begin{definition}[Record-independent measurement form]
\label{def:record}
Let \(L=S\sqcup B\), \(|S|=k\), and suppose
\[
(q{:}\Q)_{q\in B}\vdash u:\Bit^{\otimes m}.
\]
The source term is
\begin{equation}
t_{S,u}
=\lett\,x=\Enter(\vec q_S)\ \inn\ \langle u,x\rangle,
\qquad x\notin u.
\label{eq:record-source}
\end{equation}
Its deferred term is
\begin{equation}
\begin{aligned}
\Defer_S(t_{S,u})={}&
\lett\,\vec r=\New^k\ \inn\\
&\lett\,\langle\vec s,\vec r'\rangle
=C_k(\langle\vec q_S,\vec r\rangle)\ \inn\\
&\left\langle
  \left\langle u,\Enter(\vec r')\right\rangle,\vec s
 \right\rangle.
\end{aligned}
\label{eq:record-target}
\end{equation}
Here \(\New^k\) denotes a tuple of \(k\) fresh allocations.
The continuation consumes the entire register \(B\).
It may contain allocations, gates, readouts, and classical control,
but uses neither source nor record names.
\end{definition}

After the stipulated tuple isomorphisms, the source has classical
arity \(m+k\), while the target has type
\[
\Bit^{\otimes(m+k)}\otimes\Q^{\otimes k}.
\]
Both report the same ordered classical pair \((c,x)\).
The target also returns the original source register.
Left-to-right evaluation completes \(u\) before reading the record.

Every retained source name occurs once in the returned tuple.
Thus neither term duplicates a quantum name or silently drops a
spectator.
In particular, \(u=*\) is legal only when \(B=\varnothing\).

\begin{proposition}[Concrete record equation]
\label{prop:concrete-record}
In \(\ECB\),
\[
\Obs_{\BornStrategy}[\psi,t_{S,u}]
=
\Obs_{\BornStrategy}[\psi,\Defer_S(t_{S,u})].
\]
\end{proposition}

\begin{proof}
Write
\[
\psi=\sum_\kappa\ket\kappa_S\ket{\xi_\kappa}_B.
\]
For a path \(h\) of \(u\), let \(K_h\) be its path map.
The source's joint weight for \(h,\kappa\) is
\(\norm{K_h\xi_\kappa}^2\).

Allocation and copying in the target produce
\[
\sum_\kappa
\ket\kappa_S\ket{\xi_\kappa}_B\ket\kappa_R.
\]
After path \(h\), the unnormalized vector is
\[
\sum_\kappa
\ket\kappa_S(K_h\xi_\kappa)\ket\kappa_R.
\]
Record readout has the same joint weight
\(\norm{K_h\xi_\kappa}^2\).
Sum histories with the same reported continuation output.
\end{proof}

The proposition uses the specified Born semantics.
The same equation becomes a requirement on unknown strategies
below; its two typed terms remain unchanged.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}
\node[proofbox,text width=4.7cm] (src) at (0,0)
  {Destructive source\\
   read \(S\), then execute \(u\) on \(B\)};
\node[proofbox,text width=4.7cm] (def) at (6.3,0)
  {Deferred target\\
   copy \(S\) to fresh \(R\), execute \(u\), read \(R\)};
\node[proofbox,text width=6.3cm] (obs) at (3.15,-2.1)
  {Compared boundary: the classical pair \((c,\kappa)\)\\
   The target's retained source \(S\) is returned, not identified
   with the source's residual interface.};
\draw[proofarrow] (src.south)--(obs.north west);
\draw[proofarrow] (def.south)--(obs.north east);
\end{tikzpicture}
\caption{The record equation is equality of declared classical
observations. It is not equality of complete output instruments
with different residual interfaces.}
\label{fig:record-interface}
\end{figure}

\subsection{Spectators and local experiments}

For disjoint \(S,T\subseteq L\), put
\(Z=L\setminus(S\cup T)\).
The sequential experiment is
\[
\lett\,x=\Enter(\vec q_S)\ \inn\
\lett\,y=\Enter(\vec q_T)\ \inn\
\langle\langle x,y\rangle,\vec q_Z\rangle.
\]
The reverse experiment reads \(T\) first but reports the same ordered
classical pair.
Joint readout of \(S\cup T\) likewise returns \(Z\).
These terms have the same observation interface after linear tuple
rearrangement.

A local identity experiment may return its names with a constant
classical unit.
A remote allocation experiment returns the additional allocated
name.
Thus ancilla comparisons below do not use quantum weakening.

There are two record scopes:
\begin{enumerate}[label=(\roman*)]
\item \emph{readout instances}: \(S=L\) and \(u=*\);
\item \emph{continuation instances}: \(u\) consumes all of \(L\setminus S\).
\end{enumerate}
The outcome proof uses only readout instances.
The update proof uses
\[
u=\Enter(V(\vec q_{L\setminus S})).
\]
No equation for arbitrary surrounding contexts is assumed.

%=====================================================================
\section{Unknown strategies and their requirements}
\label{sec:abstract}
%=====================================================================

\begin{assumption}[Structural class]
\label{ass:strategy-class}
Only the measurement transition varies.
The admissible class has the following properties.
\begin{enumerate}[label=\textnormal{(S\arabic*)},leftmargin=3em]
\item \textbf{Qubit kinematics.}
For every finite live-name set \(L\), states are unit rays in
\(\mathcal H_L\), with ordinary tensor composition.

\item \textbf{Fixed coherent dynamics.}
All finite-register unitaries and fresh \(\ket0\) allocation act as
in Layer I, with their stated linear-algebraic composition and
tensor placement.

\item \textbf{State sufficiency.}
The outcome law \(\Prob^S_\psi\) and positive-branch residual ray
\(\Update^S_\psi(\kappa)\) depend only on the current global ray and
measured register, not on history, apparatus identity, or hidden
memory.

\item \textbf{Normalized laws and pure residuals.}
\(\Prob^S_\psi\) is a probability distribution on \(\{0,1\}^S\).
Each positive-probability outcome has a unit residual ray on
\(\mathcal H_{L\setminus S}\).
Values on zero-probability outcomes are not part of the strategy.

\item \textbf{Permutation equivariance.}
Consistent relabeling of names, tensor factors, measured positions,
and outcome coordinates transports laws and residuals accordingly.

\item \textbf{Unbounded finite resources.}
The strategy is defined at every finite size.
Experiments may use any finite number of ancillas.
Witnesses need not have the size of the system whose law is being
characterized.

\item \textbf{Evaluation convention.}
Single programs use left-to-right evaluation.
Bipartite experiments interleave their local left-to-right
executions.
General liberal scheduler independence is not assumed.
\end{enumerate}
\end{assumption}

No closure under silent quantum deletion is included.
Arbitrary input rays are admissible configurations, whether or not
a restricted gate language can prepare them exactly.

\begin{definition}[Strategy]
A strategy is a pair \(\Strategy=(\Prob,\Update)\) in the structural
class, interpreting readout by
\[
[\psi,E[\Enter(\vec q_S)]]
\redS
[\Update^S_\psi(\kappa),E[\vec\kappa]]
\quad\text{with probability }\Prob^S_\psi(\kappa)>0.
\]
\end{definition}

Safety and the step bound use only types, ownership, and normalized
branching, so terminal laws also exist for unknown strategies.
The concrete diamond, path maps, and no-signaling theorem are not
transferred before characterization.

\begin{definition}[Five operational requirements]
\label{def:requirements}
The theory \(\Theory\) consists of:
\begin{description}[style=nextline,leftmargin=2.2em]
\item[\(\Cstar\): composability.]
For disjoint \(S,T\subseteq L\), successive readout in either order
and joint readout of \(S\cup T\) yield the same ordered joint law,
with all other names returned.
On a positive first branch,
\[
\Prob^{S\cup T}_\psi(\kappa,\lambda)
=
\Prob^S_\psi(\kappa)
\Prob^T_{\Update^S_\psi(\kappa)}(\lambda).
\]
A zero first weight gives zero joint weight.
In particular,
\[
\Prob^S_\psi=\marg_S\Prob^{S\cup T}_\psi.
\]
Only the classical joint laws, not complete residual instruments,
are equated.

\item[\(\NSstar\): no-signaling.]
For every bipartition, the terminal classical law of either local
program is independent of the other program and of the admissible
interleaving.
Local programs may allocate, apply gates, read out, use classical
control, and return quantum spectators.
They exchange neither names nor messages.

\item[\(\Nstar\): nullity.]
For every \(\psi,S,\kappa\),
\[
M^S_\kappa\psi=0
\quad\Longrightarrow\quad
\Prob^S_\psi(\kappa)=0.
\]
The experiment reads \(S\) and returns its complement.
This is a zero-support condition, not a vacuum condition or a Born
probability formula.

\item[\(\Kstar\): continuity.]
At every fixed finite live register and measured subset,
\[
[\psi]\longmapsto\Prob^S_\psi
\]
is continuous from ray space to the finite probability simplex,
equivalently in total variation.
No continuity of \(\Update\) is assumed.

\item[\(\Rstar\): records.]
For every configuration of Definition~\ref{def:record},
\[
\Obs_{\Strategy}[\psi,t_{S,u}]
=
\Obs_{\Strategy}[\psi,\Defer_S(t_{S,u})].
\]
The continuation consumes the entire complementary register and
does not use the first reported outcome.
\end{description}
\end{definition}

Each comparison has an explicit typed experiment.
The requirements do not assume probability covariance under arbitrary
computational-basis permutations; the needed symmetry is derived
below.

%=====================================================================
\section{Inhabitation and characterization architecture}
\label{sec:main}
%=====================================================================

Define the Born strategy by
\[
\Prob^S_\psi(\kappa)=\norm{M^S_\kappa\psi}^2,
\qquad
\Update^S_\psi(\kappa)
=
\left[
\frac{M^S_\kappa\psi}{\norm{M^S_\kappa\psi}}
\right]
\]
on positive branches.

\begin{theorem}[Inhabitation]
\label{thm:inhabitation}
The Born strategy belongs to the structural class and satisfies
\(\Cstar,\NSstar,\Nstar,\Kstar,\Rstar\).
\end{theorem}

\begin{proof}
The formulas give normalized laws and pure residual rays,
are state sufficient and phase invariant, and are equivariant under
consistent name and tensor permutation.
They are defined at every finite size with the fixed coherent
dynamics and evaluation convention.

Composability is Lemma~\ref{lem:concrete-C}.
No-signaling is Theorem~\ref{thm:internal-ns}.
A zero destructive component has zero squared norm, proving nullity.
Each squared norm is continuous, and there are finitely many
outcomes, proving continuity.
Proposition~\ref{prop:concrete-record} proves records.
\end{proof}

\begin{theorem}[Characterization]
\label{thm:main}
A strategy in Assumption~\ref{ass:strategy-class} satisfies
Definition~\ref{def:requirements} if and only if it is the Born
strategy.
For every finite configuration, measured subset \(S\), and outcome
\(\kappa\),
\[
\Prob^S_\psi(\kappa)=\norm{M^S_\kappa\psi}^2.
\]
Whenever this number is positive,
\[
\Update^S_\psi(\kappa)
\doteq
\frac{M^S_\kappa\psi}{\norm{M^S_\kappa\psi}},
\]
where \(\doteq\) denotes equality up to global phase.
No residual is specified on a zero-probability branch.
\end{theorem}

The uniqueness proof occupies
Sections~\ref{sec:locality}--\ref{sec:born}.
Its dependencies are:
\begin{center}
\small
\begin{tabularx}{\linewidth}{@{}p{.36\linewidth}X@{}}
\toprule
Step & Dependencies\\
\midrule
Remote invariance and locality &
\(\NSstar\), state sufficiency, fixed coherent dynamics,
and purification linear algebra.\\
Uniform correlations &
Remote invariance, \(\Cstar,\Nstar\).\\
Symmetry anchoring &
Locality, \(\Cstar,\Nstar,\Kstar\), and (S5).\\
Fine-graining anchoring &
Locality, uniform correlations, \(\Cstar,\Nstar,\Kstar\).\\
Whole-register Born law &
Diagonal anchoring and readout instances of \(\Rstar\).\\
Partial-register Born law &
Whole-register law and \(\Cstar\).\\
Projective residual &
Born law, \(\Cstar\), continuation instances of \(\Rstar\),
fixed gates, and state sufficiency.\\
\bottomrule
\end{tabularx}
\end{center}

The anchoring proofs are alternatives.
Nullity is not needed for locality.
Continuity is used in anchoring, not as an update-continuity premise.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[
  node distance=8mm and 8mm,
  proofbox/.append style={text width=2.9cm}
]
\node[proofbox] (remote) {Remote invariance\\\(\NSstar\)};
\node[proofbox,right=of remote] (locality)
  {Purification locality\\Reduced-state law};
\node[proofbox,right=of locality] (uniform)
  {Uniform correlations\\\(\Cstar,\Nstar\)};
\draw[proofarrow] (remote)--(locality);
\draw[proofarrow] (locality)--(uniform);

\node[proofbox,below=12mm of remote] (sym)
  {Symmetry anchoring\\\(\Cstar,\Nstar,\Kstar\), (S5)};
\node[proofbox,below=12mm of locality] (anchor)
  {Diagonal anchoring\\Either proof};
\node[proofbox,below=12mm of uniform] (fine)
  {Fine-graining anchoring\\\(\Cstar,\Nstar,\Kstar\)};
\draw[proofarrow] (locality.south west)--(sym.north east);
\draw[proofarrow] (uniform)--(fine);
\draw[proofarrow] (sym)--(anchor);
\draw[proofarrow] (fine)--(anchor);

\node[proofbox,below=12mm of sym] (whole)
  {Whole-register Born law\\Readout \(\Rstar\)};
\node[proofbox,below=12mm of anchor] (partial)
  {Partial-register law\\\(\Cstar\)};
\node[proofbox,below=12mm of fine] (update)
  {Projective update\\Continuation \(\Rstar\)};
\draw[proofarrow] (anchor.south west)--(whole.north east);
\draw[proofarrow] (whole)--(partial);
\draw[proofarrow] (partial)--(update);
\end{tikzpicture}
\caption{Uniqueness dependencies. The structural class applies
throughout. Later instrument, decoder, cutoff, and field interfaces
do not enter this graph. Inhabitation is proved separately.}
\label{fig:dependencies}
\end{figure}

%=====================================================================
\section{Locality and uniform correlations}
\label{sec:locality}
%=====================================================================

Throughout this and the next two sections, \(\Strategy\) is unknown.

\begin{lemma}[Remote invariance]
\label{lem:remote}
Under \(\NSstar\), appending fresh zero-state factors outside \(S\)
does not change \(\Prob^S_\psi\).
Applying a unitary outside \(S\) does not change it either.
\end{lemma}

\begin{proof}
Compare a remote allocation-and-return program with a remote identity
program, and schedule allocation before local readout.
No-signaling equates the local laws.
State sufficiency identifies the post-allocation law with the law
at the enlarged global state.

For a remote gate, compare its gate-and-return program with the
identity program and schedule the gate first.
\end{proof}

\begin{lemma}[Purification locality]
\label{lem:locality}
Under \(\NSstar\), global pure states with the same reduced density
operator on \(S\) have the same \(S\)-outcome law.
\end{lemma}

\begin{proof}
Pad the smaller environment by zero-state qubits until environment
dimensions agree.
Remote invariance leaves the law unchanged; consistent relabeling
identifies the environment name sets.
If
\[
\rho_S=\sum_jr_j\ketbra{e_j}{e_j}
\]
on its support, the purifications have the forms
\[
\sum_j\sqrt{r_j}\ket{e_j}\ket{f_j},
\qquad
\sum_j\sqrt{r_j}\ket{e_j}\ket{g_j},
\]
with orthonormal environment families.
The isometry \(f_j\mapsto g_j\) extends to an environment unitary.
Apply remote invariance again.
\end{proof}

Hence there is a well-defined function
\[
F_S(\rho_S)=\Prob^S_\psi,
\qquad
\rho_S=\tr_{L\setminus S}\ketbra{\psi}{\psi}.
\]
This partial trace is an algebraic construction from the stipulated
vector, not a measurement-probability postulate.

\begin{lemma}[Reduced-state continuity]
\label{lem:reduced-continuity}
Under \(\NSstar,\Kstar\), \(F_S\) is continuous on the density
operators on \(\mathcal H_S\).
\end{lemma}

\begin{proof}
Use the fixed-dimensional purification
\[
\ket{\psi_\rho}
=(\sqrt\rho\otimes I)\sum_j\ket j\ket j.
\]
Its norm is one and its reduction is \(\rho\).
Matrix square root is continuous in finite dimension, so this is a
continuous choice of vector purification.
Apply \(\Kstar\) and purification locality.
\end{proof}

\begin{theorem}[Uniform correlations]
\label{thm:uniformity}
Assume \(\Cstar,\NSstar,\Nstar\).
If
\[
\psi=\frac1{\sqrt d}
\sum_{k\in K}e^{i\theta_k}\ket k_S\ket{\eta_k}_B,
\qquad d=|K|,
\]
where the computational strings \(k\) are distinct and the
computational strings \(\eta_k\) are distinct, then
\(\Prob^S_\psi\) is uniform on \(K\).
\end{theorem}

\begin{proof}
A diagonal environment unitary removes the phases without changing
the \(S\)-law.
Write
\[
p=\Prob^S_\psi,\qquad q=\Prob^B_\psi,\qquad
\nu=\Prob^{S\cup B}_\psi.
\]
Nullity restricts \(\nu\) to \((k,\eta_k)\).
Composability gives
\[
p(k)=\nu(k,\eta_k)=q(\eta_k),
\qquad
\sum_{k\in K}p(k)=1.
\]

For a permutation \(\pi\) of \(K\), extend it to a
computational-basis permutation unitary \(\Pi_\pi\) on \(S\).
Then
\[
\Pi_\pi\psi
=\frac1{\sqrt d}
\sum_{m\in K}\ket m\ket{\eta_{\pi^{-1}(m)}}.
\]
The same vector is \(W\psi\), where \(W\) is an environment unitary
sending \(\eta_k\) to \(\eta_{\pi^{-1}(k)}\).
Its \(S\)-law remains \(p\), by invariance under \(W\).
Its \(B\)-law remains \(q\), by invariance under \(\Pi_\pi\).

For the new pairing, nullity and composability imply
\[
p(m)=q(\eta_{\pi^{-1}(m)})=p(\pi^{-1}(m)).
\]
Every permutation preserves \(p\), so \(p(k)=1/d\).
\end{proof}

Probability covariance under arbitrary basis permutations was not
assumed.
The required equality was derived by comparing two coherent
implementations of the same transformed vector.

%=====================================================================
\section{Diagonal anchoring: independent finite proofs}
\label{sec:anchoring}
%=====================================================================

Diagonal anchoring is the conclusion
\[
\rho_S\ \text{diagonal}
\quad\Longrightarrow\quad
F_S(\rho_S)(\kappa)=\bra\kappa\rho_S\ket\kappa.
\]
It is not a separate requirement.

\subsection{A three-qubit illustration}

\begin{proposition}[Three-qubit symmetric witness]
\label{prop:three}
Assume \(\Cstar,\Nstar\) and (S5).
For
\[
\Omega=\frac{\ket{011}+\ket{101}+\ket{110}}{\sqrt3},
\]
the first-qubit law is \((1/3,2/3)\), and the first-qubit reduction
is \(\diag(1/3,2/3)\).
\end{proposition}

\begin{proof}
Nullity restricts the full law to the displayed strings.
Tensor-factor permutations preserve \(\Omega\) and act transitively
on its support.
Equivariance forces equal weights, hence \(1/3\) each.
Composability gives the first-coordinate marginal.
The accompanying last-two-qubit strings are distinct, so the
first-qubit reduction has no off-diagonal entry and has the stated
diagonal.
\end{proof}

This example illustrates the mechanism; it does not by itself
establish arbitrary diagonal anchoring.

\subsection{Proof A: multiset symmetry}

\begin{theorem}[Symmetry anchoring]
\label{thm:symmetry-anchor}
Assume \(\Cstar,\NSstar,\Nstar,\Kstar\) and (S5).
Then diagonal anchoring holds.
\end{theorem}

\begin{proof}
Let \(S\) have \(n\) qubits.
First take a rational diagonal state
\[
\rho_S=\sum_{k\in K}\frac{m_k}{M}\ketbra{k}{k},
\qquad m_k\ge1,\qquad \sum_km_k=M.
\]
Zero-weight labels are omitted.

Take \(M\) blocks of \(n\) qubits.
Let \(\mathcal A\) consist of sequences
\((k_1,\ldots,k_M)\) containing exactly \(m_k\) copies of each \(k\),
and put
\[
\Omega_{\mathbf m}
=\frac1{\sqrt{|\mathcal A|}}
\sum_{a\in\mathcal A}\ket{k_1}\cdots\ket{k_M}.
\]
Block permutations are tensor-factor permutations.
They preserve this vector and act transitively on \(\mathcal A\).
Nullity and equivariance force a uniform full law.

Composability gives the first-block marginal
\[
\Pr(k_1=k)
=\frac{|\{a\in\mathcal A:a_1=k\}|}{|\mathcal A|}
=\frac{m_k}{M},
\]
since
\[
|\mathcal A|=\frac{M!}{\prod_\ell m_\ell!},
\qquad
|\{a:a_1=k\}|
=\frac{(M-1)!}{(m_k-1)!\prod_{\ell\ne k}m_\ell!}.
\]

The first-block reduction is exactly \(\rho_S\).
Completions with different first labels have different remaining
multisets, hence disjoint computational supports; all off-diagonal
first-block entries vanish.
The diagonal entries are the same counting ratios.

Locality transfers the law to every purification of \(\rho_S\).
Rational diagonal states are dense, so reduced-state continuity
proves the result for all diagonal states.
The empty register has a unique outcome.
\end{proof}

This witness uses \(nM\) qubits.
Its resource size is finite but not uniformly bounded in the rational
denominator.

\subsection{Why naive fine-graining does not suffice}

For disjoint label sets \(R_k\), \(|R_k|=m_k\), the vector
\[
\Phi_0=\frac1{\sqrt M}
\sum_k\sum_{r\in R_k}\ket k_S\ket r_{E'}
\]
has the desired reduction on \(S\).
However,
\[
\rho_{E'}
=\frac1M\sum_k\sum_{r,r'\in R_k}\ketbra r{r'}.
\]
Coherences remain within each block.
Distinct refined labels \(r\) have repeated companions \(k(r)\);
Theorem~\ref{thm:uniformity} therefore does not apply to the
\(E'\)-readout.

A further computational label distinguishes those companions.
This chooses another purification of the same \(\rho_S\);
it does not claim that a remote unitary decoheres a fixed reduced
state.

\subsection{Proof B: decohered fine-graining}

\begin{theorem}[Fine-graining anchoring]
\label{thm:fine-anchor}
Assume \(\Cstar,\NSstar,\Nstar,\Kstar\).
Then diagonal anchoring holds.
\end{theorem}

\begin{proof}
Use the rational weights above and set
\[
a=\lceil\log_2M\rceil,\qquad
b=\left\lceil\log_2\max_km_k\right\rceil.
\]
Choose disjoint
\(R_k\subseteq\{0,1\}^a\), \(|R_k|=m_k\), and injections
\[
e_k:R_k\longrightarrow\{0,1\}^b.
\]
Define
\[
\Phi=\frac1{\sqrt M}
\sum_k\sum_{r\in R_k}
\ket k_S\ket r_{E'}\ket{e_k(r)}_{E''}.
\]
Its reduction on \(S\) is \(\rho_S\).

With \(E'\) written first, each \(r\) has companion
\((k(r),e_{k(r)}(r))\).
These companions are distinct: different blocks have different
\(k\), and each \(e_k\) is injective.
Uniform correlations therefore give
\[
\Prob^{E'}_\Phi(r)=1/M
\]
on the used labels.

Let \(\nu=\Prob^{S\cup E'}_\Phi\).
Nullity restricts its support to \((k(r),r)\).
Composability makes its \(E'\)-marginal uniform.
Each \(r\) has only one allowed companion, so
\[
\nu(k(r),r)=1/M.
\]
The \(S\)-marginal is \(m_k/M\).
Locality transfers this law to every purification of \(\rho_S\),
and continuity supplies arbitrary diagonal weights.
\end{proof}

The witness uses
\[
n+\lceil\log_2M\rceil+
\left\lceil\log_2\max_km_k\right\rceil
\]
qubits.
For weights \((1/3,2/3)\), one choice is
\[
\frac1{\sqrt3}
\left(
\ket0\ket{00}\ket0+
\ket1\ket{01}\ket0+
\ket1\ket{10}\ket1
\right).
\]
The three-qubit symmetry witness is smaller for that particular law.

The numerical fine-graining argument does not use (S5) as a
probability-symmetry premise.
The structural class still contains (S5); no independence theorem
for the complete assumption package is claimed.

%=====================================================================
\section{Born laws and destructive projective residuals}
\label{sec:born}
%=====================================================================

\subsection{Whole-register records precede marginalization}

\begin{theorem}[Born probabilities]
\label{thm:born}
Assume diagonal anchoring, \(\Cstar\), and the readout instances
of \(\Rstar\).
Then, for every finite configuration and \(S\subseteq L\),
\[
\Prob^S_\psi(\kappa)=\norm{M^S_\kappa\psi}^2.
\]
\end{theorem}

\begin{proof}
First let \(S=L\).
The source
\[
t_{L,*}
=\lett\,x=\Enter(\vec q_L)\ \inn\ \langle *,x\rangle
\]
is well typed because no complementary quantum names remain.

Write \(\psi=\sum_ja_j\ket j_L\).
Before record readout, the deferred program has vector
\[
\Psi'=\sum_ja_j\ket j_L\ket j_R.
\]
Its record reduction is
\[
\rho_R=\sum_j|a_j|^2\ketbra j{j}.
\]
Diagonal anchoring gives record law \(|a_j|^2\).
The readout record equation identifies this with
\(\Prob^L_\psi(j)\).

For a proper subset, composability gives
\[
\begin{aligned}
\Prob^S_\psi(\kappa)
&=\sum_{\lambda\in\{0,1\}^{L\setminus S}}
\Prob^L_\psi(\kappa,\lambda)\\
&=\sum_\lambda|a_{\kappa\lambda}|^2
=\norm{M^S_\kappa\psi}^2.
\end{aligned}
\]
No partial-register record test with omitted spectators is used.
\end{proof}

\subsection{Residual identification by future tests}

\begin{theorem}[Projective update]
\label{thm:update}
Assume the Born outcome law, \(\Cstar\), and the continuation
instances of \(\Rstar\).
If
\[
\psi=\sum_\kappa\ket\kappa_S\ket{\xi_\kappa}_B,
\qquad
p_\kappa=\norm{\xi_\kappa}^2>0,
\]
then
\[
\Update^S_\psi(\kappa)
\doteq\frac{\xi_\kappa}{\norm{\xi_\kappa}}.
\]
\end{theorem}

\begin{proof}
Fix a positive branch \(\kappa\).
Choose unit representatives
\[
u_\kappa=\Update^S_\psi(\kappa),
\qquad
\varphi_\kappa=\xi_\kappa/\norm{\xi_\kappa}.
\]
If \(B=\varnothing\), its Hilbert space is one dimensional and the
claim is immediate.

For a unitary \(V\) on \(B\), use
\[
t_V=
\lett\,x=\Enter(\vec q_S)\ \inn\
\langle\Enter(V(\vec q_B)),x\rangle.
\]
By the unknown strategy's transition rule and state sufficiency,
the joint source weight for \((\lambda,\kappa)\) is
\[
p_\kappa\,\Prob^B_{Vu_\kappa}(\lambda).
\]
This does not use a Born update.

The deferred vector after copying and applying \(V\), before either
readout, is
\[
\Psi'_V
=\sum_j\ket j_S(V\xi_j)_B\ket j_R.
\]
The target reads \(B\), then \(R\), and returns \(S\).
Composability equates its joint law to joint \(B\cup R\) readout.
The established Born outcome law gives joint weight
\[
\abs{\bra\lambda V\ket{\xi_\kappa}}^2.
\]
Records therefore imply
\[
\Prob^B_{Vu_\kappa}(\lambda)
=\abs{\bra\lambda V\ket{\varphi_\kappa}}^2.
\]
Using the established outcome law on the left,
\[
\abs{\bra\lambda V\ket{u_\kappa}}^2
=
\abs{\bra\lambda V\ket{\varphi_\kappa}}^2
\]
for every \(V,\lambda\).

Choose \(V\varphi_\kappa=\ket{0^{|B|}}\).
Then
\[
\abs{\bra{0^{|B|}}V\ket{u_\kappa}}^2=1,
\]
so the unit rays agree.
\end{proof}

The test unitary may be selected separately for each fixed branch.
Each individual experiment still has a continuation independent of
its first outcome.
Equality of the \emph{joint} reported laws permits conditioning on
that outcome after the experiment.
No single unitary must map all conditional vectors to one vector.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}
\node[proofbox,text width=4.8cm] (source) at (0,0)
  {Source: unknown residual \(u_\kappa\)\\
   Joint weight
   \(p_\kappa\Prob^B_{Vu_\kappa}(\lambda)\)};
\node[proofbox,text width=4.8cm] (target) at (6.4,0)
  {Deferred target: fixed coherent vector\\
   Joint weight
   \(\lvert\langle\lambda|V|\xi_\kappa\rangle\rvert^2\)};
\draw[proofarrow] (source)--node[above,font=\small]
  {\(\Rstar\)} (target);
\node[proofbox,text width=7.0cm] (test) at (3.2,-2.1)
  {Fix \(\kappa\), then choose
   \(V\varphi_\kappa=\ket0\).\\
   Equality of joint laws forces
   \(\lvert\langle0|V|u_\kappa\rangle\rvert^2=1\).};
\draw[proofarrow] (source.south)--(test.north west);
\draw[proofarrow] (target.south)--(test.north east);
\end{tikzpicture}
\caption{Residual identification uses the outcome theorem already
proved, not the concrete update rule. The branch-specific choice of
test is external to the experiment's record-independent continuation.}
\label{fig:residual-test}
\end{figure}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Inhabitation is Theorem~\ref{thm:inhabitation}.
For an arbitrary model of the five requirements,
Theorem~\ref{thm:fine-anchor} gives diagonal anchoring,
Theorem~\ref{thm:born} gives Born probabilities, and
Theorem~\ref{thm:update} gives every positive-branch residual ray.
These are precisely the data of the strategy.
\end{proof}

\begin{corollary}[Scheduler independence after characterization]
\label{cor:scheduler}
Every model of \(\Theory\) has the liberal observational confluence
of \(\ECB\).
\end{corollary}

\begin{proof}
Its transitions have been identified with the Born transitions.
Apply Theorem~\ref{thm:confluence}.
\end{proof}

\subsection{Dense coherent gate languages}

\begin{corollary}[Dense-gate variant]
\label{cor:dense}
The characterization remains valid when exact CNOT is available
and finite available gate circuits are dense, up to phase, in the
unitary group on every finite register, with all other assumptions
retained.
\end{corollary}

\begin{proof}
Remote invariance first holds for available circuits.
At fixed dimension, approximate an arbitrary remote unitary and use
\(\Kstar\) to extend the invariance to its limit.
This supplies the transformations required for locality and uniform
correlations.
Witness rays are admissible inputs regardless of exact preparability.

Record terms use exact CNOT.
In the update proof, take available \(V_j\) converging to a unitary
mapping \(\varphi_\kappa\) to \(\ket0\).
The equal squared-amplitude identities pass to the limit.
No continuity of the unknown update map is needed.
\end{proof}

%=====================================================================
\section{Stability and represented measurements}
\label{sec:consequences}
%=====================================================================

\subsection{Resource-budgeted record stability}

For finite laws and unit rays, define
\[
\TV(P,Q)=\frac12\sum_x|P(x)-Q(x)|,
\qquad
D(u,v)=\sqrt{1-|\braket u v|^2}.
\]
The latter is the trace distance between the corresponding pure-state
density operators.

The next theorem concerns the record stage only.
It does not derive approximate anchoring from approximate versions
of the first four requirements.

\begin{theorem}[Budgeted stability of records]
\label{thm:stability}
Fix a total live-qubit budget \(N\) and \(\varepsilon\ge0\).
Suppose a strategy in the structural class satisfies exact
\(\Cstar\) and:
\begin{enumerate}[label=(\roman*)]
\item For every configuration with at most \(N\) live qubits and
diagonal measured reduction,
\[
\TV(\Prob^S_\psi,\diag\rho_S)\le\varepsilon.
\]
\item Every record source and target whose executions remain within
\(N\) live qubits obey
\[
\TV\!\left(
\Obs_{\Strategy}[\psi,t_{S,u}],
\Obs_{\Strategy}[\psi,\Defer_S(t_{S,u})]
\right)\le\varepsilon.
\]
\end{enumerate}
Then:
\begin{enumerate}[label=(\alph*)]
\item If \(\psi\) has \(n\) live qubits and \(2n\le N\), then
\[
\TV(\Prob^S_\psi,\Born^S_\psi)\le2\varepsilon
\]
for every \(S\), where
\(\Born^S_\psi(\kappa)=\norm{M^S_\kappa\psi}^2\).

\item If \(|S|=k\) and \(2(n+k)\le N\), the joint law of
\[
\lett\,x=\Enter(\vec q_S)\ \inn\
\langle\Enter(V(\vec q_{L\setminus S})),x\rangle
\]
is within \(3\varepsilon\) of its Born joint law for every \(V\).

\item Under the budget in (b), if
\[
b=\norm{M^S_\kappa\psi}^2\ge\gamma>0,
\qquad
\varepsilon\le\gamma/8,
\]
the branch has positive strategy probability, and
\[
D\!\left(
\Update^S_\psi(\kappa),
\frac{M^S_\kappa\psi}{\sqrt b}
\right)
\le
\min\left\{1,\sqrt{\frac{6\varepsilon}{\gamma}}\right\}.
\]
\end{enumerate}
\end{theorem}

\begin{proof}
For (a), the whole-register record experiment adds \(n\) fresh
qubits.
Approximate records cost at most \(\varepsilon\);
approximate anchoring of the record reduction costs at most another
\(\varepsilon\).
Exact composability and contraction under marginalization give
every measured subset.

For (b), comparison with the deferred experiment costs
\(\varepsilon\).
Before deferred readout, the vector is
\[
\Psi'_V=\sum_j\ket j_S(V\xi_j)_B\ket j_R
\]
on \(n+k\) qubits.
Exact composability replaces the successive \(B,R\) readouts by a
joint readout.
Part (a), applied to this intermediate vector, costs
\(2\varepsilon\) and requires \(2(n+k)\le N\).
The Born weight is
\(\abs{\bra\lambda V\ket{\xi_\kappa}}^2\).
The triangle inequality gives \(3\varepsilon\).

For (c), write
\[
p=\Prob^S_\psi(\kappa),\quad
u=\Update^S_\psi(\kappa),\quad
\varphi=M^S_\kappa\psi/\sqrt b.
\]
Part (a) yields \(|p-b|\le2\varepsilon\), hence
\(p\ge3\gamma/4>0\).
If the complement is empty, its residual ray is unique.
Otherwise choose \(V\varphi=\ket0\).
The Born joint probability of \(\kappa\) followed by
\(\lambda\ne0\) is zero, so (b) gives
\[
p\,\Prob^B_{Vu}(\lambda\ne0)\le3\varepsilon.
\]
Apply (a) to \(Vu\); its required budget is covered by the assumed
larger budget. Then
\[
\begin{aligned}
D(u,\varphi)^2
&=1-|\bra0V\ket u|^2\\
&\le\frac{3\varepsilon}{p}+2\varepsilon\\
&\le\frac{4\varepsilon}{\gamma}
   +\frac{2\varepsilon}{\gamma}
=\frac{6\varepsilon}{\gamma},
\end{aligned}
\]
using \(\gamma\le1\).
Finally \(D\le1\).
\end{proof}

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[node distance=8mm]
\node[proofbox,text width=3.0cm] (initial)
  {Original configuration\\\(n\) live qubits};
\node[proofbox,text width=3.2cm,right=of initial] (defer)
  {Update-test deferral\\\(n+k\) live qubits};
\node[proofbox,text width=3.7cm,right=of defer] (full)
  {Whole-register test of the intermediate vector\\
   \(2(n+k)\) live qubits};
\draw[proofarrow] (initial)--(defer);
\draw[proofarrow] (defer)--(full);
\end{tikzpicture}
\caption{The sufficient stability budget counts record qubits for
intermediate whole-register tests. It is not merely the peak of the
original source and its first deferral.}
\label{fig:stability-budget}
\end{figure}

A positive lower branch-weight bound is necessary for this form of
conditional estimate: a small unconditional discrepancy may be
concentrated on a rare branch.
No general repeated-deferral error theorem is inferred.

\subsection{Mixed states and finite adaptivity}

\begin{corollary}[Mixed-state extension]
\label{cor:mixed}
In a model of \(\Theory\), evaluation through a purification of a
laboratory density operator \(\rho\) gives
\[
\Pr(\kappa)=\tr(P^S_\kappa\rho),
\qquad
\rho'_\kappa
=
\frac{\tr_S(P^S_\kappa\rho P^S_\kappa)}
     {\tr(P^S_\kappa\rho)}
\]
on positive branches.
Both expressions are independent of the purification.
\end{corollary}

\begin{proof}
Apply the probability and update theorems to a purification.
Trace its inaccessible purifying factors from the conditioned
residual.
The formulas depend only on \(\rho\).
Purifying names can be returned as inert spectators in the total
pure configuration; no term-level discard is needed.
\end{proof}

\begin{corollary}[Finite adaptive execution]
\label{cor:adaptive}
Every finite program with a first-order interface in a model of
\(\Theory\) has its Born instrument.
Its terminal classical observations are independent of the liberal
scheduler.
\end{corollary}

\begin{proof}
Characterization identifies each reached readout's probabilities
and positive-branch residuals.
Induction on the finite remaining evaluation tree identifies all
path maps and reported-output instruments.
Scheduler independence follows from Corollary~\ref{cor:scheduler}.
\end{proof}

\subsection{Rotated readout and POVMs}

For \(\ket{u_\kappa}=V\ket\kappa\), define the macro
\[
\Enter_V(\vec q_S)=\Enter(V^\dagger(\vec q_S)).
\]
Its law is
\(\bra{u_\kappa}\rho_S\ket{u_\kappa}\), and its residual is
proportional to
\((\bra{u_\kappa}_S\otimes I)\psi\).

For a finite POVM \((E_x)_x\), the map
\[
V_E\varphi=\sum_x\sqrt{E_x}\varphi\otimes\ket x
\]
is an isometry because \(\sum_xE_x=I\).
After finite qubit encoding and zero-state padding, it extends to a
unitary.
Reading the outcome register and returning the quantum residual
implements
\[
\Pr(x)=\tr(\rho E_x).
\]
A finite classical decoder handles non-power-of-two label sets.
Unused padded labels have zero weight on the encoded input subspace.
This is one implementation; the POVM alone does not specify all
possible conditional maps.

\begin{corollary}[Finite instrument representation]
\label{cor:instrument}
Let
\[
\Phi_x(\rho)=\sum_jM_{xj}\rho M_{xj}^\dagger,
\qquad
\sum_{x,j}M_{xj}^\dagger M_{xj}=I
\]
be a finite-dimensional instrument with fixed input and quantum
output spaces.
After finite qubit encodings, an Enter program realizes these maps
on its declared classical and quantum outputs.
With an untouched reference \(B\), its branch map is
\(\Phi_x\otimes\id_B\).
\end{corollary}

\begin{proof}
Let \(J_{\mathrm{in}}\) and \(J_{\mathrm{out}}\) be isometric qubit
encodings of the input and output spaces.
Choose a qubit register large enough to accommodate the encoded
output, a computational register for \((x,j)\), and zero padding.
On the encoded zero-ancilla input subspace prescribe
\[
J_{\mathrm{in}}\varphi\otimes\ket0
\longmapsto
\sum_{x,j}
J_{\mathrm{out}}M_{xj}\varphi
\otimes\ket{x,j}\otimes\ket0_{\mathrm{pad}}.
\]
Completeness makes this prescription isometric.
Enlarge the zero-ancilla input register if necessary so that input
and target are subspaces of the same finite qubit space.
Complete orthonormal bases to extend the prescription to a unitary.

Implement the unitary, destructively read the index and padding
registers, decode \(x\), delete unreported classical indices by
\(\dropBit\), and return the encoded quantum output.
On the encoded input, the resolved path maps are the encoded
\(M_{xj}\), with zero padding fixed.
Summing the unreported \(j\) gives \(\Phi_x\).
Every operation acts trivially on \(B\), proving the reference claim.
\end{proof}

This theorem represents a specified instrument by a program after
the primitive is fixed.
It does not characterize an independently declared instrument
primitive or derive a physical apparatus implementing the program.

%=====================================================================
\section{After Enter: records, instruments, decoders, and cutoffs}
\label{sec:interfaces}
%=====================================================================

This section is an interface dictionary.
It adds no premise to Theorem~\ref{thm:main}.
Its finite statements are proved below; companion citations identify
related source records rather than transfer unproved apparatus or
field results into the characterization.

\subsection{D1: three distinct measurement interfaces}

After characterization, write \(L=S\sqcup B\).
A classical register is represented below by a diagonal matrix
algebra. It is not an additional live quantum carrier in the term
language merely because Hilbert-space notation is used for its
labels.

The three interfaces distinguished in
Cheung's En03-A~\cite[definitions
\SourceLabel{def:enter}, \SourceLabel{def:recording},
and \SourceLabel{def:nondestructive}]{CheungEn03A}
are:

\paragraph{Destructive Enter.}
Its complete classical/quantum channel is
\begin{equation}
\mathcal M_S(\rho)
=
\sum_z\ketbra z{z}_R\otimes M^S_z\rho(M^S_z)^\dagger.
\label{eq:destructive-interface}
\end{equation}
The output residual is \(B\); the factor \(S\) is absent.

\paragraph{Coherent recording.}
The copying isometry is
\[
A_S=\sum_z\ket z_R\otimes P^S_z,
\qquad
A_S^\dagger A_S=I,
\]
and the coherent channel is
\begin{equation}
\mathcal C_S(\rho)=A_S\rho A_S^\dagger.
\label{eq:coherent-interface}
\end{equation}
Both \(S\) and the quantum record carrier \(R\) remain.
Off-diagonal coherences in \(R\) are retained in the joint state.
This is not yet a classical readout.

\paragraph{Represented nondestructive projective instrument.}
Copying and then destructively reading the record carrier implements
\begin{equation}
\mathcal I^{\mathrm{nd}}_S(\rho)
=
\sum_z\ketbra z{z}_R\otimes P^S_z\rho P^S_z.
\label{eq:nondestructive-interface}
\end{equation}
Its classical record is \(R\), and its quantum residual interface is
\(S\otimes B\).
It is represented by allocation, CNOT, and Enter; it is not the
destructive primitive.

These formulas follow from the characterized semantics.
They do not constitute another derivation or axiom of the Born rule.

\begin{definition}[Record and continuation]
A record is a classical value already produced by Enter or obtained
by reading a coherent record carrier, together with a declared
continuation on the surviving quantum names.
Retained names remain separately owned.
Equality of classical records does not identify all coherent
implementations or their residual instruments.
\end{definition}

\subsection{D2: record pullback versus instrument compatibility}

\begin{proposition}[Exact record compatibility]
\label{prop:pullback}
Let \(T\) be a finite-dimensional CPTP map from a fine input space to
a coarse space, let \((E_w)_w\) be a coarse POVM, and let
\((\Pi_w)_w\) be a fine POVM with the same labels.
The record laws
\[
\tr(T(\rho)E_w),\qquad \tr(\rho\Pi_w)
\]
agree for every input density operator and every \(w\) if and only if
\begin{equation}
T^*(E_w)=\Pi_w\qquad\text{for every }w.
\label{eq:pullback}
\end{equation}
Here \(T^*\) is the trace-dual map.
\end{proposition}

\begin{proof}
The difference is
\[
\tr\bigl(\rho[T^*(E_w)-\Pi_w]\bigr).
\]
The bracket is Hermitian.
Vanishing expectation on all density operators, in particular its
eigenvector states, is equivalent to the bracket being zero.
The reverse implication is immediate.
\end{proof}

This is the finite pullback criterion recorded in
En03-A~\cite[theorem \SourceLabel{thm:pullback}]{CheungEn03A}.
It determines effects, not complete selective maps.

For instruments \((\Phi_w)_w\) and \((\Psi_w)_w\) with identified
residual output spaces, full implementation compatibility is instead
\[
\Psi_w\circ T=\Phi_w
\qquad\text{for every }w.
\]
Equality on all matrix units certifies this map identity and therefore
also equality with every untouched reference.
Its trace consequence is record compatibility, but the converse
fails.

\begin{example}[Equal records, different residuals]
\label{ex:equal-records}
For a qubit input and \(z\in\{0,1\}\), define
\[
\Phi_z(\rho)
=\bra z\rho\ket z\,\ketbra0{0},
\qquad
\Psi_z(\rho)
=\bra z\rho\ket z\,\ketbra1{1}.
\]
Both are complete instruments with effects \(\ketbra z{z}\).
Thus they have identical Born record laws for every input.
Their conditional quantum outputs differ on every positive branch.

Both instruments are represented by Enter followed by allocation
and, for \(\Psi\), a fixed \(X\) gate on the fresh output.
They do not define two different Enter strategies.
A later computational readout of the returned output distinguishes
them perfectly.
\end{example}

Thus record compatibility is a pullback, whereas residual
compatibility requires a separate instrument certificate.
The example supplies a self-contained instance of the
record/residual distinction associated with
En03-A~\cite[section on residual instruments,
including \SourceLabel{thm:obstruction}]{CheungEn03A}.

\begin{definition}[Compiled-instrument interface]
A compiled-instrument interface consists of:
\begin{enumerate}[label=(\roman*)]
\item a finite Enter program and declared classical and quantum outputs;
\item a dependency graph recording classical inputs to operations and
order constraints imposed by shared quantum resources;
\item complete selective maps at its boundary;
\item a certificate of the exact composition, exchange, or
implementation identities claimed.
\end{enumerate}
Correctness concerns the complete selective maps, not only outcome
effects. Existence of a physical implementation certificate is
additional data; no general external-apparatus compiler theorem is
asserted.
\end{definition}

\subsection{Complete process data: the direction of implication}

\begin{proposition}[Adaptive equality from complete process equality]
\label{prop:process}
Consider two finite adaptive models on identified accessible spaces.
Suppose their initial accessible states agree and, after every
permitted setting and history, their interval channels and complete
selective instruments agree.
Then all permitted adaptive record laws agree, including with an
untouched reference.
For an equal-prior binary randomized test, the type-I and type-II
errors satisfy
\[
\alpha+\beta=1.
\]
For arbitrary record laws \(P_0,P_1\),
\[
\alpha+\beta\ge1-\TV(P_0,P_1).
\]
\end{proposition}

\begin{proof}
Induction through the finite experiment tree gives equality of every
unnormalized accessible conditional state.
Taking its trace gives equality of history weights and hence record
laws. Tensoring the assumed map identities with the reference
identity gives the same induction with a reference.

If \(\varphi\in[0,1]\) is the probability of deciding for model \(1\),
then
\[
\alpha+\beta
=\mathbb E_0\varphi+\mathbb E_1(1-\varphi)
=1+\mathbb E_0\varphi-\mathbb E_1\varphi.
\]
The difference of expectations has magnitude at most total variation.
\end{proof}

This is the implication supplied by Psy02-B's
\SourceLabel{thm:process}~\cite{CheungPsy02B}.
It does \emph{not} state the converse.
In particular, that theorem alone is not a residual-instrument
nonidentifiability theorem.

Whether equal records identify a residual map depends on the
permitted future experiments and accessible output algebra.
If arbitrary tomographic tests of an identified accessible residual
are allowed, differences such as Example~\ref{ex:equal-records} are
detectable.
If the comparison boundary excludes those outputs or tests, record
equality need not identify them.

\subsection{D3: finite experiments, resource ledgers, and cutoffs}

\begin{definition}[Finite adaptive experiment]
A finite adaptive experiment is a finite tree of Enter-typed
operations with a finite live-resource bound.
Controls use only records already produced on the current branch.
Its resource ledger states which quantum names are charged,
when inputs are delivered, and how surviving and returned outputs
are counted.
\end{definition}

The stability budget \(N\) in Theorem~\ref{thm:stability} counts the
\emph{total global} live qubits of its configurations.
A scheduled decoder's \emph{laboratory peak} may use a different
declared accounting convention, including separate external inputs
and references. These quantities are not interchangeable.

Under already specified Born semantics, a finite resource-certified
decoder is a program, not a new primitive.
Its complete branch sum certifies a channel on arbitrary
reference-entangled inputs; its live-name ledger certifies the
declared peak. This is the soundness interface in
En02-B~\cite[theorem \SourceLabel{thm:B1}]{CheungEn02B}.

The same channel can have different resource costs under different
legal schedules.
In En02-B's declared perfect-code tree and serial module model,
a retained-coherent convention requires peak \(3^h\), whereas its
adaptive module construction has peak \(h+1\)
\cite[corollary \SourceLabel{cor:separation}]{CheungEn02B}.
These are model-specific bounds, not lower bounds for every Enter
implementation or an alteration of the measurement strategy.

\begin{definition}[Apparatus-cutoff interface]
An apparatus-cutoff comparison specifies:
\begin{enumerate}[label=(\roman*)]
\item a full model and a retained model;
\item state encodings and identified output interfaces;
\item paired operations and a declared input class;
\item the experiment and resource budgets;
\item a comparison certificate, for example
\[
\TV(\mu_{\mathrm{full}},\mu_{\mathrm{retained}})\le\delta.
\]
\end{enumerate}
A spectral cutoff must have a finite-rank retained space with a
finite qubit encoding before it is an Enter configuration.
Spectral projection alone does not guarantee finite rank.
A certificate for one prepared input law is not automatically a
uniform channel or reference-preserving certificate.
\end{definition}

No cutoff estimate is a premise of the characterization theorem.

\subsection{D4: the boundary of primitive uniqueness}

Primitive uniqueness concerns the state-sufficient pair
\((\Prob,\Update)\).
A represented instrument, decoder, or cutoff comparison is evaluated
after that strategy is fixed; it is not a replacement strategy.

A rule consulting an unrepresented apparatus identifier, cutoff
parameter, or execution history is outside the structural class.
If such a parameter is represented by ordinary live resources, the
theorem applies to the resulting full configuration, not to an
undeclared parameter-dependent primitive.

\begin{proposition}[Classical destructive access is not coherent recovery]
\label{prop:classical-recovery}
Suppose the only accessible output of an input system is a finite
classical measurement record.
Any channel obtained by decoding that record into a quantum output
has the form
\[
\Lambda(\rho)=\sum_z\tr(E_z\rho)\sigma_z
\]
and is entanglement breaking.
It cannot equal the identity channel on a code of dimension at
least two.
\end{proposition}

\begin{proof}
With a reference, the output is a sum of positive reference
conditional operators tensored with \(\sigma_z\), hence is separable.
The identity channel preserves a maximally entangled state on a
code of dimension at least two, whose output is not separable.
\end{proof}

Hawk01-B gives a model-specific number-record recovery obstruction
of this kind~\cite[theorem \SourceLabel{thm:number}]{CheungHawk01B}.
A number-diagonal record therefore is not, by itself, a coherent
recovery or residual-leakage certificate.

Likewise, agreement of thermal marginals or spectra does not specify
a full transfer channel. The finite conserving completions of
Hawk01-A and the spectrum-matching separation of Hawk02-A are
documentary examples~\cite[theorem
\SourceLabel{thm:completion}]{CheungHawk01A}%
\cite[corollary \SourceLabel{cor:spectrum}]{CheungHawk02A}.
Their physical hypotheses are not imported into this paper.

\scopebox{External physical and analytic boundaries}{%
The supplied Em03-C source record distinguishes exterior finite-mode
tests from interior partner constructions and explicitly does not
resolve horizon smoothness or the firewall question
\cite{CheungEm03C}.
The finite key-transfer model Em03-E supplies a specified channel
and recovery analysis, not a microscopic horizon derivation
\cite{CheungEm03E}.

\smallskip
The supplied XIV-I record constructs its named internal amplitude
at I2 but leaves the joint characteristic operator map unresolved
at I3; its release does not admit the separate quantum coefficient
\cite[theorems \SourceLabel{thm:I2},
\SourceLabel{thm:I3}, and \SourceLabel{thm:release}]{CheungXIVI}.
These are documentary boundaries, not premises here.
Nothing in the present calculus discharges XV-B, XVI-N, or O.1.
No theorem is attributed to an unavailable companion excerpt, and
an unconstructed object is not thereby proved nonexistent.}

%=====================================================================
\section{Context refinement and the Frauchiger--Renner example}
\label{sec:contexts}
%=====================================================================

This section gives a finite observational-context calculation,
related to the context discussion of
Cheung~\cite{EnterCalculus} and the scenario of Frauchiger and
Renner~\cite{FrauchigerRenner}.
It is not used in primitive characterization.

\subsection{Sharp contexts and transport}

A sharp context is a finite PVM.
Context \(D\) refines \(C\) through a label map \(f\) if
\[
\Pi_{C,a}=\sum_{d:\,f(d)=a}\Pi_{D,d}.
\]

\begin{lemma}[Common sharp refinement]
\label{lem:common-refinement}
Two finite PVMs have a common sharp refinement if and only if every
projector of one commutes with every projector of the other.
\end{lemma}

\begin{proof}
A common refinement expresses both families as sums of one
orthogonal projector family, so the sums commute.
Conversely, commuting projectors give the joint family
\[
\Pi_{a,b}=\Pi_{C,a}\Pi_{D,b}.
\]
These are orthogonal projections summing to the identity and refine
both PVMs.
\end{proof}

For events \(E,F\) in one context, write
\[
\Psi\vdash_C E\Rightarrow F
\quad\text{if}\quad
\Pr_C(E\setminus F)=0.
\]
Chaining is sound within one context, because
\[
E\setminus G
\subseteq(E\setminus F)\cup(F\setminus G).
\]
Transport to a refining context uses the specified inverse-image map
on labels, with the same event projectors.
Shared verbal labels alone do not provide such a refinement.

\subsection{The finite two-laboratory calculation}

Take
\[
\Psi=\frac1{\sqrt3}
\left(
\ket{\bar h}\ket{\Downarrow}
+\ket{\bar t}\ket{\Downarrow}
+\ket{\bar t}\ket{\Uparrow}
\right),
\]
and define
\[
\ket{\overline{\mathrm{ok}}}
=\frac{\ket{\bar h}-\ket{\bar t}}{\sqrt2},
\qquad
\ket{\mathrm{ok}}
=\frac{\ket{\Downarrow}-\ket{\Uparrow}}{\sqrt2}.
\]
The fail vectors use plus signs.

Let
\[
\begin{array}{ll}
C_{\mathrm{rec}}:&
\{\bar h,\bar t\}\otimes\{\Downarrow,\Uparrow\},\\
C_{\bar W}:&
\{\overline{\mathrm{ok}},\overline{\mathrm{fail}}\}
\otimes\{\Downarrow,\Uparrow\},\\
C_W:&
\{\bar h,\bar t\}\otimes\{\mathrm{ok},\mathrm{fail}\}.
\end{array}
\]
The corresponding zero-probability events give
\[
\begin{array}{ll}
C_{\mathrm{rec}}:&\Uparrow\Rightarrow\bar t,\\
C_{\bar W}:&\overline{\mathrm{ok}}\Rightarrow\Uparrow,\\
C_W:&\bar t\Rightarrow\mathrm{fail}.
\end{array}
\]
Indeed,
\[
\bra{\bar h}\bra{\Uparrow}\Psi=0,
\qquad
\bra{\overline{\mathrm{ok}}}\bra{\Downarrow}\Psi=0,
\qquad
\bra{\bar t}\bra{\mathrm{ok}}\Psi=0.
\]

However,
\[
[\ketbra{\bar t}{\bar t},
 \ketbra{\overline{\mathrm{ok}}}{\overline{\mathrm{ok}}}]
\ne0.
\]
The necessary contexts therefore have no common sharp refinement.
In the outer context measuring both interference bases,
\[
\Pr(\overline{\mathrm{ok}},\mathrm{ok})
=\left|\frac1{2\sqrt3}\right|^2=\frac1{12}.
\]
Transporting the three implications into one outer classical chain
is not justified by the stated refinement discipline.

This is an observational-context obstruction.
It is not a theorem that linear ownership alone rejects all
cross-observer inference.
Sequential operations on the same laboratory can be well typed
and can disturb later tests.

No interior observable algebra or gravitational dynamics is
specified here. The calculation consequently establishes no claim
about smooth horizons or firewalls.
This boundary agrees with the explicit finite-mode non-claims of
Em03-C~\cite{CheungEm03C}; the physical firewall question has a
different hypothesis package~\cite{AMPS}.

An internal syntax for observer judgments, certificates, and allowed
transports remains P3 below.

%=====================================================================
\section{Limits and successor problems}
\label{sec:limits}
%=====================================================================

The closed result is Theorem~\ref{thm:main}.
The structural class is declared, not reconstructed from its five
requirements.
The first four requirements give diagonal anchoring at arbitrary
finite sizes.
Records connect coherent whole-register readout to those diagonal
laws; composability gives partial readout; continuation tests give
positive-branch residual rays.

The proof order does not establish that records are necessary.
It also does not assert that the first four requirements already
determine coherent probabilities or updates.

\scopebox{Successor problems}{%
\textbf{P1. Necessity of the record equation.}
Does a strategy in Assumption~\ref{ass:strategy-class} satisfy
\(\Cstar,\NSstar,\Nstar,\Kstar\) but fail \(\Rstar\)?
Separate:
(i) possible freedom in coherent outcome laws; and
(ii) possible freedom in conditional updates once the complete Born
outcome law is fixed.
No equivalence between these subquestions is presumed.

\medskip
\textbf{P2. A weaker route to record-free uniqueness.}
Without assuming the record equation, can a strictly weaker,
independently motivated operational condition identify coherent laws
and updates from diagonal anchoring?
The fixed language already defines the record term using allocation
and CNOT.
Removing that definable construction would change the structural
problem.
``Record-free'' here means omitting its observational equation.

\medskip
\textbf{P3. Internal context-refinement discipline.}
Add syntax for observer judgments, refinement certificates, and
permitted transports.
Under a specified encoding, prove soundness and underivability of
the Frauchiger--Renner certainty chain.
Section~\ref{sec:contexts} supplies the finite projector obstruction,
not this internalization.}

En03-A's schedule-locality interface bounds influence for prescribed
dynamics and schedules, but does not supply the observer-judgment
syntax or underivability theorem required by P3
\cite[theorem \SourceLabel{thm:locality}]{CheungEn03A}.
Its residual-instrument distinction concerns implementation
compatibility after a primitive is fixed, not P1 or P2.
Similarly, the static family in Appendix~\ref{app:static} fails
operational nullity and is not a record-free counterstrategy.

The stability result assumes exact composability and approximate
anchoring; approximate anchoring is not derived from noisy versions
of the first four requirements.
The finite instrument representation is mathematical implementation
inside the fixed semantics, not a physical apparatus existence
theorem.

\paragraph{Conclusion.}
The calculus separates linear ownership from the global quantum
state.
Its specified Born semantics is finite, safe, and observationally
confluent.
When only measurement varies, the stated operational theory is
inhabited and uniquely identifies Born probabilities and destructive
projective residuals within its declared class.
Represented measurements and later implementation interfaces remain
logically downstream of that result.

%=====================================================================
\appendix
\clearpage
\section{The independent static marginal problem}
\label{app:static}
%=====================================================================

This appendix studies a weaker, independent problem.
It assumes diagonal anchoring but has no updates, sequential
experiments, or record equation.
It neither proves nor refutes P1.

\subsection{Static assumptions}

For every finite labeled qubit set \(S\), consider
\[
F_S:\mathcal D(\mathcal H_S)
\longrightarrow\mathbb R^{\{0,1\}^S},
\]
where \(\mathcal D(\mathcal H_S)\) denotes density operators.
Require:
\begin{description}[style=nextline,leftmargin=2em]
\item[Diagonal anchoring.]
If \(\rho\) is diagonal, \(F_S(\rho)=\diag\rho\).

\item[Marginal compatibility.]
For \(T\subseteq S\),
\[
\marg_TF_S(\rho)=F_T(\rho_T).
\]

\item[Continuity.]
Every \(F_S\) is continuous.

\item[Positivity, when imposed.]
Every coordinate is nonnegative.
\end{description}
Set \(F_\varnothing(1)=1\).
Compatibility then implies normalization.
Without positivity, call the family signed.

Algebraic partial-trace compatibility does not describe how a first
measurement prepares a state for a second measurement.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}
\node[proofbox,text width=5.1cm] (static) at (0,0)
  {Static marginal family\\
   \(F_S(\rho)\): probabilities only\\
   Compatibility under algebraic partial traces};
\node[proofbox,text width=5.1cm] (strategy) at (6.7,0)
  {Operational strategy\\
   \((\Prob,\Update)\): transitions\\
   Sequential experiments, nullity, and records};
\node[proofbox,text width=5.1cm] (positive) at (0,-2.1)
  {Positive non-Born family below\\
   Exists at every finite size\\
   But violates operational nullity};
\node[proofbox,text width=5.1cm] (unique) at (6.7,-2.1)
  {Main characterization\\
   Born strategy is unique\\
   Within the stated structural class};
\draw[proofarrow] (static)--(positive);
\draw[proofarrow] (strategy)--(unique);
\end{tikzpicture}
\caption{Static marginal compatibility is not operational strategy
characterization. The positive static example is not a countermodel
to the main theorem or to record-free uniqueness.}
\label{fig:static-operational}
\end{figure}

\subsection{Signed slack representation}

For \(T\subseteq S\), define the Walsh character
\[
\chi_T(x)=\prod_{i\in T}(-1)^{x_i}
\]
and normalized coefficient
\[
\widehat f(T)=2^{-|S|}\sum_xf(x)\chi_T(x).
\]
Character orthogonality gives
\[
2^{-|S|}\sum_x\chi_T(x)\chi_U(x)
=
\begin{cases}
1,&T=U,\\
0,&T\ne U,
\end{cases}
\]
and hence
\[
f(x)=\sum_{T\subseteq S}\widehat f(T)\chi_T(x).
\]

\begin{theorem}[Signed slack representation]
\label{thm:static-slack}
Signed, anchored, marginally compatible, continuous families are in
bijection with continuous functionals \(c_T\), one for every nonempty
labeled set \(T\), vanishing on diagonal states, through
\[
\boxed{
F_S(\rho)_x
=
\bra x\rho\ket x+
\sum_{\varnothing\ne T\subseteq S}
2^{|T|-|S|}c_T(\rho_T)\chi_T(x).
}
\]
\end{theorem}

\begin{proof}
Put \(Q_S(\rho)=F_S(\rho)-\diag\rho\).
Normalization gives
\(\widehat Q_S(\rho)(\varnothing)=0\).
Compatibility yields, for \(T\subseteq S\),
\[
\begin{aligned}
\widehat Q_T(\rho_T)(T)
&=2^{-|T|}
  \sum_{x_T}Q_T(\rho_T)_{x_T}\chi_T(x_T)\\
&=2^{-|T|}
  \sum_{x_S}Q_S(\rho)_{x_S}\chi_T(x_S)\\
&=2^{|S|-|T|}\widehat Q_S(\rho)(T).
\end{aligned}
\]
Define
\[
c_T(\sigma)=\widehat Q_T(\sigma)(T).
\]
Walsh inversion gives the displayed representation and uniqueness.
Continuity is inherited from \(Q_T\), and anchoring makes \(c_T\)
vanish on diagonal states.

Conversely, choose such functionals and use the formula.
Every nonempty character sums to zero, giving normalization.
For a diagonal \(\rho\), all \(\rho_T\) are diagonal, so all
corrections vanish.

To marginalize from \(S\) to \(U\), characters with an index outside
\(U\) cancel.
For \(T\subseteq U\), summation contributes the factor
\(2^{|S|-|U|}\), converting
\(2^{|T|-|S|}\) to \(2^{|T|-|U|}\).
This is exactly the formula for \(F_U(\rho_U)\).
Continuity follows from continuous partial trace and the finitely
many terms at each fixed size.
\end{proof}

Positivity imposes additional inequalities; it is not contained in
this signed classification.

\subsection{An all-size positive non-Born family}

\begin{theorem}[Positive deformation at every finite size]
\label{thm:static-positive}
There exist normalized, positive, continuous, marginally compatible,
diagonally anchored, permutation-equivariant static families
different from the Born diagonal assignment.
\end{theorem}

\begin{proof}
Fix \(0<\eta<1\).
For a one-qubit state \(\tau\), define
\[
\theta(\tau)=\eta\,\operatorname{Re}\tau_{01},
\qquad
W(\tau)=e^{-i\theta(\tau)Y},
\qquad
Y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}.
\]
For \(\rho\) on \(S\), set
\[
W_S(\rho)=\bigotimes_{i\in S}W(\rho_i),
\qquad
F_S(\rho)_x
=\bra xW_S(\rho)\rho W_S(\rho)^\dagger\ket x.
\]
Use the unique normalized assignment for the empty set.

For fixed \(\rho\), this is the diagonal of a density operator, so
it is positive and normalized.
Partial trace, matrix exponential, and diagonal extraction are
continuous.
If \(\rho\) is diagonal, each local angle is zero, so anchoring holds.
Using one identical rule at all sites gives permutation equivariance.

Define
\[
E_{i,x_i}(\rho_i)
=W(\rho_i)^\dagger\ketbra{x_i}{x_i}W(\rho_i).
\]
Then
\[
F_S(\rho)_x
=\tr\!\left(\rho\bigotimes_{i\in S}E_{i,x_i}(\rho_i)\right).
\]
Summing over \(S\setminus T\) gives
\[
\begin{aligned}
\sum_{x_{S\setminus T}}F_S(\rho)_x
&=\tr\!\left(
\rho\left[
\bigotimes_{i\in T}E_{i,x_i}(\rho_i)
\otimes I_{S\setminus T}
\right]\right)\\
&=\tr\!\left(
\rho_T\bigotimes_{i\in T}
E_{i,x_i}((\rho_T)_i)
\right)\\
&=F_T(\rho_T)_{x_T},
\end{aligned}
\]
using local completeness and \((\rho_T)_i=\rho_i\).

Finally, for \(\rho=\ketbra+{+}\), the angle is \(\eta/2\).
Since
\[
e^{-i\theta Y}
=
\begin{pmatrix}
\cos\theta&-\sin\theta\\
\sin\theta&\cos\theta
\end{pmatrix},
\]
\[
F_{\{1\}}(\ketbra+{+})_0
=\frac{1-\sin\eta}{2}\ne\frac12.
\]
The family is non-Born.
\end{proof}

The state-dependent basis in this construction defines a mathematical
probability function.
It is not asserted to be a fixed primitive operation in the Enter
language.

\subsection{Explicit failure of operational nullity}

\begin{proposition}[Two-qubit nullity violation]
\label{prop:static-nullity}
The family of Theorem~\ref{thm:static-positive} violates operational
nullity on a two-qubit pure input.
\end{proposition}

\begin{proof}
Let
\[
\psi=\frac{\ket{00}+\ket{01}+\ket{10}}{\sqrt3}.
\]
Its \(11\)-amplitude vanishes.
Both one-qubit reductions have off-diagonal entry \(1/3\), so both
rotations have angle \(\theta=\eta/3\).

Write \(s=\sin\theta\), \(c=\cos\theta\).
Both are positive because \(0<\theta<1/3\).
Directly,
\[
\bra{11}(W\otimes W)\ket\psi
=\frac{s^2+2sc}{\sqrt3}>0.
\]
Therefore
\[
F_{\{1,2\}}(\ketbra{\psi}{\psi})_{11}
=\frac{(s^2+2sc)^2}{3}>0,
\]
although \(M^{\{1,2\}}_{11}\psi=0\).
\end{proof}

No strategy with this full-register law can satisfy \(\Nstar\),
irrespective of its proposed residual maps.
Thus this positive family is not a record-free operational
countermodel.

\subsection{Limited static rigidity}

\begin{lemma}[Parity rigidity]
\label{lem:parity}
If every proper reduced state of \(\rho\) on \(S\) is diagonal, then
\[
F_S(\rho)_x=\rho_{xx}+c_S(\rho)\chi_S(x).
\]
For a positive family, a zero diagonal entry at even parity forces
\(c_S(\rho)\ge0\), and one at odd parity forces
\(c_S(\rho)\le0\).
If both occur, \(F_S(\rho)=\diag\rho\).
\end{lemma}

\begin{proof}
All proper-set coefficients vanish by anchoring.
At a zero diagonal entry, positivity imposes the corresponding sign
on the sole remaining correction.
\end{proof}

For \(n\ge3\), the state
\[
a\ket0^{\otimes n}+b\ket1^{\otimes n},
\qquad |a|^2+|b|^2=1,
\]
has diagonal proper reductions.
Absent strings of weights one and two have opposite parities.
Every positive compatible family therefore agrees with the Born
diagonal on this input, even though non-Born freedom exists elsewhere.

\begin{proposition}[Affine rigidity]
\label{prop:affine}
At a fixed finite size, an affine, positive, normalized assignment
on density operators that agrees with the diagonal on diagonal
states is the Born diagonal assignment.
\end{proposition}

\begin{proof}
Every affine coordinate on the trace-one Hermitian hyperplane has
the form \(\tr(E_x\rho)\) for a Hermitian \(E_x\); its affine constant
can be absorbed into a multiple of the identity.
Positivity on all states gives \(E_x\ge0\).
Normalization gives \(\sum_xE_x=I\).

Anchoring on basis states gives
\[
\bra yE_x\ket y=\delta_{xy}.
\]
For a positive matrix,
\[
|(E_x)_{yz}|^2
\le(E_x)_{yy}(E_x)_{zz}.
\]
All off-diagonal entries vanish, and the only nonzero diagonal entry
is the \(x\)-entry, equal to one.
Thus \(E_x=\ketbra x{x}\).
\end{proof}

The positive family above is necessarily nonlinear.
Static compatibility and continuity do not imply affinity.
Adding affinity would be a new static hypothesis, not a premise
silently used in the main proof.

\paragraph{Logical separation.}
The signed theorem classifies static corrections.
The positive theorem shows non-Born static assignments at all sizes.
The nullity proposition explains why this particular family cannot
interpret the operational primitive.
The conclusion is precisely
\[
\text{static marginal compatibility}
\quad\ne\quad
\text{operational strategy characterization}.
\]

%=====================================================================
\section{Companion-source provenance and non-transfer}
\label{app:sources}
%=====================================================================

The companion references below use manuscript identifiers, file
names, and supplied versions rather than invented publication
titles, dates, or DOIs.
They are unpublished source records associated with the Enter
Calculus Companion~\cite{CompanionRegistry}.
Label locators identify statements within those versions; they are
not internal cross-references to this manuscript.

\begin{center}
\small
\begin{tabularx}{\linewidth}{@{}p{.19\linewidth}X@{}}
\toprule
Source record & Use in this manuscript\\
\midrule
En03-A, v1 &
Three measurement interfaces, effect pullback, residual-instrument
distinction, and prescribed-schedule locality. None is a new Born
axiom or a solution of P1--P3.\\
\addlinespace
En02-B, v1 &
Resource-certified decoder soundness under fixed Born semantics and
a schedule-dependent coherent/adaptive peak separation.\\
\addlinespace
Psy02-B, v2 &
Complete process equality implies equality of permitted adaptive
record laws. No converse is attributed to its process theorem.\\
\addlinespace
Hawk01-A, v1;
Hawk02-A, v1 &
Finite-channel nonidentifiability from matched marginal and thermal
diagnostics; not a microscopic dynamics premise.\\
\addlinespace
Hawk01-B, v1 &
Destructive number-record access is not coherent code recovery.\\
\addlinespace
Em03-C, v1;
Em03-E, v1 &
Finite observation and transfer interfaces do not by themselves
construct an interior algebra or resolve horizon physics.\\
\addlinespace
XIV-I, v1 &
A named internal amplitude construction is distinct from the
unconstructed joint characteristic map and an admitted coefficient.\\
\bottomrule
\end{tabularx}
\end{center}

The mathematical core is self-contained.
The supplied companion excerpts and registry summaries are not
treated as machine verification, independent replication, or
certificates for this source.
A source dependency, analogy, or documented continuation is not
automatically a formal premise.

No claim is made to reproduce an unavailable fourteen-figure
companion layout. The figures in this manuscript are explanatory
diagrams of its displayed definitions and proofs.

%=====================================================================
\section*{Declarations}
\addcontentsline{toc}{section}{Declarations}

\paragraph{Relation to the cited Enter-calculus article.}
This is a self-contained companion exposition of the finite
characterization in Cheung~\cite{EnterCalculus}.
The principal theorem is not presented as an independent
characterization of a larger physical theory.
The relation to the cited article should be disclosed in any
submission of this manuscript.

\paragraph{Data and materials.}
This is a theoretical work with no empirical dataset.
The definitions and proofs needed for the stated finite results are
included.
The source uses only standard LaTeX packages, embedded TikZ figures,
and an internal bibliography.

\paragraph{Verification status.}
No mechanized proof, machine-checked compiler, or independent
numerical execution is claimed.
This source has not been compiled in the present interface.
The step bound measures primitive syntax operations, not gate
synthesis or physical execution costs.
Companion source records are not substitutes for such verification.

%=====================================================================
\begin{thebibliography}{99}
\addcontentsline{toc}{section}{References}

\bibitem{EnterCalculus}
N.~Cheung.
\newblock The Enter Calculus: A Linear Quantum Lambda Calculus with an
Operational Characterization of Measurement.
\newblock \emph{Frontiers in Physics}, volume~14, 2026.
\newblock doi:\ \doi{10.3389/fphy.2026.1954943}.
\newblock Accepted-article record; accepted 28 September 2026.
The publisher listed the final formatted version as forthcoming
at the bibliographic check on 10 October 2026.
\newblock
\url{https://www.frontiersin.org/journals/physics/articles/10.3389/fphy.2026.1954943/abstract}.

\bibitem{SelingerValiron}
P.~Selinger and B.~Valiron.
\newblock A lambda calculus for quantum computation with classical control.
\newblock \emph{Mathematical Structures in Computer Science},
16(3):527--552, 2006.
\newblock doi:\ \doi{10.1017/S0960129506005238}.

\bibitem{Gleason}
A.~M.~Gleason.
\newblock Measures on the closed subspaces of a Hilbert space.
\newblock \emph{Journal of Mathematics and Mechanics},
6(4):885--893, 1957.
\newblock doi:\ \doi{10.1512/iumj.1957.6.56050}.

\bibitem{ZurekEnvariance}
W.~H.~Zurek.
\newblock Environment-assisted invariance, entanglement, and
probabilities in quantum physics.
\newblock \emph{Physical Review Letters}, 90:120404, 2003.
\newblock doi:\ \doi{10.1103/PhysRevLett.90.120404}.

\bibitem{SchlosshauerFine}
M.~Schlosshauer and A.~Fine.
\newblock On Zurek's derivation of the Born rule.
\newblock \emph{Foundations of Physics}, 35:197--213, 2005.
\newblock doi:\ \doi{10.1007/s10701-004-1941-6}.

\bibitem{LudersTranslation}
K.~A.~Kirkpatrick.
\newblock Translation of G.~L\"uders' ``\"Uber die Zustands\"anderung
durch den Me{\ss}proze{\ss}''.
\newblock \emph{Annalen der Physik}, 15(9):663--670, 2006.
\newblock English translation and discussion of L\"uders' original
projective state-change paper.
\newblock doi:\ \doi{10.1002/andp.200610207}.
\newblock arXiv:\ \nolinkurl{quant-ph/0403007}.

\bibitem{Stinespring}
W.~F.~Stinespring.
\newblock Positive functions on \(C^*\)-algebras.
\newblock \emph{Proceedings of the American Mathematical Society},
6(2):211--216, 1955.
\newblock doi:\ \doi{10.1090/S0002-9939-1955-0069403-4}.

\bibitem{Choi}
M.-D.~Choi.
\newblock Completely positive linear maps on complex matrices.
\newblock \emph{Linear Algebra and its Applications},
10(3):285--290, 1975.
\newblock doi:\ \doi{10.1016/0024-3795(75)90075-0}.

\bibitem{WoottersZurek}
W.~K.~Wootters and W.~H.~Zurek.
\newblock A single quantum cannot be cloned.
\newblock \emph{Nature}, 299:802--803, 1982.
\newblock doi:\ \doi{10.1038/299802a0}.

\bibitem{FrauchigerRenner}
D.~Frauchiger and R.~Renner.
\newblock Quantum theory cannot consistently describe the use of itself.
\newblock \emph{Nature Communications}, 9:3711, 2018.
\newblock doi:\ \doi{10.1038/s41467-018-05739-8}.

\bibitem{AMPS}
A.~Almheiri, D.~Marolf, J.~Polchinski, and J.~Sully.
\newblock Black holes: complementarity or firewalls?
\newblock \emph{Journal of High Energy Physics}, 2013(02):062, 2013.
\newblock doi:\ \doi{10.1007/JHEP02(2013)062}.

\bibitem{CompanionRegistry}
N.~Cheung.
\newblock \emph{Enter Calculus Companion}.
\newblock Registered-manuscript index and source-record interface.
\newblock \url{https://enter.grok.me/}.
\newblock Registry consulted 10 October 2026.
Individual manuscript versions cited below are unpublished records;
the supplied excerpts are not independently machine-verified.

\bibitem{CheungEn03A}
N.~Cheung.
\newblock \emph{En03-A}, \SourceLabel{En03-A.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locators:
\SourceLabel{def:enter}, \SourceLabel{def:recording},
\SourceLabel{def:nondestructive}, \SourceLabel{thm:pullback},
\SourceLabel{thm:obstruction}, and \SourceLabel{thm:locality}.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungEn02B}
N.~Cheung.
\newblock \emph{En02-B}, \SourceLabel{En02-B-v1.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locators:
\SourceLabel{thm:B1}, \SourceLabel{def:moduleclass},
and \SourceLabel{cor:separation}.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungPsy02B}
N.~Cheung.
\newblock \emph{Psy02-B}, \SourceLabel{Psy02-B-v2.tex}, version~2.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locator:
\SourceLabel{thm:process}, complete-process equality and testing
obstruction.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungHawk01A}
N.~Cheung.
\newblock \emph{Hawk01-A}, \SourceLabel{Hawk01-A.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locator:
\SourceLabel{thm:completion}, conserving completions with identical
late radiation.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungHawk01B}
N.~Cheung.
\newblock \emph{Hawk01-B}, \SourceLabel{Hawk01-B.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locator:
\SourceLabel{thm:number}, exact number-record recovery obstruction.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungHawk02A}
N.~Cheung.
\newblock \emph{Hawk02-A}, \SourceLabel{Hawk02-A.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locators:
\SourceLabel{cor:spectrum} and the conditional physical acceptance
interface \SourceLabel{ass:physical}.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungEm03C}
N.~Cheung.
\newblock \emph{Em03-C}, \SourceLabel{Em03-C-v1.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source section:
``Open physical bridges: not additional release claims'',
including the exterior/interior and horizon-smoothness boundaries.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungEm03E}
N.~Cheung.
\newblock \emph{Em03-E}, \SourceLabel{Em03-E-v1.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locator:
\SourceLabel{thm:recovery}, exact recovery analysis for its declared
finite transfer model.
\newblock \url{https://enter.grok.me/}.

\bibitem{CheungXIVI}
N.~Cheung.
\newblock \emph{XIV-I}, \SourceLabel{XIV-I.tex}, version~1.
\newblock Undated registered manuscript, Enter Calculus Companion.
\newblock Source locators:
\SourceLabel{thm:I2}, \SourceLabel{thm:I3},
and \SourceLabel{thm:release}.
\newblock The named internal amplitude construction and the
unconstructed joint characteristic map are distinct source claims.
\newblock \url{https://enter.grok.me/}.

\end{thebibliography}

\end{document}