E.10 All Residue Completion 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 final statement
On this page · Permalink · Source line 3
Let \(p\) be a prime, let \(m>0\) divide \(p-1\), put \(N=mp\) and \(h=(p-1)/m\), and let \(0\le j<N\). The original rational packet is defined by
For every \(n,k,u\in{\mathbb N}\), the new formal result establishes
Here \(\Delta_h f(n)=f(n+h)-f(n)\). The corresponding rational valuation statement is zero-safe:
For the normalized coefficients, the exact correction is retained:
The manuscript's odd-prime, positive-\(u\) theorem is a specialization. The formal statement also includes zero row, zero order, zero multiplier, and the \(p=2,m=1\) subcase. This does not assert a different or broader external dyadic conjecture.
| Inventory | Prior v0.9.0 | Current source corpus |
|---|---|---|
| Named manuscript-proved items covered | 23/24 | 24/24 |
| Active mathematical modules | 57 | 70 |
| Explicit theorem declarations | 630 | 753 |
| Explicit definitions audited separately | 128 | 148 |
The 123 added theorem declarations include supporting lemmas and examples. They are not 123 independent discoveries. Three classical inputs and two conjectures remain separately tracked. The original manuscript and all 57 upstream proof modules are preserved unchanged.
Principal declaration. KomorebiPaperIX.Theorem75.global_finite_difference states the integrality and both precision bounds together, for the original coefficient functions. Its hypotheses are primality, \(m>0\), \(m\mid p-1\) and \(j<mp\), not an assumed flatness or weightedness certificate.
1. Stability of the weighted differential ring
On this page · Permalink · Source line 37
The recovered checkpoint used the actual weighted subring
Its coefficient condition is identified with the one in the previously checked singular-Amice development. The failed ThetaWeighted draft is retained separately; the repaired active source checks the complete formal-series statement below.
Put
The coefficient formula
proves \(\Theta{\mathcal W_p}\subseteq{\mathcal W_p}\). If the floor weight increases between \(d\) and \(d+1\), then \(p\mid d+1\), which compensates for that increase.
The normalized defect is not assumed to be a derivation. Its proved product rule contains the two middle Leibniz sums:
The coefficients of \(\mathcal B_p\) are the actual integral quotients \(\binom{p^2}{a}/p\) and \(\binom pa/p\). Derivative stability and this correction formula show that the elements \(F\in{\mathcal W_p}\) satisfying \(B_\Theta F\in{\mathcal W_p}\) are closed under the finite ring operations.
The scalar input is proved for every natural \(b\), including nonunits:
Because \(\Theta(1+T)^b=b(1+T)^b\), the binomial expansion of \(T^p=((1+T)-1)^p\) then proves stability of the divided generator \(T^p/p\). For \(d=pq+r\), \(0\le r<p\), every weighted monomial has the exact factorization
The scalar \(p^qa_d\) is integral by the actual weight condition. Thus all weighted monomials, and all finite weighted polynomials, satisfy the defect condition.
Finally, \([T^d]B_\Theta F\) depends only on coefficients through \(d+p^2\). Replacing \(F\) by this finite prefix proves the result for the entire formal series, without an analytic convergence assumption:
Modules. WeightedAmiceRing, FrobeniusSquare, ThetaWeighted.
2. Actual substitution and singular higher differences
On this page · Permalink · Source line 80
Let
All substitutions use Mathlib's actual formal exponential, logarithm, and substitution maps. The chain rule gives
The implementation also proves the inverse-substitution identity
The relevant integral subring is the Hurwitz subring
It is not coefficientwise integrality of ordinary power-series coefficients. The precise connection is
Since every iterate of \(\Theta\) preserves \({\mathcal W_p}\), the right side is integral. Therefore \(\mathcal E({\mathcal W_p})\subseteq{\mathcal H({\mathbb Z}_p)}\). Applying the same statement to every \(B_\Theta^sF\) proves
This is the proved transfer that was missing in the earlier attempt. No weighted Mahler pairing is assumed; the formal differential route supplies an alternative bridge.
Application to the actual singular ratios
On this page · Permalink · Source line 111
The preceding v0.9.0 source independently constructs
The notation \(t^{-c}H_{N,c}\) means removing its proved initial zero coefficients. For each \(c=ap\), \(1\le a<m\), that source proves \(R_{ap}(\log(1+T))\in{\mathcal W_p}\). The new transfer consequently proves flatness of the same rational ratio after scalar extension to \({\mathbb Q}_p\).
The actual ratio is also proved to be an expansion in \(t^N\), so its coefficients vanish outside multiples of \(N\). Constructed \({\mathbb Z}_p\) lifts and the established coefficient criterion now give, for its literal Hurwitz coefficients \(r_a(n)\),
The separate rational precision theorem is obtained through the coefficient-lift equality. Divisibility in the field \({\mathbb Q}_p\) is never substituted for this assertion.
Modules. WeightedDworkTransfer, SeriesDifferenceBridge, RatioSeriesSupport.
3. Nonsingular propagation without an assumed limit
On this page · Permalink · Source line 128
For consecutive original sections, the already defined ratios satisfy
Differentiating the first relation, using the relation for \(R_{c-1}\), and cancelling a section whose leading coefficient is proved nonzero gives the actual Riccati equation
It is not an equation imposed on a replacement ratio. Write
Both have zero constant coefficient. With \(\Lambda_c=tD+c\), the equation becomes
When \(p\nmid c\), define the actual inverse coefficientwise:
On \(p\)-supported degrees, \(d+c\) is a genuine \(p\)-adic unit. The proof establishes Hurwitz integrality of this solution, its support, both inverse identities, and preservation of full flatness using the earlier all-order Euler commutator theorem. The singular pivots \(c=ap\) are never declared to be units.
Now define explicit iterations
If \(q\) is flat and \(p\)-supported, every iterate has those properties. The crucial link to the actual ratio is an exact finite-prefix theorem:
Indeed,
The second factor has zero constant term. Multiplication therefore raises the established agreement prefix by one; coefficientwise division by \(d+c\) preserves that prefix.
For fixed \(s,d\), the coefficient \(d![t^d]B_D^sy\) depends only on the coefficients of \(y\) through \(d+p^2s\). Choosing the matching finite iterate proves its integrality. This establishes flatness of the actual \(y\), and hence of \(R_c\), without postulating flatness of the solution or invoking an unproved analytic fixed-point theorem.
Modules. EulerSeriesInverse, RiccatiFlatPropagation, RatioRiccati.
4. All-residue assembly and original coefficients
On this page · Permalink · Source line 170
The standard-window source and inverse results supply \(R_1\) and \(F_{N,0}\). Induction over \(1\le c<N\) now has two proved cases. At \(p\mid c\), the singular weighted estimate and the new substitution theorem give flatness. At \(p\nmid c\), the preceding Riccati propagation applies. Thus every actual ratio \(R_c\) is flat.
Let \(K_j(t)\) be the normalized section kernel with constant coefficient one. The constructed unnormalized Euler series is
The source/inverse identities and the factorial successor identity prove
The product formula is not an assembly hypothesis. Proved flatness of all factors and the original product-closure theorem establish flatness of the full family.
Coefficient extraction identifies, literally,
The support outside multiples of \(N\) is proved separately. The constructed integral lift therefore represents the original rational coefficient function. The existing saturation criterion and the proved step-multiple argument give the ideal bound at every order, row, and multiplier. Multiplication by \(j!\) commutes with finite differences, giving precisely the displayed normalization loss.
Exact examples outside the standard window
On this page · Permalink · Source line 190
For \((p,m,j)=(3,2,3)\), the source derives
Consequently,
This attains \(\min(2,2\cdot1)=2\). At the regular address \(j=4\) beyond the singular boundary, the source likewise proves
and applies the universal exponent-two bound to this actual coefficient function.
The earlier no-loss counterexample is retained: \(v_3(C_{6,3}(2)-C_{6,3}(1))=0\). Proving the corrected theorem does not make that false normalized claim true.
Modules. AllRatiosDwork, AllResidueEuler, Theorem75, AllResidueExamples.
5. Verification record and claim boundary
On this page · Permalink · Source line 211
Each local module is rebuilt in a fresh output directory, with warnings treated as errors. A live \#print axioms audit checks every registered declaration, permitting only propext, Classical.choice and Quot.sound, or subsets.
| Required release check | Inventory |
|---|---|
| Local proof modules | 70 |
| Named theorem declarations | 753 |
| Explicit definitions | 148 |
| Expected axiom reports | 901 |
| Pinned dependency revisions | 9 |
| Deliberate invalid-proof controls | 33 |
| Infrastructure and release tests | 235 |
The accompanying JSON verification record, not the existence of this table, determines whether the actual run passed. The final package also includes a fresh-extraction replay record, checksums, the declaration inventory, and the updated manuscript coverage ledger.
The negative controls preserve the earlier rejected false equalities, placeholders, invalid normalizations, and unit pivots. Four new controls demand an extra power in the sharp singular example, remove the factorial loss, misuse a composite base, or center a ratio at the wrong constant. An infrastructure timeout or missing import is not an accepted negative result.
Independent finite checks
On this page · Permalink · Source line 228
The standard-library Python mirror checks 328 complete residue families for primes \(2,3,5,7,11\), including 233 higher-residue families. It checks 4,264 integral unnormalized coefficients, 22,137 normalized and 22,137 unnormalized difference bounds, and 1,640 comparisons with a separately computed ordinary reciprocal. Further checks cover 108 weighted differential iterations, 205 integer Frobenius-square cases and 180 exact Picard agreement prefixes.
These are finite exact-arithmetic checks, not extracted Lean code and not substitutes for the universal formal proofs. The old normalization counterexample and the new sharp exponent-two example remain visible.
Preservation and limitations
On this page · Permalink · Source line 233
All 57 earlier proof modules and the original 28-page status-corrected manuscript are retained unchanged. The new supplement and amendments give the current proof route. Historical failed drafts and interrupted recovery attempts are retained separately from accepted builds. Historical tests that assert an older unfinished status now read that frozen historical status; current tests require the actual unconditional capstone theorem before accepting completion.
The portable Lean and Mathlib versions are pinned. Mathlib's compiled dependency cache is reused, not independently rebuilt. The historical numerical experiment suite and Papers I–VIII are not rerun. The two native conjectures remain unproved. No independent historical-priority assessment is made. Manuscript-to-Lean correspondence remains mathematical review, not a theorem equating natural-language prose with formal types.