Paper IV · Lean sources

Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Source files 119

Source locations and editions

Files are shown relative to Paper_IV_Verification_Closeout_v1.1.0/formalization/lean/.

Historical editions keep their original paths. Package caches and build files are omitted.

119 files

KomorebiPaperIV.lean
153 lines · 0 declaration locations
AlgebraicCompletion.leanKomorebiPaperIV/
458 lines · 27 declaration locations
AlignedExponentialRadii.leanKomorebiPaperIV/
116 lines · 7 declaration locations
AnalyticCycles.leanKomorebiPaperIV/
96 lines · 6 declaration locations
AnalyticReciprocalLaws.leanKomorebiPaperIV/
123 lines · 11 declaration locations
AnalyticTaylorAlgebra.leanKomorebiPaperIV/
74 lines · 9 declaration locations
AnalyticTaylorDifferential.leanKomorebiPaperIV/
58 lines · 4 declaration locations
Appell.leanKomorebiPaperIV/
155 lines · 13 declaration locations
BellCompletion.leanKomorebiPaperIV/
133 lines · 11 declaration locations
BranchZetaContinuation.leanKomorebiPaperIV/
154 lines · 16 declaration locations
BranchedDirichlet.leanKomorebiPaperIV/
116 lines · 8 declaration locations
CanonicalPartialFractions.leanKomorebiPaperIV/
145 lines · 13 declaration locations
CanonicalProductGrowth.leanKomorebiPaperIV/
122 lines · 7 declaration locations
CanonicalProductMultiplicity.leanKomorebiPaperIV/
137 lines · 13 declaration locations
CanonicalProductQuotient.leanKomorebiPaperIV/
86 lines · 9 declaration locations
CompactReciprocal.leanKomorebiPaperIV/
59 lines · 3 declaration locations
CompanionBridge.leanKomorebiPaperIV/
94 lines · 5 declaration locations
CompanionCompletion.leanKomorebiPaperIV/
174 lines · 10 declaration locations
CompanionSpectrum.leanKomorebiPaperIV/
94 lines · 8 declaration locations
CompleteHomogeneous.leanKomorebiPaperIV/
106 lines · 18 declaration locations
CubicZeroCorrection.leanKomorebiPaperIV/
88 lines · 7 declaration locations
CyclicFilters.leanKomorebiPaperIV/
156 lines · 12 declaration locations
DerivativeGrowth.leanKomorebiPaperIV/
86 lines · 2 declaration locations
DerivativeWeightedZeta.leanKomorebiPaperIV/
170 lines · 18 declaration locations
DiagonalFredholm.leanKomorebiPaperIV/
98 lines · 13 declaration locations
DiagonalNuclear.leanKomorebiPaperIV/
88 lines · 13 declaration locations
DiagonalTrace.leanKomorebiPaperIV/
91 lines · 7 declaration locations
DominantExponential.leanKomorebiPaperIV/
113 lines · 7 declaration locations
EarlyCompletion.leanKomorebiPaperIV/
275 lines · 12 declaration locations
EntireBridge.leanKomorebiPaperIV/
246 lines · 25 declaration locations
EntireQuotientGrowth.leanKomorebiPaperIV/
152 lines · 7 declaration locations
ExactZetaModels.leanKomorebiPaperIV/
220 lines · 13 declaration locations
ExponentialBounds.leanKomorebiPaperIV/
67 lines · 7 declaration locations
ExponentialRemainder.leanKomorebiPaperIV/
137 lines · 9 declaration locations
ExponentialZetaComparison.leanKomorebiPaperIV/
138 lines · 11 declaration locations
FiniteAnalytic.leanKomorebiPaperIV/
178 lines · 10 declaration locations
FiniteModels.leanKomorebiPaperIV/
367 lines · 34 declaration locations
FormalExponential.leanKomorebiPaperIV/
206 lines · 15 declaration locations
FullCanonicalProduct.leanKomorebiPaperIV/
154 lines · 17 declaration locations
FullZeroCounting.leanKomorebiPaperIV/
87 lines · 8 declaration locations
FullZeroSummability.leanKomorebiPaperIV/
171 lines · 14 declaration locations
HadamardIdentification.leanKomorebiPaperIV/
60 lines · 4 declaration locations
HurwitzLattice.leanKomorebiPaperIV/
120 lines · 8 declaration locations
HypergeometricAnalytic.leanKomorebiPaperIV/
136 lines · 9 declaration locations
HypergeometricCompletion.leanKomorebiPaperIV/
204 lines · 10 declaration locations
IndicatorGeometry.leanKomorebiPaperIV/
155 lines · 17 declaration locations
IndicatorLimit.leanKomorebiPaperIV/
123 lines · 7 declaration locations
InfiniteSymmetric.leanKomorebiPaperIV/
137 lines · 14 declaration locations
JensenZeroGrowth.leanKomorebiPaperIV/
86 lines · 5 declaration locations
KernelAudit.leanKomorebiPaperIV/
1221 lines · 0 declaration locations
LargeZeroCompletion.leanKomorebiPaperIV/
142 lines · 4 declaration locations
LeadingPoleBounds.leanKomorebiPaperIV/
106 lines · 9 declaration locations
NearestPoleExpansion.leanKomorebiPaperIV/
81 lines · 3 declaration locations
NewtonDeterminant.leanKomorebiPaperIV/
131 lines · 4 declaration locations
NormalizedAnalyticPowers.leanKomorebiPaperIV/
94 lines · 6 declaration locations
NormalizedEntire.leanKomorebiPaperIV/
113 lines · 9 declaration locations
NormalizedExactOrder.leanKomorebiPaperIV/
115 lines · 5 declaration locations
NormalizedGrowth.leanKomorebiPaperIV/
69 lines · 5 declaration locations
NormalizedOrder.leanKomorebiPaperIV/
61 lines · 1 declaration location
NormalizedProduct.leanKomorebiPaperIV/
44 lines · 3 declaration locations
NormalizedZeroBell.leanKomorebiPaperIV/
62 lines · 4 declaration locations
ODESolutions.leanKomorebiPaperIV/
174 lines · 14 declaration locations
OperatorEncodingBridge.leanKomorebiPaperIV/
57 lines · 4 declaration locations
OrbitPoleReduction.leanKomorebiPaperIV/
76 lines · 5 declaration locations
ParameterThetaCompletion.leanKomorebiPaperIV/
1000 lines · 70 declaration locations
PointwiseAddition.leanKomorebiPaperIV/
71 lines · 4 declaration locations
PointwiseFilters.leanKomorebiPaperIV/
202 lines · 12 declaration locations
PoleCoefficientBounds.leanKomorebiPaperIV/
56 lines · 4 declaration locations
PoleRemoval.leanKomorebiPaperIV/
114 lines · 13 declaration locations
PoleTaylor.leanKomorebiPaperIV/
110 lines · 9 declaration locations
PrincipalPartCoefficients.leanKomorebiPaperIV/
48 lines · 4 declaration locations
PrincipalPartUniqueness.leanKomorebiPaperIV/
78 lines · 3 declaration locations
QuarticExactZeros.leanKomorebiPaperIV/
156 lines · 9 declaration locations
QuotientExponential.leanKomorebiPaperIV/
107 lines · 9 declaration locations
ReciprocalCompletion.leanKomorebiPaperIV/
667 lines · 29 declaration locations
ReciprocalCore.leanKomorebiPaperIV/
254 lines · 28 declaration locations
ReducedCanonicalProduct.leanKomorebiPaperIV/
97 lines · 11 declaration locations
ReducedEntire.leanKomorebiPaperIV/
87 lines · 9 declaration locations
ReducedZeroCounting.leanKomorebiPaperIV/
139 lines · 13 declaration locations
ReducedZeros.leanKomorebiPaperIV/
122 lines · 8 declaration locations
RegularPolygonGap.leanKomorebiPaperIV/
137 lines · 13 declaration locations
SecantAsymptotic.leanKomorebiPaperIV/
136 lines · 14 declaration locations
SectionCycles.leanKomorebiPaperIV/
355 lines · 26 declaration locations
SemanticChecks.leanKomorebiPaperIV/
430 lines · 43 declaration locations
SharpGrowth.leanKomorebiPaperIV/
175 lines · 17 declaration locations
SignedCorrectionCompletion.leanKomorebiPaperIV/
171 lines · 9 declaration locations
SignedDerivativeAsymptotics.leanKomorebiPaperIV/
101 lines · 6 declaration locations
SignedDominance.leanKomorebiPaperIV/
57 lines · 3 declaration locations
SignedFiniteExceptions.leanKomorebiPaperIV/
82 lines · 5 declaration locations
SignedGlobalExhaustion.leanKomorebiPaperIV/
131 lines · 4 declaration locations
SignedRealPhase.leanKomorebiPaperIV/
105 lines · 11 declaration locations
SignedSectorConfinement.leanKomorebiPaperIV/
188 lines · 11 declaration locations
SignedSectorExhaustion.leanKomorebiPaperIV/
125 lines · 4 declaration locations
SignedZeroCorrection.leanKomorebiPaperIV/
90 lines · 7 declaration locations
SignedZeroLocalization.leanKomorebiPaperIV/
339 lines · 16 declaration locations
SignedZeroOrbits.leanKomorebiPaperIV/
121 lines · 6 declaration locations
SignedZeroSequence.leanKomorebiPaperIV/
175 lines · 13 declaration locations
SimplePoleParts.leanKomorebiPaperIV/
111 lines · 7 declaration locations
SublinearExponentialRigidity.leanKomorebiPaperIV/
90 lines · 4 declaration locations
SublinearHadamard.leanKomorebiPaperIV/
54 lines · 1 declaration location
TangentBoundary.leanKomorebiPaperIV/
70 lines · 5 declaration locations
ThetaCore.leanKomorebiPaperIV/
120 lines · 10 declaration locations
ThetaZeroBell.leanKomorebiPaperIV/
70 lines · 5 declaration locations
UniformDominantSectors.leanKomorebiPaperIV/
113 lines · 9 declaration locations
WeightedGrowthSummability.leanKomorebiPaperIV/
94 lines · 3 declaration locations
WeightedZeroCounts.leanKomorebiPaperIV/
96 lines · 13 declaration locations
Wronskians.leanKomorebiPaperIV/
114 lines · 9 declaration locations
ZeroEnumeration.leanKomorebiPaperIV/
166 lines · 9 declaration locations
ZeroGeometry.leanKomorebiPaperIV/
147 lines · 10 declaration locations
ZeroLatticeComparison.leanKomorebiPaperIV/
119 lines · 14 declaration locations
ZeroMomentCoefficients.leanKomorebiPaperIV/
158 lines · 10 declaration locations
ZeroMomentDerivatives.leanKomorebiPaperIV/
85 lines · 7 declaration locations
ZeroMomentLogarithm.leanKomorebiPaperIV/
127 lines · 4 declaration locations
ZeroPerturbation.leanKomorebiPaperIV/
252 lines · 15 declaration locations
ZeroSequenceAsymptotics.leanKomorebiPaperIV/
81 lines · 8 declaration locations
ZeroSequenceCounting.leanKomorebiPaperIV/
84 lines · 4 declaration locations
ZeroZetaContinuation.leanKomorebiPaperIV/
135 lines · 17 declaration locations
ZeroZetaConvergence.leanKomorebiPaperIV/
153 lines · 19 declaration locations
ZeroZetaDecomposition.leanKomorebiPaperIV/
94 lines · 11 declaration locations