E.8. Eighth Lean Block 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

The all-residue Theorem 7.5 remains pending. This release proves its full saturated higher-power estimate throughout the standard window, rather than only a period modulo \(p\). For every prime \(p\), positive \(m\mid p-1\), \(0\le j<p\), and natural \(n,k,u\), put \(h=(p-1)/m\). Then

The unnormalized family \(j!C_{mp,j}(n)\) satisfies the same bound. Both statements concern the original rational coefficient function, identified with its actual integral \(p\)-adic lift. They include \(p=2\), \(k=0\), \(n=0\), and the additional harmless case \(u=0\).

Coverage remains 23 of 24 named manuscript-proved items. Three classical inputs and two conjectures remain separate. The new result covers every permissible residue when \(m=1\), but not the range \(p\le j<mp\) when \(m>1\).

Permalink · Source line 4

The cumulative corpus has 526 explicit theorem declarations and 107 explicit definitions in 47 modules. Counts include support lemmas and examples, not independent discoveries. All 38 upstream proof modules and seven earlier supplements are preserved.

Permalink · Source line 28

The normalized defect is not an ordinary derivation Let \(A\) be a commutative algebra over a characteristic-zero field \(K\), and let \(U\) be an actual \(K\)-derivation. The source defines

The coefficients of each \(M_q\) are proved integral: the middle entries of a prime-power binomial row are divisible by \(p\). In Lean they are implemented as natural quotients, with exact division proved before the product identity is used. Induction on derivative order establishes the full Leibniz formula and hence

The middle terms are essential. At \(p=3\), \(f=t\) and \(g=t^2\), the constant coefficient of \(B(fg)\) is \(-2\), whereas that of \(B(f)g+fB(g)\) is zero. This inequality is itself Lean-checked.

Permalink · Source line 31

Let \(I\subset A\) be a subring stable under \(U\). Define

The definitions contain no product or inverse closure requirement. Since \(B\) commutes with \(U\), derivatives of a bounded element remain bounded. Induction on \(r\) in the displayed product rule then proves closure under multiplication. The finite middle sums use the lower-order induction hypothesis, not the desired next-order conclusion.

For an actual inverse \(fg=1\), applying the product rule and multiplying by \(g\) gives

If \(g\in I\), induction on \(r\) proves boundedness of \(g\) from boundedness of \(f\). At each successor stage the preceding stage supplies boundedness of \(g\) needed on the right. Passing to all finite orders proves reciprocal closure for an integral inverse.

Principal targets. DworkAlgebra.B_mul DworkClosure.bounded_mul, DworkClosure.bounded_inverse DworkClosure.flat_mul, DworkClosure.flat_inverse

Permalink · Source line 45

Connecting differential expressions to coefficient divisibility The specialization works inside \({\mathbb Q}_p[[t]]\) and uses factorial-scaled coefficients

The source constructs \(I_p\) as a subring. Actual exponential-series multiplication gives

These identities prove multiplication and derivative stability of the lattice. Membership does not require ordinary power-series coefficients to lie in \({\mathbb Z}_p\).

Permalink · Source line 64

For \(f\in I_p\) with constant coefficient one, the usual power-series reciprocal is used. Its inverse equation yields the exact coefficient recurrence

Strong induction proves that all of these coefficients are integral. Combining this construction with the preceding all-order theorem proves flatness of the actual reciprocal. No flatness or integrality of that reciprocal is assumed in the normalized-series specialization.

Permalink · Source line 78

Define the literal coefficient defect

The new source proves, for every \(s,d\),

For an integral coefficient \(x\), it proves the bridge

Thus the differential definition is equivalent to the existing coefficient-level Dwork criterion. Division occurs in \({\mathbb Q}_p\), while the assertion after division is membership in \({\mathbb Z}_p\). It is not divisibility in the field. Zero coefficients satisfy every finite precision condition.

Principal targets. HurwitzDworkClosure.integral_inverse HurwitzDworkClosure.flat_product, HurwitzDworkClosure.flat_reciprocal HurwitzDworkClosure.decode_B_iterate HurwitzDworkClosure.normalized_mem_iff, HurwitzDworkClosure.flat_encode_iff

Permalink · Source line 86

The standard interval without an analytic power-series-in-the-index premise On Hurwitz coefficients, the actual Euler operator plus \(c\) is

Direct induction proves its commutator with every defect iterate:

Suppose \(a\) is integral and supported at degrees divisible by \(p\), and \(p\nmid c\). Every supported pivot \(d+c\) is proved to be a unit of \({\mathbb Z}_p\). The defect preserves this support. Induction in the commutator identity therefore proves

This is a reflection theorem on the integral supported domain. It does not assume flatness of the proposed preimage, and does not assert invertibility at a singular pivot \(p\mid c\).

Permalink · Source line 107

Set \(N=mp\) and, for \(0\le j<p\), define integral Hurwitz coefficients

The inverse binomial is constructed using the actual unit pivots already proved by Lucas reduction. Its image in \({\mathbb Q}_p\) is proved equal to the displayed reciprocal.

For \(j=0\), \(g_0\) is the literal \(N\)-divisibility indicator. Because \(N\mid p(p-1)\), the two shifts in \(\delta g_0\) agree and \(\delta g_0=0\). It is flat at every order. The actual binomial identity gives

As \(1\le j+1<p\), the nonsingular reflection theorem inductively proves flatness of every \(g_j\) in the standard window. There is no uniform-convergence assumption in this argument.

Principal targets. EulerDefect.iterated_commutator, EulerDefect.flat_of_euler_flat StandardWindowDwork.kernel_coe, StandardWindowDwork.kernel_euler_step StandardWindowDwork.kernel_flat

Permalink · Source line 126

Actual reciprocal, actual rational sequence, every order and step multiple The factorial-ratio identity is proved coefficient by coefficient:

The right side is precisely the normalized source kernel from the first block, not a replacement family. The earlier rational identity for its reciprocal is transported to \({\mathbb Q}_p[[t]]\). A separate encoding theorem identifies the reciprocal's coefficients with the already constructed \({\mathbb Z}_p\) lifts of the original \(C_{N,j}(r)\).

All-order reciprocal closure therefore gives flatness of the actual packed Euler coefficient sequence. The earlier coefficient-extraction theorem now has a proved antecedent for every \(j<p\), and yields

A new finite telescoping argument proves the extension to arbitrary natural multiples of \(h\). Its first-step identity is

Commutation of differences and induction on their order transfer any fixed ideal bound valid on a forward tail. The required precision \(\min(k,mn)\) is nondecreasing as the starting row advances. Hence

The scalar-extension bridge identifies these differences with the original rational coefficient function. The rational theorem explicitly allows zero differences, avoiding the library's finite valuation convention at zero. Since \(j!\) is a unit for \(j<p\), both normalized and unnormalized versions have the same precision.

Scope. The proof includes all primes, all rows and orders, and all natural step multipliers. For \(m=1\), the standard window is the complete allowed residue range. For larger \(m\), residues \(p\le j<mp\) are not covered by this theorem. The earlier one-power period is not the source of the new higher-power estimate.

Principal targets. StandardWindowDwork.window_is_reciprocal, StandardWindowDwork.standard_window_flat StandardWindowDwork.standard_window_global_bound StandardWindowPrecision.normalized_window_precision StandardWindowPrecision.unnormalized_window_precision StandardWindowPrecision.modulus_p_complete_family

Permalink · Source line 148

The coverage count is unchanged; the unresolved theorem now has a stronger proved part The original rational recurrence gives

Consequently, the new source proves

This attains the bound \(\min(2,2\cdot1)=2\). A claim of a third power is rejected. The separate cubic example proves that the normalized differential defect is not an ordinary derivation. Controls also reject an asserted unit pivot at \(c=p\) and the prime-power binomial-divisibility formula at a composite base.

Permalink · Source line 182

The cumulative verifier rebuilds all 47 modules and audits all 633 explicit declarations: 526 theorems and 107 definitions. Warnings are errors, unexpected axiom dependencies are rejected, and 27 deliberately invalid proof controls are tested. The allowed transitive axioms remain propext, Classical.choice and Quot.sound. Exact results, compiler commands and source hashes are in the accompanying machine-readable reports.

All 189 infrastructure and release tests passed. Independent exact-arithmetic mirrors checked 3,040 normalized and 3,040 unnormalized bounds in 95 standard-window families, 6,596 source defects and 6,596 reciprocal defects, 75 product identities, 360 inverse-closure cases, 720 Euler commutators and 150 telescoping identities. They are finite Python mirrors, not code extracted from Lean and not substitutes for the universal proofs.

Failed development snapshots and diagnostics are preserved separately. Historical source files and earlier supplements remain unchanged. Mathlib's pinned compiled cache is reused, not independently rebuilt; the original historical numerical suite is not rerun. The manuscript-to-formal correspondence remains a mathematical review.

Permalink · Source line 196

The all-residue Theorem 7.5 requires the additional range \(p\le j<mp\). Its supporting prose proof treats singular ratios at \(c=p,2p,\ldots,(m-1)p\) through weighted Amice estimates and a dual Mahler pairing, then propagates across the intervening indices. Those actual-family estimates and the full remaining propagation are not supplied by this release. A unit argument at \(p\nmid c\) cannot be used at \(p\mid c\).

Release boundary: 23/24 named manuscript-proved items, with Theorem 7.5 still pending. The two conjectures remain unproved. The proved standard-window result is an infinite family, but no numerical proportion of the remaining work is inferred from the width of that window.

Permalink · Source line 203