16 Formalization ledger for version 1.0.0
On this page · Visual guide: What is evidence, and for what? · Permalink · Source line 2974
The preserved v1.0.0 release was built with Lean 4 v4.34.0-rc2 and Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06 [deMouraUllrich2021], [mathlib2020]. Its 151 theorem-map rows resolve to 1164 unique declarations in the namespace Komorebi.PaperIV: 953 theorem declarations and 211 constructions. The recorded namespace audit scanned 2234 declarations, including 1999 theorem declarations. The historical warning fatal build and supplied kernel audit allowed only propext, Classical.choice, and Quot.sound as standard transitive axioms.
| Manuscript records | Compiled Paper IV scope |
|---|---|
| 3.1–3.3 | Actual holomorphic root filters, convergent coefficient selection, orthogonal resolution, the exact range–covariance characterization, and the complete pointwise cyclic product law. The formal versions hold as well. |
| 4.1–4.5 and 5.1–5.8 | Entire sections, finite exponential formulas, derivative cycles, both Wronskians, and unique entire ODE basis expansions. Both pointwise addition laws and denominator symmetries are checked. The exact ordinary hypergeometric formula follows from the omitted-parameter list, Gamma normalization, and Mathlib's everywhere convergent series. |
| 6.1–6.6 | Quotient-algebra power bases and actual exponential-series convergence in the finite-dimensional coefficient topology. Both pointwise section-coordinate identities. Signed-shift powers, all matrix-exponential entries, group laws and trace are checked. The characteristic polynomial \(X^N+1\), its distinct roots, exact spectrum and determinant one are proved. |
| 7.1–7.8 | Named reciprocal families, exact parameter recurrences, Bell formula, parameter degree and leading coefficient, and polynomial divisibility. Parameter addition holds with any single fixed holomorphic logarithm on the stated domain. Newton's recurrence gives the literal Hessenberg determinant. All three compact reciprocal-polynomial formulas are checked. |
| 8.1–8.5 | The full tangent coefficient series has the exact kappa and factorial normalization, including \(N=1\). Reciprocal differentiation holds on every stated fixed logarithm domain. The actual higher Riccati identity holds at every point where the denominator is nonzero. |
| 9.1–9.10 | Arbitrary-parameter residue reciprocals and their analytic germs, polynomial degree and leading term, sparse Appell laws, joint convolution, monicity and covariance. The Hasse and derivative-truncation encodings are proved equal. The named Appell polynomial satisfies both the forward action and the exact \(\Phi_{N,j}(\partial_x^N)^r\) inverse formula. |
| 10.1–10.4 | Exact formal theta reconstruction, polynomial lift and degree, literal divisibility by \(u\) and, for even \(N\), by \(u+1\), and the theta Newton recurrence with its first coefficient. |
| 11.2, 11.4–11.11 | Two-sided maximum-modulus bounds prove exact order and type. The indicator limsup formula holds in every direction, including ties. Dominant-exponential errors and zero freeness are uniform on compact sets avoiding ties. Near cancellation and the order-two zero set are checked. For \(N\geq3\), gap and remainder bounds, sector confinement, global exhaustion and multiplicity identities give the full large-zero-string theorem. The real leading correction, quadratic exponential error, signed derivative asymptotic, eventual alternating sign and cubic correction are checked. |
| 11.13–11.15 | The reduced series is entire, and \({\mathsf D}_N(z)=\Delta_N(z^N)\) preserves multiplicity away from zero. Finite exceptional sets, eventual positive simple reduced zeros, and their stated displacement are checked, including \(N=2\). Both full disk-counting laws retain all exceptional multiplicities. The full-zero reciprocal sums have exact thresholds \(s>1\) and \(s>1/N\), including boundary divergence. |
| 12.1 | For every \(N\geq2\), the complete multiplicity-indexed product converges uniformly on compact sets and equals \(\Delta_N\). Jensen and Poisson estimates prove rigidity of the actual quotient from derived growth bounds. No growth certificate remains. The original-variable product for \({\mathsf D}_N\) is also checked. |
| 12.2–12.4 | The actual diagonal operator is trace class, with a basis-independent trace and determinant given by limits of actual finite compressions. Infinite complete homogeneous coefficients are limits of finite monomial sums. Every normalized section has exact order \(1/N\). For \(N\geq2\) its full zero product and zero-moment Bell formulas are proved. The actual complex-power germ at zero has the named residue Taylor coefficients. |
| 12.6–12.10 | The normalized logarithm on each zero free disk has the convergent zero-moment series. Its coefficients equal \(\kappa_{N,m}\) and satisfy Newton's recurrence. The Mittag–Leffler tangent expansion converges absolutely and locally uniformly away from poles. Tangent coefficients and the named reciprocal and theta families have their exact zero-moment Bell formulas. The full tangent series is identified with the analytic function. |
| 13.1–13.4 | Analytic division constructs each simple-zero principal part. Its leading coefficient is uniquely determined. Removing the principal parts gives a holomorphic remainder and the exact factorial-scaled Cauchy estimate. Both leading-term errors are bounded, with the first absent for \(r=1\). Rotation gives the orbit-reduced main term. The secant formula holds as a ratio limit, with an exponentially vanishing relative error. |
| 14.2–14.4, 14.6 | The exact all-zero sums retain analytic multiplicity. Their sharp absolute-convergence domains, boundary divergence and local uniform convergence are checked. Both Hurwitz comparisons, entire corrections, global meromorphic continuations, unique simple poles and exact residues are proved. The order-two/four models have identically zero corrections. Branch choices on the finite exceptional part change the continuation by an entire function and preserve its pole and residue. |
| 14.8 | The derivative-weighted series uses every actual simple zero and genuine logarithms with bounded arguments. Absolute and local uniform convergence and an entire sum are proved for \(N\geq3\). For \(N=2\), absolute/local uniform convergence and holomorphy hold on \(\Re s>1\). |
The declaration-level theorem map is authoritative for the preserved v1.0.0 contract. Its release records full scoped coverage of all 68 theorem like records: 68 full, zero partial, and zero unmapped. Rows 143–151 close the final fifteen partial records without altering their statements or assumptions. Imported standard fact 11.1 remains imported. Formal identities, normalized analytic germs, and fixed logarithm domain identities retain their respective stated meanings. Finite computations do not change these proof boundaries.