E.9. Singular Amice Supplement

Checkpoint scope. This complete source body retains the status of its dated original supplement. Earlier pending or partial-coverage labels are historical; the final core records their resolution.

Permalink · Source line 2

Let \(p\) be prime, let \(m\mid p-1\), and put \(N=mp\). For \(1\le a<m\), put \(c=ap\) and define the original exponential section and ratio by

The quotient is interpreted after removing its forced zero. This block proves, for the actual rational coefficients \(\alpha_d\),

Equivalently, every \(p^{\lfloor d/p\rfloor}\alpha_d\) belongs to the actual completed ring \({\mathbb Z}_p\). The zero-safe alternative is explicit in the formal rational statement.

This is the weighted estimate of Proposition 4.7 in the supporting argument. It is not yet the singular higher finite-difference theorem. The full all-residue Paper IX Theorem 7.5 remains pending, and full manuscript coverage stays at 23 of 24.

Permalink · Source line 4

The 104 added declarations include 30 declarations in four previously compiled research modules, now included in the cumulative audit, and 74 declarations in six new modules. They include supporting lemmas and examples, not independent discoveries. All 47 earlier checked proof modules are preserved byte for byte.

No hidden estimate. The final weighted-ratio theorem assumes primality, the modulus divisibility, and the specified residue bounds. It does not assume weighted section membership, reciprocal closure, the ratio identity, a Mahler pairing or the desired higher-difference bound. Pages 2–5 describe the constructed objects and proved bridges.

Permalink · Source line 26

Work first in an arbitrary commutative ring \(R\). If \(z^p=1\), set

Expanding \(((z-1)+1)^p=1\) and using divisibility of every interior binomial coefficient in prime row \(p\) gives

Every other degree-\(p\) product of the two generators of \(I\) also belongs to \(PI\). The formal ideal proof therefore establishes

For \(q=p\lfloor q/p\rfloor+(q\bmod p)\), strong induction and the factorial valuation identity give

In detail, write \(b=\lfloor q/p\rfloor\). Then

No integral-domain hypothesis or division in a field is used here.

Now take the integral cyclic group ring

and assume \(N\mid p(p-1)\). Thus \((x^{p-1})^p=1\). Each genuine consecutive block

belongs to \((p,x^{p-1}-1)\). This follows from the actual polynomial identity

modulo \(p\), not from a hypothesized valuation of the product.

For the falling factorial \((x)_d=\prod_{i=0}^{d-1}(x-i)\), grouping into consecutive blocks gives

Every integral residue coordinate therefore satisfies

Dividing a coordinate by \(d!\) is done only afterward, using \(v_p(d!)=\lfloor d/p\rfloor+v_p(\lfloor d/p\rfloor!)\). This establishes the weighted denominator estimate before any field-valued divisibility could make it vacuous.

Modules. CyclotomicFiltration, PrimeBlockPolynomial, and CyclicAmiceCoefficients.

Permalink · Source line 31

An integral coordinate estimate becomes relevant only after connecting it to the manuscript's generating functions. For a residue \(r\in{\mathbb Z}/N{\mathbb Z}\), define

The implementation uses the actual formal logarithm and substitution in \({\mathbb Q}[[T]]\). It proves

and hence the coefficient recurrence

The initial values are \(F_r(0)=\mathbf1_{r=0}\).

Independently, let \(b_{d,r}\) be the residue-\(r\) coordinate of \((x)_d\) in \(R_N\). Actual group-ring multiplication gives

Induction comparing these two recurrences proves

Thus the cyclic coefficient is not an unrelated stand-in for a section coefficient. For the canonical label \(0\le c<N\), the formal section is also proved equal to the original ExponentialSection. originalSection used in the existing Euler project.

Permalink · Source line 82

The class used in the formalization is

The integral-coordinate estimate from page 2 now proves

for every residue \(r\), including the singular ones. Rational coefficients are mapped into \({\mathbb Q}_p\) by the actual coefficient ring homomorphism.

The same source package retains the earlier independent formal identity

over a commutative \({\mathbb Q}\)-algebra. The section bridge above does not rely on selecting or averaging roots in a cyclotomic extension.

Principal targets. factorial_coeff_section; section_weighted_integral; weighted_section.

Permalink · Source line 110

Let \(w(d)=\lfloor d/p\rfloor\). Since \(w(i)+w(d-i)\le w(d)\), the coefficient formula for a product proves closure of \({\mathcal W_p}\) under multiplication. Additive closure is immediate. For \(U\in{\mathcal W_p}\) with \(U(0)=1\), strong induction in the actual reciprocal coefficient recurrence proves

This inverse property is a theorem, not an additional field in a structure encoding weighted series.

Permalink · Source line 130

The derivative coefficient is \((d+1)a_{d+1}\). If \(p\nmid d+1\), the adjacent weights agree. If \(p\mid d+1\), the integer factor \(d+1\) compensates for the one-unit weight increase. Therefore ordinary differentiation preserves \({\mathcal W_p}\).

For the actual logarithm, its coefficient denominator is \(d\), and the proved inequality

implies \(\log(1+T)\in{\mathcal W_p}\). Consequently

also preserves \({\mathcal W_p}\).

Permalink · Source line 137

Put \(c=ap<N\) and define the actual normalized kernel

Let \(\ell(T)=\log(1+T)/T\), defined by shifting logarithm coefficients, not by inverting \(T\). Set

The formal proof establishes \(U(0)=1\) and the exact factorization

It follows coefficientwise that

Because \(p^a\mid(ap)!\) and \(\lfloor(d+ap)/p\rfloor=a+\lfloor d/p\rfloor\), the already proved section estimate gives \(U\in{\mathcal W_p}\). Thus \(U^{-1}\in{\mathcal W_p}\) as well. The factorial divisibility is derived from the pinned Legendre valuation theorem.

Boundary. The original positive-address section has zero constant coefficient. It is not the series to which unit inverse closure is applied.

Permalink · Source line 150

For a positive address \(c\), the rational ratio is independently constructed from the original kernels:

The scalar factor \(c\) is necessary. The source proves the cleared identity

This connects the constructed object to the original unnormalized ratio \(A_{c-1}/A_c\). It does not assign the desired transformed formula as its definition.

After actual logarithmic substitution and the chain rule,

Insert the proved factorization \(H_{N,c}(\log(1+T))=T^cU/c!\). Leibniz differentiation and cancellation of that nonzero section give

All differentiation, substitution, nonzeroness and cancellation obligations are proved in the source.

For \(c=ap\), the second summand belongs to \({\mathcal W_p}\) by the closure results on page 4. The first does too: shifting the logarithm coefficient loses at most one unit of the floor weight, so \(p\ell(T)\in{\mathcal W_p}\), and the integer \(a\) supplies the remaining factor. Therefore

The final rational coefficient theorem states the bound with an explicit zero alternative. No finite-valued default valuation at zero is used as the meaning of unlimited precision.

Permalink · Source line 171

The source proves that the actual ratio has constant coefficient \(c\), not one. In the concrete case \(N=6,c=3\), the universal theorem gives weighted membership and the constant coefficient is proved to be \(3\).

It also derives \({[T^{3}]}H_{3,0}(\log(1+T))=1/6\) from the actual differential recurrence and checks its valuation \(v_3(1/6)=-1\). Thus weighted membership does not mean ordinary coefficient integrality. This value attains the allowed floor weight at degree three.

Principal target. SingularRatioAmice.paper_singular_amice_estimate. The theorem's assumptions contain only the declared arithmetic parameter conditions.

Permalink · Source line 200

The cumulative inventory consists of 57 modules, 630 explicit theorem declarations and 128 explicit definitions. The release verifier compiles every module in dependency order into a new directory, treats warnings as errors, and requests a transitive axiom report for all 758 listed declarations. The allowed axioms remain propext, Classical.choice and Quot.sound.

The verifier retains the previous 27 invalid-proof controls and adds two: incorrectly promoting a weighted coefficient to an integral one, and incorrectly normalizing the singular ratio constant to one. Missing imports, panics and timeouts do not qualify as successful negative controls. The preserved source checker rejects proof placeholders, added axioms, and selected kernel-bypass constructs.

The Python infrastructure suite now contains 209 tests. Four old cumulative-count assertions initially failed against the extended inventory. Their original files and failed test output are preserved; the historical tests now inspect the frozen eighth-block inventory where appropriate, while current-corpus tests enforce the new counts.

Permalink · Source line 207

The new exact-rational regression program is a separate implementation, not Lean extraction. Its checked scope is:

Permalink · Source line 214

For \(p=3,N=6,c=3\), this independent computation obtains the degree-six ratio coefficient \(1/10080\), with valuation \(-2\), attaining the allowed weight. This particular coefficient calculation is recorded as a finite regression, not as a new Lean theorem. A violating modulus \(p=3,N=4\) yields a section coefficient of valuation \(-4\) at degree nine, showing that the modulus divisibility hypothesis cannot simply be discarded.

Permalink · Source line 224

To obtain the singular higher-difference theorem, the weighted coefficient estimate must still be connected to the dual Mahler polynomial filtration and its integral pairing. The argument must then establish the required ratio flatness, propagate between singular indices, and assemble the original all-residue Euler family. None of these obligations is replaced by the finite regression tests.

The full manuscript register remains 23/24. Neither conjecture is resolved. The original manuscript is unchanged. Mathlib's pinned compiled cache is reused, not independently rebuilt. Frozen compiler logs, source hashes, failed drafts, and fresh-extraction results accompany the release; its machine-readable audit is authoritative about the runs actually performed.

Permalink · Source line 227