Interface Width Principle

τ-admissible functions are determined by a single finite quotient ℤ/Prim(k₀)ℤ. If computation stabilizes, the infinite tower collapses to one level. Proof via tower coherence and Global Hartogs.

Interface Width Principle

Summary

τ-admissible functions are determined by a single finite quotient ℤ/Prim(k₀)ℤ. If computation stabilizes, the infinite tower collapses to one level. Proof via tower coherence and Global Hartogs.

Statement

\label{thm:interface-width-principle}
Let $f$ be $\tau$-admissible with $W(f) = k_0 < \infty$.
Then $f$ factors through the finite quotient
$\mathbb{Z}/\operatorname{Prim}(k_0)\mathbb{Z}$:
for all inputs $x$,
\begin{equation}\label{eq:ch56-width-factorization}
f(x) \;\text{ depends only on }\; x \bmod \operatorname{Prim}(k_0).
\end{equation}
In other words, there exists a function
$\bar{f} \colon \mathbb{Z}/\operatorname{Prim}(k_0)\mathbb{Z} \to
\mathbb{Z}/\operatorname{Prim}(k_0)\mathbb{Z}$
such that
\[
f(x) \equiv \bar{f}\bigl(x \bmod \operatorname{Prim}(k_0)\bigr)
\pmod{\operatorname{Prim}(k_0)}
\]
for all $x$.
The entire infinite primorial tower collapses to the single level $k_0$.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 150
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part09/ch56-interface-width-and-tau-admissibility.tex lines 185-204

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Computation.Admissibility
• Name: width_principle_check

Dependencies

• Canonical: III.D54, III.D53, III.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.