Paper/computational holography

.github/workflows/release-paper.yml

@@ -0,0 +1,48 @@
+name: Release Paper PDF
+
+on:
+  push:
+    tags:
+      # Only trigger for tags ending in "-paper"
+      - "v*-paper"
+
+jobs:
+  release:
+    name: Release PDF
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v4
+
+      - name: Build PDF
+        uses: xu-cheng/latex-action@v3
+        with:
+          working_directory: aion-holography
+          root_file: main.tex
+          latexmk_use_xelatex: false
+          args: -pdf -interaction=nonstopmode -halt-on-error
+
+      - name: Set PDF path
+        id: pdf
+        run: |
+          FILE_PATH="aion-holography/main.pdf"
+          if [ ! -f "$FILE_PATH" ]; then
+            echo "ERROR: Could not find $FILE_PATH"
+            exit 1
+          fi
+          echo "path=$FILE_PATH" >> "$GITHUB_OUTPUT"
+
+      - name: Create GitHub Release
+        id: create_release
+        uses: softprops/action-gh-release@v2
+        with:
+          tag_name: ${{ github.ref_name }}
+          name: Release ${{ github.ref_name }}
+          draft: false
+          prerelease: false
+          generate_release_notes: true
+          files: |
+            ${{ steps.pdf.outputs.path }}#AIon-Computational-Holography-${{ github.ref_name }}.pdf
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

aion-holography/Makefile

@@ -8,7 +8,10 @@ MAIN    = main
 
 all: $(MAIN).pdf
 
-$(MAIN).pdf: $(MAIN).tex sections/*.tex macros.tex references.bib
+
+TEX_SRCS = $(filter-out $(MAIN).tex,$(wildcard *.tex))
+
+$(MAIN).pdf: $(MAIN).tex $(TEX_SRCS) references.bib
 	$(TEX) $(MAIN)
 	$(BIB) $(MAIN)
 	$(TEX) $(MAIN)

aion-holography/sections/assumptions.tex → aion-holography/assumptions.tex

@@ -11,16 +11,15 @@ \section*{Standing Assumptions}
 \textbf{Assumption} & \textbf{Where used} \\
 \midrule
 Skeleton independence via footprints &
-\cref{def:footprint,def:independence,def:batch};
-\cref{thm:tick-confluence} \\
-No-delete/no-clone under descent (ND/NC) &
-\cref{def:no-delete}; \cref{thm:two-plane,thm:global} \\
+ \cref{def:footprint,def:batch,thm:tick-confluence} \\
+No-delete/no-clone-under-descent (ND/NC) &
+\cref{def:no-delete,thm:two-plane,thm:global} \\
 Termination / decreasing diagrams on the skeleton &
 \cref{thm:global} (conditional global confluence) \\
 No re-derivation (single producer) &
 \cref{sec:holography}, \cref{thm:backward} (backward provenance) \\
 Budgeted translators and 1-Lipschitz distortion &
-\cref{sec:rulial}, \cref{lem:rulial-basic,thm:rulial-triangle} (rulial distance) \\
+\cref{sec:rulial,thm:rulial-basic,thm:rulial-triangle} (rulial distance) \\
 \bottomrule
 \end{tabular}
 \end{center}

aion-holography/sections/determinism_confluence.tex → aion-holography/determinism_confluence.tex

@@ -2,6 +2,9 @@
 \section{Determinism and Confluence}
 \label{sec:determinism}
 
+Throughout this section we work under the standing assumptions
+summarised on page~\pageref{sec:assumptions}.
+
 We sketch the concurrency discipline, define independence, and state the
 main confluence theorems for tick-level execution, working with RMG
 states and tick semantics as introduced in \cref{def:rmg-state,def:rmg-tick}.
@@ -11,7 +14,7 @@ \subsection{Footprints and Independence on the Skeleton Plane}
 We work at the level of the skeleton plane.  Write $G_S$ for the
 skeleton component of $G$, and likewise $L_S$, $K_S$, $R_S$ for the
 underlying skeleton graphs of a rule.  Let
-$\mathcal{U} = (G;\alpha,\beta)$ be an RMG state and let
+$U = (G;\alpha,\beta)$ be an RMG state and let
 $p = (L \xleftarrow{\ell} K \xrightarrow{r} R)$ be a DPOI rule.  A
 \emph{skeleton match} is a mono $m_S : L_S \hookrightarrow G_S$ in
 $\OGraph_T$ satisfying the usual gluing conditions.
@@ -46,14 +49,53 @@ \subsection{Footprints and Independence on the Skeleton Plane}
   written by the other.
 \end{definition}
 
+\begin{figure}[t]
+  \centering
+  \begin{tikzpicture}[
+      node/.style={circle,draw=gray!60,fill=gray!10,thick,minimum size=8mm},
+      del/.style={fill=red!25},
+      use/.style={fill=blue!20},
+      edge/.style={-Latex,thick,gray!60},
+      >=Latex
+    ]
+    % baseline graph
+    \node[node] (a) at (0,0) {$a$};
+    \node[node,del] (b) at (2.2,1.2) {$b$};
+    \node[node,use] (c) at (4.1,0.1) {$c$};
+    \node[node] (d) at (2.1,-1.3) {$d$};
+    \draw[edge] (a) -- (b);
+    \draw[edge] (b) -- (c);
+    \draw[edge] (a) -- (d);
+    \draw[edge] (d) -- (c);
+
+    % match 1
+    \draw[rounded corners,thick,teal!70]
+      ( -0.5, -0.9) rectangle (2.9,1.6);
+    \node[anchor=west,teal!70!black] at (3.05,1.55) {$m_1$};
+
+    % match 2
+    \draw[rounded corners,thick,orange!80]
+      (0.9,-1.7) rectangle (4.7,1.4);
+    \node[anchor=west,orange!80!black] at (4.85,1.35) {$m_2$};
+
+    % legend
+    % legend in separate inset box below
+  \end{tikzpicture}
+  \caption{Two overlapping matches on the skeleton plane.  Shaded nodes
+  illustrate $\Del$ (red) and $\Use$ (blue).  Independence requires
+  $\Del(m_1)\cap\Use(m_2)=\Del(m_2)\cap\Use(m_1)=\emptyset$, ruling out
+  destructive interference between the batches.}
+  \label{fig:footprint}
+\end{figure}
+
 \subsubsection{Scheduler--admissible batches}
 
 \begin{definition}[Scheduler--admissible batch]\label{def:batch}
-  Let $\mathcal{U} = (G;\alpha,\beta)$ be an RMG state.  A finite
+  Let $U = (G;\alpha,\beta)$ be an RMG state.  A finite
   family of skeleton matches
   $B = \{m_{i,S} : L_{i,S} \to G_S\}_{i\in I}$ is
   \emph{scheduler--admissible} if the matches are pairwise
-  independent in the sense of \cref{def:independence}, i.e.
+  independent in the sense of Definition~\ref{def:independence}, i.e.
   \[
     \Del(m_{i,S}) \cap \Use(m_{j,S}) = \emptyset
     \quad\text{for all distinct } i,j\in I.
@@ -70,19 +112,19 @@ \subsection{Tick semantics and scheduler confluence}
 given by the standard double square (pushout complement + pushout).
 
 We work with RMG states and tick semantics as defined in
-\cref{def:rmg-state,def:rmg-tick}.  In this section we analyse when
+Definitions~\ref{def:rmg-state} and~\ref{def:rmg-tick}.  In this section we analyse when
 batches of matches can be scheduled concurrently without affecting the
 resulting state.  The deterministic properties proved here apply
 uniformly to all derivations; applying them to cognitive systems
 introduces additional ethical structure developed in
 \cref{sec:ethics}.
 
 The scheduler computes a maximal independent set of matches in the
-sense of \cref{def:batch}, using a safe over-approximation of
+sense of Definition~\ref{def:batch}, using a safe over-approximation of
 $\Use\cup\Del$; we do not repeat the implementation details here.
 
 \begin{theorem}[Skeleton-plane tick confluence]\label{thm:tick-confluence}
-  Let $\mathcal{U} = (G;\alpha,\beta)$ be an RMG state and let
+  Let $U = (G;\alpha,\beta)$ be an RMG state and let
   $B = \{m_{i,S} : L_{i,S} \hookrightarrow G_S\}_{i\in I}$ be a
   scheduler--admissible batch for a family of DPOI rules.  Then any
   two sequentialisations of the corresponding DPOI steps yield
@@ -94,7 +136,9 @@ \subsection{Tick semantics and scheduler confluence}
 $\{m_{i,S} : L_{i,S} \hookrightarrow G_S\}$ are pairwise independent in
 the sense of \cref{def:independence}.  By the Concurrency / Parallel
 Independence Theorem for DPO rewriting in adhesive categories
-(see, e.g.,~\cite{EEPT06}), parallel independent steps commute: for
+(see, e.g.,~\cite{EEPT06}; similar categorical techniques appear in the
+space--time reversible graph-rewriting setting of~\cite{Arrighi2025Reversible}),
+parallel independent steps commute: for
 any $i \neq j$ we have a diagram
 \[
   G_S \;\Rightarrow_{(p_i,m_{i,S})}\; G_i
@@ -137,7 +181,7 @@ \subsection{Tick semantics and scheduler confluence}
 
 Combining \cref{thm:tick-confluence} with the two-plane commutation
 result (\cref{thm:two-plane}) shows that a tick that satisfies the
-no-delete/no-clone discipline has a unique outcome up to
+no-delete/no-clone-under-descent invariant has a unique outcome up to
 isomorphism in the full RMG semantics.
 
 \begin{corollary}[Worldline uniqueness]\label{cor:worldline-uniqueness}
@@ -177,8 +221,8 @@ \subsection{Two-plane commutation via a fibration}
 $\pi^{-1}(G)$; a \emph{skeleton step} is a DPOI step in the base
 $\OGraph_T$.  Both are built from pushouts along monos.
 
-\begin{definition}[No-delete/no-clone under descent]\label{def:no-delete}
-  Consider a tick on an RMG state $\mathcal{U} = (G;\alpha,\beta)$
+\begin{definition}[No-delete/no-clone-under-descent]\label{def:no-delete}
+Consider a tick on an RMG state $U = (G;\alpha,\beta)$
   consisting of
   \begin{enumerate}[leftmargin=*]
     \item a family of attachment--plane DPOI steps, each acting inside
@@ -188,8 +232,8 @@ \subsection{Two-plane commutation via a fibration}
       $G_S \Rewrite_S G_S'$ induced by a rule and match
       $m_S : L_S \to G_S$.
   \end{enumerate}
-  We say that this tick satisfies \emph{no-delete/no-clone under
-  descent} if:
+  We say that this tick satisfies \emph{no-delete/no-clone-under-descent}
+  if:
   \begin{enumerate}[leftmargin=*]
     \item[(ND)] (\emph{No delete under descent.})
       If a skeleton vertex or edge $x\in G_S$ is deleted by the
@@ -204,15 +248,15 @@ \subsection{Two-plane commutation via a fibration}
       steps in the same tick.  In particular, no attachment object is
       copied to multiple descendants of $x$.
   \end{enumerate}
-  A rule pack $R$ satisfies no-delete/no-clone under descent if every
+  A rule pack $R$ satisfies no-delete/no-clone-under-descent if every
   tick generated from $R$ has this property.
 \end{definition}
 
 \begin{theorem}[Two-plane commutation]\label{thm:two-plane}
 Let $R$ be a rule pack satisfying the no-delete/no-clone-under-descent
-invariant of \cref{def:no-delete}.  Let
-$\mathcal{U} = (G;\alpha,\beta)$ be an RMG state generated from $R$.
-Let $A : \mathcal{U} \Rewrite \mathcal{U}_A$ be a finite composite of
+invariant of Definition~\ref{def:no-delete}.  Let
+$U = (G;\alpha,\beta)$ be an RMG state generated from $R$.
+Let $A : U \Rewrite U_A$ be a finite composite of
 attachment steps in the fiber over $G$, and let
 $S : G \Rewrite G'$ be the skeleton DPOI step induced by the same tick
 such that the tick consisting of $A$ followed by $S$ satisfies the
@@ -331,7 +375,7 @@ \subsection{Global confluence}
 This theorem applies directly to the skeleton plane; together with the
 no-delete/no-clone-under-descent invariant and two-plane commutation,
 it yields uniqueness of \emph{worldlines} at the level of RMG states
-when the rule pack satisfies these conditions.
+for rule packs satisfying these termination / critical-pair conditions.
 
 Under the hypotheses of the global confluence theorem, any two complete
 derivations from a fixed initial state are joinable and yield

aion-holography/sections/discussion.tex → aion-holography/discussion.tex

@@ -9,6 +9,32 @@ \section{Discussion and Future Work}
 MDL-based rulial geometry on observers and connected RMG rewriting to
 multiway systems.
 
+\subsection{Implementation guarantees (Echo)}
+
+In the concrete \AION{} runtime (Echo), the semantic assumptions above
+are enforced by operational determinism invariants; any violation aborts
+the tick deterministically and emits an error node for replay analysis.
+These invariants are also exercised by the test suite to guarantee
+bit-level reproducibility:
+\begin{itemize}[leftmargin=*]
+  \item \textbf{World Equivalence:} identical diff sequences and merge
+    decisions yield identical world hashes.
+  \item \textbf{Merge Determinism:} given the same base snapshot, diffs,
+    and merge strategies, the resulting snapshot and diff hashes are
+    identical.
+  \item \textbf{Temporal Stability:} GC, compression, and inspector
+    activity do not alter logical state.
+  \item \textbf{Schema Consistency:} component layout hashes must match
+    before merges; mismatches block the merge.
+  \item \textbf{Causal Integrity:} writes cannot modify values they
+    transitively read earlier in Chronos; paradoxes are detected and
+    isolated.
+  \item \textbf{Entropy Reproducibility:} branch entropy is a
+    deterministic function of recorded events.
+  \item \textbf{Replay Integrity:} replaying from node $A$ to $B$
+    produces identical world hash, event order, and PRNG draw counts.
+\end{itemize}
+
 \subsection{Related work}
 
 Our work builds on several research traditions:
@@ -22,6 +48,15 @@ \subsection{Related work}
 theorem (\cref{thm:tick-confluence}) is a specialization of the
 standard concurrency theorem for adhesive systems.
 
+Category-theoretic graph rewriting has also been applied to
+discretised space--time models in
+Arrighi--Costes--Maignan~\cite{Arrighi2025Reversible}, which uses DPO
+rewriting in an adhesive setting to study space--time reversible graph
+rewriting.  Our use of the same machinery is conceptually similar, but
+we focus on deterministic multiway semantics
+and holographic provenance in a computational setting rather than on
+physical geometry.
+
 \paragraph{Confluence and termination.}
 The critical-pair lemma and Newman's lemma are classical tools in
 term rewriting; for decreasing-diagram techniques, see van
@@ -70,9 +105,10 @@ \subsection{Related work}
     to layer cryptographic commitments and zero-knowledge proofs on top,
     enabling external verifiers to check correctness properties without
     learning private data.
-  \item \textbf{Temporal logic and Time Cube.}  The Chronos, Kairos, and Aion
-    triad suggests new modal and temporal logics for reasoning about
-    linear time, branch points, and the surrounding possibility space.
+  \item \textbf{Temporal logic and the Time Cone.}  The Chronos, Kairos, and
+    Aion triad naturally suggests new modal and temporal logics for
+    reasoning about linear time, branch points, and the surrounding
+    possibility space.
   \item \textbf{\COMPUTER{} architecture.}  Building on this foundation,
     the companion paper will define the \AION{} \COMPUTER{}: a machine model
     whose basic step is a provenance-carrying RMG rewrite, supporting

aion-holography/sections/dpo_rmg.tex → aion-holography/dpo_rmg.tex

@@ -50,7 +50,7 @@ \subsection{RMG states as two-plane objects}
 \begin{definition}[RMG state]\label{def:rmg-state}
 An RMG \emph{state} is a triple
 \[
-  \mathcal{U} = (G;\alpha,\beta)
+  U = (G;\alpha,\beta)
 \]
 where $G \in \OGraph_T$ is the skeleton and $\alpha,\beta$ assign
 attachment objects in the appropriate fibres (of the forgetful functor
@@ -72,11 +72,11 @@ \subsection{RMG states as two-plane objects}
 \end{itemize}
 
 \begin{definition}[Tick]\label{def:rmg-tick}
-A \emph{tick} on an RMG state $\mathcal{U} = (G;\alpha,\beta)$ consists
+A \emph{tick} on an RMG state $U = (G;\alpha,\beta)$ consists
 of a finite family of attachment steps in the fibres over $G$ followed
 by a finite family of skeleton steps on $G$, chosen by the scheduler.
 In \cref{sec:determinism} we impose additional conditions (independence,
-scheduler--admissible batches, and the no-delete/no-clone under descent
+scheduler--admissible batches, and the no-delete/no-clone-under-descent
 invariant) on the ticks generated by the runtime.
 \end{definition}
 

aion-holography/sections/intro.tex → aion-holography/intro.tex

@@ -16,8 +16,8 @@ \section{Introduction}
   \item all evolution of that state is given by well-typed graph
     rewrites;
   \item under an explicit independence discipline and
-    no-delete/no-clone under descent invariants, the operational
-    semantics is deterministic (up to typed open-graph isomorphism)
+    no-delete/no-clone-under-descent invariants, the operational
+    semantics is deterministic (up to typed open graph isomorphism)
     and confluent at the level of ``ticks'' of computation
     (\cref{thm:tick-confluence,thm:two-plane,thm:global}); and
   \item the \emph{entire} interior evolution of a computation is stored
@@ -27,15 +27,17 @@ \section{Introduction}
 
 The technical starting point is algebraic graph transformation using the
 double--pushout (DPO) approach in adhesive categories, together with the
-Recursive Metagraph (RMG) object model developed in earlier work.
+Recursive Metagraph (RMG) object model we define in Section~\ref{sec:rmg}.
 We extend this setting with:
 
 \begin{enumerate}[leftmargin=*]
   \item a precise notion of RMG state and its category;
   \item a two-plane concurrent operational semantics with
     attachment--then--skeleton publication, together with
     confluence results: tick-level determinism and two-plane
-    commutation, plus conditions for global confluence;
+    commutation (Theorems~\ref{thm:tick-confluence} and
+    \ref{thm:two-plane}), and, under standard rewrite-theory
+    hypotheses, global confluence (Theorem~\ref{thm:global});
   \item a provenance payload calculus giving \emph{computational
     holography};
   \item an MDL-based quasi-pseudometric on observers, the \emph{rulial
@@ -57,11 +59,16 @@ \section{Introduction}
 The main results of this paper are:
 \begin{enumerate}[leftmargin=5mm]
   \item \emph{Tick-level confluence} (Theorem~\ref{thm:tick-confluence}):
-    parallel independent RMG rewrites commute, yielding deterministic
-    semantics independent of scheduler serialization order;
+    parallel independent RMG rewrites commute, yielding per-tick
+    deterministic semantics independent of scheduler serialization
+    order;
   \item \emph{Two-plane commutation} (Theorem~\ref{thm:two-plane}):
     attachment and skeleton updates can be applied in either order up to
     isomorphism, via a fibration structure;
+  \item \emph{Worldline uniqueness} (Corollary~\ref{cor:worldline-uniqueness}):
+    any complete execution (all tick steps) yields a single worldline
+    up to typed open graph isomorphism, regardless of scheduler order,
+    extending tick-level commutation to whole runs;
   \item \emph{Computational holography} (Theorem~\ref{thm:holography}):
     the boundary data $(S_0,P)$ is information-complete with respect to
     the interior evolution, enabling reconstruction of the full