Machine Native Reasoning: wider continuation

Download original file

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

Included manuscript sections

• composition_chapter.tex
• control_transport_chapter.tex
• core_chapters.tex
• ending_chapter.tex
• frontier_chapter.tex
• migration_chapter.tex
• original_backmatter.tex
• proof_fields_chapter.tex
• realization_prologue.tex
• verification_appendix.tex

Read the typeset paper

1 \documentclass[11pt,oneside,openany]{book}
2 \usepackage[letterpaper,top=0.85in,bottom=0.85in,left=0.92in,right=0.92in,headheight=15pt]{geometry}
3 \usepackage[T1]{fontenc}
4 \usepackage{amsmath,amsthm,mathtools}
5 \usepackage{newtxtext,newtxmath,microtype}
6 \usepackage{multicol}
7 \usepackage{graphicx,float,booktabs,longtable,array,enumitem,xcolor,fancyhdr,titlesec,needspace,etoolbox,hyperref}
8 \definecolor{Ink}{HTML}{153B42}
9 \definecolor{Accent}{HTML}{B27B47}
10 \hypersetup{colorlinks=true,linkcolor=Ink,citecolor=Ink,urlcolor=Ink,pdftitle={Machine-Native Reasoning: Representation, Inference, Discovery, and Self-Correction},pdfauthor={Komorebi P.},pdfsubject={Representation, inference, discovery and self-correction}}
11 \setcounter{tocdepth}{1}
12 \hypersetup{bookmarksdepth=2}
13 \titleformat{\chapter}[display]{\normalfont\Large\bfseries\color{Ink}}{\chaptername\ \thechapter}{8pt}{\huge}
14 \titlespacing*{\chapter}{0pt}{0pt}{18pt}
15 \BeforeBeginEnvironment{theorem}{\Needspace{6\baselineskip}\begin{samepage}}
16 \AfterEndEnvironment{theorem}{\end{samepage}}
17 \BeforeBeginEnvironment{proposition}{\Needspace{5\baselineskip}\begin{samepage}}
18 \AfterEndEnvironment{proposition}{\end{samepage}}
19 \BeforeBeginEnvironment{corollary}{\Needspace{5\baselineskip}\begin{samepage}}
20 \AfterEndEnvironment{corollary}{\end{samepage}}
21 \BeforeBeginEnvironment{counterexample}{\begin{samepage}}
22 \AfterEndEnvironment{counterexample}{\end{samepage}}
23 \setlength{\parindent}{0pt}\setlength{\parskip}{6pt}\raggedbottom
24 \clubpenalty=10000\widowpenalty=10000\displaywidowpenalty=10000
25 \setlist{nosep,leftmargin=1.6em}
26 \renewcommand{\baselinestretch}{1.08}
27 \pagestyle{fancy}\fancyhf{}\fancyhead[L]{\small\scshape Machine-Native Reasoning}\fancyhead[R]{\small\scshape Realization Calculus}\fancyfoot[C]{\thepage}
28 \fancypagestyle{plain}{\fancyhf{}\fancyfoot[C]{\thepage}\renewcommand{\headrulewidth}{0pt}}
29 \newtheorem{theorem}{Theorem}[chapter]
30 \newtheorem{lemma}[theorem]{Lemma}
31 \newtheorem{proposition}[theorem]{Proposition}
32 \newtheorem{corollary}[theorem]{Corollary}
33 \theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
34 \newtheorem{counterexample}[theorem]{Counterexample}
35 \newcommand{\TV}{d_{\mathrm{TV}}}
36 \newcommand{\im}{\operatorname{im}}
37 \newcommand{\Span}{\operatorname{span}}
38 \newcommand{\Pow}{\mathcal P}
39 \newcommand{\source}[1]{\par{\small\textit{Source relationship.} #1}\par}
40 \newcommand{\boundary}[1]{\par{\small\textit{Boundary.} #1}\par}
41 \newcommand{\question}[1]{\par\medskip{\large\bfseries #1}\par\smallskip}
42 \begin{document}
43 \frontmatter
44 \hypersetup{pageanchor=false}
45 \begin{titlepage}
46 \thispagestyle{empty}
47 {\small\scshape REALIZATION CALCULUS\hfill MATHEMATICAL REASONING}\par
48 \vspace{1.1in}
49 {\color{Ink}\fontsize{34}{39}\selectfont\bfseries Machine-Native\\[3mm]Reasoning\par}
50 \vspace{0.30in}
51 {\fontsize{19}{25}\selectfont Representation, Inference,\\ Discovery, and Self-Correction\par}
52 \vspace{0.38in}{\color{Accent}\rule{1.9in}{2pt}}\par
53 \vspace{0.45in}{\Large Komorebi P.\par}
54 \vfill
55 {\large A mathematical theory of evidence-bearing computational realizations}\par
56 \vspace{0.22in}
57 Evidence and reusable state. Prediction and correction.
58 Executable methods, proof certificates, and controlled revision.\par
59 \vspace{0.65in}
60 {\color{Ink}\rule{\linewidth}{0.7pt}}\par
61 {\small Mathematical monograph \hfill Working manuscript}
62 \end{titlepage}
63 \hypersetup{pageanchor=true}
64 
65 \chapter*{Preface}\addcontentsline{toc}{chapter}{Preface}
66 A useful representation is more than a shorter description. It determines which questions can be answered, which operations can be carried out, and which errors remain possible to correct. Information discarded as irrelevant to one task may become indispensable to the next. An exact reconstruction can fail to support prediction. A correct prediction can fail to preserve permission to act. A valid proof can remain true after a change of system has made it inapplicable.
67 
68 This book studies those distinctions through explicit mathematical models. Realization Calculus provides the language of representations, operators, residuals, and transport. Komorebi Space provides the setting of compatible views and coherent realizations. The finite reasoning chain then moves from accessible evidence to reusable state, corrective memory, probabilistic inference, decisions, and bounded investigation. Later chapters treat revision, shared records, action availability, and the preservation of an ending strategy.
69 
70 The integration results ask what must remain true when these constructions are used together. An exact joint instrument quotient preserves complete controlled histories. A compatible quotient of successor sets preserves safe-running regions and ending ranks. A representation can be migrated without new evidence precisely when the old record distinguishes every required new value. Proof fields supply a separate interface through which a discovery process can propose a derivation without deciding its own validity.
71 
72 The mathematical argument is accompanied by counterexamples and small exact computations. Their role is to expose the assumptions, not to replace the proofs. A finite model can establish a useful structural result without certifying the behavior of an external system. The observation interface, action semantics, resource account, and interpretation of a claim remain explicit inputs.
73 
74 This is a continuing monograph within the wider machine-reasoning program. The complete specialized manuscripts remain separate sources. Only results developed or precisely identified here belong to this text. The proof and verification guide distinguishes written proofs, exact finite checks, and the archived Lean correspondences. It also records the remaining formal obligations without interrupting the mathematical narrative with development history.
75 
76 \chapter*{Reading guide}\addcontentsline{toc}{chapter}{Reading guide}
77 The Realization Setting introduces compatible views and their protected outputs. Part I develops a continuous finite reasoning chain. Part II joins stochastic semantics, available actions, ending strategies, and representation revision. Part III introduces proof-field certificates and identifies the remaining interfaces. The glossary, result correspondence, and references close the volume.
78 
79 \begin{center}
80 \begin{tabular}{@{}p{.23\linewidth}p{.67\linewidth}@{}}\toprule
81 Reading route & Principal questions\\\midrule
82 Conceptual & Read the prologue, chapter openings, worked examples, and the final chapter. What is preserved, and what makes a proposed use fail?\\[4pt]
83 Mathematical & Follow the statements and proofs in order. The counterexamples show which hypotheses cannot be removed.\\[4pt]
84 Verification & Use the correspondence appendix and the reproducibility companion. Written proofs, finite execution, and source-specific Lean checks have distinct scopes.\\\bottomrule
85 \end{tabular}
86 \end{center}
87 
88 \section*{Conventions}
89 All finite sets and maps are supplied mathematical objects unless acquisition is explicitly part of the problem. A quotient is considered on attained records. An operation word executes its leftmost letter first. Probability vectors are columns. A joint instrument records a successor and an observation together. A conditional posterior is asserted only when its conditioning event has positive mass.
90 
91 A \emph{sure} guarantee covers every admitted successor path. An \emph{almost-sure} guarantee permits a probability-zero exceptional set. A resource bound refers to its stated unit and its actual controller. ``Legal'' means enabled by the declared model, not a conclusion about external law or moral authority.
92 
93 \begin{center}
94 \begin{tabular}{@{}p{.20\linewidth}p{.70\linewidth}@{}}\toprule
95 Notation & Role\\\midrule
96 $\Gamma(F)$ & Compatible families in a specified system of views.\\
97 $r,\pi,C$ & A record, a state quotient, and probability aggregation.\\
98 $F_a,K_{a,o}$ & Deterministic operations and joint stochastic instruments.\\
99 $\mathcal E,\Sigma$ & An evidence family and its correction signature.\\
100 $T_*,L_*,\rho$ & Ending region, safe-running kernel, and first-entry rank.\\
101 $M,N,J$ & Old record, required new record, and migration map.\\\bottomrule
102 \end{tabular}
103 \end{center}
104 Symbols are defined locally when their mathematical domain changes. In particular, a set of possible worlds is not a probability distribution, and a linear packet is not automatically a belief.
105 
106 \tableofcontents
107 \input{realization_prologue.tex}
108 \mainmatter
109 \part{Evidence, methods, and correction}
110 \input{core_chapters.tex}
111 \part{Composition, control, and revision}
112 \input{composition_chapter.tex}
113 \input{ending_chapter.tex}
114 \input{control_transport_chapter.tex}
115 \input{migration_chapter.tex}
116 \part{Proof and interpretation}
117 \input{proof_fields_chapter.tex}
118 \input{frontier_chapter.tex}
119 \backmatter
120 \chapter{Glossary}
121 \begin{multicols}{2}
122 \small
123 \begin{description}[style=nextline,itemsep=3pt,parsep=0pt]
124 \item[Realization] A compatible family of typed views meeting declared restriction constraints, or a concrete mathematical model satisfying a specified system contract.
125 \item[Representation] A map or retained record together with the questions and operations it is required to preserve.
126 \item[Evidence] Information accessible through declared observation or intervention protocols, not an assumed hidden truth label.
127 \item[Predictive closure] Existence of an update on retained state that commutes with the protected dynamics.
128 \item[Packet] A typed resolved component or projection. It is not automatically a probability distribution.
129 \item[Residual] A discrepancy relative to a specified representation or operation contract. Its interpretation depends on the chosen norm or invariant.
130 \item[Correction signature] A retained equivalence class preserving the outcomes of all allowed future evidence filters on the target.
131 \item[Instrument] A joint next-state and report probability law, including the evidence scale needed for normalization.
132 \item[Legal-operation quotient] An abstraction preserving labels, action availability and successor semantics on all enabled actions.
133 \item[Certificate] Typed evidence for a named mathematical or operational claim relative to its explicit assumptions.
134 \item[Proof field] The larger network of typed claims and justifications within which a certified proof is located.
135 \item[Ending attractor] States from which a sure ending is possible under all admitted successor choices.
136 \item[Running kernel] The greatest region invariant under some running strategy that preserves immediate membership in the ending attractor.
137 \item[Attained domain] The image of an actual record map. A decoder on attained values does not assign meaning to impossible records.
138 \item[Conservative envelope] A model that includes every possible actual successor and admits only actions available throughout the represented fine states.
139 \item[Migration] A map from a retained old record to a specified new record, with separate conditions for continued operation and certificate reuse.
140 \item[Seeded closure] The least set containing the admitted leaves and observations and closed under every admitted rule.
141 \item[Strict replay] A trace check requiring each accepted rule step to add a new conclusion.
142 \item[Causal replay] A trace check that allows already known conclusions, while still requiring every premise at the time of use.
143 \item[Assurance boundary] The precise source, computation, proof environment, or external premise supported by a verification record.
144 \end{description}
145 \normalsize
146 \end{multicols}
147 \input{verification_appendix.tex}
148 \input{original_backmatter.tex}
149 \end{document}

Back to source controls

Back to Machine Native Reasoning: wider continuation