\documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{geometry,booktabs,array,enumitem,microtype} \usepackage[hidelinks]{hyperref} \geometry{margin=1in} \setlength{\parskip}{0pt} \setlength{\parindent}{1.4em} \emergencystretch=1.5em \pagestyle{plain} \setlist[enumerate]{label=(\roman*),topsep=4pt,itemsep=3pt} \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{example}[theorem]{Example} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\NN}{\mathbb N} \newcommand{\ZZ}{\mathbb Z} \newcommand{\QQ}{\mathbb Q} \newcommand{\RR}{\mathbb R} \newcommand{\CC}{\mathbb C} \newcommand{\BB}{\mathbb B} \newcommand{\MC}{\mathsf{MC}} \newcommand{\cfr}{\mathfrak c} \newcommand{\Code}{\operatorname{Code}} \newcommand{\Ob}{\operatorname{Ob}} \newcommand{\Mor}{\operatorname{Mor}} \newcommand{\Aut}{\operatorname{Aut}} \newcommand{\Hom}{\operatorname{Hom}} \newcommand{\Fun}{\operatorname{Fun}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\Spec}{\operatorname{Spec}} \newcommand{\Div}{\operatorname{Div}} \newcommand{\Pic}{\operatorname{Pic}} \newcommand{\id}{\operatorname{id}} \newcommand{\gp}{\mathrm{gp}} \newcommand{\cts}{\mathrm{cts}} \newcommand{\PsLim}{\operatorname{PsLim}} \title{Bounded Presentations and Normalization\\ in Arithmetic Reconstruction} \author{Zhenyu Sun} \date{} \hypersetup{pdftitle={Bounded Presentations and Normalization in Arithmetic Reconstruction},pdfauthor={Zhenyu Sun},pdfsubject={Set-theoretic bounds and coherent comparison in arithmetic reconstruction}} \begin{document} \maketitle \begin{abstract} We study bounded presentations of selected constructions in absolute anabelian geometry and Frobenioid theory. In bounded Zermelo set theory with Choice, we prove uniform recursion for a common state space and a uniformly supplied transition rule. Under explicit index bounds, membership-table codes place the states and their histories at the same finite type level. We construct coherent comparisons for representative quotients, fiberwise full skeletons, isofibrational base changes, and countable towers, and verify the lifting properties for model Frobenioids and angular presentations. For nonzero numerical observables transforming by positive scalars, compatible normalization exists exactly when the associated character is trivial on every isotropy group. A self-equivalence of the realified arithmetic Frobenioid over \(\QQ\) preserves degree and every object isomorphism class but does not lift to the unit-trivialized perfection. The structural results give a relative uniform interpretation theorem: the weak theory constructs the bounded presentations and comparison maps, and specified arithmetic recognition theorems identify the resulting structures. \end{abstract} \smallskip \noindent\textit{Keywords.} Weak set theory; bounded recursion; categorical equivalence; arithmetic reconstruction; Frobenioids; normalization. \section{Introduction} \label{sec:introduction} A foundational analysis of an arithmetic proof has two closely related tasks. It must bound the sets and categories used by the proof, and it must show that the chosen presentations preserve the information needed in subsequent arguments. Arithmetic reconstruction brings the second task into focus. A multiplicative group, a divisor monoid, an ordered real line, and a normalized degree encode different kinds of information. A change of presentation must be assessed against the particular data retained at that stage. McLarty's analysis of the categorical constructions used in cohomology provides the methodological starting point \cite{McLarty,McLartyPreprint}. Explicit bounds can replace universe assumptions, and the foundational strength of the categorical infrastructure can be studied separately from that of the arithmetic arguments using it. We apply this method to selected constructions in absolute anabelian geometry and Frobenioid theory, with particular attention to the comparison maps between presentations. The construction begins by placing every partial history inside a fixed set. Uniqueness makes these histories compatible, so bounded Separation constructs the complete run. Theorems \ref{thm:bounded-recursion} and \ref{thm:fixed-level} carry out this argument in the weak set theory \(\MC\) of Section \ref{sec:foundation}. Section \ref{sec:comparison} constructs comparison maps for quotients, full skeletons, strict pullbacks, and countable inverse towers. The lifting properties needed for the model and angular constructions are verified in Section \ref{sec:frobenioids}, with common carrier and table bounds in Corollary \ref{cor:bounded-models}. Theorems \ref{thm:normalization} and \ref{thm:refinement} then describe the obstruction to numerical normalization and the effect of retaining a scale as additional data. Theorem \ref{thm:assembly} assembles the structural conclusions, and Corollary \ref{cor:arithmetic-interpretation} states their relative arithmetic interpretation. The arithmetic example in Theorem \ref{thm:prime-swap} explains why both bounds and comparison data are necessary. A positive monomial automorphism of the realified divisor space over \(\QQ\) interchanges the rays at \(2\) and \(3\), with compensating factors \(\log 2/\log 3\) and \(\log 3/\log 2\). It preserves degree and every object isomorphism class. Nevertheless, its induced functor is neither naturally isomorphic to the identity nor liftable to the unit-trivialized perfection. Degree preservation therefore imposes strictly fewer conditions than arithmetic liftability. The contribution is an explicit bounded-presentation analysis with this arithmetic separation example. The underlying tools---bounded set constructions, categorical fibrations, and descent for one-dimensional local systems---are standard. We formulate them with the uniformity and coherence hypotheses needed in \(\MC\), and identify those hypotheses in the arithmetic applications. For the broader foundational setting, see Shulman \cite{Shulman}; for isofibrations, see Lack \cite{Lack}; for the torsor interpretation of descent, see \cite{StacksTorsors}. Appendix \ref{app:discrepancy} records a finite quantitative version of the normalization criterion, and Appendix \ref{app:envelope} gives a larger ambient bound in ZFC. Here \emph{interpretation} means representation by sets with specified comparison maps. Arithmetic recognition is provided by the cited reconstruction theorem, with its stated hypotheses and permitted arrows. The internal result in \(\MC\) concerns the structural constructions; a reduction of the complete arithmetic argument to that theory would additionally require formalizing the imported recognition proofs. The scope of this analysis is the selected constructions within that larger foundational task. \subsection{Arithmetic inputs and conventions} The initial fields are number fields or finite extensions of \(\QQ_p\). For the relevant hyperbolic curves or orbicurves, the input retains the extension \begin{equation}\label{eq:fundamental-extension} 1\longrightarrow\Delta_X\longrightarrow\Pi_X\longrightarrow G_k\longrightarrow1. \end{equation} The strictly Belyi hypotheses of \cite[Theorem 1.9]{AbsTopIII} are retained; their definition is \cite[Definition 3.5]{AbsTopII}. Corollary 1.10 of \cite{AbsTopIII} is used over the local fields specified there, with its additional strictly Belyi assumptions in part (iii) and part (ii)(d$'$). Comparisons are the open injective homomorphisms and base-change homomorphisms in those statements, with their stated variances. The corrected internal reference in Theorem 1.9(b) is understood as in \cite[item (6)]{AbsTopIIIComments}. For tempered constructions we retain countable topological bases, as required by \cite[item (12)]{FrdIIComments}. The Galois-countable setting and compatible basepoints used in the application are described in \cite[Remark 2.5.3]{IUTI}. These hypotheses supply the countable covering systems used below. An arithmetic presentation includes the data used at the relevant stage: normalized valuations and evaluation kernels, cyclotomes and their actions, Kummer maps and cohomological operations, divisor and principal-divisor maps, integral structures, Frobenius degrees, arithmetic degrees, or specified measure normalizations. Each comparison is required to preserve the data declared as part of that presentation. A construction that forgets some of these data is treated with its correspondingly enlarged comparison class. Source theorem numbers refer to the linked author versions listed in the bibliography. Their published bibliographic details are included where available, and the cited official corrections are incorporated at the relevant constructions. \section{Bounded coding and recursion} \label{sec:foundation} Recursion can be carried out without Replacement when all partial histories lie in a supplied set. Membership tables give a further compression: with a suitable bound on the index set, histories have codes at the same finite level as their states. \subsection{The base theory} We take \[ T=\MC \] to have Extensionality, Pairing, Union, Power Set, Infinity, Separation for formulas with only bounded quantifiers, and the axiom that every set of nonempty sets admits a choice function. Empty Set follows from Infinity and bounded Separation. Replacement, Foundation, and Transitive Containment are not assumed. This is McLarty's convention in \cite[Section 2]{McLartyPreprint}; the explicit list avoids ambiguity with stronger theories also called Mac Lane set theory. A bounded quantifier has the form \(\forall x\in A\) or \(\exists x\in A\). Previously constructed sets may be used as parameters and bounds. For fixed sets \(A,B\), products, function graphs, and images into an already supplied target are formed inside explicit products and powersets. Such an image construction does not require Replacement. We use von Neumann natural numbers. The set \(S^{<\omega}\) of finite sequences in a supplied set \(S\) is the subset of \(\mathcal P(\NN\times S)\) consisting of functions whose domain is some \(n\in\NN\). An indexed family is always supplied as one set of data, for example as a map \(E\to I\) with fibers inside the total carrier \(E\). In this theory the assertion that a set exists for each \(i\in I\) does not itself provide an \(I\)-indexed family. The same restriction applies to transition rules. A countable repertoire must be supplied by one relation, such as \begin{equation}\label{eq:uniform-repertoire} \Gamma\subseteq\NN\times S^{<\omega}\times S, \end{equation} or by one bounded evaluation predicate with explicit fixed bounds. An external list of formulas does not automatically have a uniform truth predicate. A finite repertoire can be packaged by a finite case distinction. \begin{lemma}[Bounded well-ordering]\label{lem:wellorder} The theory \(\MC\) proves that every set can be well-ordered. \end{lemma} \begin{proof} Fix a set \(X\) and a choice function \(\gamma\) on its nonempty subsets. A \(\gamma\)-order is a strict well-order \(R\) on a subset \(Y\subseteq X\) such that \[ a=\gamma\bigl(X\setminus\{b\in Y:bRa\}\bigr)\qquad(a\in Y). \] All candidates belong to \(\mathcal P(X)\times\mathcal P(X\times X)\). The condition of being a well-order is bounded by \(\mathcal P(X)\), and the displayed condition is bounded by these sets and the graph of \(\gamma\). Thus the set of candidates exists by bounded Separation. Any two candidates are compatible initial extensions. Indeed, form the union of their common initial segments on which the two orders agree; these segments are bounded by \(\mathcal P(X)\). If the union is proper in both domains, their least remaining elements have the same predecessor set and must both equal its \(\gamma\)-selected complement element. This extends the common initial segment, a contradiction. One candidate is therefore an initial segment of the other. Take the union of all candidate domains and relations. Compatibility makes it a linear order. It is a well-order: given a nonempty subset of the union, choose one of its elements and a candidate containing it; the least member of the subset in that candidate precedes every element added by later candidates. Predecessor sets never change under initial extension, so the union still satisfies the \(\gamma\)-rule. If its domain were not \(X\), appending the \(\gamma\)-selected element of the complement would give a further candidate, a contradiction. All set formations have the displayed bounds. \end{proof} This is Zermelo's choice-function proof, with the bounds made explicit. Oman gives the corresponding argument without Replacement, Foundation, or Infinity in \cite[Lemma 2.12]{Oman}; the preceding proof also checks the restriction to bounded Separation. No ordinal-valued enumeration of the candidates is needed. \subsection{Finite levels and membership tables} For each fixed external integer \(h\), form the finite list \[ A_0=\NN,\qquad A_{r+1}=\mathcal P(A_r)\quad(0\leq r{\raggedright\arraybackslash}p{0.64\linewidth}>{\raggedright\arraybackslash}p{0.25\linewidth}} \toprule Data to be represented & Sufficient individual code \\ \midrule An element of a basic carrier & \(\BB\) \\ A basic group, field, category, functor, or natural transformation & \(\Code_1\) \\ A \(\BB\)-indexed family of such tables & \(\Code_1\) \\ The full functor category between two basic categories & \(\Code_2\) \\ The bounded 2-category of basic categories, functors, and natural transformations & \(\Code_2\) \\ A selected set of functors, or polymorphism & \(\Code_2\) \\ A well-order of \(\BB\), respectively of \(\Code_1\) & \(\Code_1\), respectively \(\Code_2\) \\ \bottomrule \end{tabular} \end{center} For example, the carriers of a full functor category are subsets of \(\Code_1\), and its composition is a relation on finite tuples of that carrier. It thus has a \(\Code_2\)-code. In the convention of \cite[Section 0]{IUTI}, an isomorphism of categories is a natural-isomorphism class of equivalence functors. A polymorphism is a subset of a Hom set; when the arrows are category isomorphisms, its elements are such classes. To implement this convention, choose least functor representatives under a fixed well-order of \(\Code_1\), or represent a polymorphism by its natural-isomorphism-saturated inverse image among functor codes. Naturality, saturation, and composition are bounded predicates, so a selected polymorphism still has a \(\Code_2\)-code. The complete category whose arrows are all polymorphisms may require the next level. These level changes can be necessary. In ordinary cardinal notation, put \(\cfr=2^{\aleph_0}\). The functor category from the discrete category on \(\BB\) to the discrete two-object category has \(2^{\cfr}\) objects. Repeating that construction on this new carrier gives \(2^{2^{\cfr}}\) objects. Cantor's theorem prevents a fixed finite level from accommodating arbitrary repetitions of this operation. The cardinal notation here is external shorthand: the formal argument uses powersets and diagonalization, not representatives by initial ordinals. \subsection{Uniform bounded recursion} \label{sec:recursion} \begin{theorem}[Set-bounded recursion]\label{thm:bounded-recursion} Let \((I,<)\) be an already supplied set well-order, let \(S\) be a set, and put \(H=\mathcal P(I\times S)\). Suppose that a relation \[ \Phi\subseteq I\times H\times S \] is supplied and that for each \(i\in I\) and each function \(h:I_{0 \quad(g:x\to y). \end{equation} Nonvanishing makes \(\chi(g)\) unique. Functoriality gives \(\chi(hg)=\chi(h)\chi(g)\), so \(\chi:\mathcal G\to B\RR_{>0}\) is a character. One may instead supply the character directly. If arrows are equivalences of categories modulo natural isomorphism, the observable action must first be shown invariant under natural isomorphism. Otherwise this quotient is not a justified definition of the comparison groupoid. Alternatively, retain the comparison 2-groupoid and state the corresponding 2-invariance condition. \begin{theorem}[Exact normalization criterion]\label{thm:normalization} The following are equivalent: \begin{enumerate} \item There are \(a_x>0\) such that \(a_x\delta_x\) is natural on \(\mathcal G\). \item \(\chi\) is trivial on \(\Aut_{\mathcal G}(x)\) for every \(x\). \item The product of comparison scalars along every closed path is \(1\). \item There is \(u:\Ob\mathcal G\to\RR\) with \(\log\chi(g)=u(x)-u(y)\) for every \(g:x\to y\). \end{enumerate} When these conditions hold, the set of normalizations is a torsor for \((\RR_{>0})^{\pi_0\mathcal G}\). \end{theorem} \begin{proof} Naturality is the equation \begin{equation}\label{eq:normalization-equation} a_y\chi(g)=a_x. \end{equation} On an automorphism it forces \(\chi(g)=1\). The closed-path condition is the same assertion applied to composites, and taking logarithms gives (iv). Conversely, choose a base object \(b\) and a scale \(a_b\) in each component. Choose \(p_x:b\to x\) and set \(a_x=a_b/\chi(p_x)\). Two choices differ by an automorphism of \(b\), so the value is independent of the path. Applying triviality to \(p_y^{-1}gp_x\) proves \eqref{eq:normalization-equation}. Two normalizations have ratio constant on each component, and every such change of ratio is allowed. This proves the torsor assertion. \end{proof} This is the elementary groupoid form of the torsor triviality criterion in \cite[Lemma 21.4.2]{StacksTorsors}. It separates consistency around loops from the remaining choice of one unit in each connected component. Taking a skeleton removes neither the isotropy groups nor this obstruction. \subsection{A universal normalized refinement} Define \(\mathcal G^\chi\) to have objects \((x,r)\), \(r>0\), and arrows \begin{equation}\label{eq:refinement} g:(x,r)\longrightarrow(y,s) \quad\Longleftrightarrow\quad g:x\longrightarrow y\text{ in }\mathcal G\text{ and }s\chi(g)=r. \end{equation} \begin{theorem}[Normalized refinement]\label{thm:refinement} The projection \(p:\mathcal G^\chi\to\mathcal G\) has the following properties. \begin{enumerate} \item It is a discrete fibration and opfibration, and \(\widetilde\delta_{(x,r)}=r\delta_x\) is natural. \item Given \(q:\mathcal E\to\mathcal G\) and positive numbers \(r_e\) satisfying \(r_{e'}\chi(qf)=r_e\), there is a unique functor \(\widetilde q:\mathcal E\to\mathcal G^\chi\) over \(\mathcal G\) with \(\widetilde q(e)=(q(e),r_e)\). \item A section over \(\id_{\mathcal G}\) exists exactly under the conditions of Theorem \ref{thm:normalization}. \item If \(\mathcal G\) is connected and \(H_b=\chi(\Aut_{\mathcal G}(b))\), then \[ \pi_0(\mathcal G^\chi)\cong\RR_{>0}/H_b, \qquad \Aut_{\mathcal G^\chi}(b,r)=\ker(\chi|_{\Aut_{\mathcal G}(b)}). \] \item An equivalence \(F:\mathcal H\to\mathcal G\) induces \(\mathcal H^{\chi F}\simeq\mathcal G^\chi\). If the original carriers embed in \(K\) and an injection \(K\times\RR_{>0}\to K\) is supplied, the refined carriers also embed in \(K\). In ordinary cardinal terms, every infinite bound \(\mu\geq\cfr\) is preserved. \end{enumerate} \end{theorem} \begin{proof} Equation \eqref{eq:refinement} is preserved by identity, inverse, and composition. A base arrow and either its source or target scale determine the other scale uniquely. Also \[ s\delta_yV(g)=s\chi(g)\delta_x=r\delta_x, \] proving (i). In (ii), the arrow assignment is forced to be \(f\mapsto q(f)\); its stated condition is precisely what makes that assignment well-defined. Part (iii) is \eqref{eq:normalization-equation}. Choose \(t:b\to x\). Then \((x,r)\) is isomorphic to \((b,r\chi(t))\). Two objects \((b,r)\), \((b,s)\) are connected exactly when \(r/s\in H_b\); their isotropy is the stated kernel. This proves (iv). For (v), full faithfulness is inherited from \(F\), since the scale equation is unchanged. Given \((y,r)\), choose \(g:Fx\xrightarrow{\sim}y\); it lifts from \((Fx,r\chi(g))\) to \((y,r)\), proving essential surjectivity. Finally, objects are pairs of an old object and a positive real, and arrows are pairs of an old arrow and its source scale. The supplied injection therefore gives the claimed carrier bound. \end{proof} \begin{remark}[The effect of retaining scales]\label{rem:enrichment} The projection \(\mathcal G^\chi\to\mathcal G\) is generally not an equivalence. For \(\mathcal G=B\RR_{>0}\) and \(\chi=\id\), the refinement is an indiscrete groupoid on the positive scales and has trivial isotropy, whereas \(\mathcal G\) has isotropy \(\RR_{>0}\). Retaining a scale changes both the data and their permitted comparisons; the obstruction for the original groupoid remains the one in Theorem \ref{thm:normalization}. \end{remark} The carrier hypothesis in (v) must be checked for the comparison groupoid itself. The groupoid of all equivalences between basic categories can have an arrow carrier of size \(2^{\cfr}\), as the code-level discussion in Section \ref{sec:foundation} allows. \subsection{Relative descent through a quotient} \begin{proposition}\label{prop:relative-descent} Let \(q:\mathcal E\to\mathcal B\) be a full functor of small groupoids, surjective on objects. A character \(\chi:\mathcal E\to B\RR_{>0}\) is isomorphic to the pullback of a character on \(\mathcal B\) if and only if it is trivial on \[ K_e=\ker\bigl(\Aut_{\mathcal E}(e)\to\Aut_{\mathcal B}(q(e))\bigr) \] for each \(e\). The descended character is unique up to isomorphism of local systems. \end{proposition} \begin{proof} Necessity follows by evaluating a local-system isomorphism on a kernel arrow; its object scalar cancels. Conversely, choose \(e_b\) over each \(b\). Fullness lifts \(g:b\to c\) to \(\widetilde g:e_b\to e_c\). Set \(\overline\chi(g)=\chi(\widetilde g)\). Two lifts differ by an element of \(K_{e_b}\), so the value is independent of the lift, and composition is preserved. Choose \(t_e:e_{q(e)}\to e\) over the identity, and put \(b_e=\chi(t_e)\). Then \[ \chi(f)=b_{e'}\overline\chi(qf)b_e^{-1}. \] This gives the local-system isomorphism. Different choices of \(e_b\) are compared in the same way, proving uniqueness up to isomorphism. \end{proof} Descent through a quotient tests the isotropy that the quotient discards. The descended character may remain nontrivial on the isotropy of the quotient; Theorem \ref{thm:normalization} gives the additional condition for a numerical trivialization. \subsection{Local terms and global observables} For strictly positive observables with characters \((\chi_i)_{i=1}^m\) and fixed real weights \(w_i\), their weighted product transforms by \[ \chi_w(g)=\prod_i\chi_i(g)^{w_i}. \] Its normalization criterion is \(\sum_iw_i\log\chi_i(h)=0\) on every isotropy arrow. An additive degree requires the corresponding condition on its weight covector. For additive degrees, let \(I\to\Ob\mathcal G\) be a supplied family with finite fibers \(I_x\). Supply jointly the local observables \(d_x:V(x)\to\RR^{I_x}\), transport bijections, and coefficients below. Suppose the images of the local observables span their target spaces, and transport is monomial: \[ d_y(V(g)v)_{\pi_g(i)}=c(g,i)d_x(v)_i, \] with the usual composition laws for the permutations \(\pi_g\) and positive coefficients \(c(g,i)\). Positive weights make \(\sum_iw_x(i)d_x(v)_i\) natural exactly when \begin{equation}\label{eq:weighted-degree} w_y(\pi_g(i))c(g,i)=w_x(i). \end{equation} Apply Theorem \ref{thm:normalization} to the groupoid of pairs \((x,i)\): the criterion is \(c(g,i)=1\) for every automorphism fixing the local index. The spanning hypothesis gives necessity by comparing coefficients; sufficiency follows by substitution. The condition is therefore a condition on stabilizers of local indices. Homogeneous assertions can survive a nontrivial character. For example, simultaneous positive scaling preserves \(t_1\leq t_2\) and \(t_1+t_2\leq t_3\), but generally not \(t_1\leq1\). The comparison action on the complete assertion determines which numerical statements descend. Appendix \ref{app:discrepancy} quantifies the obstruction on a finite comparison diagram. \section{Arithmetic degree and a nonliftable self-equivalence} \label{sec:counterexample} \subsection{The degree character of a realified Frobenioid} For the arithmetic Frobenioids of \cite[Example 6.3 and Theorem 6.4]{FrdI}, arithmetic degree identifies the relevant realified Picard group with \(\RR\). An equivalence of realifications induces multiplication by a positive scalar. If it lifts to the unit-trivialized perfections, that scalar is positive rational; if it lifts to the original arithmetic Frobenioids, the scalar is \(1\). These are implications. They do not assert converses. The scalar is multiplicative under composition and invariant under natural isomorphism, hence gives the character used in Section \ref{sec:normalization}. In a realified model, the rational-function object is the real span of the principal divisors, as in \cite[Proposition 5.3]{FrdI}. The maps \begin{equation}\label{eq:real-scaling} S_\lambda(x,\alpha)=(x,\lambda\alpha),\qquad S_\lambda(n,f,\Delta,u)=(n,f,\lambda\Delta,\lambda u) \end{equation} are defined for \(\lambda>0\). They preserve \eqref{eq:model-arrow} and \eqref{eq:model-composition}, have inverse \(S_{\lambda^{-1}}\), and satisfy \(S_\lambda S_\nu=S_{\lambda\nu}\). They preserve the integer Frobenius degree but multiply arithmetic degree by \(\lambda\). Consequently, for the group of self-equivalences modulo natural isomorphism, the degree character is surjective and admits the section \(\lambda\mapsto[S_\lambda]\). A comparison system allowing all these self-equivalences cannot admit a single numerical normalization on its unmarked objects. Restricting to comparisons that lift to the original arithmetic Frobenioids removes this scalar obstruction, by the cited theorem. It may also impose further restrictions, as the next example shows. \subsection{A finite-dimensional calculation} \begin{proposition}\label{prop:atomic} Let \(r\geq1\), \(\Phi=\RR_{\geq0}^r\), and \(\delta_w(x)=\sum_iw_ix_i\), where \(w_i>0\). Put \(B=\ker\delta_w\subseteq\RR^r\). The additive monoid automorphisms of \(\Phi\) whose groupified extensions preserve \(B\) have the form \[ A(e_i)=s_ie_{\sigma(i)},\qquad w_{\sigma(i)}s_i=\lambda w_i \] for \(\sigma\in S_r\) and \(\lambda>0\). Their group is \(\RR_{>0}\times S_r\), with degree character the first projection. \end{proposition} \begin{proof} An additive monoid automorphism preserves the order defined by the cone. It is rationally homogeneous, and rational approximation together with monotonicity gives real homogeneity on each coordinate ray. Its real-linear extension and inverse preserve the cone, so it permutes extreme rays. This gives the monomial form. Preservation of \(\ker\delta_w\) says that the two nonzero linear forms \(\delta_wA\) and \(\delta_w\) have the same kernel, hence differ by a scalar; positivity makes that scalar positive. Evaluating on the basis gives the displayed equations. Conjugating by \(\operatorname{diag}(w_i)\) gives \(\lambda P_\sigma\), proving the group assertion. \end{proof} The proposition describes the structured divisor automorphisms used in the following example. With weights \(\log2,\log3\), a degree-preserving interchange already fails to preserve the rational coordinate lattice. An arithmetic realification also includes the archimedean coordinate and the principal-divisor relations. \subsection{The example over \texorpdfstring{\(\QQ\)}{Q}} Take the trivial Galois extension \(\widetilde F=F=\QQ\) in \cite[Example 6.3]{FrdI}, and choose the terminal skeleton of its base category. The global realified construction over a trivial Galois base also appears in \cite[Example 3.5(i)]{IUTI}. Let \[ V=\left(\bigoplus_p\RR e_p\right)\oplus\RR e_\infty, \qquad \Phi_{\RR}=\left(\bigoplus_p\RR_{\geq0}e_p\right)\oplus\RR_{\geq0}e_\infty. \] The sums have finite support. Choose the archimedean coordinate so that \begin{equation}\label{eq:rational-degree} \delta\left(\sum_px_pe_p+x_\infty e_\infty\right) =\sum_px_p\log p+x_\infty. \end{equation} The principal divisor of \(p\) is \(b_p=e_p-(\log p)e_\infty\). Thus Proposition 5.3 of \cite{FrdI} identifies the realified rational-function object with \begin{equation}\label{eq:principal-span} B_{\RR}=\operatorname{span}_{\RR}\{b_p:p\text{ prime}\}=\ker\delta. \end{equation} Indeed, a vector in the kernel equals \(\sum_px_pb_p\). No unit theorem is needed for this equality over \(\QQ\). \begin{theorem}[Degree preservation without a perfected lift]\label{thm:prime-swap} The realified arithmetic Frobenioid associated with \(\QQ/\QQ\) has a self-equivalence \(T\) with the following properties: \begin{enumerate} \item Its arithmetic degree character is \(1\). \item It induces the identity on object isomorphism classes and on \(\Pic\cong\RR\). \item It is not naturally isomorphic to the identity functor. \item It does not lift, even up to natural isomorphism, to the unit-trivialized perfection of the original arithmetic Frobenioid, and therefore does not lift to the original Frobenioid. \end{enumerate} On the chosen terminal-base model, \(T\) is an involutive automorphism. \end{theorem} \begin{proof} Define \(A:V\to V\) by \begin{equation}\label{eq:prime-swap} A(e_2)=\frac{\log2}{\log3}e_3, \qquad A(e_3)=\frac{\log3}{\log2}e_2, \end{equation} with \(A(e_p)=e_p\) for every \(p\neq2,3\), and \(A(e_\infty)=e_\infty\). This is a positive monomial involution. Equation \eqref{eq:rational-degree} gives \(\delta A=\delta\), and \eqref{eq:principal-span} gives \(A(B_{\RR})=B_{\RR}\). By Theorem \ref{thm:model-transport}, \[ T(\alpha)=A\alpha,\qquad T(n,\Delta,u)=(n,A\Delta,Au) \] is an involutive model automorphism; the unique base arrow has been omitted. This proves (i). Objects \(\alpha,\beta\in V\) are isomorphic precisely when \(\alpha-\beta\in B_{\RR}\). One direction uses the degree-one, zero-divisor arrow supplied by that difference. Conversely, an isomorphism and its inverse have positive integer degrees whose product is one; their nonnegative zero divisors have sum zero, so both divisors vanish. Thus object classes identify with \(V/B_{\RR}\cong\RR\). Since \(A\alpha-\alpha\in B_{\RR}\), (ii) follows. If two endofunctors of the terminal-base model are naturally isomorphic, every component of the natural isomorphism has degree one and divisor zero. Apply the divisor to the naturality square for any arrow. Formula \eqref{eq:model-composition} then forces the two image arrows to have the same zero divisor. The arrow \[ (1,e_2,0):0\longrightarrow e_2 \] has divisor \(e_2\), whereas its image under \(T\) has divisor \((\log2/\log3)e_3\). This proves (iii) and also shows that a natural isomorphism cannot remove the induced prime interchange. Finally, Theorem 6.4(iii) of \cite{FrdI} states that an equivalence induced from the unit-trivialized perfection preserves the place of \(\QQ\) lying below each prime. In the present example every place is already a place of \(\QQ\), so it must be fixed. The functor \(T\) interchanges the rays at \(2\) and \(3\), which contradicts that requirement. Since its divisor action is invariant under natural isomorphism, the contradiction also excludes a lift whose realification is only naturally isomorphic to \(T\). \end{proof} The same obstruction can be seen directly in the coefficient model. By \cite[Proposition 5.3]{FrdI}, the unit-trivialized perfection has divisor monoid \[ \left(\bigoplus_p\QQ_{\geq0}e_p\right)\oplus\RR_{\geq0}e_\infty. \] Let \(J\) be its canonical functor to the realified model. If a functor \(U\) satisfied \(JU\cong TJ\), naturality on the arrow \(a=(1,e_2,0):0\to e_2\) would give \[ \Div(JU(a))=\Div(TJ(a))=\frac{\log2}{\log3}e_3, \] because every component of the comparison isomorphism has degree one and divisor zero. The left side has rational coordinates at the finite primes. The right side does not: \(\log2/\log3\in\QQ\) would imply equality between positive powers of \(2\) and \(3\). This gives a second proof of nonliftability using the explicit realification map. The comparison groupoid in this example allows all equivalences of the underlying realified category. If the identification of its prime set with the places of \(\QQ\) is retained as fixed marking data, the displayed transposition is excluded. The example shows that the image of the arithmetically liftable equivalences is strictly smaller than the kernel of the degree character, even among functors acting trivially on object isomorphism classes. It therefore supplies a concrete distinction between numerical descent and preservation of the finer arithmetic structure. \section{Arithmetic reconstruction} \label{sec:arithmetic} We now identify the carriers and comparison data for the arithmetic constructions specified in Section \ref{sec:introduction}. The cardinal estimates in this section are made in ZFC, using the cited arithmetic and countability results. The formulas for structural transport have the bounded form developed above. Section \ref{sec:assembly} combines these two parts in a relative interpretation statement. \subsection{Arithmetic carrier bounds} \begin{lemma}\label{lem:continuum-operations} The carrier bound \(\cfr\) is preserved by subsets, representative quotients, finite and countable products, disjoint unions over at most \(\cfr\) summands of size at most \(\cfr\), and direct limits of such diagrams. It is also preserved by countable inverse limits, finite-word constructions, finite-support sums, algebraic closures of fields of size at most \(\cfr\), and metric completions. Continuous maps from a separable space to a Hausdorff space of size at most \(\cfr\) form a set of size at most \(\cfr\). \end{lemma} \begin{proof} Use \(\cfr^{\aleph_0}=\cfr\), \(\cfr\cdot\cfr=\cfr\), and finite tuple coding. Direct limits are quotients of disjoint unions; countable inverse limits are subsets of countable products. Algebraic closures adjoin at most \(\cfr\) algebraic elements, and completions use equivalence classes of Cauchy sequences. A continuous map into a Hausdorff space is determined by its values on a countable dense subset. \end{proof} \begin{proposition}[Arithmetic carrier bounds]\label{prop:arithmetic-size} For the initial data specified in Section \ref{sec:introduction}, each of the following specified arithmetic presentations has carriers of size at most \(\cfr\); the same bound holds for a jointly supplied family of these presentations indexed by a set of size at most \(\cfr\): \begin{enumerate} \item the fields, their relevant algebraic closures and completions, finite-type function fields, point sets, and finite-support divisor groups; \item the arithmetic fundamental groups of the fixed finite-puncture curves used in the reconstruction, and the Galois-countable tempered groups in the stated setting; \item the cyclotomic coefficient objects, the displayed low-degree continuous cochain and cohomology groups, Kummer images, normalized valuations, and evaluation data; \item the specified direct limits over finite extensions and finite sets of punctures; \item the number-field, local, tempered, and angular Frobenioid presentations listed below, provided any additional base category is itself supplied with this bound. \end{enumerate} This is a carrier bound for the displayed objects, not for every ambient full function space or every set of candidate substructures. \end{proposition} \begin{proof} Number fields and their algebraic closures are countable. Finite extensions of \(\QQ_p\), their algebraic closures, and their completions have size at most \(\cfr\). Finite algebraic data code the function fields and finite-type coordinate objects. A second-countable Hausdorff space embeds into \(\mathcal P(\NN)\) by recording membership in a numbered basis. The relevant profinite groups have countable bases. For number fields, finite extensions are specified by countably many polynomials. For local fields, finite extensions can be controlled by polynomial approximations over a countable dense subfield and Krasner's lemma. For a fixed finite-puncture curve, the topological finite generation of the geometric fundamental group and the countably based arithmetic quotient give the same countability; this setting is recorded in \cite[Remark 2.5.3(ii)(E2)]{IUTI}. The tempered case uses the stated Galois-countability assumptions and \cite[item (12)]{FrdIIComments}, rather than an assertion about arbitrary tempered groups. In the Galois-countable presentation, choose a decreasing cofinal sequence \(N_n\) of open normal subgroups, with countable discrete quotients \(G/N_n\). Then \(G\) embeds in their countable product. Countable continuous actions can be presented on subsets of \(\NN\); their action maps are determined by values on a countable dense subgroup. Every point of such an action receives an equivariant map from some \(G/N_n\). Naturality therefore determines a fiber-functor automorphism from its components on this covering family, giving an injection into \[ \prod_n\operatorname{Sym}(G/N_n), \] which has size at most \(\cfr\). This bounds the group reconstructed from the covering category, not just the initial group presentation. Finite-degree continuous cochains are bounded by Lemma \ref{lem:continuum-operations}, and kernels, images, and cohomology quotients preserve the bound. The profinite coefficient objects are represented by countable finite layers. Valuation and evaluation families are relations indexed by the relevant points. A local-field curve can have \(\cfr\) closed points, so the finite-puncture index family need not be countable; the direct limits still have size at most \(\cfr\). Constructing addition adds a ternary relation to an existing carrier. For number-field arithmetic Frobenioids, \cite[Example 6.3]{FrdI} uses countably many finite places and finitely many archimedean places on each finite extension; finite-support divisor data have the required bound. The local construction in \cite[Example 1.1]{FrdII} uses subobjects of the local multiplicative and valuation data, again with that bound. The model formulas in Section \ref{sec:frobenioids} then use finite tuples only. For the tempered Frobenioid in \cite[Section 3]{EtTh}, the universal combinatorial covering has countable graph coordinates. The divisor coordinates in Proposition 3.2(i) are countable. Integer divisors embed in \(\ZZ^{\NN}\), their perfections embed in \(\QQ^{\NN}\), and their realifications embed in \(\RR^{\NN}\). Only these injections are needed. In particular, perfection is not interchanged with an infinite product: rational coordinates in the perfection of an integral product have a common denominator. Definition 3.3 uses the specified countable filters. We use the March 2022 corrections: log-meromorphic functions satisfy the stated tempered root-extraction condition, and uniqueness of the closure subgroup is distinguished from uniqueness of its representing filtration index \cite[items (i), (xvi), and (xl)]{EtThComments}. The stronger function condition selects a subclass of the original bounded carrier. Proposition 3.4(ii) identifies the kernel of the rational-function-to-divisor map with \(\mathcal O_L^\times\); its image and kernel have size at most \(\cfr\), so its source does also. Definition 3.6(ii) and Theorem 3.7(i) give the relevant model construction and its isotropic and model properties. For angular presentations, one-dimensional coordinate lines over \(\RR\) or \(\CC\), angular regions, positive radii, and scalar arrows admit \(\cfr\)-sized parameter sets. The complex angular subsets are open connected subsets of the circle, of which there are at most \(\cfr\). Only the finite archimedean base data and their continuous embeddings occur. Taking frames over each exact object of the supplied base gives the same bound after base change, by Proposition \ref{prop:angular}. \end{proof} The fibers of connected covers are nonempty transitive group sets, so equivariant transition maps between them are surjective. On a countable cofinal tower, a chosen point lifts recursively at every stage. The state space consists of the supplied fiber elements, so Theorem \ref{thm:bounded-recursion} gives a bounded compatible family. Countability alone would not establish this for a tower with arbitrary nonsurjective transition maps. Equivalently, the indiscrete groupoids of the fibers have isofibrational bonding maps, and Theorem \ref{thm:tower} applies. The tempered divisor argument uses countable coordinate spaces, not finite support. Conversely, the number-field divisor argument uses finite support. These are separate reasons for the same cardinal bound. \begin{proposition}[The birational Galois group]\label{prop:large-galois} The full absolute Galois group of \(\QQ_p(t)\) has cardinality \(2^{\cfr}\). \end{proposition} \begin{proof} The classes of \(t-a\), \(a\in\QQ_p\), are independent in \(\QQ_p(t)^\times/(\QQ_p(t)^\times)^2\). A valuation at \(t=a\) detects the corresponding exponent in any finite product. Therefore the multiquadratic extension obtained by adjoining all \(\sqrt{t-a}\) has Galois group \[ (\ZZ/2)^{\QQ_p}. \] It is a quotient of the absolute Galois group, proving the lower bound. An algebraic closure of \(\QQ_p(t)\) has size \(\cfr\), and its automorphism group has size at most \(\cfr^{\cfr}=2^{\cfr}\), proving the upper bound. \end{proof} Thus a passage from fixed finite-puncture fundamental groups to the unrestricted birational Galois group is a genuine increase in carrier size. It cannot be treated as a countable inverse limit without further justification. Presenting the algebraic closure on \(\BB\) codes each automorphism by a member of \(\Code_1\), so the full group has carrier in \(\Code_1\) and operation tables in \(\Code_2\). Its topology may be specified by the bounded stabilizer basis. This particular increase is therefore accommodated by the displayed finite levels, although the full set of all open subsets would require separate type accounting. \subsection{Basepoint transport and continuous cohomology} Let \(p:\omega_b\Rightarrow\omega_c\) be an isomorphism of fiber functors. It induces \[ \phi_p:\Aut(\omega_b)\longrightarrow\Aut(\omega_c), \qquad a\longmapsto pap^{-1}. \] For \(p'=hp\), one has \(\phi_{p'}=c_h\phi_p\), while at every covering object \(Y\), \(p'_Y=h_Yp_Y\). Path composition gives \(\phi_{qp}=\phi_q\phi_p\). A change of algebraic-closure identification similarly acts by a Galois automorphism and reindexes subgroups by \(H\mapsto hHh^{-1}\). The full arithmetic family retains these actions and reindexings. It is not obtained by declaring inner automorphisms to be literal identities on the algebraic closure. \begin{lemma}[Inner transport with coefficients]\label{lem:inner-cohomology} Let \(G\) be a topological group and \(M\) a topological abelian \(G\)-module. Simultaneous inner conjugation on \(G\) and the corresponding action on \(M\) induces the identity on the cohomology of continuous homogeneous cochains. \end{lemma} \begin{proof} For continuous equivariant cochains \(F:G^{n+1}\to M\), simultaneous transport is \[ (T_gF)(h_0,\ldots,h_n) =gF(g^{-1}h_0g,\ldots,g^{-1}h_ng) =F(h_0g,\ldots,h_ng). \] For \(n\geq1\), set \begin{align*} (K_gF)(h_0,\ldots,h_{n-1}) ={}&\sum_{i=0}^{n-1}(-1)^i F(h_0,\ldots,h_i,h_ig,h_{i+1}g,\ldots,h_{n-1}g). \end{align*} Each term is continuous and equivariant. With the alternating deletion differential, the internal faces cancel in pairs, leaving \[ dK_g+K_gd=T_g-\id. \] In degree zero this reads \(K_g(dF)(h_0)=F(h_0g)-F(h_0)\). Hence the induced cohomology action is the identity. \end{proof} For a topological group isomorphism \(\phi:G\to H\) and compatible coefficient isomorphism \(u:M\to N\), transport is explicitly \[ F\longmapsto\bigl[(h_0,\ldots,h_n)\mapsto uF(\phi^{-1}h_0,\ldots,\phi^{-1}h_n)\bigr]. \] It preserves composition and compatible coefficient pairings, hence cup products. Restriction is natural. For transfer from a finite-index open subgroup, transporting a finite set of coset representatives gives the same formula on the target, and changing representatives gives the same cohomology map. Kummer maps are compared with their roots-of-unity coefficients transported as well. The homotopy does not justify omitting this coefficient transport. Where profinite coefficients are presented by finite layers, the formulas are compatible with those layer maps. \subsection{Index normalization} \begin{lemma}\label{lem:index-normalization} Let \(M_i\) be \(\widehat{\ZZ}\)-modules on which multiplication by every positive integer is injective. Suppose linear maps \(f_{ji}:M_i\to M_j\) and positive integers \(d_{ji}\) satisfy \[ f_{ji}(M_i)\subseteq d_{ji}M_j. \] There is a unique linear map \(n_{ji}\) with \(d_{ji}n_{ji}=f_{ji}\). If \[ f_{ki}=f_{kj}f_{ji},\qquad d_{ki}=d_{kj}d_{ji}, \] then \(n_{ki}=n_{kj}n_{ji}\). \end{lemma} \begin{proof} The image condition gives existence pointwise; injectivity gives uniqueness and linearity. Multiplying the asserted composition identity by \(d_{ki}\), using linearity and the two hypotheses, gives \(f_{ki}\) on both sides. Injectivity proves equality. \end{proof} Remark 1.10.1 of \cite{AbsTopIII} specifies normalization by the geometric subgroup index for the geometric cyclotome, and by the base Galois subgroup index for the \(H^2\)-identification. The required divisibility is part of that arithmetic compatibility input. Lemma \ref{lem:index-normalization} supplies uniqueness and the composition law once this input is available. It neither treats \(1/d\) as an element of \(\widehat{\ZZ}\) nor applies such division indiscriminately to all transfer maps. \subsection{Addition, valuations, and numerical markings} Proposition 1.3 of \cite{AbsTopIII} reconstructs addition functorially from triples arising from proper hyperbolic curves over algebraically closed fields: \[ \left(K^\times,\{v_x:K^\times\twoheadrightarrow\ZZ\}_x, \{U_x=\{f:f(x)=1\}\}_x\right). \] An isomorphism preserving this triple transports the reconstructed addition to the one prescribed by the same algorithm on the target. The valuation maps, including their generators, are required data; retaining only their kernels does not meet the hypothesis, as Remark 1.3.1 emphasizes. The subsequent local-field reconstruction uses the continuity and evaluation compatibilities stated in Corollary 1.10. These are arithmetic recognition inputs, not consequences of abstract equivalence of arbitrary categories. If Haar measure on a locally compact group enters a comparison, the normalization is similarly explicit. For a topological group isomorphism carrying a normalization region \(\Lambda\) to \(\Lambda'\), the conditions \[ 0<\mu(\Lambda)=\mu'(\Lambda')<\infty \] identify the pushed-forward Haar measure by uniqueness. An unmarked Haar-measure ray determines no such equality of numbers. A bound for the data used in the argument need only encode the measurable regions and values actually used; the full completed measure graph can occupy a higher code level. A supplied degree or volume comparison must also preserve the relevant global weights, as Section \ref{sec:normalization} explains. \section{A relative uniform interpretation theorem} \label{sec:assembly} \begin{definition}[Bounded reconstruction data]\label{def:specification} Bounded reconstruction data consist of: \begin{enumerate} \item jointly supplied initial presentations, parameter carriers, and state-code sorts in a fixed finite list \(A_0,\ldots,A_h\), together with a supplied run-index well-order \((I,<)\) or one uniformly bounded family of such index orders; \item uniformly supplied constructor rules, including any limit-stage rules, satisfying totality and closure in the declared state sorts; \item changes of presentation given by equivalence functors and invertible comparison natural transformations, preserving the declared structural data and satisfying the specified unit and composition coherence equations; any additional noninvertible arithmetic arrows are supplied separately, with the functoriality asserted for them; \item for strict categorical assembly, an expression using iterated pullbacks with a specified isofibrational leg at every step in each compared presentation, fiberwise full skeletons or full subcategories vertically essentially surjective in every exact fiber, and countable towers with isofibrational bonding maps; \item for each quotient, the specified invariant data, and for each numerical observable, its transformation law under the permitted comparisons. \end{enumerate} All indexed families and all selectors occur as single bounded sets of graphs. A claimed arithmetic identification is included as a separate recognition assertion with its stated hypotheses and arrow class. Output equivalences under a change of presentation use the equivalence and invertibility conditions in (iii), as in Propositions \ref{prop:spans} and \ref{prop:tower-equivalence}. \end{definition} The hypotheses are verified separately for each constructor. For example, the model Frobenioid constructor has the equations \eqref{eq:model-arrow}--\eqref{eq:model-composition}; its comparison rule is Theorem \ref{thm:model-transport}; its strict base-change property follows from the displayed cartesian lift. An anabelian addition constructor requires the valuation and evaluation triple just stated and invokes the particular arithmetic recognition theorem for it. \begin{theorem}[Bounded coherent assembly]\label{thm:assembly} For each fixed collection of bounded reconstruction data, the following implications are provable in \(\MC\). \begin{enumerate} \item Every permitted run and its comparison data have one fixed set bound. Under the level hypotheses of Theorem \ref{thm:fixed-level}, the complete family of runs has a membership-table code at the stated level; iteration itself adds no new level. \item Representative quotients, ordinary skeletal comparison, fiberwise full skeletons, and the specified strict base changes and towers admit the comparison maps constructed above. The categorical comparison equivalences are fully faithful and transport the declared structural functors and comparison cells. Representative quotients preserve precisely the specified quotient-invariant data. \item A nonzero observable transforming by a positive character admits compatible objectwise normalization exactly when that character is trivial on isotropy. Retaining normalization as additional data gives the universal refinement \(\mathcal G^\chi\). Its object and arrow carriers have codes in the same supplied carrier \(K\) whenever an injection \(K\times\RR_{>0}\to K\) is supplied; its structure tables use the corresponding fixed relation-table level. The carriers \(A_r\) for \(r\geq1\) have such injections. \end{enumerate} \end{theorem} \begin{proof} Theorem \ref{thm:bounded-recursion} and Corollary \ref{cor:uniform-parameters} construct the runs. For a uniformly supplied family of index orders, the same partial-solution construction uses the parameter-dependent initial-segment predicate on the common total index carrier. Theorem \ref{thm:fixed-level} gives the compressed code statement. Proposition \ref{prop:quotient}, formula \eqref{eq:skeleton-coherence}, Proposition \ref{prop:fiberwise-skeleton}, Theorem \ref{thm:pullback}, Proposition \ref{prop:spans}, and Theorem \ref{thm:tower} give the successive comparisons. Their defining formulas are bounded, and the retained comparison maps supply the stated coherence. Part (iii) is Theorems \ref{thm:normalization}--\ref{thm:refinement}. \end{proof} \begin{corollary}[Relative arithmetic interpretation]\label{cor:arithmetic-interpretation} Suppose bounded reconstruction data are realized by the arithmetic presentations under examination, and the specified arithmetic recognition assertions hold. Then these presentations identify with the structures recognized by those assertions, compatibly with their allowed comparisons and retained markings. \end{corollary} \begin{proof} Apply the recognition assertions to the bounded data and compose their stated comparisons with the structural comparisons of Theorem \ref{thm:assembly}. \end{proof} The corollary is a semantic consequence in ordinary mathematics. An internal version over \(\MC\) uses the recognition assertions as formulas and hypotheses in the same coded language. The fixed data in Definition \ref{def:specification} give a theorem schema; no uniform truth predicate for an external list of arithmetic theorems is involved. For the constructions examined here, Proposition \ref{prop:arithmetic-size} supplies the basic carrier bounds. Corollary \ref{cor:bounded-models} gives bounded presentations and comparisons for the model and angular constructions. Basepoint change, coefficient transport, and index normalization are governed by the explicit formulas in Section \ref{sec:arithmetic}. Arithmetic recognition identifies the resulting presentations with the fields, cyclotomes, and Frobenioids described in the cited theorems. The examples show why the hypotheses on comparison and descent are needed. A small groupoid may carry a nontrivial scale character; a tower of equivalences may have an empty strict limit; a degree-preserving realified equivalence may fail to lift to the unit-trivialized perfection. The categorical comparison equivalences preserve automorphism groups and supply the comparison cells used to transport the declared data. Interpreting an entire arithmetic proof in \(\MC\) also requires proofs in that theory of the existence, totality, and recognition assertions for each arithmetic constructor. The present results establish the bounded structural constructions and their comparisons. The arithmetic example shows that a size bound and a preserved numerical invariant can still leave an obstruction to arithmetic liftability. \appendix \section{Finite comparison diagrams}\label{app:discrepancy} If \(g:x\to x\) has \(\chi(g)\neq1\), then every objectwise rescaling leaves \begin{equation}\label{eq:loop-drift} \left|\log\chi(g^n)\right|=n\left|\log\chi(g)\right| \end{equation} unchanged. Thus no finite multiplicative distortion bound can hold over all iterated traversals of that loop. This is a statement about accumulated scale discrepancy; it does not assert that a finite collection of one-step comparisons has unbounded error. \begin{proposition}[Finite-diagram discrepancy]\label{prop:minimax} Let a finite connected directed multigraph have real edge labels \(a_e\); reversing an edge reverses the sign. Then \begin{equation}\label{eq:minimax} \min_{u}\max_e\left|a_e+u_{t(e)}-u_{s(e)}\right| =\max_C\frac{|a(C)|}{|C|}, \end{equation} where \(C\) runs over simple cycles in the underlying multigraph, with signs according to traversal. Loops and cycles formed by parallel edges are included. Empty maxima in this nonnegative optimization problem are interpreted as zero; in particular, the right side is zero for a forest. \end{proposition} \begin{proof} Summing residuals around a cycle cancels the vertex potentials and proves the lower bound. Let \(\eta\) be the right side. The inequalities for the upper bound are \[ u_{t(e)}-u_{s(e)}\leq\eta-a_e,\qquad u_{s(e)}-u_{t(e)}\leq\eta+a_e. \] Give the two orientations these weights. Every directed closed walk decomposes into simple cycles and reverse-edge pairs. The former have nonnegative weight by the definition of \(\eta\), and the latter have weight \(2\eta\). Hence there are no negative cycles. Add a source with zero-weight arrows to all vertices; shortest-path distances can be attained among the finitely many simple paths, and satisfy the inequalities. They give a minimizing potential. \end{proof} This is a standard difference-constraint argument related to cycle-mean optimization \cite{Karp}; the proof is included to specify exactly the norm and the cycles involved. For a triangle with oriented labels \(0,0,\log2\), the optimum is \((\log2)/3\), while repeated traversal has discrepancy \(n\log2\). \section{A coarse ZFC envelope} \label{app:envelope} For comparison with the finite-level method, there is a useful larger envelope available in ZFC alone. Set \[ \kappa=\beth_{\omega_1},\qquad H_\kappa=\{x:|\operatorname{TC}(\{x\})|<\kappa\}. \] \begin{proposition}\label{prop:envelope} In ZFC, \(\kappa\) is a strong limit of cofinality \(\omega_1\), and \(|H_\kappa|=\kappa\). The class \(H_\kappa\) is a set closed under finite set constructions, powersets, function sets, representative quotients, full functor categories of its small categories, and externally supplied \(\NN\)-indexed families of its members and their products. Limits and colimits stay in it whenever the entire supplied diagram belongs to it. For fixed \(C\in H_\kappa\) and fixed ordinal \(\lambda<\kappa\), the pro- and ind-presentations of \(C\) indexed by categories with object and arrow carriers contained in \(\lambda\) also form categories in \(H_\kappa\). \end{proposition} \begin{proof} If \(\mu<\kappa\), choose \(\alpha<\omega_1\) with \(\mu\leq\beth_\alpha\); then \(2^\mu\leq\beth_{\alpha+1}<\kappa\). The beth sequence is cofinal, and any countable collection of its indices is bounded below \(\omega_1\), proving the cofinality assertion. Pointed well-founded extensional relations on ordinal carriers \(\mu<\kappa\) give at most \(\sum_{\mu<\kappa}\mu\cdot 2^{|\mu|^2}=\kappa\) codes. Mostowski collapse and Replacement collect their decoded sets, yielding \(|H_\kappa|\leq\kappa\). The ordinals below \(\kappa\) give the reverse bound. Finitely many hereditary sizes below \(\kappa\) have a common infinite bound \(\mu\); the displayed powerset and function constructions have hereditary size at most \(2^\mu<\kappa\). For a countable family, cofinality supplies one such common \(\mu\), and \(\mu^{\aleph_0}\leq2^\mu\). A whole diagram in \(H_\kappa\) already has a common hereditary bound on its index, values, and arrows, so the product/equalizer and sum/quotient descriptions apply. Functors and natural transformations are bounded function graphs. For pro-presentations, fix an index-carrier bound \(\lambda<\kappa\) in advance, for both objects and arrows. Put \(\nu=\max(\aleph_0,|\lambda|,|\operatorname{TC}(\{C\})|)\). There are at most \(2^\nu\) codes for index categories on subsets of \(\lambda\) and their diagrams in \(C\). In the Hom formula \[ \Hom_{\operatorname{Pro}(C)}(X,Y) =\lim_{\longleftarrow\,j}\lim_{\longrightarrow\,i}\Hom_C(X_i,Y_j) \] each inner colimit has size at most \(\nu\), and the outer limit has size at most \(\nu^{|\lambda|}\leq2^\nu\). The complete object and arrow sets, with their composition graphs, consequently have a common hereditary bound below \(\kappa\). The ind case is dual. \end{proof} This envelope is not a Grothendieck universe. Each \(\beth_\alpha\), \(\alpha<\omega_1\), belongs to \(H_\kappa\), and so does the index set \(\omega_1\), but the full family has hereditary size \(\kappa\) and does not belong to \(H_\kappa\). Thus pointwise membership of an arbitrarily indexed family is insufficient. Likewise, the proposition fixes \(\lambda\) for pro-objects; it does not put all diagrams of all index sizes below \(\kappa\) into one member of \(H_\kappa\). This construction uses ZFC beth recursion and no inaccessible-cardinal axiom. It bounds the listed operations even when they raise finite code levels. The proof of the \(\MC\) theorem instead uses the fixed bounds of Section \ref{sec:foundation}; unrestricted powerset iteration remains outside that fixed-level argument. \bibliographystyle{plain} \bibliography{references} \end{document}