E.7. Seventh 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

This block completes Corollary 8.5 of the unchanged status-corrected manuscript by an independent finite-field argument. It does not assume the still-pending global finite-difference theorem, item 7.5.

Twenty-three of 24 named manuscript-proved items now have formal coverage. The cumulative corpus contains 439 named theorem declarations and 94 explicit definitions across 38 modules. Three classical inputs and two conjectures remain separately tracked. All 31 upstream proof modules and the six earlier supplements remain unchanged.

Permalink · Source line 4

The counts include supporting lemmas, conditional implications, and exact examples. They are not counts of independent discoveries. The conditional implications do not promote their antecedents to proved facts.

Permalink · Source line 22

In characteristic \(p\), both the first and \(p\)th coefficient shifts obey a Leibniz rule for Hurwitz convolution. A section supported at multiples of \(m\), with \(m\mid p-1\), has equal first and \(p\)th shifts. Its constructed reciprocal inherits this equality. Identifying that reciprocal with the existing reduced Euler sequence gives its period on the positive-index tail.

Permalink · Source line 25

Theorem 7.5 asks for powers as high as \(p^{\min(k,mn)}\) and covers nonstandard residue classes. A period modulo \(p\) does not establish that stronger result. This release proves a genuine standard-window mod-\(p\) fragment and precise conditional interfaces for the remaining argument, while keeping item 7.5 pending.

Permalink · Source line 28

A characteristic-\(p\) argument without factorial division For sequences \(f,g:{\mathbb N}\to K\), where \(K\) is a field, define

These are Hurwitz coefficients. The notation does not divide by \(d!\) in \({\mathbb F}_p\). In particular, the implementation is not ordinary power-series multiplication with undefined inverse factorials in positive characteristic.

The identity sequence is \(\mathbf1(d)=\delta_{d0}\). The new source proves the actual higher product rule

The argument starts with Pascal's identity for the first shift, then inducts on \(a\). All sums are finite at each coefficient.

Permalink · Source line 31

For prime \(p\) and characteristic \(p\), every interior binomial coefficient in row \(p\) vanishes. Hence

The first-shift rule has exactly the same form. Both are checked for the literal coefficient product.

Suppose \(g(0)=1\). The source constructs \(f\) by the full triangular recurrence

and proves \(f\star g=\mathbf1\). It also proves cancellation: if \(a\star g=0\), then \(a=0\), by induction on the first nonzero coefficient.

If \(U^pg=Ug\), differentiate the inverse equation with both operators and subtract. The terms involving \(f\star(Ug)\) cancel, leaving

The proved cancellation law yields

The section identity is an explicit premise of this general reciprocal lemma; the next page proves that premise for the specific section used by the Euler sequence.

Principal targets. Hurwitz.shift_convolution, Hurwitz.prime_shift_convolution Hurwitz.convolution_left_eq_zero HurwitzInverse.inverse_convolution HurwitzInverse.inverse_prime_difference

Permalink · Source line 47

Corollary 8.5; manuscript page 21 Work over \({\mathbb F}_p={\mathbb Z}/p{\mathbb Z}\). For positive \(m\mid p-1\), take the literal section

It satisfies \(g_m(0)=1\). Since \(p\equiv1\pmod m\), the conditions \(m\mid d+p\) and \(m\mid d+1\) are equivalent. The source therefore proves \(U^pg_m=Ug_m\).

Let \(f_m\) be the reciprocal constructed on the previous page. A separate strong-induction proof establishes its actual support:

This support is not included as an assumption of the construction.

Permalink · Source line 76

Evaluate \(f_m\star g_m=\mathbf1\) at \(d=mn\). Reindex the surviving summation indices by \(i=mq\) using the proved support. The result is

The fifth block independently constructed the unique sequence \(e_n^{(m,p)}\) satisfying this triangular system. Applying that uniqueness theorem gives

Thus the reciprocal really is connected to the manuscript's Lucas-reduced inverse.

Permalink · Source line 90

Write \(h=(p-1)/m\). For \(n\ge1\), evaluate \(U^pf_m=Uf_m\) at the nonnegative degree \(mn-1\):

Since \(mn+p-1=m(n+h)\), the identified sequence satisfies

Induction gives \(e_{n+uh}^{(m,p)}=e_n^{(m,p)}\) for every \(u\ge0\). This proves a period, not necessarily the least positive period. The proof also includes \(p=2\), where \(m=1\) and \(h=1\).

Principal targets. WindowPeriod.section_prime_shift WindowPeriod.inverse_off_support, WindowPeriod.inverse_on_support WindowPeriod.uniform_standard_window_period WindowPeriod.multiple_period

Permalink · Source line 101

Consequences for the standard window; not the full Theorem 7.5 The fifth block constructed integral lifts \(\widehat C_{mp,j}(n)\in{\mathbb Z}_p\) of the original rational coefficients when \(0\le j<p\), and proved that their residues equal \(e_n^{(m,p)}\).

Applying the actual residue map and its kernel ideal to the new period gives

for \(n\ge1\) and \(u\ge0\). Every higher positive difference is a difference of terms already divisible by \(p\). Consequently,

A ring-homomorphism lemma identifies the image of these differences in \({\mathbb Q}_p\) with the differences of the original rational coefficient function. This is not vacuous field divisibility. The valuation version uses order infinity at zero.

Permalink · Source line 118

The initial row. For \((p,m)=(3,2)\), the same reduced recurrence gives \(e_0=1\) and \(e_1=-1=2\) in \({\mathbb F}_3\). Its proposed period is one, so the positive-tail result cannot in general include row zero.

The divisor hypothesis. At \((p,m)=(5,3)\), where \(3\nmid4\), the independently computed reduced row is

Replacing \(h\) by the integer quotient \(\lfloor4/3\rfloor=1\) does not give a period: \(e_3\ne e_2\).

No automatic extra power. The original rational triangular coefficients satisfy

A period modulo \(3\) therefore cannot simply be reported as a period modulo \(9\). This is consistent with the global theorem's proposed first-difference bound; it is not a counterexample to Theorem 7.5.

Principal targets. WindowPeriod.standard_window_period_divisibility GlobalEulerBoundary.standard_window_all_orders_mod_p GlobalEulerBoundary.lifted_difference_coe PeriodExamples.period_can_fail_at_zero PeriodExamples.first_difference_precision_is_one

Permalink · Source line 133

Conditional results are not counted as completion of item 7.5 Let \(p\) be prime and \(m\) a positive divisor of \(p-1\). For a sequence \(e\) in a commutative coefficient ring, define its actual packed Hurwitz sequence

Let \(L=p(p-1)\) and \(\delta=U^{p+L}-U^p=U^{p^2}-U^p\). The source proves the operator dictionary

At the valid nonnegative coefficient degree \(d=mpn-ps\), with \(s\le mn\), this becomes

The packed sequence and difference operations are definitions. Their coefficient correspondence is proved before any divisibility assumption is introduced.

Permalink · Source line 156

Define flatness by the actual coefficientwise divisibility assertion

The new theorem proves that this hypothesis implies

First, coefficient extraction proves the triangular region \(k\le mn\). A separate induction on difference order proves that this region is equivalent to the complete saturated estimate. This implication is useful over \({\mathbb Z}_p\); interpreting it over a field would not supply the intended integral content.

Permalink · Source line 173

Using the existing definition \(E^{(N,j)}_{Nn}=j!C_{N,j}(n)\), the source proves that multiplication by \(j!\) commutes with every iterated difference. If the unnormalized difference has precision \(A\), the normalized difference has precision \(A-v_p(j!)\). Precision is defined as

so zero and negative factorial-loss thresholds are handled correctly. For \(j<p\), the loss is zero.

Not established here. The general unnormalized Euler family has not been proved to possess the required flat integral lift, especially across singular residue intervals. The retrieved 18-page supporting prose proof uses weighted Amice/Mahler bounds, singular ratios, and nonsingular propagation. Those obligations remain, and the full arbitrary-multiple global estimate is not promoted by these interfaces.

Permalink · Source line 184

Evidence accompanies the source, not only the summary The release verifier compiles the cumulative 38-module project into an initially empty output directory, with warnings treated as errors. It checks all 439 theorem declarations and 94 explicit definitions, requiring all 533 expected axiom reports and allowing only propext, Classical.choice and Quot.sound, or subsets thereof.

The pinned runtime is Lean 4.34.0-rc2. The Mathlib revision is aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Nine dependency heads are compared with their recorded manifest pins. The compiled Mathlib cache is reused, not independently rebuilt. The source checker rejects admitted proofs and selected trust-bypass constructs; the transitive axiom audit is a separate check.

Permalink · Source line 193

The verifier retains its earlier 20 invalid-proof controls and adds three: a false row-zero period, a false nondivisor period, and an unjustified extra power of the modulus. Missing imports, timeouts and compiler panics do not count as successful rejections.

The infrastructure suite contains 162 tests. New tests verify the one-item coverage transition, preservation of the 31 upstream sources, the explicit conditional flatness premise, resolution of partial targets, and continued pending status of 7.5. Historical census tests use their frozen release snapshots. Current census assertions use the new inventory.

Permalink · Source line 201

The new rational and finite-field mirrors passed 4,848 reciprocal coefficient rows, 2,592 higher-Leibniz cases, 4,520 reciprocal prime-shift cases, 3,720 period comparisons, and 1,476 standard-window rational rows. They also checked 1,104 rational period differences, 620 higher differences modulo \(p\), and 586 Dwork extraction interfaces. Eleven invalid input configurations were rejected.

A further 4,096 finite tests of the remaining global bound passed. These do not prove that bound and do not change the coverage count. All mirrors are independent Python implementations, not execution extracted from Lean. The original historical numerical suite was not rerun.

Permalink · Source line 206

The original manuscript and all six earlier supplements remain unchanged. The new amendment replaces the period's dependence on the still-pending global theorem with the direct proof. Development failures, source snapshots and logs are kept separately from the release run. A second clean build from a freshly extracted archive is recorded in the companion release audit.

Run bash Run-Portable.sh /path/to/kit to repeat the current unit tests, cumulative finite mirrors, and Lean verification. Run python scripts/check_manifest.py to check the delivered file snapshot. The manifest does not claim that every prose sentence is equivalent to its Lean type; that correspondence remains a mathematical review.

Permalink · Source line 211