E.3. Third 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 release continues the unchanged 28-page status-corrected Paper IX manuscript and the checked second block. It completes the recorded scopes of Lemmas 5.1 and 5.2, Theorem 5.3 and Corollary 5.4. All 13 upstream proof modules and both earlier mathematical supplements remain byte-identical.

Fourteen of 24 named manuscript-proved items now have formal coverage; ten remain pending. Three classical inputs and two conjectures are tracked separately. The cumulative corpus has 219 named theorem declarations and 53 explicit definitions in 17 modules. The 56 added theorems include supporting identities and exact examples, not 56 independent discoveries.

Permalink · Source line 4

The inverse coefficients are defined from a genuine unit power series and connected to \(z^2/\sinh^2z\). The source is the paper's explicit rational formula, not an abstract integral input. Its valuation calculation proves the stronger statement that every even source coefficient is a \(2\)-adic unit. Formal-series multiplication and coefficient extraction then yield the Euler identity with the correct falling factorial. The omitted-tail theorem gives divisibility in the actual completed integer ring \({\mathbb Z}_2\).

The clean cumulative run compiled all 17 modules, matched all 272 expected transitive axiom reports and rejected eight invalid-proof controls. All 49 infrastructure and release tests passed. Exact-rational regression checks are recorded separately from the universal proofs.

Permalink · Source line 21

This is a formalization companion, not a revised primary manuscript. The unnumbered Bernoulli closed form for the inverse coefficients is not universally formalized here. Formal-series identities do not establish analytic convergence. The corrected global odd-prime finite-difference theorem remains pending. Historical numerical evidence is not presented as a fresh reproduction.

Permalink · Source line 26

Lemmas 5.1 and 5.2; manuscript page 14 Define the rational subring

Its ring laws follow from the actual nonarchimedean norm. For every \(q\in\mathcal O_2\), the code constructs its element in Mathlib's completed ring \({\mathbb Z}_2\), and proves that the underlying value in \({\mathbb Q}_2\) is the rational cast of \(q\). No integrality claim is hidden in a coercion.

Permalink · Source line 28

Use a squared formal variable \(u\) and define

The constant term is proved to be one. The factorial valuation bound gives

Thus every \(k_m\) belongs to \(\mathcal O_2\). A general coefficientwise subring theorem is proved by strong induction using the actual unit-inverse coefficient formula. Applied to \(K\), it establishes

The reciprocal's coefficients are therefore proved integral; the proof does not assume them integral in order to obtain the final congruence. Their connection to the intended hyperbolic function is proved on the next page.

Permalink · Source line 36

At even degree \(2r\), define the literal rational source

Both numerator and denominator are nonzero. The pinned Mathlib lifting-the-exponent theorem gives

Because \(2r+1\) is odd, the denominator has the same valuation. Consequently,

The code proves actual IsUnit status for the constructed \({\mathbb Z}_2\) element. This strengthens the manuscript's integrality conclusion without changing its source. The argument applies at \(r=0\), where \(R_0=1\), as well as at every later row.

Principal targets. Dyadic.kernel_coefficient_integral, Dyadic.beta_integral Dyadic.source_valuation, Dyadic.sourcePadic_isUnit

Permalink · Source line 53

Generating-function foundations for Theorem 5.3 Work in \({\mathbb Q}[[t]]\). The formal exponential and rescaling homomorphism are the same checked objects used in the second block. Define

Let \(B(t)=K(t^2)^{-1}=\sum_{m\geq0}\beta_mt^{2m}\) and let

These series are constructed independently from the definitions on the preceding page.

Permalink · Source line 71

Coefficient extraction proves the cleared identity

A separate identity from the formal exponential gives

Since \(K(t^2)\) has constant term one, its reciprocal exists as a unit. Multiplication then proves

This is the precise formal meaning of \(B(t)=t^2/\sinh^2t\). The forced quadratic zero is removed first; the proof does not claim that \(\sinh t\) itself is an invertible formal power series.

Permalink · Source line 84

From the formula for \(R_{2r}\), coefficient arithmetic proves

The product relation for the formal hyperbolic cosines yields

This equality is proved after multiplication by \(t^2\) and cancellation of that monomial in the formal-series ring. It is not an assumed source-transform relation.

Rescale the reciprocal by \(t\mapsto2t\). The unit inverse law and the preceding identity now give

The right side is connected to the same integral signed Euler sequence constructed in the previous release. These are equalities of full formal series, not fixed-degree polynomial experiments.

Principal targets. DyadicSeries.beta_original_generating_function DyadicSeries.source_shift_identity, DyadicSeries.source_times_cosh DyadicSeries.dyadic_reconstruction_series

Permalink · Source line 99

Theorem 5.3 and Corollary 5.4; manuscript pages 14–15 The reciprocal coefficients \(\beta_m\) use an ordinary power expansion. In contrast, the source and Euler series use exponential coefficients. Extracting degree \(2r\) from \(B(2t)F(t)={\operatorname{sech}} t\) therefore gives

The formal proof uses the actual natural-number descending factorial and proves its factorial-quotient identity for \(2m\leq2r\). The odd coefficient terms vanish by a proved parity argument. The binomial EGF product then supplies the falling factorial, rather than treating it as an extra assumed factor.

Both row indexing by \(r\) and the literal even-degree version with hypothesis \(\operatorname{Even}(n)\) are checked. All rows include degree zero. The exact identity is a rational equality with the Euler coefficient's integer-to-rational cast made explicit.

Permalink · Source line 120

For \(M\geq0\), define

The integral rational factors are embedded into \({\mathbb Z}_2\) using their proved witnesses. The cast of this \({\mathbb Z}_2\) truncation into \({\mathbb Q}_2\) is proved to equal the cast of the literal rational truncation.

Each omitted term has \(m\geq M+1\). Its remaining factors lie in \({\mathbb Z}_2\), so the checked weighted-tail theorem proves

This is not divisibility in \({\mathbb Q}\) or \({\mathbb Q}_2\), where division by any nonzero scalar would make the claim vacuous. A second theorem supplies the equivalent rational statement

It follows from actual \({\mathbb Z}_2\) divisibility and the proved rational/completed-field bridge. No precision assertion is passed in as a hypothesis.

Permalink · Source line 132

When \(M\geq r\), the sum retains every term and \(T_M(2r)=E_{2r}\) exactly, in both rational and dyadic coordinates. The zero-error case is included; no finite valuation of zero is used. This is a separate dyadic construction, not substitution of \(p=2\) into the odd-length theorem.

Principal targets. DyadicReconstruction.dyadic_reconstruction DyadicReconstruction.dyadic_supercongruence DyadicReconstruction.normalized_error_integral

Permalink · Source line 149

Example 5.5 and controls against incorrect normalizations The actual reciprocal recurrence gives

These values are obtained from the general formal-series definition. They are not substituted as independent input data for the reconstruction theorem. The source formula gives

Using the retained Euler anchor \(E_8=1385\), Lean checks the literal decomposition

Permalink · Source line 156

The checked nonzero error valuations are

They exceed the uniform guarantees; these two examples do not establish a universally stronger exponent.

Permalink · Source line 185

Omitting the rescaling \(2^{2m}\) already breaks the degree-two identity: the altered sum is \(1\), whereas \(E_2=-1\). Confusing ordinary beta coefficients with EGF coefficients would replace \(\beta_1=-1/3\) by \(-2/3\); a checked inequality excludes that normalization. A deliberately false claim that the depth-zero degree-eight error has valuation at least six is rejected.

These three negative proof files are separate from the active mathematical modules. The verifier also retains the five earlier invalid controls, including the normalized all-residue counterexample. Rejection of an attempted proof is an engineering control; the actual counterexample theorems establish the mathematical failures.

Principal targets. DyadicExamples.beta_one, DyadicExamples.source_anchor_values DyadicExamples.manuscript_error_zero_valuation DyadicExamples.manuscript_error_three_valuation

Permalink · Source line 195

Actual results for the v0.3.0 source snapshot

Permalink · Source line 204

The clean cumulative run used Lean 4.34.0-rc2, with compiler warnings treated as errors. Mathlib is pinned to

aeb72f1e9981b6d35b426b16dca7759be3e7ba06.

Every expected axiom report uses only propext, Classical.choice and Quot.sound, or a subset. No additional project axiom or admitted proof is permitted. The verifier audits the explicit declaration inventory, not every generated declaration or all imported Mathlib proofs.

Independent regressions. Exact Python integers and rational fractions check even degrees through 96. The 2,548 truncation cases include 1,176 nonzero errors and 1,372 exact zeros. Zero is handled separately. Kernel and reciprocal integrality and source unit status are checked in 49 cases each. Ninety-seven series coefficients agree. Forty-eight finite comparisons with the Bernoulli closed form pass, but do not prove that unnumbered formula universally. Both older independent Python suites were also rerun. None of these mirrors is Lean-extracted code or a reproduction of the original historical experiments.

Development failures. Eight of 15 captured development checks failed before repair. Their exact inactive source snapshots and diagnostics are retained separately. The seven successful development checks do not substitute for the clean cumulative release run. All 13 upstream proof files, the original corrected PDF, and both earlier supplements remain unchanged. Previous metadata and original test copies are preserved under provenance/second_block/.

Ten pending named items. These are 6.2 (finite units), 7.2–7.5 (Mahler and finite differences), 8.3 and 8.5 (residue independence and period), 9.1 and 9.2 (recurrence jumps), and 10.1 (CRT factorization). Three classical inputs and both conjectures remain separate. The corrected global finite-difference claim is not promoted by the dyadic proof.

Trust and reproduction. The pinned compiled Mathlib cache was reused, not independently rebuilt. The integral-source proof invokes the pinned library's LTE theorem; this project does not reprove LTE. Papers I–VIII and the historical numerical suite were not rerun. The source hashes, commands, axiom output, and raw logs accompany the release. The external release audit separately records archive integrity and post-packaging replay. Manuscript correspondence remains a mathematical review, not an automated semantic-equivalence theorem.

Run bash Run-Portable.sh /path/to/extracted/kit. The runtime is separate from this ZIP. The full source-level scope and target names are in coverage.json and the third-block ledger.

Permalink · Source line 220