The Number Builder: Enclosure Sequences in the Laws of Form Calculus as a Constructive Route to Computable Reals

#1. Introduction

The foundations of real analysis standardly rest on either set-theoretic objects (Dedekind cuts over the full power set of $\mathbb{Q}$) or machine-theoretic ones (Turing machines, Type-Two computability). Both groundings import apparatus far heavier than what the working content of analysis seems to require. Spencer-Brown's Laws of Form (LoF) offers a third candidate: a minimal calculus whose sole primitive is the mark — a distinction — and whose distinctive expressive device is re-entry, the appearance of a form inside its own space.

The conjecture investigated here is that re-entry alone suffices to construct every computable real, via a finite program we call a Number Builder: a finite LoF expression schema such that iterating its re-entry step produces a nested sequence of enclosures — rational intervals — whose widths shrink by a computable schedule and whose intersection is exactly the target real.

This program matters for three reasons. First, it would ground computable analysis in a calculus with fewer primitives than a universal machine: distinction, nesting, and re-entry. Second, it aligns with the position argued in the QNFO corpus [9], [10], [11] that the "breadth" of the non-computable reals is physically and mathematically vacuous, and that all substantive content of the continuum lives in the computable ("deep") reals; a builder that generates exactly the computable reals makes that thesis constructive rather than merely critical. Third, it yields a concrete formalization target: the theorems stated in Section 3 are of a shape that a proof assistant can adjudicate.

We are explicit about epistemic status throughout. What is proved here: the enclosure semantics (Proposition 1), closure under arithmetic with width propagation (Proposition 2), and the worked enclosures of $e$ and $\pi$ with every arithmetic step shown. What is conjectural: that every Type-Two computable real admits a Number Builder, and the completed proof-assistant formalization. Section 6 states falsification conditions precisely.

#2. Background and Related Work

We discuss all eleven works of the provided bibliography, in its order and numbering. Several are far afield of our topic; we cite them honestly, for what they genuinely contribute, and flag thin connections where they are thin.

[3] gives a constructive proof of the uncountability of the reals that relies on order completeness rather than sequential completeness, uses neither the axiom of choice nor excluded middle, and applies to the MacNeille reals. This is the closest methodological relative of our program: our enclosure sequences are exactly nested, order-theoretic objects, and the LoF builder grounds the reals in their order structure (nested rational intervals) rather than in Cauchy sequences. The constructive status of [3] shows that order-completeness arguments can be carried out without classical apparatus, the ambient logic in which a LoF-based builder naturally lives.

[8] develops exact real number computation extracted from proofs in constructive type theory, with an axiomatization of the reals designed so that correctness proofs abstract away from representation subtleties. This is the direct technical bridge for our formalization test: our Section 3 program — define enclosure sequences, prove enclosure uniqueness and closure — is precisely the kind of development [8] envisages, and our Proposition 2 is the enclosure-based analogue of the exact-arithmetic operation correctness proved there. A Lean/Coq implementation of the Number Builder would be an instance of proof extraction in their sense.

[9] (The Computable Continuum: Depth Without Breadth) argues that the uncountability of the reals conflates Archimedean completeness ("depth") with set-theoretic cardinality explosion ("breadth"), and that all physically relevant properties are preserved by the computable reals. Our conjecture supplies the constructive complement to this critical claim: if every computable real arises from a finite Number Builder, then the computable fragment is not merely a subfield that happens to suffice, but a generated, finitely specified structure. Each re-entry step adds one unit of convergent depth and no breadth at all.

[10] (Depth, Breadth, and Valuation) extends the framework with a third axis, valuation, treating $p$-adic completions as information carriers alongside depth and breadth. For our purposes it supplies the ontological framing in which a mark-based builder is natural: distinctions as the primitive from which both real and $p$-adic structure is built. We do not pursue the $p$-adic axis here (see Section 6).

[11] (The ℚ-vs-ℝ Question) argues that physical law requires only the rational numbers. Taken literally this is stronger than our target — we retain the computable reals as ideal limits of rational enclosures — but it motivates our insistence that every builder step operate on rationals and produce rational bounds, so that the entire apparatus is executable over $\mathbb{Q}$ with the reals appearing only as intersections.

[1] constructs the realisations and integral structures of the adjoint motive of a newform and verifies part of the Tamagawa number conjecture by the Taylor–Wiles method. The connection is illustrative rather than methodological: the arithmetic quantities at stake (periods, $L$-values) are, when real, computable reals, and hence in principle targets for a Number Builder; the conjecture-driven character of [1] also parallels our conjecture-first presentation.

[5] proves the local Tamagawa number conjecture for Tate motives over tamely ramified fields using $(\varphi,\Gamma_K)$-modules and a reciprocity law. As with [1], the real constants governed by such conjectures fall within the computable fragment our builder is designed to generate.

[7] proves the weak local Tamagawa number conjecture for Hecke characters in the remaining non-critical cases, under restrictions from Iwasawa theory of imaginary quadratic fields. Together with [1] and [5] it establishes that the frontier of arithmetic conjectures concerns structured, computable real and $p$-adic quantities — the population our builder would cover.

[2] gives a short, direct proof of Chvátal's conjecture on intersecting families in downsets, subsuming Kleitman's and a version of Kahn's conjecture. We cite it as a model of a structural generation result: a maximal object shown to be forced by the axioms of the setting. Our Proposition 1 has the same shape — the enclosure is forced to a unique limit by the builder's contraction rule — and [2] exemplifies the outcome we hope for: a long-standing conjecture resolving cleanly once the right framework is found.

[4] surveys the Caccetta–Hággkvist conjecture and Hamidoune's additive-number-theoretic attacks on it for Cayley and vertex-transitive graphs. It illustrates the other epistemic path: decades of partial results for restricted classes without full resolution — the risk our program runs if the re-entry formalization proves too weak for general computable reals.

[6] proves congruences for harmonic numbers $H_n = \sum_{k=1}^{n} 1/k$ modulo $p^2$, confirming a conjecture of Z.-W. Sun. It is a reminder that finite, exactly computable rational arithmetic — the substrate of our builders — already supports nontrivial number-theoretic content, and that conjecture-then-proof is a productive cycle at the rational level our builder inhabits.

We note candidly that [1], [2], [4], [5], [6], [7] are cited for framing and analogy, not for technical dependence; the load-bearing relatives of this paper are [3], [8], [9], [10], and [11]. No prior work we are aware of connects the LoF re-entry calculus to computable analysis; the Number Builder conjecture appears to be new.

#3. Methods

#3.1 The LoF calculus and re-entry

The Laws of Form calculus has one primitive operation, the mark (a distinction drawing an inside and an outside), and two rules: calling (a doubled mark cancels) and crossing (a mark under which nothing stands annihilates what it encloses). Expressions are nested containers. The distinctive LoF device is re-entry: an expression may contain a marker standing for itself, so that unfolding the expression regenerates it. A re-entrant form is not a fixed finite string but a rule for unfolding: each act of re-entry produces one more level of nesting. We write a re-entry form as $r_E$ for an expression $E$ containing a re-entry marker.

#3.2 Enclosure sequences

Definition 3.1 (Enclosure sequence). An enclosure sequence is a pair $(E_0, \sigma)$ where $E_0$ is a finite LoF expression with a distinguished re-entry marker and $\sigma$ is a computable step function; the $n$-th iterate $E_n$ is obtained by applying $\sigma$ to the re-entry marker of $E_{n-1}$, appending one nested enclosure.

Definition 3.2 (Interpretation). The interpretation map $I$ sends each $E_n$ to a rational interval $I(E_n) = [a_n, b_n]$ with $a_n \leq b_n$, $a_n, b_n \in \mathbb{Q}$, such that the nesting condition $I(E_{n+1}) \subseteq I(E_n)$ holds. The builder converges to $x \in \mathbb{R}$ if $\bigcap_n I(E_n) = \{x\}$, and has computable error bounds if the width function $w_n = b_n - a_n$ admits a computable $\rho: \mathbb{N} \to \mathbb{Q}_{\gt 0}$ with $w_n \leq \rho(n)$ and $\rho(n) \to 0$.

Definition 3.3 (Number Builder). A Number Builder for a real $x$ is a finite specification $(E_0, \sigma, I)$ whose enclosure sequence converges to $x$ with computable error bounds.

The finite expression is the program; the infinite unfolding is its execution. This is the LoF analogue of a Turing machine: finite description, potentially infinite operation, and the output at stage $n$ is not a digit string but a bracket on the answer — a two-sided error bound, exactly the shape of output in exact real arithmetic [8].

#3.3 Canonical re-entry schedules

Two schedules are used in this paper.

Halving re-entry. Given an enclosure $[a_n, b_n]$ and the rational midpoint $m_n = (a_n + b_n)/2$, the step emits the half selected by a computable predicate $P$ (e.g., "$x \lt m_n$", decidable on rationals for any computable $x$ given as a Cauchy name):

with width $w_{n+1} = w_n / 2$.

Series re-entry. The step appends the next rational term $t_k$ of a convergent series with a proven tail bound $R_n$: the enclosure at stage $n$ is $[S_n, S_n + R_n]$ where $S_n = \sum_{k=0}^{n} t_k$ and $R_n \geq \sum_{k \gt n} |t_k|$ is a computable rational overestimate of the tail. For alternating series with decreasing magnitudes, the remainder theorem gives the tighter two-sided form used in Section 4.3: the true sum lies between consecutive partial sums, with error at most the first omitted term.

Both schedules are finite LoF expressions with re-entry: the halving re-entry re-enters on the predicate; the series re-entry re-enters on the summation index.

#3.4 Propositions

Proposition 1 (Unique limit with explicit rate). Let $(a_n, b_n)$ be an enclosure sequence with $w_n \to 0$. Then there is a unique real $x \in \bigcap_n [a_n, b_n]$, and for every $n$,

Proof. Nestedness gives $a_n \leq a_{n+1} \leq b_{n+1} \leq b_n$, so $(a_n)$ is monotone nondecreasing and bounded above by every $b_m$; by order completeness of $\mathbb{R}$ (constructively, by regularity of the interval family in the sense of [3]) $a_n \to a$ and $b_n \to b$ with $a \leq b$. Since $b - a \leq b_n - a_n = w_n$ for all $n$ and $w_n \to 0$, we get $a = b =: x$. For any $n$, $x \in [a_n, b_n]$ gives $|x - a_n| \leq b_n - a_n = w_n$, and identically for $b_n$. $\blacksquare$

Proposition 2 (Closure under arithmetic). Let $x, y$ have enclosure sequences with widths $w^{(x)}_n, w^{(y)}_n$. Then:

with $w^{(xy)}_n \leq c^{(x)}_n\, w^{(y)}_n + c^{(y)}_n\, w^{(x)}_n + w^{(x)}_n w^{(y)}_n$, where $c^{(x)}_n = \max(|a^{(x)}_n|, |b^{(x)}_n|)$ and similarly for $y$. Reciprocal: if $0 \notin [a^{(x)}_n, b^{(x)}_n]$ for all $n$, then (for a positive interval) $[1/b^{(x)}_n,\, 1/a^{(x)}_n]$ encloses $1/x$ with width $w^{(1/x)}_n = w^{(x)}_n / (a^{(x)}_n b^{(x)}_n)$.

Proof sketch. Addition: for $x \in [a^{(x)}_n, b^{(x)}_n]$ and $y \in [a^{(y)}_n, b^{(y)}_n]$, $x + y \in [a^{(x)}_n + a^{(y)}_n,\, b^{(x)}_n + b^{(y)}_n]$ and the width is the sum. Multiplication: $xy$ is monotone in each factor on intervals of fixed sign, so it lies between the min and max of the four corner products; the width bound follows from $|xy - a^{(x)}_n a^{(y)}_n| \leq |x|\,|y - a^{(y)}_n| + |a^{(y)}_n|\,|x - a^{(x)}_n| + |x - a^{(x)}_n|\,|y - a^{(y)}_n|$ and $|x| \leq c^{(x)}_n$. Reciprocal: $1/t$ is decreasing on a positive interval, so $1/x \in [1/b^{(x)}_n, 1/a^{(x)}_n]$, with width $1/a^{(x)}_n - 1/b^{(x)}_n = (b^{(x)}_n - a^{(x)}_n)/(a^{(x)}_n b^{(x)}_n)$. $\blacksquare$

Since $w_n \to 0$ for both inputs, all three operation widths also tend to $0$, so the outputs are again enclosure sequences of unique reals. This is the enclosure-calculus version of exact-arithmetic correctness [8].

#3.5 The conjecture and its component theorems

Conjecture (Number Builder Conjecture). Every computable real admits a Number Builder.

This decomposes into three target theorems, stated as goals for a proof-assistant formalization (Lean or Coq), not as results proven in this paper:

• T1 (Unique enclosure). Each Number Builder encloses a unique real within computable error bounds. Proposition 1 establishes this at the level of enclosure sequences; the open part is that every well-formed re-entry expression denotes such a sequence.
• T2 (Arithmetic closure). If $x$ and $y$ have Number Builders with known contraction schedules, then $x+y$, $x-y$, $xy$, and (where $y \neq 0$) $x/y$ have Number Builders obtained by composing the step functions, with computable schedules. Proposition 2 establishes the interval-arithmetic core.
• T3 (Type-Two equivalence). A real admits a Number Builder if and only if it is Type-Two computable (there is a machine mapping $1^k$ to a rational within $2^{-k}$ of $x$). The forward direction is immediate from Definition 3.3: output $a_n$ at precision demand $k$ once $\rho(n) \leq 2^{-k+1}$. The reverse direction — that every Type-Two computable real can be re-expressed as a re-entry form — is the substantive half and the core of the conjecture.

#3.6 Formalization plan

The proof-assistant test proceeds in three stages: (1) define enclosure sequences as a dependent record (endpoints as rationals, nestedness and width-decay as hypotheses) and mechanize Propositions 1–2; (2) define the re-entry syntax as an inductive type of LoF expressions with a self-reference constructor, and prove that every well-formed re-entry expression denotes an enclosure sequence; (3) prove T3 by transporting Cauchy names through the width schedule. Stage (1) is routine; stage (2) requires a guardedness condition on self-reference, analogous to guarded recursion; stage (3) is the open conjectural core. No stage is completed in this paper.

#4. Analysis

Every number in this section is derived here from stated inputs; no external numerical data is used beyond standard mathematical identities, which are named as inputs.

#4.1 Halving re-entry: step count for a target width

Inputs. Initial width $w_0 = 1$ (a unit interval); target width $10^{-6}$; halving gives $w_n = 2^{-n} w_0$.

Derivation. We need $2^{-n} \lt 10^{-6}$, i.e. $2^n \gt 10^6$. Since $2^{10} = 1024$ and

while $2^{19} = 524{,}288 \lt 10^6$, the minimum step count is

So the halving builder reaches a $10^{-6}$-enclosure in $20$ re-entry steps — $20$ bits of decision information, matching $10^{-6} \approx 2^{-19.93}$ since $\log_2 10^6 = 6\log_2 10 \approx 6 \times 3.3219 = 19.93$, requiring ceiling $20$.

Addition under halving. By Proposition 2 with $w^{(x)}_n = w^{(y)}_n = 2^{-n}$:

still exponentially decreasing; one extra step restores any target width.

#4.2 Series re-entry: a fully explicit enclosure of $e$

Input (standard identity). $e = \sum_{k=0}^{\infty} 1/k!$.

Tail bound. For $k \geq n+1$, $k! \geq (n+1)!\,(n+2)^{k-(n+1)}$, so

where the last inequality reduces to $(n+1)! \cdot \frac{n+1}{n+2} \geq n!\, n$, i.e. $(n+1)^2 \geq n(n+2) = n^2 + 2n$, i.e. $n^2 + 2n + 1 \geq n^2 + 2n$, true.

Take $n = 6$. Then

Partial sum. $S_6 = \sum_{k=0}^{6} 1/k! = 1 + 1 + \frac{1}{2} + \frac{1}{6} + \frac{1}{24} + \frac{1}{120} + \frac{1}{720}$. Over the common denominator $720$:

the numerator accumulating as $720 + 720 = 1440$; $+360 = 1800$; $+120 = 1920$; $+30 = 1950$; $+6 = 1956$; $+1 = 1957$.

Enclosure. Since $\frac{1957}{720} = \frac{1957 \times 6}{4320} = \frac{11742}{4320}$,

with width exactly $w_6 = \frac{1}{4320} \approx 2.3148 \times 10^{-4}$. Sanity

#References

[1] Adjoint motives of modular forms and the Tamagawa number conjecture. arXiv:2512.02348v2. https://arxiv.org/abs/2512.02348v2 [2] Chvátal's conjecture: a proof from The Book. arXiv:2609.28404v2. https://arxiv.org/abs/2609.28404v2 [3] A constructive Knaster-Tarski proof of the uncountability of the reals. arXiv:1902.07366v1. https://arxiv.org/abs/1902.07366v1 [4] The Caccetta-Haggkvist conjecture and additive number theory. arXiv:math/0603469v1. https://arxiv.org/abs/math/0603469v1 [5] On the local Tamagawa number conjecture for Tate motives over tamely ramified fields. arXiv:1508.06031v2. https://arxiv.org/abs/1508.06031v2 [6] Proof of a congruence for harmonic numbers conjectured by Z.-W. Sun. arXiv:1108.1171v2. https://arxiv.org/abs/1108.1171v2 [7] The local Tamagawa number conjecture for Hecke characters, II. arXiv:math/0701634v2. https://arxiv.org/abs/math/0701634v2 [8] Extracting efficient exact real number computation from proofs in constructive type theory. arXiv:2202.00891v1. https://arxiv.org/abs/2202.00891v1 [9] DOI 10.5281/zenodo.21672990. QNFO: The Computable Continuum: Depth Without Breadth. [10] DOI 10.5281/zenodo.21672990. QNFO: Depth, Breadth, and Valuation: A Unified Ontology of the Physical Continuum. [11] DOI 10.5281/zenodo.21664651. QNFO: The ℚ-vs-ℝ Question: Why Physical Law Requires Only the Rational Numbers.