E.2 Second 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 28-page status-corrected Paper IX manuscript. It completes formal coverage of Lemma 4.1, Theorem 4.2 and Corollary 4.3. The original manuscript and all eight first-block proof modules remain unchanged.
Ten of 24 named manuscript-proved items are now covered in their recorded scopes. Fourteen remain pending. Three classical inputs and two conjectures are tracked separately. The cumulative corpus has 163 named theorem declarations and 37 explicit definitions in 13 modules. The 74 new theorems include auxiliary identities and concrete examples; they are not 74 independent discoveries.
| Item | New formal coverage | Theorems |
|---|---|---|
| 4.1 | Literal odd-power EGF and its even part | 18 |
| 4.2 | Integral Euler and signed zigzag coefficient bridges | 29 |
| 4.2, 4.3 | Exact reconstruction, matrix rows and truncation | 16 |
| Example | Exact scalar anchors and sharpness controls | 11 |
| Total added across five modules | 74 |
The five added modules are: OddPowerSeries, EulerCoefficients, ZigzagCoefficients,
OddEulerReconstruction and OddEulerExamples.
A useful scope strengthening
On this page · Permalink · Source line 23
The algebraic proof needs oddness, not primality. The exact reconstruction and the integer divisibility statement are therefore checked for every positive odd length \(p\), including \(p=1\) and odd composites. The manuscript's odd-prime statement follows as a specialization. This is a sharpening of assumptions in this development, not a historical-priority claim. Even lengths are not included; a checked row-zero counterexample shows why.
What is not completed
On this page · Permalink · Source line 26
The weighted dyadic theory and the general corrected odd-prime finite-difference theorem remain pending. No continuum convergence or analytic summability theorem is inferred from the formal power-series equalities in this block. The historical numerical study is not being relabelled as a fresh experiment.
1. The actual odd-power generating function
On this page · Permalink · Source line 29
Lemma 4.1; manuscript page 10 Work in the rational formal power-series ring \({\mathbb Q}[[t]]\). Define
The formal exponential is Mathlib's PowerSeries.exp; scalar substitution is its actual rescale homomorphism. We define
The constant term of \(\cosh_a\) is proved to be one, so the reciprocal used here is a genuine unit inverse.
From finite sums to a series identity
On this page · Permalink · Source line 43
Coefficient extraction proves
An induction on the actual finite summation length establishes the telescoping identity
For odd \(p\) this gives, without a geometric-series convergence assumption,
This is an equality of complete formal series, not a fixed-degree polynomial check.
Even projection is identified coefficientwise
On this page · Permalink · Source line 58
For any formal series \(f\), let \(\operatorname{EvenPart}(f)=(f(t)+f(-t))/2\). Its \(n\)th coefficient is proved to be the coefficient of \(f\) when \(n\) is even and zero otherwise. Rescaling the inverse law proves \({\operatorname{sech}}(-t)={\operatorname{sech}}(t)\). The exponential multiplication identity then gives
and hence
Both the full and even EGF formulas are derived from the original integer sum. Neither is supplied as a hypothesis.
Principal targets. OddPower.source_as_exponentials OddPower.source_times_cosh OddPower.odd_source_egf, OddPower.odd_source_even_egf
2. Integral Euler coefficients and the zigzag bridge
On this page · Permalink · Source line 75
Coefficient foundations for Theorem 4.2 The first block already constructed \(C_{N,j}(r)\) by the manuscript's triangular recurrence. At \((N,j)=(2,0)\), every diagonal binomial coefficient equals one. Its denominator-clearing product is therefore one, and \(C_{2,0}(r)\) is an integer.
The source defines \(E_{2r}\) as the integer numerator of that rational coefficient and proves that its rational cast equals \(C_{2,0}(r)\). Set \(E_{2r+1}=0\). The actual exponential-section identity from the first block proves
Thus the integer sequence is connected to the intended signed Euler family, rather than merely assigned the name Euler.
The inverse coefficients are integral by construction
On this page · Permalink · Source line 84
Define the integer binomial convolution
The product formula for actual EGFs gives
Odd coefficients vanish by parity. In particular, every \(b_m\) is an integer; this is the integrality required by the later congruence.
Connecting to the paper's \(Z_n\) convention
On this page · Permalink · Source line 95
The paper defines \(Z_n\) through \(\sec t+\tan t\). The Lean construction uses Mathlib's actual formal sine and cosine series and defines
It proves the sine and cosine derivative identities, \(\sin^2t+\cos^2t=1\), and
Sign substitution in the squared variable carries the hyperbolic cosine kernel to the actual cosine kernel. The same homomorphism carries their inverses and their squares. Extracting the even coefficient in the derivative of tangent yields
This formula is proved, not assumed as an input to reconstruction. The formalization follows the generating-function definition of zigzag numbers; it does not additionally formalize their interpretation as counts of alternating permutations.
Principal targets. EulerCoefficients.euler_egf, EulerCoefficients.inverse_coeff_cast Zigzag.derivative_tan, Zigzag.inverse_is_signed_zigzag
3. Exact reconstruction and the triangular matrix
On this page · Permalink · Source line 115
Theorem 4.2; manuscript page 11 For odd \(p\), rescaling the already proved inverse law gives
Multiplying the even-source identity by \({\operatorname{sech}}^2(pt)\) therefore proves
Actual EGF multiplication now gives the integer coefficient formula
The formal proof first extracts the sum over all indices and then proves that the odd summands vanish. A checked even-index summation identity supplies the displayed change of variables.
Substituting the independently proved signed-zigzag identity recovers the manuscript's notation. For every even degree \(n\),
The Lean version uses \(n=2r\) to avoid ambiguous natural-number division. Every even natural degree has that form. Primality is not used in this equality.
The row action is connected to the matrix entries
On this page · Permalink · Source line 136
Reversing the finite sum and using binomial symmetry gives the actual source-index row action
where
The row-action equality, the diagonal identity \(U_{r,r}=1\), and vanishing above the diagonal are all checked. The arithmetic weight is also explicit:
No inverse-coordinate identity, unit diagonal or weight bound is assumed for these rows.
Principal targets. OddEuler.odd_reconstruction_series OddEuler.odd_euler_reconstruction OddEuler.odd_euler_reconstruction_zigzag OddEuler.row_action, OddEuler.row_diagonal, OddEuler.row_weight
4. Uniform truncation and a sharp exact example
On this page · Permalink · Source line 161
Corollary 4.3 and Example 4.4 For row \(2r\) and depth \(M\), the actual truncation is
Every omitted term has \(m\ge M+1\). Its other factors are integers, so the first-block omitted-tail theorem, now applied to the proved Euler identity, gives
This is not divisibility in \({\mathbb Q}\), where a nonzero divisor would make the assertion vacuous. The statement holds for every row and depth. For an odd prime it is precisely the claimed supercongruence. If \(M\ge r\), complete retention is proved exact.
The displayed manuscript row is kernel-checked
On this page · Permalink · Source line 172
The scalar anchors are derived from the same general coefficient recurrence:
The literal source sums at \(p=5\) give
Consequently,
The source proves both
Thus the guaranteed power is attained in this example. No stronger uniform exponent is inferred.
Oddness cannot be silently dropped
On this page · Permalink · Source line 195
For length two, \(S_0(2)=1-1=0\), whereas \(E_0=1\). The row-zero reconstruction already fails. The source proves this failure, and the release verifier separately attempts and rejects an invalid proof of the even-length identity.
Principal targets. OddEuler.odd_euler_supercongruence OddEuler.odd_prime_supercongruence, OddEuler.full_depth_exact OddEulerExamples.manuscript_error_sharp OddEulerExamples.even_length_reconstruction_fails
5. Verification, reproducibility, and remaining work
On this page · Permalink · Source line 204
Cumulative release evidence
| Check | Result |
|---|---|
| Fresh cumulative proof-module compilation | 13/13 |
| Named theorem declarations audited | 163/163 |
| Explicit definitions audited | 37/37 |
| Exact dependency-revision checks | 9/9 |
| Invalid proof controls rejected as intended | 5/5 |
| Infrastructure and release-contract unit tests | 33 passed |
| New captured development attempts | 15 |
| Development attempts failing before correction | 8 |
The pinned runtime is Lean 4.34.0-rc2 and Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Every final module compiled with warnings treated as errors. All 200 expected axiom reports were resolved and used only propext, Classical.choice and Quot.sound, or subsets. The audit is of explicit project declarations. Mathlib's compiled cache was reused, not independently rebuilt.
The negative controls cover a false equality, a proof placeholder, the old false normalized finite-difference bound, the false even-length extension, and a false extra digit of precision. Missing imports and timeouts do not count as successful rejection. The placeholder is rejected by warnings-as-errors, and sorryAx is separately excluded from the axiom audit.
Independent finite arithmetic checks
On this page · Permalink · Source line 225
Exact Python mirrors passed 234 reconstruction rows and 2,340 truncation-depth cases for odd lengths 1 through 35 and even degrees 0 through 24. They also checked 468 coefficients of each generating-function identity, 13 signed-zigzag bridges and seven invalid-input controls. These are rational/integer calculations, not executions extracted from Lean. The first-block mirror suite was rerun separately. The original historical numerical suite was not recovered or rerun.
Provenance and limits
On this page · Permalink · Source line 228
All eight upstream proof files, the original 28-page corrected manuscript and the first supplement are preserved. The initial clean baseline and a preliminary successful second-block build are separate from the final build that includes the explicit matrix row-action theorem. Eight failed development drafts and their diagnostics are retained, not counted as successful proofs. An unsupported interactive container invocation was replaced by successful noninteractive runtime recovery; every archive-part hash and the combined hash matched.
Fourteen manuscript-proved items remain pending. The next coherent target is the separately weighted dyadic reconstruction. The global finite-difference theorem, three classical inputs and two conjectures have not been promoted by this block.
Reproduce. Run bash Run-Portable.sh /path/to/extracted/kit. This performs unit tests, both independent regression suites, and a fresh Lean build. The kit is separate; native Windows is not tested. Precise commands, source hashes, raw compiler logs, scope entries, and failures accompany the release. Manuscript-to-Lean correspondence remains a mathematical review, not an automated semantic-equivalence theorem.