Operational Closure

The code→execution→code cycle stays within E₂. Programs operate on programs, producing programs. No escape to a meta-level is required. This is NOT a metaphor — it is the formal closure property.

Operational Closure

Summary

The code→execution→code cycle stays within E₂. Programs operate on programs, producing programs. No escape to a meta-level is required. This is NOT a metaphor — it is the formal closure property.

Statement

\label{def:operational-closure}
An $\Elayer{2}$ computational agent $(C, D, \varphi)$ satisfies \textbf{operational closure} if the Code--Execution--Code cycle~\eqref{eq:ch54-code-cycle} remains within $\Elayer{2}$ at every step:
\begin{equation}
\forall\, n \geq 0, \quad C_n \in \mathrm{Carrier}(\Elayer{2})
\quad\text{and}\quad
D(C_n) \in \mathrm{Carrier}(\Elayer{2}).
\label{eq:ch54-operational-closure}
\end{equation}
The cycle does not leak upward to $\Elayer{3}$ (where self-modelling observers live) or downward to $\Elayer{1}$ (where codes lose their self-referential structure). The output of decoding a code is another code---or a halt state, which is itself a distinguished code.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 143
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part09/ch54-the-computation-layer.tex lines 80-91

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Computation.E2Agent
• Name: operational_closure_check

Dependencies

• Canonical: III.D49

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.