KomorebiPaperIV.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.CyclicFilters
7 import KomorebiPaperIV.SectionCycles
8 import KomorebiPaperIV.FormalExponential
9 import KomorebiPaperIV.Appell
10 import KomorebiPaperIV.FiniteAnalytic
11 import KomorebiPaperIV.ReciprocalCore
12 import KomorebiPaperIV.AlgebraicCompletion
13 import KomorebiPaperIV.ThetaCore
14 import KomorebiPaperIV.EarlyCompletion
15 import KomorebiPaperIV.HypergeometricCompletion
16 import KomorebiPaperIV.FiniteModels
17 import KomorebiPaperIV.ReciprocalCompletion
18 import KomorebiPaperIV.ParameterThetaCompletion
19 import KomorebiPaperIV.BellCompletion
20 import KomorebiPaperIV.EntireBridge
21 import KomorebiPaperIV.Wronskians
22 import KomorebiPaperIV.CompanionBridge
23 import KomorebiPaperIV.CompanionCompletion
24 import KomorebiPaperIV.CompanionSpectrum
25 import KomorebiPaperIV.ODESolutions
26 import KomorebiPaperIV.AnalyticCycles
27 import KomorebiPaperIV.ExponentialBounds
28 import KomorebiPaperIV.ZeroGeometry
29 import KomorebiPaperIV.ZeroPerturbation
30 import KomorebiPaperIV.ExponentialRemainder
31 import KomorebiPaperIV.RegularPolygonGap
32 import KomorebiPaperIV.SignedZeroLocalization
33 import KomorebiPaperIV.SignedZeroCorrection
34 import KomorebiPaperIV.SignedSectorConfinement
35 import KomorebiPaperIV.SignedSectorExhaustion
36 import KomorebiPaperIV.SignedGlobalExhaustion
37 import KomorebiPaperIV.SignedZeroOrbits
38 import KomorebiPaperIV.SignedDerivativeAsymptotics
39 import KomorebiPaperIV.SignedDominance
40 import KomorebiPaperIV.SignedFiniteExceptions
41 import KomorebiPaperIV.ReducedEntire
42 import KomorebiPaperIV.ReducedZeros
43 import KomorebiPaperIV.SignedZeroSequence
44 import KomorebiPaperIV.ZeroSequenceAsymptotics
45 import KomorebiPaperIV.ZeroSequenceCounting
46 import KomorebiPaperIV.ReducedCanonicalProduct
47 import KomorebiPaperIV.WeightedZeroCounts
48 import KomorebiPaperIV.ZeroEnumeration
49 import KomorebiPaperIV.FullZeroCounting
50 import KomorebiPaperIV.ReducedZeroCounting
51 import KomorebiPaperIV.FullZeroSummability
52 import KomorebiPaperIV.ZeroZetaConvergence
53 import KomorebiPaperIV.LargeZeroCompletion
54 import KomorebiPaperIV.SignedRealPhase
55 import KomorebiPaperIV.SignedCorrectionCompletion
56 import KomorebiPaperIV.CubicZeroCorrection
57 import KomorebiPaperIV.DerivativeGrowth
58 import KomorebiPaperIV.BranchedDirichlet
59 import KomorebiPaperIV.DerivativeWeightedZeta
60 import KomorebiPaperIV.ExponentialZetaComparison
61 import KomorebiPaperIV.HurwitzLattice
62 import KomorebiPaperIV.ZeroLatticeComparison
63 import KomorebiPaperIV.ZeroZetaDecomposition
64 import KomorebiPaperIV.ZeroZetaContinuation
65 import KomorebiPaperIV.BranchZetaContinuation
66 import KomorebiPaperIV.QuarticExactZeros
67 import KomorebiPaperIV.ExactZetaModels
68 import KomorebiPaperIV.FullCanonicalProduct
69 import KomorebiPaperIV.CanonicalProductMultiplicity
70 import KomorebiPaperIV.CanonicalProductQuotient
71 import KomorebiPaperIV.SublinearExponentialRigidity
72 import KomorebiPaperIV.EntireQuotientGrowth
73 import KomorebiPaperIV.CanonicalProductGrowth
74 import KomorebiPaperIV.HadamardIdentification
75 import KomorebiPaperIV.CanonicalPartialFractions
76 import KomorebiPaperIV.ZeroMomentDerivatives
77 import KomorebiPaperIV.ZeroMomentCoefficients
78 import KomorebiPaperIV.ThetaZeroBell
79 import KomorebiPaperIV.ZeroMomentLogarithm
80 import KomorebiPaperIV.DominantExponential
81 import KomorebiPaperIV.SharpGrowth
82 import KomorebiPaperIV.IndicatorGeometry
83 import KomorebiPaperIV.UniformDominantSectors
84 import KomorebiPaperIV.AlignedExponentialRadii
85 import KomorebiPaperIV.IndicatorLimit
86 import KomorebiPaperIV.SemanticChecks
87 import KomorebiPaperIV.AnalyticTaylorAlgebra
88 import KomorebiPaperIV.AnalyticTaylorDifferential
89 import KomorebiPaperIV.CompleteHomogeneous
90 import KomorebiPaperIV.DiagonalFredholm
91 import KomorebiPaperIV.DiagonalNuclear
92 import KomorebiPaperIV.DiagonalTrace
93 import KomorebiPaperIV.InfiniteSymmetric
94 import KomorebiPaperIV.JensenZeroGrowth
95 import KomorebiPaperIV.LeadingPoleBounds
96 import KomorebiPaperIV.NearestPoleExpansion
97 import KomorebiPaperIV.NormalizedEntire
98 import KomorebiPaperIV.NormalizedExactOrder
99 import KomorebiPaperIV.NormalizedGrowth
100 import KomorebiPaperIV.NormalizedOrder
101 import KomorebiPaperIV.NormalizedProduct
102 import KomorebiPaperIV.NormalizedZeroBell
103 import KomorebiPaperIV.NormalizedAnalyticPowers
104 import KomorebiPaperIV.OrbitPoleReduction
105 import KomorebiPaperIV.PoleCoefficientBounds
106 import KomorebiPaperIV.PoleRemoval
107 import KomorebiPaperIV.PoleTaylor
108 import KomorebiPaperIV.PrincipalPartCoefficients
109 import KomorebiPaperIV.PrincipalPartUniqueness
110 import KomorebiPaperIV.SecantAsymptotic
111 import KomorebiPaperIV.SimplePoleParts
112 import KomorebiPaperIV.SublinearHadamard
113 import KomorebiPaperIV.WeightedGrowthSummability
114 
115 
116 import KomorebiPaperIV.PointwiseFilters
117 import KomorebiPaperIV.PointwiseAddition
118 import KomorebiPaperIV.AnalyticReciprocalLaws
119 import KomorebiPaperIV.OperatorEncodingBridge
120 import KomorebiPaperIV.TangentBoundary
121 import KomorebiPaperIV.CompactReciprocal
122 import KomorebiPaperIV.NewtonDeterminant
123 import KomorebiPaperIV.HypergeometricAnalytic
124 import KomorebiPaperIV.QuotientExponential
125 
126 /-!
127 # Projector-Resolved Seed Calculus IV
128 
129 Formal-power-series, finite root-of-unity and quotient-algebra models,
130 companion-shift identities, reciprocal parameter recurrences, residue-section
131 Appell systems, tangent/Riccati identities, theta polynomials, entire transfer
132 and signed functions, analytic Wronskians, and companion trace formulas. The exact companion spectrum, entire ODE basis, order-two zeros, and quantitative
133 near-cancellation lemma are included. Local positive real simple zero strings for all N >= 3, explicit canonical
134 remainder estimates, and quantitative correction bounds are proved. Exact sector
135 confinement, global exhaustion, rotation and multiplicity identities, disk-index
136 uniqueness, and original-denominator derivative error bounds are included.
137 The reduced entire denominator, finite exceptional sets, named zero sequences,
138 sharp tail summability thresholds, bounded-error tail counting, and an entire
139 canonical tail product are proved. Full multiplicity-weighted counting and
140 convergence exponents, unique global zero strings with derivative asymptotics,
141 and the exact zero-zeta convergence half-planes and holomorphy are now proved.
142 Real leading corrections, alternating derivative signs, the explicit cubic
143 correction, and derivative-weighted zeta convergence/holomorphy are proved.
144 Unweighted Hurwitz continuation with exact poles/residues, branch dependence,
145 and the exact order-two/four models are proved. Jensen and Poisson estimates
146 now prove rigidity of the actual canonical-product quotient, completing
147 Hadamard identification. Sharp maximum-modulus order and type, the full
148 indicator polygon including tie directions, and uniform zero-free dominant
149 sectors are proved. Mittag-Leffler partial fractions, normalized
150 logarithm series, Newton zero sums and their tangent, reciprocal and theta
151 Bell coefficient formulas are proved. The specialized diagonal determinant, complete homogeneous form, normalized-section product/order/Bell identities and nearest-pole asymptotics are now proved. Pointwise filters/addition, Gamma-normalized hypergeometric evaluation, actual quotient-algebra exponential convergence, fixed-logarithm laws, the Newton determinant, compact reciprocal formulas, global Riccati identity and the named operator inverse close the final 15 partial records.
152 -/
153 

Back to source controls