B.9. Paper IX: compatible towers with prescribed parameters

Author: Komorebi P. — 8 September 2026.

This block constructs actual compatible polynomial towers from initial solved-block surjectivity, for every compatible integer parameter path. For a prime base, it constructs such a path for every p-adic parameter in the initial ball and proves an exact polynomial endpoint with all retained precisions. The six new mathematical modules compile; the release verification report records the authoritative fresh-build and axiom-audit results.

Permalink · Source line 5

Let \(q>0\), \(L\ge1\), and

Write \(S_q=\mathbb Z/q\mathbb Z\), and let the actual reduced Jacobian blocks be

Assume \(J_x\) is surjective. A vector divisibility condition below is coordinatewise.

Integer prescribed-path theorem. For every supplied path \(t:\mathbb N\to\mathbb Z^k\) satisfying

there is a single tower \(z:\mathbb N\to\mathbb Z^{m+k}\) with

The parameter equality is exact in integers. For \(a\le b\),

Consequently \(J_{z(n)}=J_x\) at every level. No later surjectivity or per-step solvability is assumed. This theorem includes positive composite bases and \(q=1\).

Arbitrary p-adic target theorem. Now let \(q=p\) be prime. For every

there are a compatible integer tower \(z\) as above and \(b\in\mathbb Z_p^{m+k}\) such that

A compatible integer parameter path converging to \(\tau\) is constructed in the proof, with its initial representative fixed exactly. A separate theorem accepts every supplied compatible integer path with limit \(\tau\) and retains its exact coordinates in the constructed tower.

Exact branching. At any stage \(n\), put \(N=L+n\). For every parameter digit \(v\in\mathbb F_p^k\), let

Here \(p^Nv\) means any integer representative of \(v\), multiplied by \(p^N\); the residue class does not depend on the representative. Then

Surjectivity implies \(e\le m\). This is a count of distinct actual next-level residue classes. It does not count integer representatives or entire infinite towers.

Square solved-block uniqueness. If \(m=e\), every prescribed \(\tau\) has exactly one root in the original ball:

Thus all valid integer parameter approximations and all lifting choices with the same target have the same endpoint. This does not assert uniqueness of the integer representatives in the tower. All prime statements include \(p=2\).

Permalink · Source line 18

At depth \(N\ge1\), suppose \(F(a)=q^Nr\) and a desired next integer parameter target satisfies \(t'-\operatorname{free}(a)=q^Nw\), with \(w\in\mathbb Z^k\). Surjectivity supplies a solved digit \(u\in S_q^m\) satisfying

Choose an integer representative \(\widetilde u\), and set

The parameter quotient is the supplied integer \(w\). Therefore \(\operatorname{free}(a')=t'\) exactly. The checked polynomial Taylor identity gives

Its quadratic remainder is divisible by \(q^{2N}\), and \(2N\ge N+1\). Also \(a'\equiv a\pmod q\), so evaluation of every polynomial partial derivative gives the same reduced Jacobian. Induction on the level, carrying the root, exact parameters, and fixed solved Jacobian as its state, constructs the entire integer tower. The existence proof uses ordinary classical choice; it does not supply an optimized computational lifting algorithm.

For a p-adic target \(\tau\), use \(t(0)=t_0\) and, for \(n\ge1\), the canonical integer representatives of \(\tau\bmod p^{L+n}\). The initial congruence hypothesis and the truncation precision imply

Subtracting successive precision relations gives compatibility in \(\mathbb Z_p\); the checked faithful integer-divisibility theorem gives compatibility in \(\mathbb Z\). These precision relations also give convergence to \(\tau\).

The compatible vector-tower completion theorem constructs \(b\), proves convergence, and retains every stage precision. Continuous polynomial evaluation and the increasing root precision give \(F(b)=0\). Each parameter coordinate has both the corresponding coordinate of \(b\) and \(\tau\) as its limit, so uniqueness of limits gives exact parameter equality.

For every proposed next parameter digit, the previously checked obstruction is \([\bar r+K_av]\in S_p^e/\operatorname{im}J_a\). The fixed solved Jacobian is surjective, so this class vanishes for every digit at every stage. The actual lift fiber is a torsor for \(\ker J_a\). Rank-nullity gives its cardinality \(p^{m-e}\).

When \(m=e\), the new solved-Jacobian definition is definitionally the existing square block used by the checked continuous parameter chart. Every root in the initial ball with the given parameters is that chart point. Applying this to any two roots proves equality, including endpoints obtained by different constructions.

Permalink · Source line 86

The inherited checked example \(F(Y,T)=T\), \(p=2\), \(x=0\), \(L=1\) has a surjective full Jacobian but zero solved block. Prescribing parameter digit \(1\) forces \(T=2\pmod4\), so no next root exists. Full-Jacobian surjectivity cannot replace the hypothesis on the prescribed solved block.

The new checked example \(F(Y_1,Y_2,T)=Y_1\) has a surjective solved block \((1,0)\). Nevertheless \((0,0,0)\) and \((0,2,0)\) are distinct exact roots in the same modulo-two ball with identical parameters. Uniqueness therefore requires the square solved case. The corresponding negative control deliberately attempts the stronger false conclusion and must be rejected by Lean.

Depth \(L\ge1\) is essential for the Taylor step used here. The general singular case can have a nonzero next obstruction after an earlier zero obstruction. Neither the finite one-step criterion nor this smooth theorem establishes unrestricted singular persistence.

Permalink · Source line 137