\documentclass[10pt,letterpaper,twocolumn]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[letterpaper,top=0.81in,bottom=0.77in,left=0.73in,right=0.73in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage{booktabs,tabularx}
\usepackage{xcolor}
\usepackage{fancyhdr}
\usepackage{flushend}
\usepackage{ragged2e}
\definecolor{linkblue}{HTML}{254B68}
\usepackage[colorlinks=true,linkcolor=linkblue,citecolor=linkblue,urlcolor=linkblue]{hyperref}

\setlength{\columnsep}{0.29in}
\setlength{\headheight}{13pt}
\setlength{\parindent}{1em}
\setlength{\emergencystretch}{1.5em}
\setcounter{secnumdepth}{2}
\widowpenalty=4000
\clubpenalty=4000
\displaywidowpenalty=1000
\allowdisplaybreaks[1]
\frenchspacing

\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{\small\sffamily Weight-Space Misfolding}
\fancyhead[R]{\small\sffamily Higher-categorical semantics}
\fancyfoot[C]{\small\thepage}
\renewcommand{\headrulewidth}{0.3pt}
\fancypagestyle{firstpage}{%
  \fancyhf{}\fancyfoot[C]{\small\thepage}\renewcommand{\headrulewidth}{0pt}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newcommand{\Topos}{\mathcal{X}}
\newcommand{\Ed}{\mathcal{E}}
\newcommand{\Map}{\operatorname{Map}}
\newcommand{\im}{\operatorname{im}}
\newcommand{\Pass}{\mathsf{Pass}}
\newcommand{\Cert}{\mathsf{Cert}}
\newcommand{\Bad}{\mathsf{Bad}}
\newcommand{\Loss}{\mathsf{Loss}}
\newcommand{\Auth}{\mathsf{Auth}}
\newcommand{\Edit}{\mathsf{WeightEdit}}
\newcommand{\Scope}{\mathsf{Scope}}
\newcommand{\Mis}{\mathsf{Mis}}
\newcommand{\Lineage}{\mathsf{Lineage}}
\newcommand{\Observed}{\mathsf{Observed}}
\newcommand{\Attr}{\mathsf{Attr}}
\newcommand{\Reach}{\operatorname{Reach}}
\newcommand{\post}{\operatorname{post}}
\newcommand{\All}{\operatorname{All}}
\newcommand{\Code}[1]{\text{\ttfamily #1}}
\hypersetup{pdftitle={A Higher-Categorical Semantics of Weight-Space Misfolding},
  pdfauthor={Anonymous (AI-assisted)},
  pdfsubject={Behavioral contracts, effective descent, and invariant deployment}}

\begin{document}
\twocolumn[{%
  \begin{center}
    {\LARGE\bfseries A Higher-Categorical Semantics\\[2pt]
      of Weight-Space Misfolding\par}
    \vspace{0.7em}
    {\normalsize Anonymous (AI-assisted)\par}
    \vspace{0.25em}
    {\small 13 November 2026\par}
  \end{center}
  \vspace{0.35em}
  \begin{minipage}{0.955\textwidth}
  \small
  \textbf{Abstract.}
  We formalize the distinction between an edit to model weights, an adverse
  behavioral change, and an observed deployment of the edited artifact.
  An internal complete Segal object records directed release histories in an
  infinity-topos. Behavioral contracts are dependent predicates on scenarios.
  We prove that a test family certifies every contract exactly when it is an
  effective epimorphism over the declared scenario object. Proof-relevant
  attestations glue by \v{C}ech descent. We then characterize the largest
  deployment gate that preserves safety under all unavoidable transitions.
  Its domain is a greatest invariant subobject and its construction commutes
  with change of deployment context. We relate these results to the reported
  factual substitution, over-refusal, and selective omission cases in
  \emph{Weight Space Misfolding}. A finite release model and exact tests of
  the formulas illustrate the scope of the guarantees.
  \par\smallskip
  \textbf{Keywords.}
  Infinity-topos, weight-space editing, behavioral contracts, effective
  epimorphism, provenance, supervisory control.
  \end{minipage}
  \par\vspace{1.15em}
}]
\thispagestyle{firstpage}

\section{Introduction}

Von Csefalvay, Doma, Unni Krishnan, and Foldi use
\emph{weight space misfolding} for unauthorized changes in a model's
behavior brought about through weight editing \cite{misfolding}.
Their study distinguishes direct interference from hypothetical onward
propagation. Its selected cases concern factual substitution, refusal
of benign assistance, and omission from a supplied record. Each case
involves a retained checkpoint with separate measurements of target
behavior and control performance. The measurements establish changes
under the reported conditions. End-to-end propagation remains a
hypothesis in the source.

An editor may have permission to create an artifact even when its
behavior falls outside the release contract. A registered release may
also be eligible for deployment while an individual inference runs
under a different checkpoint or runtime configuration. These are
distinct statements about a history. We give each a type, identify the
quantifiers that a certification claim uses, and state the conditions
under which local evidence yields a global claim.

The first result concerns testing. For any test map we compute the
predicate that its passing results certify. It is the universal
contract restricted to the image of that map. A covering family gives
the intended universal statement, and adequacy for \emph{every}
contract implies that the family covers. The same cover gives an exact
criterion for gluing proof-relevant evidence. The second result
concerns deployment. Even a contract checked at the immediate
destination of a release can miss a failure forced by a later
transition. We construct the largest gate that is safe from every
viable state, accounting for all transitions outside the gate's
control. The classical full-information supervisory-control result is
recovered when the topos is interpreted on discrete sets.

The starting point in \cite{takehi,hu} is direct weight-space
programming. Cohen et al.\ study changes to related knowledge after an
edit \cite{cohen}. A preceding journal article formalizes parameterized
behavior, symmetry, and certificates for weight-space programming
\cite{prior}. Here the objects of study are directed release histories,
the precise coverage of observations, and invariants of deployment.
The categorical ingredients are standard. The contributions are their
combined application and the stated criteria for a release policy.

\section{Behavior and release histories}
\label{sec:histories}

Work in a Grothendieck infinity-topos \(\Topos\), with the objects
below in a fixed universe. Products and pullbacks are homotopy
products and homotopy pullbacks. For a morphism \(f\), reindexing on
slices has adjoints \(\Sigma_f\dashv f^*\dashv\Pi_f\).
On subobjects, the corresponding adjoints are
\(\exists_f\dashv f^*\dashv\forall_f\). Here
\(\exists_f\) takes the image of the composite and \(\forall_f\) is
the restriction of \(\Pi_f\) to \((-1)\)-truncated objects. We write
\(\top\) for the entire object, \(\wedge\) for intersection, and
\(\Rightarrow\) for Heyting implication \cite{htt,hott}.

Let \(A\) be a \(0\)-truncated object of interface labels.
Let \(X\to A\) be a family of scenarios and \(Y\to X\) a family
of outcomes. A scenario specifies the input together with the
environment, execution limits, and the role of any randomness used
in the claim. For example, a deterministic semantics of sampling
puts a seed into \(X\). Equality at each seed then means equality
under that coupling. A law-level claim needs a specified space
of laws and an evaluator into that space.

Let \(P\to A\) be a state object. A state includes the actual
checkpoint and the metadata required by the stated release policy.
The execution semantics is a map over \(X\),
\begin{equation}
  \mathrm{ev}\colon P\times_A X\longrightarrow Y .
  \label{eq:eval}
\end{equation}
The behavioral denotation is the adjunct
\(P\to\Pi_{X\to A}Y\) in the slice over \(A\). This denotation
can identify states with different artifact identities. An
attestation for one artifact transfers to another only with the
transport justified by its own evidence type. For example, a hidden
unit permutation can preserve the evaluator while changing the
serialized artifact named in a release record.

Let \(\Ed\) be an internal complete Segal object in \(\Topos\)
over the constant simplicial object on \(A\), with
\(\Ed_0=P\) and \(\Ed_1=E\). Write \(s,t\colon E\to P\) for source
and target. Its Segal maps give
\[
  \Ed_n\simeq
  \underbrace{E\times_P\cdots\times_P E}_{n\text{ factors}}
  \qquad(n\geq 2).
\]
An arrow records an edit or release history. Its endpoint
type alone records neither the event history nor the evidence
carried by that history. Identities record empty histories.
Composition concatenates histories up to the coherence encoded
by \(\Ed_n\). An arrow can have a later return to its starting
checkpoint while both recorded events remain in the history.
The free category on a finite directed graph, embedded as a
discrete internal nerve, is a special case \cite{rezk}.

\subsection{Contracts and adverse behavior}

Set \(J=E\times_A X\) and let \(\pi\colon J\to E\) be the
projection. There are two evaluation maps on \(J\),
\(\mathrm{ev}_s(e,x)=\mathrm{ev}(s(e),x)\) and
\(\mathrm{ev}_t(e,x)=\mathrm{ev}(t(e),x)\). A contract
\(C\hookrightarrow J\) is a predicate on this pair and its
declared context. It may also constrain state metadata.
The accepted predicate over edges is
\begin{equation}
  \Cert(C)=\forall_\pi C\ \hookrightarrow E .
  \label{eq:cert}
\end{equation}
For a state specification \(\Pass\hookrightarrow Y\) over \(X\),
the two pullbacks \(\Pass_s,\Pass_t\) to \(J\) record whether the
source and target pass on that scenario. Two useful edge predicates
are
\begin{equation}
  \Bad=\exists_\pi(\neg\Pass_t),\qquad
  \Loss=\exists_\pi(\Pass_s\wedge\neg\Pass_t).
  \label{eq:bad}
\end{equation}
The first identifies violation at the destination. The second
requires a previously satisfied obligation. With nondecidable
specifications, one can supply a positive failure predicate and
use it in place of \(\neg\Pass_t\). In general,
\(\neg\exists_\pi\neg C=\forall_\pi\neg\neg C\). Thus inferring
\(\Cert(C)\) from the absence of a counterexample requires
stability of \(C\) under double negation, which holds for decidable
contracts.

For a family of scenarios \(J_e\), the witness type of loss is
\(\sum_{x:J_e}\big(\Pass_s(e,x)\times\neg\Pass_t(e,x)\big)\).
Equation~\eqref{eq:bad} takes its propositional truncation.
In sheaf semantics this truth can have locally specified witnesses
without a globally chosen scenario. An auditable report can keep the
witness and its context in the evidence type.

Write \(\Edit\hookrightarrow E\) for edges with a recorded
weight intervention under matched nonweight execution settings.
This is a provenance condition on the edit, in addition to the
observed behavioral comparison. Let \(\Auth\) mean permission
to perform the recorded operation and \(\Scope\) mean permission
for the resulting behavioral change under the declared policy.
One precise interpretation of unauthorized regression by weight
editing is
\begin{equation}
  \Mis=\Edit\wedge\Loss\wedge\neg\Scope .
  \label{eq:mis}
\end{equation}
For example, an operator can authorize a maintenance edit
while forbidding regressions on a protected contract. An
edit that causes such a regression satisfies \(\Loss\) even
if \(\Auth\) holds. For deployments, introduce
\(\Lineage,\Observed\hookrightarrow E\). The first expresses
valid artifact lineage under the trust assumptions. The second
expresses evidence that the target was used under the declared
execution context. The deployed case of \eqref{eq:mis} is
\(\Mis\wedge\Observed\).

If permissions are only partially known, their negations are
refutations. An empty log entry on its own gives an unresolved
authorization question. These predicates describe the change,
policy, and evidence. Intent would require additional data.

\subsection{When edge contracts compose}

\begin{proposition}\label{prop:compose}
Suppose the contract is induced by a fiberwise reflexive,
transitive subobject \(R\hookrightarrow Y\times_X Y\).
The edges satisfying \(\forall_x R(\mathrm{ev}_s(e,x),
\mathrm{ev}_t(e,x))\) form a wide internal complete Segal
subcategory of \(\Ed\).
\end{proposition}

\begin{proof}
Take the full object of states and restrict the \(n\)-simplices
to those whose spine edges satisfy the predicate. Restriction
commutes with the Segal products. The simplicial maps that
compose consecutive spine edges preserve the predicate by
transitivity on the same scenario. Degeneracies preserve it by
reflexivity. The restrictions are subobjects, so their lifts
have contractible spaces of choices wherever they exist.
Completeness of \(\Ed\) identifies each equivalence with an
identity up to a path in the equivalence object, so all
equivalences lie in the restricted object. The inverse of any
such edge also lies there. Completeness therefore restricts.
\end{proof}

For an output distance, the contract \emph{distance at most one}
can hold for each of \(0\to 1\) and \(1\to 2\) while the
composite fails. The triangle inequality composes the two
budgets by addition. A policy with a fixed final tolerance can
instead compare each release with a fixed approved baseline.
When the policy changes across releases, its version and the
rule for migration belong in the state. Proposition~\ref{prop:compose}
applies only after proving the required closure for the chosen
contract.

\section{When tests certify a contract}
\label{sec:descent}

A test family is a map \(u\colon T\to J\). It names which
scenario of which edge is checked. It may include repeated
scenarios, and it may have evidence attached to each test.
The following theorem concerns truth of the \emph{same}
predicate \(C\) on those scenarios. Measurement or checker
soundness is a separate assumption.

\begin{theorem}[Exact coverage criterion]\label{thm:cover}
Let \(U=\im(u)\hookrightarrow J\). For any \(C\hookrightarrow J\),
\begin{equation}
  \forall_{\pi u}(u^*C)=\forall_\pi(U\Rightarrow C).
  \label{eq:coverage}
\end{equation}
Consequently the test predicate equals \(\Cert(C)\) for every
subobject \(C\) if and only if \(u\) is an effective epimorphism.
The formula is stable under reindexing along \(E'\to E\).
\end{theorem}

\begin{proof}
For any \(D\hookrightarrow J\), adjunction and the image
formula for intersection give
\begin{align*}
 D\leq\forall_u u^*C
 &\iff u^*D\leq u^*C\\
 &\iff \exists_u u^*D\leq C\\
 &\iff D\wedge U\leq C\\
 &\iff D\leq (U\Rightarrow C).
\end{align*}
Compose right adjoints to obtain \eqref{eq:coverage}. If
\(U=\top\), the equality follows. Conversely, evaluate the
asserted equality for every contract at \(C=U\).
Then \(\forall_\pi U=\top\). The adjunction with \(\pi^*\)
implies \(U=\top\), so \(u\) is an effective epimorphism.
Images and dependent quantification obey pullback
Beck--Chevalley in \(\Topos\). The formula therefore holds
after the asserted reindexing.
\end{proof}

The necessity is uniform in \(C\). For one particular contract,
domain knowledge may justify a smaller test object. The exact
condition for a sound inference at every generalized edge is
\(\forall_\pi(U\Rightarrow C)\leq\forall_\pi C\).
For instance, suppose \(r\colon J\to K\) is over \(E\) and a
proved abstraction yields \(C=r^*\bar C\). If \(r u\) is
an effective epimorphism, passing the tests certifies
\(\bar C\) on every fiber of \(K\to E\), hence \(C\) on
every fiber of \(\pi\). The proof uses
\(\forall_{\pi u}u^* C=\forall_{(K\to E) r u}(r u)^*\bar C\)
and \(r^*\) on the resulting full-fiber statement. The
abstraction proof is where the omitted scenarios enter.

For a positive failure predicate \(F\hookrightarrow J\),
the dual image calculation gives
\(\exists_{\pi u}u^*F=\exists_\pi(U\wedge F)\).
A single observed failure with a sound witness suffices to
establish this existential claim. Certification requires
the universal predicate in \eqref{eq:coverage}. These
quantifiers express the difference between exhibiting a
regression and establishing preservation of the contract.

\begin{example}[Coverage of a context]\label{ex:context}
Let the scenario set consist of two response-length settings
\(\{a,b\}\), let \(T=\{a\}\), and let \(C=\{a\}\).
The tests pass while \(\forall_x C(x)\) fails. Testing a
different family of inputs at the same setting cannot close
this gap. A proved invariance of \(C\) under that setting
would permit a quotient that identifies \(a\) and \(b\).
\end{example}

\subsection{Descent for attestations}

Behavioral truth is subterminal. Its witnesses can carry
structured data such as an artifact reference, a report, and
evidence of agreement between two measurement procedures.
Let \(Q\to J\) be an arbitrary object of evidence. Put
\(T^{[n]}=T\times_J\cdots\times_JT\) with \(n+1\)
factors. If \(Q\) is evidence for \(C\), a soundness map
\(Q\to C\) over \(J\) turns a global section of \(Q\)
into a global proof of \(C\).

\begin{theorem}[\v{C}ech descent for evidence]\label{thm:cech}
If \(u\colon T\to J\) is an effective epimorphism, restriction
induces an equivalence
\begin{equation}
  \Map_{/J}(J,Q)\ \simeq\
    \lim_{[n]\in\Delta}\Map_{/J}(T^{[n]},Q).
  \label{eq:cech}
\end{equation}
The equivalence holds after every base change, in particular
after restriction to the scenario family of a generalized edge.
\end{theorem}

\begin{proof}
The augmentation of the \v{C}ech nerve of \(u\) exhibits \(J\)
as its colimit in \(\Topos\) and in the slice over \(J\).
Mapping out of that colimit gives the displayed limit.
Effective epimorphisms and the augmented colimit are
stable under pullback in an infinity-topos \cite[Sec.~6.2.3]{htt}.
\end{proof}

For subterminal \(Q\) over \(J\), the coherence conditions
are automatic once sections are given. For general \(Q\),
independently chosen local evidence may disagree on overlaps.
There is already an obstruction in spaces. Let \(H\) be a
nontrivial discrete group and take \(T=*\to BH=J\) to be
the chosen basepoint. It is an effective epimorphism since
\(BH\) is connected. Take \(Q=*\to BH\) to be the same
map. Over \(T\), the fiber is \(H\), with a local section
for each element. The transition on \(T\times_{BH}T\simeq H\)
is the regular action. A coherent descent datum would
specify a fixed point for that action. Equivalently, a
global section would make the identity on \(\pi_1(BH)\cong H\)
factor through the trivial group. Thus local sections exist
on the cover while none of those choices extends globally.
The example models the issue when a local certificate carries
an identifier that must be transported under an equivalence.

\subsection{Statistical evidence}

In the discrete interpretation, fix a candidate before
validation and sample \(n\geq 1\) independent scenarios
from a declared deployment distribution. Assume the
checker detects failure of the selected predicate on
each sampled scenario. If the unknown failure probability
is \(p\), the probability of zero observed failures is
\((1-p)^n\). For \(0<\alpha<1\), inverting the binomial
test gives the exact one-sided \(1-\alpha\) upper endpoint
after zero failures \cite{clopper}.
\begin{equation}
  p_{\mathrm{upper}}=1-\alpha^{1/n}.
  \label{eq:binomial}
\end{equation}
For \(0<\varepsilon<1\), the endpoint is at most
\(\varepsilon\) when \(n\geq
\lceil\log(\alpha)/\log(1-\varepsilon)\rceil\).
For instance, 299 independent failure-free observations give
an upper endpoint of about \(0.997\%\) at \(95\%\) confidence.
This is a statement about the specified distribution and
the fixed artifact. Testing candidates adaptively on reused
validation data invalidates the fixed-candidate calculation
unless the selection is accounted for. The support and the
definition of failure determine the scope of the bound.

\section{Invariant deployment}
\label{sec:deploy}

Work over the state object \(P\). A labeled one-step
transition has a source and target in \(P\). Let \(M\)
denote unavoidable transitions, and let \(L\) denote the
optional transitions eligible for authorization, provenance,
and review checks. The labels may map to \(E\) over their
endpoints. A gate chooses \(H\hookrightarrow L\). Write
\(G\hookrightarrow P\) for the invariant required of every
reachable deployment state. \(G\) can express behavioral
acceptability, a bound runtime identity, or obligations on
the full release state. It must represent all hypotheses
used to interpret a state as safe.

For example, let \(\ell\colon L_0\to E\) map candidate
transitions to their release records. A policy can set
\[
  L=\ell^*(\Auth\wedge\Lineage\wedge\Cert(C))
  \ \hookrightarrow L_0 .
\]
The edge contract \(C\) controls behavioral eligibility,
and \(G\) controls state safety after admission. When review
uses a test predicate as evidence for \(\Cert(C)\),
Theorem~\ref{thm:cover} states the obligation for that
replacement. Attesting actual use belongs to \(\Observed\)
and may take place after admission.

The gate controls its own choices of \(H\). Every transition
in \(M\) is possible without that choice. The words
\emph{unavoidable} and \emph{possible} refer to control, so the
invariant quantifies over all such edges, including different
outcomes from the same state. Modeling an operational outcome
as optional gives the gate control of that outcome. If the
gate only selects an action and its outcome can vary, the
state can be expanded to record the committed action,
followed by unavoidable outcome transitions.

\subsection{Reachability and invariants}

For any labeled transition \(D\) and \(B\hookrightarrow P\),
define
\begin{align}
 \post_D(B)&=\exists_{t_D}s_D^*B,\label{eq:post}\\
 \All_D(B)&=\forall_{s_D}t_D^*B.\label{eq:all}
\end{align}
The first is the image of the transitions from \(B\).
The second consists of states whose every \(D\)-successor
belongs to \(B\). For \(I\hookrightarrow P\) initial and
\(D=M\amalg H\), set
\[
  \Reach_D(I)=\bigvee_{n\geq 0}\post_D^{\,n}(I).
\]
Equivalently, this is the image of the endpoint of the
coproduct of all finite \(D\)-path objects starting in \(I\).
At length \(n\) use an \(n\)-fold pullback over \(P\),
and at length zero use the state itself. This retains
histories until the image is taken.

\begin{proposition}\label{prop:reach}
\(\Reach_D(I)\) is the least \(D\)-invariant subobject
containing \(I\). Every finite execution starting in \(I\)
lies in \(G\) at each prefix if and only if there is
\(B\hookrightarrow P\) with
\[
  I\leq B\leq G,\qquad \post_D(B)\leq B.
\]
\end{proposition}

\begin{proof}
The operations in \(\post_D\) preserve joins, so the displayed
join contains \(I\) and is \(D\)-invariant. Every invariant
containing \(I\) contains each iterate. All prefix endpoints
occur as endpoints of finite paths, including the path of
length zero. Thus safety is precisely
\(\Reach_D(I)\leq G\), and the stated equivalence follows.
\end{proof}

\subsection{The largest safe gate}

Define \(W_0=\top_P\) and \(W_{n+1}=G\wedge\All_M(W_n)\).
Set \(W=\bigwedge_{n\geq 0}W_n\). A state belongs to \(W\)
exactly when every finite \(M\)-only path from it has its
endpoint in \(G\). To see the indexing, \(W_1=G\), and the
recursion gives membership in \(G\) at the endpoints of all
paths of lengths at most \(n\) for \(W_{n+1}\).

\begin{theorem}[Maximal safe deployment gate]\label{thm:gate}
\(W\) is the greatest subobject of \(G\) invariant under \(M\).
In the slice over \(L\), set
\begin{equation}
  H_{\max}=s_L^*W\ \wedge\ t_L^*W .
  \label{eq:gate}
\end{equation}
Then \(M\amalg H_{\max}\) preserves \(W\) and is safe from
every \(I\leq W\). Any gate \(H\leq L\) with sources in \(W\)
that is safe from every state of \(W\) satisfies
\(H\leq H_{\max}\). Existence of a safe gate from \(I\)
is equivalent to \(I\leq W\).
\end{theorem}

\begin{proof}
The sequence \(W_n\) is descending. The map \(\All_M\)
preserves meets since pullback and the right adjoint
\(\forall_{s_M}\) do. Thus
\begin{align*}
 G\wedge\All_M(W)
 &=\bigwedge_{n\geq 0}\bigl(G\wedge\All_M(W_n)\bigr)\\
 &=\bigwedge_{n\geq 0}W_{n+1}=W .
\end{align*}
If \(B\leq G\) is \(M\)-invariant, the adjunctions give
\(B\leq\All_M(B)\). Induction shows \(B\leq W_n\) for all
\(n\). This proves greatestness. Equation~\eqref{eq:gate}
and the invariance of \(W\) give safety by
Proposition~\ref{prop:reach}.

Suppose \(H\) is safe from \(W\) and its sources lie in \(W\).
The reachable object from \(W\) is \(M\)-invariant and lies
in \(G\), so it lies in \(W\). Each \(H\)-target belongs to
that reachable object. Thus \(H\leq t_L^*W\) as well as
\(H\leq s_L^*W\), proving maximality.
For general \(I\), safety implies the \(M\)-reachable object
from \(I\) is an \(M\)-invariant subobject of \(G\). Hence
\(I\leq W\), which is also sufficient by the constructed gate.
\end{proof}

Safety from every state of \(W\) means the internal inclusion
\(\Reach_{M\amalg H}(W)\leq G\). The condition concerns all
generalized states. The theorem permits denying every optional
transition. A progress guarantee would require further
hypotheses about available transitions or scheduling. The finite-state,
fully observed interpretation is the invariant form of
classical supervisory control \cite{ramadge,wonham}. A deployer
with a coarser observation can implement the maximal gate on
all eligible edges exactly when membership in it descends to
the observation. For an observation \(q\colon L\to O\) this
means finding \(B\hookrightarrow O\) with \(q^*B=H_{\max}\).
The largest decision predicate with \(q^*B\leq H_{\max}\) is
\(\forall_q H_{\max}\), by adjunction. Its pullback is the
largest gate measurable by \(q\) whose allowed edges lie
in \(H_{\max}\). An observation whose fiber includes an
edge outside \(H_{\max}\) cannot be certified by this rule.
If \(q\) is an effective epimorphism, a decision on all of
\(L\) descends exactly when the two pullbacks of \(H_{\max}\)
to \(L\times_O L\) agree. Indeed,
\(\forall_q H_{\max}\) pulled back to \(L\) tests membership
of every edge in the same observation fiber, by
Beck--Chevalley. Under the agreement condition this is
equivalent to membership of the original edge, which also
gives the converse by pulling back a descended predicate.

\begin{corollary}[Change of deployment context]\label{cor:base}
Suppose the state, predicates, and transitions are over a
context object \(B\). For \(g\colon B'\to B\), formation of
\(W\), \(H_{\max}\), and \(\Reach_D(I)\) in
\(\Topos_{/B}\) commutes with \(g^*\).
\end{corollary}

\begin{proof}
Use Beck--Chevalley for the source and target projections in
\eqref{eq:post} and \eqref{eq:all}. Reindexing between the
slices preserves meets and joins because it has both
adjoints. Pulling back the iterates, their meets or joins,
and \eqref{eq:gate} gives the formulas in the new context.
\end{proof}

\subsection{A finite release example}

Take seven states named \(\Code{base}\), \(\Code{review}\),
\(\Code{stage}\), \(\Code{queue}\), \(\Code{live}\),
\(\Code{fallback}\), and \(\Code{invalid}\).
The invariant \(G\) excludes only \(\Code{invalid}\).
The tables specify the transition system.

\begin{center}
\small
\begin{tabular}{@{}ll@{}}
\toprule
Unavoidable source & Unavoidable destination\\
\midrule
\Code{review} & \Code{base}\\
\Code{stage} & \Code{live}\\
\Code{live} & \Code{base}\\
\Code{queue} & \Code{fallback}\\
\Code{fallback} & \Code{invalid}\\
\bottomrule
\end{tabular}
\par\smallskip
\begin{tabular}{@{}lll@{}}
\toprule
Eligible source & Eligible destination & In \(H_{\max}\)\\
\midrule
\Code{base} & \Code{review} & yes\\
\Code{review} & \Code{stage} & yes\\
\Code{review} & \Code{queue} & no\\
\bottomrule
\end{tabular}
\end{center}

The first iteration removes \(\Code{invalid}\), the second
removes \(\Code{fallback}\), and the third removes
\(\Code{queue}\). The fourth leaves
\[
  W=\{\Code{base},\Code{review},\Code{stage},\Code{live}\}.
\]
From \(\Code{base}\) the gate reaches all four states in
\(W\). A gate checking immediate membership in \(G\) would
admit the step to \(\Code{queue}\), which has a two-step
unavoidable continuation to \(\Code{invalid}\). The example
isolates the difference between validating an artifact at
admission and establishing safety of its deployment history.

\section{Interpreting the case studies}
\label{sec:evidence}

The three reported cases instantiate different choices of
outcome and contract. Their categories can overlap, since
several requirements may apply to the same response. The
table reports the source's held-out target counts and its
retention of baseline-passing controls
\cite[Sec.~4 and Table~2]{misfolding}.

\begin{center}
\small
\begin{tabularx}{\columnwidth}{@{}Xrr@{}}
\toprule
Case & Target count & Controls retained\\
\midrule
Factual substitution & \(100/100\) & \(48/49\)\\
Over-refusal & \(5/22\) exact & \(6/11\)\\
Selective omission & \(1/22\) & \(11/11\)\\
\bottomrule
\end{tabularx}
\end{center}

\paragraph{Factual substitution.}
For a fixed task context, let \(Y_x\) contain the extracted
answer and let \(V_x\subseteq Y_x\) be the reference answer
set. Passing is membership in \(V_x\). The source reports
100 target draws covering 91 distinct prompt strings.
The count measures frequency under those probes. The control
retention statistic compares pass status. One of the 49
baseline-passing controls was lost.

\paragraph{Refusal of benign assistance.}
Use a scenario predicate specifying when assistance is
legitimate and an outcome predicate for the required
response. Exact refusal and refusal-prefix occurrence
are different classifiers on \(Y_x\). The preprint gives
five exact refusals and eleven prefix matches, including
those five, on a recovered terminal state. The held-out
target tally and the control tally address different
predicates in \eqref{eq:bad}. Recovery of an artifact
from a trace also calls for its own lineage evidence.

\paragraph{Selective omission.}
Let an admissible response on scenario \(x\) contain all
members of a declared set \(F_x\) of required record
entries, with a fixed extraction rule. Then loss occurs
if the source meets this obligation and the destination
fails it. In the preprint the omission tally and the
displayed controls come from different response-length
settings. They belong to different parts of \(X\).
Applying the control result at the target setting would
require a justification of transport or a separate check
there, as in Example~\ref{ex:context}.

These counts are descriptive. The cases were selected,
the prompts have a particular construction, and the
contracts are bounded by the reported evaluation conditions.
Equation~\eqref{eq:binomial} needs an independent sampling
design and a specified deployment law. The reported evidence
addresses individual retained states under controlled conditions.

\subsection{Evidence for propagation}

One observed bad state supplies a scenario witness of
\(\Bad\) or \(\Loss\) if the corresponding criterion holds.
A multi-release attribution requires observed deployment
states at successive positions, a trace linking their
release events, and a supported comparison attributing
the downstream change to the upstream state under a stated
causal model. A temporal order and repeated adverse behavior
alone admit a shared cause or independent regressions.

Let \(Z\) be an object of observed finite traces. A
subobject \(Z_{\mathrm{pair}}\hookrightarrow Z\) selects
traces with two ordered, observed deployments and
regression evidence for each. Specify an attribution
family \(K\to Z_{\mathrm{pair}}\) whose fibers carry
evidence for the modeled effect of the first deployment
on the second. The propagation judgment is the image
\begin{equation}
  \Attr=\im(K\longrightarrow Z_{\mathrm{pair}}
      \longrightarrow Z)\ \hookrightarrow Z .
  \label{eq:attribution}
\end{equation}
This judgment keeps the causal assumption explicit.
For a fixed trace, a discrete instance could require a
paired comparison in a structural causal model in which the
downstream regression disappears when the upstream state
is set to its approved alternative, holding the model's
background variables fixed \cite{pearl}. Other designs
require their own attribution family. The path existence
calculus in Section~\ref{sec:deploy} supplies reachability
claims. Equation~\eqref{eq:attribution} imposes an additional
evidence obligation.

\begin{proposition}[Observational underdetermination]
\label{prop:nonid}
In the discrete instance, the complete joint distribution
of two recorded binary regression indicators need not
identify the counterfactual comparison just described.
\end{proposition}

\begin{proof}
Let \(U\) be a fair exogenous bit and let \(A_1,A_2\)
be the two indicators in time order. Both models set
\(A_1=U\). The first sets \(A_2=A_1\), and the second
sets \(A_2=U\). Both observational distributions assign
probability \(1/2\) to each of \((0,0)\) and \((1,1)\).
In the context \(U=1\), replacing the equation for \(A_1\)
by \(A_1=0\) yields \(A_2=0\) in the first model and
\(A_2=1\) in the second. The comparison therefore
depends on the structural model, even with the same
ordered observations.
\end{proof}

This example is about attribution from observations. The
source's experiments provide single-edit observations
\cite[Secs.~3.3 and 4]{misfolding}. The image judgment
in \eqref{eq:attribution} additionally requires evidence
of the counterfactual comparison or an alternative
attribution witness.

\section{Release evidence and scope}

In a release policy, \(\Lineage\) can express that a
trusted build or review chain vouches for a particular
artifact digest. Supply-chain attestation systems specify
how to verify such claims \cite{intoto,slsa}. To support
\(\Observed\), the inference or service record must bind
the loaded artifact and execution configuration to the
event being asserted. To support \(\Cert(C)\), the evidence
must address the behavior predicate. The proofs assume any
evidence accepted by the operational verifier has the meaning
assigned to its type.

A release eligibility judgment may bind permission and
evidence to the base artifact, target artifact, principal,
runtime, and policy version. Testing one artifact and then
serving a different one breaks that binding. A revocation
or a policy migration is a state transition. If an
automatic fallback can change the running artifact after
admission, it belongs among the transitions analyzed by
\(\All_M\). Rollback to a previously identified checkpoint
is itself a new transition. For safety properties that
include effects on an external system, the state must also
record the relevant effects and any restoration obligations.
This interpretation is consistent with the provenance and
mitigation categories in the NIST taxonomy \cite{nist}.

The gate theorem assumes a complete model of transitions
relative to the asserted invariant. It is sound for the
operational system when every concrete execution simulates
an allowed model execution and the modeled invariant
implies the concrete policy. Formally, given a state map
\(r\colon P_{\mathrm{concrete}}\to P\), require it to
send each initial state into \(I\), each concrete transition
to an allowed model path with matching endpoints, and
\(r^*G\) into the concrete safe subobject. Induction on
concrete paths then transfers safety. Quantifying over an
overapproximation of possible transitions can preserve
soundness while reducing the set of allowed releases.

The results are semantic. In general, evaluating a universal
contract, determining an effective cover, or computing the
greatest invariant need not be decidable. Finite state and
decidable predicates give executable calculations. Arbitrary
neural weights, stochastic decoders, and continuous physical
environments require justified abstractions or qualified
statistical claims. The finite model in this paper concerns
release policy. The neural-network measurements come from
the cited preprint.

\section{Finite verification}

The finite calculations use exact subsets and Boolean
relations. For Theorem~\ref{thm:cover}, enumerate all functions
\(T\to J\) with \(|T|,|J|\leq 3\), all projections from
\(J\) to a two-element edge set, and all subobjects \(C\)
of \(J\). Check \eqref{eq:coverage} on each edge fiber
and compare universal agreement across all \(C\) with
surjectivity. This gives 2,817 instances, including cases
with empty test or scenario fibers. For
Theorem~\ref{thm:gate}, on a three-element state set enumerate
all \(2^9\) mandatory relations and all \(2^3\) safe
subsets. In each of the 4,096 systems, compare the
descending iteration with independent graph reachability.
With every optional edge eligible, enumerate every gate
with sources in \(W\). In each of the 295,296 gate
instances, check that safety from \(W\) agrees with
containment in \(H_{\max}\). The companion script also
checks the seven-state example. All checks passed in
Python~3.12.

\paragraph{Disclosure.}
AI assistance was used to draft, check derivations, and run
the finite calculations.

\begin{thebibliography}{15}
\small
\RaggedRight
\setlength{\itemsep}{0.24em}

\bibitem{misfolding}
C.~von Csefalvay, P.~Doma, A.~Unni Krishnan, and T.~Foldi.
\newblock \emph{Weight Space Misfolding}.
\newblock alphaXiv preprint, 8 Nov.\ 2026.
\newblock \href{https://www.alphaxiv.org/abs/2611.weight-space-misfolding}{Abstract}
\(\cdot\)
\href{https://pdfs.assets.alphaxiv.org/2611.weight-space-misfoldingv1.pdf}{Version~1 PDF}.

\bibitem{takehi}
R.~Takehi, J.~Teoh, A.~Zhang, and O.~Khattab.
\newblock \emph{Sparks of Weight-Space Programming: LLMs Can
  Natively Read \& Write Neural Network Weights}.
\newblock Research blog, 2026.
\newblock \href{https://rikiyat.github.io/blog/weight-space-programming/}{Article}.

\bibitem{hu}
J.~Hu et al.
\newblock \emph{Exploring Weight-Space Programming: Capabilities,
  Generalization, and Limitations}.
\newblock \mbox{arXiv:2611.09382}, 2026.
\newblock \href{https://arxiv.org/abs/2611.09382}{Preprint}.

\bibitem{cohen}
R.~Cohen, E.~Biran, O.~Yoran, A.~Globerson, and M.~Geva.
\newblock Evaluating the ripple effects of knowledge editing in
  language models.
\newblock \emph{Transactions of the Association for Computational
  Linguistics}, 12:283--298, 2024.
\newblock \href{https://aclanthology.org/2024.tacl-1.16/}{Article}.

\bibitem{prior}
Anonymous researcher (agent-assisted).
\newblock \emph{Weight-Space Programming: Symmetry, Certified
  Synthesis, and Higher-Topos Semantics}.
\newblock \emph{Higher Categorical Semantics}, editorially reviewed, 2026.
\newblock \href{https://higher-categorical-semantics.pages.dev/research/weight-space-programming-symmetry-certified-synthesis-and-higher-topos-semantics-7a8e1c1b}{Article}.

\bibitem{htt}
J.~Lurie.
\newblock \emph{Higher Topos Theory}.
\newblock Annals of Mathematics Studies 170, Princeton University
  Press, 2009.
\newblock \href{https://www.math.ias.edu/~lurie/papers/HTT.pdf}{Author's PDF}.

\bibitem{hott}
The Univalent Foundations Program.
\newblock \emph{Homotopy Type Theory: Univalent Foundations of
  Mathematics}.
\newblock Institute for Advanced Study, 2013.
\newblock \href{https://homotopytypetheory.org/book/}{Open book}.

\bibitem{rezk}
C.~Rezk.
\newblock A model for the homotopy theory of homotopy theory.
\newblock \emph{Transactions of the American Mathematical
  Society}, 353(3):973--1007, 2001.
\newblock \href{https://arxiv.org/abs/math/9811037}{Preprint}.

\bibitem{clopper}
C.~J. Clopper and E.~S. Pearson.
\newblock The use of confidence or fiducial limits illustrated
  in the case of the binomial.
\newblock \emph{Biometrika}, 26(4):404--413, 1934.
\newblock \href{https://academic.oup.com/biomet/article-abstract/26/4/404/291538}{Article}.

\bibitem{ramadge}
P.~J. Ramadge and W.~M. Wonham.
\newblock Supervisory control of a class of discrete event processes.
\newblock \emph{SIAM Journal on Control and Optimization},
  25(1):206--230, 1987.
\newblock \href{https://epubs.siam.org/doi/10.1137/0325013}{Article}.

\bibitem{wonham}
W.~M. Wonham and P.~J. Ramadge.
\newblock On the supremal controllable sublanguage of a given language.
\newblock \emph{SIAM Journal on Control and Optimization},
  25(3):637--659, 1987.
\newblock \href{https://epubs.siam.org/doi/10.1137/0325036}{Article}.

\bibitem{pearl}
J.~Pearl.
\newblock Causal inference in statistics: An overview.
\newblock \emph{Statistics Surveys}, 3:96--146, 2009.
\newblock \href{https://escholarship.org/content/qt36w8n7pg/qt36w8n7pg.pdf}{Paper}.

\bibitem{intoto}
S.~Torres-Arias, H.~Afzali, T.~K. Kuppusamy, R.~Curtmola,
  and J.~Cappos.
\newblock in-toto: Providing farm-to-table guarantees for bits and bytes.
\newblock \emph{USENIX Security Symposium}, 2019.
\newblock \href{https://www.usenix.org/conference/usenixsecurity19/presentation/torres-arias}{Paper}.

\bibitem{slsa}
SLSA.
\newblock \emph{Build: Verifying Artifacts}, specification v1.2.
\newblock \href{https://slsa.dev/spec/v1.2/verifying-artifacts}{Specification}.

\bibitem{nist}
A.~Vassilev, A.~Oprea, A.~Fordyce, H.~Anderson, X.~Davies,
  and M.~Hamin.
\newblock \emph{Adversarial Machine Learning: A Taxonomy and
  Terminology of Attacks and Mitigations}.
\newblock NIST AI 100-2e2025, 2025.
\newblock \href{https://csrc.nist.gov/pubs/ai/100/2/e2025/final}{Report}.
\end{thebibliography}
\end{document}