E.5. Fifth 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 manuscript and the checked fourth block. It completes Proposition 6.2, Corollary 8.3 and Theorem 10.1 in the scopes stated below. All 21 upstream proof files and the four earlier mathematical supplements remain unchanged.

Twenty of 24 named manuscript-proved items now have formal coverage; four remain pending. Three classical inputs and two conjectures are tracked separately. The cumulative project contains 333 named theorem declarations and 77 explicit definitions across 28 modules.

Permalink · Source line 4

The 61 new theorems include supporting lemmas and examples, not 61 independent discoveries. Pinned Mathlib supplies finite-field, unit-group, ideal-power, \(p\)-adic residue and Chinese-remainder results. The new modules connect these to the actual packet coefficients, explicit finite lifts, and existing selectors.

Permalink · Source line 22

Rational coefficients are not reduced through an imaginary map \({\mathbb Q}\to{\mathbb F}_p\). The proof first constructs their integral lifts in \({\mathbb Z}_p\) and establishes equality in \({\mathbb Q}_p\). Root representatives are actual units at the requested precision, not unchanged residues that need not satisfy the root equation modulo \(p^\ell\).

Permalink · Source line 25

The fresh cumulative Lean build compiled all 28 modules with warnings treated as errors, matched 410 declaration axiom reports, and rejected all 17 invalid-proof controls. All 103 infrastructure and release tests passed. Independent finite regressions are recorded separately from the proofs. A separate release audit records the archive's fresh-extraction rebuild and integrity checks.

Permalink · Source line 28

Corollary 8.3; manuscript pages 19–20 Fix a prime \(p\), an integer \(m\geq1\) and a window address \(0\leq j<p\). The earlier project defines the rational packet coefficients by the actual recurrence

The previous Lucas theorem proves

The last congruence makes each diagonal entry a unit in the actual completed ring \({\mathbb Z}_p\).

Permalink · Source line 30

For a ring \(R\), a triangular row system \(T\), right-hand side \(b\), and proved unit pivots \(d_n=T_{nn}\), define

The new ring-level solver uses well-founded recursion. Its row identities and unique-solution property are proved. The source also proves compatibility of this solver with ring homomorphisms into fields.

Specializing to \(R={\mathbb Z}_p\) constructs \(c^{(p)}_{m,j}(n)\). Mapping to \({\mathbb Q}_p\) and comparing with the original rational forward substitution gives

Thus every original standard-window coefficient is \(p\)-integral, for every row. Integrality is a conclusion, not an additional hypothesis on the coefficients.

Permalink · Source line 43

Independently define \(e^{(m,p)}\) over \({\mathbb F}_p\) by the unit-diagonal system

Its recurrence and uniqueness are checked. Applying the actual homomorphism \(\pi:{\mathbb Z}_p\to{\mathbb F}_p\) to the integral row, and then Lucas reduction, proves

For \(j,k<p\), a separate ideal statement gives

The formal solver also covers \(m=0\); the manuscript uses \(m\geq1\). No global finite-difference theorem or period assertion enters this proof.

Principal targets. WindowIndependence.coeffPadic_coe, .standard_window_integral WindowIndependence.residue_independence, .reduced_unique WindowIndependence.two_window_addresses_congruent

Permalink · Source line 56

Proposition 6.2; odd-prime branch Let \(p\) be prime, \(\ell\geq1\), and

Define actual units in the same ring by

The Lean source writes \(\ell=L+1\), so zero precision is excluded without truncated natural-number subtraction.

Permalink · Source line 75

Euler's unit-group exponent gives

Reduction to the actual field \({\mathbb F}_p\) commutes with powers. Its Frobenius identity gives

Consequently,

The manuscript's finite existence conclusion is obtained directly. The proof does not assume a Hensel lift or an already supplied root representative.

Permalink · Source line 88

The source proves the actual kernel statement

For \(x\equiv y\pmod p\), the checked ideal-power lifting theorem gives

If \(w^{p-1}=1\), then \(w^p=w\) and hence \(w^{p^k}=w\) for every \(k\). Therefore two roots with the same residue are equal. The decomposition is unique whenever its second factor reduces to one. Multiplicativity of both factors is also proved.

For \(p=3,\ell=2,a=2\), the checked values are

The unlifted representative \(2\) is not a square root of one modulo nine.

Principal targets. FiniteUnits.finite_unit_decomposition, .power_lift_congruence FiniteUnits.omega_unique, .decomposition_unique FiniteUnits.omega_mul, .principal_mul

Permalink · Source line 107

Finite refinements and Proposition 6.2's dyadic branch For \(1\leq k\leq\ell\), let

be the actual reduction homomorphism. It induces a map on units. The explicit construction satisfies

The proof uses the exponent factorization \(p^{\ell-1}=p^{k-1}p^{\ell-k}\) and the already proved Frobenius invariance of a lifted root. Principal factors also satisfy

At precision one the principal factor is exactly one. These are coherent finite certificates; no infinite inverse limit or topological unit-group equivalence is constructed in this release.

Permalink · Source line 130

Now let \(\ell\geq2\) and \(a\in({\mathbb Z}/2^\ell{\mathbb Z})^\times\). The actual units of \({\mathbb Z}/4{\mathbb Z}\) are exhausted by \(1\) and \(-1\). Define

The source uses \(\ell=L+2\). It proves

The sign is uniquely determined by the residue modulo four, and cancellation gives uniqueness of the principal factor.

The checked example \(a=3\) modulo eight has sign \(7=-1\) and principal factor \(5\):

The code separately proves \(1=-1\) in \({\mathbb Z}/2{\mathbb Z}\) but \(1\neq-1\) in \({\mathbb Z}/4{\mathbb Z}\). Modulo two alone cannot identify the sign. The generic prime-power construction at \(p=2\) only asks for a principal residue modulo two and is not silently substituted for this stronger mod-four factorization.

Principal targets. UnitRefinement.omega_compatible, .principal_compatible, .principal_power DyadicUnits.dyadic_unit_decomposition, .decomposition_unique

Permalink · Source line 152

Theorem 10.1; manuscript page 22 Let \(a\geq0\), let \(M\) be odd, and put \(N=2^aM\). Coprimality is derived from oddness:

The construction uses the actual Chinese-remainder ring equivalence

Its bijectivity and component formula are checked. On a natural representative \(r\), the components are precisely its reductions modulo the two factors, not arbitrary coordinate labels.

Permalink · Source line 177

For natural indices \(n,r\), the source proves

For the original coefficient selector

take the canonical label \(0\leq r<N\). The logical equivalence yields the actual equality of sequence operators

This statement holds for coefficients in any type with zero. A separate theorem lifts the equality coefficientwise to the existing formal power-series selectors over any semiring.

The cases \(a=0\) and \(M=1\) are included. The corresponding one-element residue ring is not excluded. Oddness of \(M\) already implies positivity.

Permalink · Source line 189

CRT factors addresses, not the visibility weights or valuation filtrations associated with those addresses. Nothing in this proof gives an equal-weight decomposition at every prime or an additional analytic convergence theorem.

Coprimality cannot be discarded. The distinct classes \(0\) and \(2\) modulo four both map to \((0,0)\) when both components are reduced modulo two. The source checks this counterexample. It also checks a composite-modulus failure of the Fermat exponent and a coefficient outside the standard window that is not \(3\)-adically integral.

Principal targets. CRTPackets.address_bijective, .address_components, .residue_equivalence CRTPackets.packet_factorization, .series_packet_factorization FiniteArithmeticExamples.outside_window_not_integral

Permalink · Source line 210

Cumulative release evidence The fresh build started with an empty output directory under Lean 4.34.0-rc2 and Mathlib revision

All nine dependency revisions matched the runtime manifest and repository heads.

Permalink · Source line 219

Dependencies are among propext, Classical.choice and Quot.sound, or subsets thereof. The source scan excludes admitted proofs, new axioms, and selected trust bypasses. The five new rejection controls cover root lifting, primality, dyadic signs, integrality, and coprimality.

Permalink · Source line 238

The exact Python mirrors passed 2,132 standard-window coefficient rows, 1,476 prime-power unit cases, 555 exhaustive root-uniqueness checks, 4,594 precision comparisons and 576 multiplicativity comparisons. The dyadic suite checked 454 decompositions and their uniqueness. CRT covered 1,240 addresses and 6,200 selector cases. Thirteen invalid inputs were rejected.

These are independently implemented finite arithmetic checks, not code extracted from Lean or replacements for its universal proofs. Their deterministic mathematical payload is replayed separately from elapsed time in the fresh-extraction release audit.

Permalink · Source line 241

Eleven of 18 development checks failed before repair, on lemma interfaces, coercions, finite cases, and simplification. Their inactive snapshots and diagnostics are retained. All 21 upstream proof files and four earlier supplements are unchanged. Edition-specific test updates retain archived originals.

Permalink · Source line 246

Three classical inputs and two conjectures remain separate. Mathlib's cache was reused, not independently rebuilt. Earlier papers and historical experiments were not rerun. The preserved manuscript must be read with the cumulative supplements and amendments.

Permalink · Source line 257