Beta coding and arithmetic sequence witnesses

For $d>0$, induction on $b$ gives unique division $b=qd+r$, $r<d$: at zero use $(0,0)$; from $(q,r)$ use $(q,r+1)$ if $r+1<d$, and $(q+1,0)$ if $r+1=d$. If two such expressions had $q<q\mathrm{\prime }$, then $qd+r<(q+1)d\le q\mathrm{\prime }d\le q\mathrm{\prime }d+r\mathrm{\prime }$, impossible; interchange them for the other inequality. Thus quotient and remainder are unique. These arguments use natural-number induction and elementary distributivity/order, each derivable in PA by induction from F1.

To derive the required congruence theorem, repeatedly replace $(u,v)$ with $(v,\mathrm{rem}(u,v))$ while $v>0$. The positive second coordinate strictly decreases, so strong induction on the second coordinate $v$ gives termination, uniformly in $u$ (also when $u<v$). Common divisors are unchanged because $u=qv+r$ iff $r=u-qv$. Maintaining integer linear combinations of the original pair (integers represented as differences of naturals) shows that the final positive divisor $g$ is $su+tv$. It divides both original numbers, and every common divisor divides it. Thus coprime $u,v$ have $su+tv=1$. For residues $A,B$ the integer $Avt+Bus$ is congruent to A modulo u and B modulo v. Taking its nonnegative residue modulo uv gives a simultaneous solution. Uniqueness modulo uv follows since a number divisible by u and v is divisible by uv: multiply $su+tv=1$ by the quotient after division by u. Iterating combines any finite pairwise coprime list.

Use the Q remainder graph $R(b,d,r):=(d=0\wedge r=0)\vee [d\mathrm{\ne }0\wedge r\le b\wedge r<d\wedge \mathrm{\exists }q\le b(b=q\cdot d+r)]$. At numeral b,d, F2 restricts r and q to finite lists of numerals. Step 1.1 identifies the one correct remainder; every other pair is refuted by closed calculations, and the correct pair supplies existence. If d=0 the first clause forces r=0. Substituting the term $1+(i+1)c$ into the divisor place gives the beta graph. At numeral inputs the divisor is a numeral by F2, so the same unique-value conclusion follows.

For $a_0,\dots ,a_n$, choose $j>\max (n+1,a_0,\dots ,a_n)$ and $c=j!$. Let $d_i=1+(i+1)c$. If a prime p divided both $d_i,d_k$ with $i\mathrm{\ne }k$, it would divide $(i-k)c$. It cannot divide c, since it divides $1+(i+1)c$, so it divides $\mathrm{\mid }i-k\mathrm{\mid }\le n<j$, and then divides j!, a contradiction. Here every integer greater than one has a prime divisor by taking its least divisor greater than one; that divisor is prime by minimality. The prime-divides-product assertion follows from the Bezout identity when it does not divide one factor. Thus the moduli are pairwise coprime, and step 2.1 gives b with remainder $a_i<d_i$ at each modulus. The empty list requires no congruences.

For the PA assertion, division and the Euclidean argument above are inductions on naturals, with integer coefficients stored as pairs of naturals. For every j and bound B, PA proves there is C>B divisible by every positive t<=j: the induction starts with C=B+1 for j=0; from a witness C at j take C(j+1) at j+1. This uses a single existential induction invariant and does not presuppose sequence coding or a factorial function. PA bounds the old beta values by $1+nc$ for $i<n$. Choose $j>n+1,a,1+nc$ and such a C>j divisible by 1,...,j, and use new moduli $1+(i+1)C$. The coprimality argument of step 3.1 uses precisely this divisibility property. Induction on $k\le n+1$ combines the first k congruences as in step 2.1, keeping the running product of their moduli and the current residue as existential witnesses; the induction hypothesis is a formula asserting those witnesses exist. The first n residues are $\beta (b,c,i)$, whose existence and uniqueness follow from division, and the last is a. Thus the formal PA induction produces the new code and proves every specified coordinate equation. Repeating extension supplies any internally given finite history; for a fixed external list step 3.1 already supplies its code.