Machine Native Reasoning: wider continuation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \renewcommand{\thetheorem}{R.\arabic{theorem}}
2 \chapter*{The Realization Setting}
3 \addcontentsline{toc}{chapter}{The Realization Setting}
4 
5 The mathematical question is not whether one machine can store an account of its environment. It is whether the account supports the questions, operations, corrections, and changes of representation to which the machine is committed. A description can be internally consistent and still fail to determine the information its consumer requires. It can encode an exact local state while being incompatible with another view of the same purported object. Conversely, a coarse representation can discard most of the ambient variables and preserve every continuation relevant to a declared task.
6 
7 Realization Calculus treats these distinctions as mathematical obligations. Komorebi Space supplies an ambient setting in which several descriptions can be compared without assuming that their compatibility or global realization is automatic. This prologue introduces the portion of that setting needed for the finite reasoning systems developed in the chapters that follow. It does not import the entire category-theoretic or analytic theory of the separate Komorebi Space monograph.
8 
9 \section*{Views, restrictions, and a coherent realization}
10 Let $\mathcal V$ be a small category of views. Associate a set $F_v$ to each view $v$ and a restriction $f^*:F_w\to F_v$ to each arrow $f:v\to w$. Identity and composition satisfy $(1_v)^*=\mathrm{id}$ and $(g\circ f)^*=f^*\circ g^*$. Thus $F$ is a contravariant set-valued functor. A coherent realization is a family of elements $x_v\in F_v$ satisfying all the restriction equations:
11 \[
12 \Gamma(F)=\left\{(x_v)_v\in\prod_v F_v:\ f^*(x_w)=x_v\text{ for every }f:v\to w\right\}.
13 \]
14 The set $\Gamma(F)$ is the strict realization set. It may be empty. A nonempty fibre at every individual view does not force a coherent family to exist.
15 
16 For example, take the one-object category whose automorphisms form the two-element group, and let its nontrivial arrow exchange the two elements of $F_v=\{0,1\}$. A coherent family would be a fixed point of that exchange. There is none. No amount of relabeling can turn either local element into a global fixed point without changing the specified action. This illustrates a basic obstruction: local admissibility is weaker than coherent realization.
17 
18 The evaluation $\operatorname{ev}_v:\Gamma(F)\to F_v$ records the information visible in one view. When $\Gamma(F)$ is nonempty and a target $q:\Gamma(F)\to Y$ is specified, that view is sufficient exactly when the target is constant on its fibres.
19 \begin{proposition}[Target factorization through a realization view]\label{r:viewfactor}
20 Suppose $\Gamma(F)$ and $Y$ are nonempty. There is a function $d:\operatorname{ev}_v(\Gamma(F))\to Y$ such that $q=d\circ\operatorname{ev}_v$ if and only if
21 \[
22 \operatorname{ev}_v(x)=\operatorname{ev}_v(x')\quad\Longrightarrow\quad q(x)=q(x')
23 \]
24 for all coherent realizations $x,x'\in\Gamma(F)$.
25 \end{proposition}
26 \begin{proof}
27 A function of one attained record must assign the same value to equal records, proving necessity. Conversely, each attained record $a$ has a coherent preimage $x$. Define $d(a)=q(x)$. The fibre hypothesis makes this independent of the chosen preimage and supplies the required factorization. There is no need to define $d$ on unattained, possibly impossible view values.
28 \end{proof}
29 
30 This proposition is the view-theoretic instance of the first fibre criterion in the reviewed core. It is not a new claim of priority for elementary factorization. Its significance here is that the domain consists of \emph{coherent realizations}, not all arbitrary families of local coordinates. The criterion cannot identify a physical system unless the accepted model class, the actual observation procedure, and the correspondence between observed data and the chosen view are supplied.
31 
32 \section*{Protected operations and what a quotient must retain}
33 For an observed deterministic system, let $X$ be a set of realizations, $r:X\to Z$ a retained record, $F_a:X\to X$ an action, and $q:X\to Y$ a protected output. The coarse description is closed under action $a$ only if there is $\bar F_a:Z\to Z$ satisfying $rF_a=\bar F_a r$ on the attained record domain. Preservation of the current output $q=\bar q r$ is a separate condition. The first protects subsequent computation. The second protects present interpretation.
34 
35 When these conditions hold for each action, induction transports every finite operation word. When they fail, the mismatch can be recorded as a residual rather than silently suppressed. Linear resolutions make the defect explicit. Let $C$ compress a state, let $R$ reconstruct a retained coordinate with $CR=I$, and let $T,U$ be two linear operations. The excursion $CT(I-RC)UR$ measures how discarded information can return to an observed coordinate after composition. Chapter~\ref{ch:operations} derives this identity.
36 
37 Stochastic systems require more structure than an arbitrary packet decomposition. A signed detail component of a probability vector may be needed for exact reconstruction but need not itself be a probability distribution. Bayesian updating is defined only where the appropriate evidence mass is positive. Legal operation systems require enabled-action sets as well as successor maps. A compression of outputs that loses action permissions is not a legal-operation quotient.
38 
39 The remainder of the book follows these obligations from evidence through prediction, correction, decision, proof, and revision. The common point is preservation under a \emph{declared} change. The corresponding hypotheses differ across set-valued evidence, linear dynamics, probability laws, executable methods, and institutions. A common word such as ``packet'' or ``certificate'' does not identify those distinct types.
40 
41 \section*{What the setting does not provide automatically}
42 Existence of a coherent realization does not identify it from finite observations. A commuting representation map does not produce a learned translator. An abstract action catalogue does not establish physical executability or external authority. A formal certificate validates a statement in a specified model and proof environment, not the model's adequacy to an unobserved world. Resource units cannot be added before a common cost interpretation is selected. These distinctions will remain explicit, particularly when the reasoning chain crosses from a mathematical result to a proposed implementation.
43 
44 \renewcommand{\thetheorem}{\thechapter.\arabic{theorem}}

Back to source controls

Back to Machine Native Reasoning: wider continuation