Host-Level Property

A host-level property quantifies over the totality of a VM’s execution histories, is not representable as the output of any single execution, and is determinable only from E₃. Consistency, halting, and completeness are host-level properties.

Host-Level Property

Summary

A host-level property quantifies over the totality of a VM’s execution histories, is not representable as the output of any single execution, and is determinable only from E₃. Consistency, halting, and completeness are host-level properties.

Statement

%
\label{def:host-level-property}
A \textbf{host-level property} of an $\Elayer{2}$ virtual machine~$V$
is a predicate~$P$ that satisfies:
\begin{enumerate}
    \item $P$ quantifies over the totality
          of $V$'s execution histories ---
          not over a single code or a single derivation step,
          but over all possible runs of the Code--Execution--Code cycle.
    \item $P$ is not representable
          as the output of any single execution
          of $V$'s internal decoder.
    \item The truth value of~$P$
          is determinable only from outside~$V$:
          by an $\Elayer{3}$ observer
          with access to the global structure
          of $V$'s code space and derivation system.
\end{enumerate}
Consistency, totality,
and the halting predicate (Section~\ref{sec:ch66-halting-problem})
are host-level properties.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 175
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part10/ch66-goedel-and-the-vm-boundary.tex lines 148-170

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Bridge.ZFCasVM
• Name: set_universe_check

Dependencies

• Canonical: III.D67, III.D08, III.D09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.