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

In the paper's words

We propose and partially develop the Number Builder conjecture: every computable real can be generated by a finite specification of a re-entry structure in Spencer-Brown's Laws of Form (LoF) calculus of distinctions, in which each re-entry step appends a nested rational enclosure whose interval interpretation converges to the target real with an explicit, computable error bound. We formalize enclosure sequences as finite LoF expressions with controlled re-entry, define an interpretation map sending each expression to a rational interval, and prove two component results: any nested enclosure family with width tending to zero encloses a unique real with explicit error bounds, and the resulting representation is closed under the field operations with computable width propagation. Equivalence with Type-Two computability is stated as the conjectural core, not claimed as proved. [...]

The abstract, verbatim, and its opening sentence is the claim. Every line below is quoted from the text.

Numbers it reports

1. As worked instances, we derive with full arithmetic a series enclosure of $e$ of width exactly $1/4320 \approx 2.31 \times 10^{-4}$, We also outline a projected Machin-formula enclosure of $\pi$ with width $\leq 2.98 \times 10^{-8}$ after five re-entry steps, based on an assumed contraction ratio $\lt 1/25$ per step (approximately $1.398$ decimal digits per re-entry); a full arithmetic derivation is left for future work.

   from Abstract

How it is done

1. We propose and partially develop the Number Builder conjecture : every computable real can be generated by a finite specification of a re-entry structure in Spencer-Brown's Laws of Form (LoF) calculus of distinctions, in which each re-entry step appends a nested rational enclosure whose interval interpretation converges to the target real with an explicit, computable error bound.

   from Abstract

2. Third, it yields a concrete formalization target: the theorems stated in Section 3 are of a shape that a proof assistant can adjudicate.

   from 1. Introduction

3. 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.

   from 2. Background and Related Work

4. 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].

   from 3.2 Enclosure sequences

What would falsify it

1. Section 6 states falsification conditions precisely.

   from 1. Introduction

Where the claim stops

1. As worked instances, we derive with full arithmetic a series enclosure of $e$ of width exactly $1/4320 \approx 2.31 \times 10^{-4}$, We also outline a projected Machin-formula enclosure of $\pi$ with width $\leq 2.98 \times 10^{-8}$ after five re-entry steps, based on an assumed contraction ratio $\lt 1/25$ per step (approximately $1.398$ decimal digits per re-entry); a full arithmetic derivation is left for future work.

   from Abstract

2. 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.

   from 2. Background and Related Work

3. 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$).

   from 3.5 The conjecture and its component theorems

Where to read

1. Abstract223 words · 1 min
2. 1. Introduction308 words · 1 min
3. 2. Background and Related Work853 words · 4 min
4. 3. Methods1,170 words · 5 min
5. 4. Analysis350 words · 2 min