E.4 Fourth Lean Block Supplement
On this page · Permalink · Source line 1
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.
Scope and result
On this page · Permalink · Source line 3
This release continues the unchanged 28-page status-corrected manuscript and the checked third block. It completes the recorded scopes of Theorem 7.2, Corollary 7.3 and Theorem 7.4. All 17 upstream proof files and the three earlier mathematical supplements remain unchanged.
Seventeen of 24 named manuscript-proved items now have formal coverage; seven remain pending. Three classical inputs and two conjectures are tracked separately. The cumulative project contains 272 named theorem declarations and 60 explicit definitions across 21 modules.
| New module | Scope | Theorems | Defs. |
|---|---|---|---|
FiniteMahler | 7.2 | 19 | 3 |
PadicDifferenceBounds | 7.3 | 12 | 2 |
UnitModeDifferences | 7.4 | 9 | 0 |
MahlerExamples | Exact controls | 13 | 2 |
| Total added | Three items | 53 | 7 |
The 53 additions include supporting lemmas and examples, not 53 independent discoveries. The classical Gregory–Newton and binomial-difference results are reused from pinned Mathlib. The new modules connect those results to the actual Paper IX coefficient definitions, interpolation scopes, valuation bounds, and unit modes.
Two explicit specification boundaries
On this page · Permalink · Source line 21
A finite sample through \(N\) determines \(\Delta^s f(n)\) only when \(n+s\leq N\). For arbitrary orders, the finite-coefficient identity describes the constructed interpolant, not every unknown continuation of the sample. All three versions are separately checked.
The additive valuation is extended to \({\operatorname{ord}}_p(0)=\infty\). This avoids incorrectly applying Mathlib's finite-valued default at zero to an inequality that must also cover cancellation and identically zero differences.
Verification status
On this page · Permalink · Source line 26
The fresh cumulative Lean run compiled all 21 modules with warnings as errors, matched all 332 explicit declaration axiom reports, and rejected 12 invalid-proof controls. All 74 infrastructure and release tests passed. Independent exact-rational mirrors are recorded separately from the universal proofs. The archive is also subjected to a fresh-extraction rebuild and integrity audit; its separate report records that outcome.
1. Reconstruction and finite-data scope
On this page · Permalink · Source line 29
Theorem 7.2; manuscript page 17 Let \(R\) be any commutative ring. The implementation uses the actual forward-difference operator
For a full sequence \(f:{\mathbb N}\to R\), pinned Mathlib's Gregory–Newton formula gives
The source applies the theorem to these exact definitions. A separate explicit formula relates an \(s\)-th difference to its original sampled values, so the data dependence is inspectable:
Applying Newton reconstruction to \(\Delta_1^s f\) and composing the iterated operators proves
The apparently infinite coefficient sum is finite at each natural argument. Neither continuity nor convergence is needed for these identities.
An independently defined interpolant
On this page · Permalink · Source line 48
For a finite coefficient list, define
The source proves exact coefficient extraction:
It follows that \(I_N(c)\) has the stated shifted-coefficient formula at every order, with zero coefficients beyond \(N\). Every difference of order greater than \(N\) vanishes. Its coefficients are uniquely determined by its values at \(0,\ldots,N\).
What the finite sample does and does not determine
On this page · Permalink · Source line 60
For \(c_r=\Delta_1^r f(0)\) with \(r\leq N\), the source proves
The condition is essential. The sequences \(f(n)=n\) and \(g(n)=0\) agree on the sample \(\{0\}\), but \(\Delta f(0)=1\) and \(\Delta g(0)=0\). This is a checked counterexample to unrestricted inference outside the observed stencil.
Principal targets. Mahler.finite_mahler_reconstruction, Mahler.coefficient_interpolant Mahler.difference_from_coefficients, Mahler.finite_sample_difference
2. Weighted bounds in the actual ring \({\mathbb Z}_p\)
On this page · Permalink · Source line 72
Corollary 7.3; manuscript page 18 Let \(p\) be prime. For \(x\in{\mathbb Z}_p\), define
The nonzero branch uses Mathlib's actual \(p\)-adic valuation. The implementation proves its connection to genuine integral divisibility:
This is not divisibility in \({\mathbb Q}_p\), where a nonzero scalar can divide any field element. The zero case is proved separately, so zero does not spuriously violate a positive lower bound.
The source also proves multiplicativity of this extended order, the nonarchimedean lower bound for addition, and its finite-sum consequence. The natural-number cast is connected to the actual integer binomial valuation.
The binomial valuation is retained
On this page · Permalink · Source line 86
Let \(f:{\mathbb N}\to{\mathbb Z}_p\), let \(c_r=\Delta_1^r f(0)\), and suppose
Set
Every binomial in this range is nonzero. The code proves
This is the manuscript minimum after the substitution \(r=s+j\). Coefficients outside this range have zero binomial multiplier. Weights equal to infinity are allowed, and a completely vanishing difference has order infinity.
For a uniform coefficient hypothesis, the simpler conclusion follows:
For each finite \(L\leq B_p(w;n,s)\), a separate theorem yields \(p^L\mid\Delta_1^s f(n)\) inside \({\mathbb Z}_p\). Another specialization handles arbitrary finite interpolants with infinite weights beyond their degree.
Principal targets. PadicBounds.nat_le_order_iff, PadicBounds.weighted_difference_bound PadicBounds.weighted_difference_divisibility PadicBounds.coefficient_tail_bound, PadicBounds.interpolant_weighted_bound
3. Unit modes and residue-field reduction
On this page · Permalink · Source line 114
Theorem 7.4; manuscript page 18 For \(u\) in any commutative ring, and every natural step \(h\), iteration proves
The proof unfolds the actual forward-difference operator and uses the power multiplication law. No valuation premise or geometric-difference identity is assumed. More generally, a proved divisibility \(p^k\mid u^h-1\) implies
Why a \(p\)-adic unit supplies one factor of \(p\)
On this page · Permalink · Source line 124
Now let \(u\in{\mathbb Z}_p^\times\). The actual ring homomorphism
sends \(u\) to a nonzero unit. Fermat's finite-field theorem therefore gives
Using the proved kernel identity \(\ker\pi=p{\mathbb Z}_p\), the source derives
The conclusion is not supplied as an abstract certificate. It follows from the unit hypothesis and the standard residue-field construction.
Combining it with the geometric identity establishes
These statements hold for every prime, including \(p=2\) with step one. Zero differences and order zero are included. Every multiple of the Fermat step satisfies the same lower bound.
Finite integral linear combinations
On this page · Permalink · Source line 146
For any finite index set \(S\), coefficients \(a_i\in{\mathbb Z}_p\) and units \(u_i\in{\mathbb Z}_p^\times\), linearity of the actual iterated operator gives
At \(h=p-1\), the result is divisible by \(p^s\). The empty sum is permitted. This does not prove that the general congruential Euler packets of Theorem 7.5 admit such a representation.
Principal targets. UnitModes.geometric_difference, UnitModes.unit_fermat_divisibility UnitModes.unit_mode_valuation_gain UnitModes.finite_unit_modes_valuation_gain
4. Exact examples and adversarial checks
On this page · Permalink · Source line 159
The examples use the same definitions as the general results
A polynomial anchor
On this page · Permalink · Source line 160
The actual difference table for \(f(n)=n^2\) yields
The finite interpolant therefore reconstructs \(I_2(c)(7)=49\). This checks the sign and indexing conventions, not just the names of the defined objects.
A sharp binomial-weight improvement
On this page · Permalink · Source line 167
Let
At \(n=3\) and \(s=1\), the four coefficient valuations are \((4,1,1,4)\), while the binomial valuations are \((0,1,1,0)\). Thus the refined bound is
stronger than the coefficient-only lower bound one. The source checks both the minimum and the actual result:
The valuation equality is proved in the actual completed ring \({\mathbb Z}_3\), with an independent exact integer divisibility check as well.
A sharp unit-mode gain
On this page · Permalink · Source line 182
For \(p=5\) and \(u=2\),
The source proves \(5^2\mid225\) and \(5^3\nmid225\). This example attains the guaranteed gain; no additional uniform power of \(p\) is claimed.
What fails when hypotheses or conventions are dropped
On this page · Permalink · Source line 189
The nonunit \(u=3\) at \(p=3\) gives \(\Delta_2(u^n)|_{n=0}=8\), with no factor of three. A constant unit has every positive-order difference zero, hence infinite extended valuation. The finite-sample counterexample on page 2 distinguishes a true interpolant identity from an unsupported claim about unknown continuation.
The release verifier adds four negative Lean controls: an unrestricted finite-sample inference, zero assigned finite extended valuation, nonunit valuation gain, and an extra unit-mode precision claim. All are required to fail with substantive proof diagnostics. Import errors or timeouts do not qualify as successful rejection tests.
Source. The module MahlerExamples contains these exact certificates. Principal target names are listed in the fourth-block ledger.
5. Verification record and remaining work
On this page · Permalink · Source line 196
Evidence is retained separately from conclusions
Cumulative proof checks
On this page · Permalink · Source line 197
Lean 4.34.0-rc2 rebuilt all 21 local modules into a fresh directory with warnings treated as errors. All 272 theorem declarations and 60 explicit definitions matched their expected transitive axiom reports. Only propext, Classical.choice and Quot.sound, or subsets thereof, occurred. All nine dependency pins matched. Twelve invalid-proof controls were rejected.
All 74 infrastructure and release tests passed. Historical version-specific tests use immutable metadata snapshots. Current source counts, preserved upstream hashes, exact newly covered manuscript items, remaining items and substantive mathematical boundary cases are checked by the active suite.
Ten targeted development runs preceded the cumulative build. Six failed before repair, due to elaboration, coercions, finite-sum normalization, an inferred index type, and tactic or linter diagnostics. Those drafts and compiler outputs remain in a separate inactive evidence directory. No failed draft is counted as a passing theorem.
Independent exact-rational mirrors
On this page · Permalink · Source line 204
The new standard-library Python program uses repeated difference tables and independently evaluated binomial sums. It passed 2,079 reconstructed values, 15,939 in-range sample differences, 2,600 arbitrary-interpolant differences, 900 weighted cases, 966 unit-mode cases and 350 finite-mode-sum cases. Among the weighted cases, 522 differences were zero. It also rejected 189 out-of-range stencils and 15 nonunit inputs.
These are finite tests on rational examples, not executable extraction of Lean functions, a substitute for a universal proof, or a new run of the manuscript's historical experiments.
Remaining named manuscript-proved items
On this page · Permalink · Source line 209
| Item | Remaining formalization |
|---|---|
| 6.2 | Finite unit decomposition certificates |
| 7.5 | Global odd-prime Euler finite-difference theorem |
| 8.3 | Standard-window residue independence |
| 8.5 | Uniform standard-window period |
| 9.1 | Companion-matrix jump theorem |
| 9.2 | Fibonacci packet recurrence |
| 10.1 | Arithmetic CRT packet factorization |
The three classical inputs and two conjectures remain separate. Mathlib's pinned compiled cache was reused, not independently rebuilt. No infinite Mahler convergence theorem or prime-independent arithmetic spine is proved here. The original manuscript and three earlier supplements remain unchanged; the finite-data and zero-valuation clarifications accompany them in this release.
Reproduce. Run bash Run-Portable.sh /path/to/kit. The report in verification/fourth_release/ records the cumulative build. The separately distributed release audit records archive integrity and fresh-extraction replay.