Paper X · Lean sources

Universal Residual Seeds and Conditional Occupied-System Completion

Declared contract recorded Coverage and evidence

The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.

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

Edit and run in your browser

Source files 272

Source locations and editions

Files are shown relative to current_continuation/lean/.

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

272 files

AbsoluteFrobeniusWitnesses.leanPaperX/
64 lines · 6 declaration locations
AbsoluteGaloisRestriction.leanPaperX/
77 lines · 8 declaration locations
AbsoluteIntegralFrobenius.leanPaperX/
122 lines · 13 declaration locations
AdicIdempotent.leanPaperX/
151 lines · 14 declaration locations
AffineMonodromy.leanPaperX/
85 lines · 28 declaration locations
ArithmeticCertificateExample.leanPaperX/
220 lines · 35 declaration locations
ArithmeticSystemSeparation.leanPaperX/
61 lines · 1 declaration location
AuxiliaryCyclotomicBaseChange.leanPaperX/
117 lines · 7 declaration locations
AuxiliaryCyclotomicDegree.leanPaperX/
59 lines · 3 declaration locations
AuxiliaryCyclotomicDisjoint.leanPaperX/
146 lines · 13 declaration locations
AuxiliaryCyclotomicExistence.leanPaperX/
53 lines · 2 declaration locations
AuxiliaryCyclotomicGeneralBase.leanPaperX/
54 lines · 2 declaration locations
AveragingBoundary.leanPaperX/
45 lines · 7 declaration locations
AveragingCompletion.leanPaperX/
172 lines · 11 declaration locations
AveragingExamples.leanPaperX/
214 lines · 32 declaration locations
BoundaryExamples.leanPaperX/
138 lines · 32 declaration locations
BranchingDimension.leanPaperX/
76 lines · 4 declaration locations
CarrierCompatibility.leanPaperX/
98 lines · 8 declaration locations
CarrierExamples.leanPaperX/
91 lines · 20 declaration locations
CarrierPolynomials.leanPaperX/
121 lines · 7 declaration locations
CarrierSummands.leanPaperX/
149 lines · 22 declaration locations
CertificateBoundary.leanPaperX/
119 lines · 14 declaration locations
CertificateExamples.leanPaperX/
193 lines · 20 declaration locations
CertificateIsomorphisms.leanPaperX/
85 lines · 5 declaration locations
ClassBranchLifting.leanPaperX/
108 lines · 9 declaration locations
ClassCommonSpine.leanPaperX/
88 lines · 3 declaration locations
ClassCompletion.leanPaperX/
69 lines · 6 declaration locations
ClassCompletionExamples.leanPaperX/
68 lines · 5 declaration locations
ClassFramingBoundary.leanPaperX/
83 lines · 15 declaration locations
ClassInvariants.leanPaperX/
103 lines · 15 declaration locations
CofiniteConjugacyCoverage.leanPaperX/
56 lines · 4 declaration locations
Cohomology.leanPaperX/
139 lines · 19 declaration locations
CohomologyExamples.leanPaperX/
154 lines · 20 declaration locations
CommonSpine.leanPaperX/
86 lines · 4 declaration locations
CommutativeLogarithm.leanPaperX/
58 lines · 5 declaration locations
Compactness.leanPaperX/
175 lines · 19 declaration locations
ComparisonCertificates.leanPaperX/
207 lines · 13 declaration locations
CompatibleSystemRigidity.leanPaperX/
75 lines · 6 declaration locations
CompatibleSystemSeparation.leanPaperX/
71 lines · 1 declaration location
CompletionAssembly.leanPaperX/
91 lines · 5 declaration locations
CompletionBoundary.leanPaperX/
111 lines · 11 declaration locations
CompletionExamples.leanPaperX/
104 lines · 18 declaration locations
CompletionObstructions.leanPaperX/
64 lines · 11 declaration locations
ComplexCohomology.leanPaperX/
141 lines · 15 declaration locations
ConditionalArithmeticSpine.leanPaperX/
133 lines · 7 declaration locations
CoprimeClassRepresentative.leanPaperX/
67 lines · 1 declaration location
CornerProjectors.leanPaperX/
95 lines · 2 declaration locations
CountErrorBoundary.leanPaperX/
73 lines · 9 declaration locations
Counting.leanPaperX/
83 lines · 9 declaration locations
CountingBoundaryAtlas.leanPaperX/
112 lines · 16 declaration locations
CountingBoundaryCover.leanPaperX/
101 lines · 8 declaration locations
CountingBoundaryPolar.leanPaperX/
82 lines · 16 declaration locations
CountingBoundaryTransport.leanPaperX/
50 lines · 2 declaration locations
CyclotomicAbsoluteArithmeticSeparation.leanPaperX/
89 lines · 1 declaration location
CyclotomicAbsoluteSamples.leanPaperX/
95 lines · 11 declaration locations
CyclotomicAbsoluteSeparation.leanPaperX/
80 lines · 2 declaration locations
CyclotomicCrossingBoundary.leanPaperX/
67 lines · 6 declaration locations
CyclotomicCrossingContainment.leanPaperX/
65 lines · 4 declaration locations
CyclotomicCrossingCore.leanPaperX/
106 lines · 7 declaration locations
CyclotomicCrossingExistence.leanPaperX/
128 lines · 6 declaration locations
CyclotomicCrossingPair.leanPaperX/
122 lines · 9 declaration locations
CyclotomicFrobeniusPrimes.leanPaperX/
60 lines · 3 declaration locations
CyclotomicInertiaBridge.leanPaperX/
239 lines · 14 declaration locations
CyclotomicIntegralFrobenius.leanPaperX/
177 lines · 11 declaration locations
CyclotomicPoleRigidity.leanPaperX/
91 lines · 4 declaration locations
CyclotomicPrimeCoverage.leanPaperX/
169 lines · 16 declaration locations
CyclotomicSystemSeparation.leanPaperX/
119 lines · 7 declaration locations
DenseTraceSeparation.leanPaperX/
78 lines · 4 declaration locations
DeterminantSpine.leanPaperX/
103 lines · 11 declaration locations
Digits.leanPaperX/
212 lines · 24 declaration locations
DirectedSeeds.leanPaperX/
186 lines · 29 declaration locations
FamilyBoundary.leanPaperX/
152 lines · 24 declaration locations
FamilyClassification.leanPaperX/
41 lines · 1 declaration location
FamilyExamples.leanPaperX/
179 lines · 24 declaration locations
FamilyRigidity.leanPaperX/
169 lines · 13 declaration locations
FamilySummands.leanPaperX/
88 lines · 14 declaration locations
FiniteAvoidanceBoundary.leanPaperX/
90 lines · 19 declaration locations
FiniteCarrierSummands.leanPaperX/
77 lines · 4 declaration locations
FiniteCharacters.leanPaperX/
66 lines · 5 declaration locations
FiniteFiberBranches.leanPaperX/
90 lines · 8 declaration locations
FiniteGroupAveraging.leanPaperX/
141 lines · 10 declaration locations
FiniteLogarithm.leanPaperX/
63 lines · 5 declaration locations
FinitePrimeAvoidance.leanPaperX/
109 lines · 3 declaration locations
FiniteSampleRecovery.leanPaperX/
85 lines · 6 declaration locations
FiniteSeparation.leanPaperX/
97 lines · 8 declaration locations
FormalCharts.leanPaperX/
157 lines · 13 declaration locations
FrobeniusChoiceIndependence.leanPaperX/
56 lines · 3 declaration locations
GaloisComparisonCompletion.leanPaperX/
50 lines · 2 declaration locations
GeneralArithmeticCoverage.leanPaperX/
229 lines · 22 declaration locations
GeneralCharacters.leanPaperX/
110 lines · 6 declaration locations
GeneralLogarithmExamples.leanPaperX/
73 lines · 10 declaration locations
GeneralReconstructionRecovery.leanPaperX/
119 lines · 8 declaration locations
GeneralRecoveryBoundary.leanPaperX/
73 lines · 7 declaration locations
IdealCharacterMellin.leanPaperX/
93 lines · 7 declaration locations
IdealCharacterMellinMeasurable.leanPaperX/
41 lines · 2 declaration locations
IdealCharacterMellinPole.leanPaperX/
33 lines · 1 declaration location
IdealClassCharacterBound.leanPaperX/
80 lines · 6 declaration locations
IdealClassCharacterSum.leanPaperX/
77 lines · 4 declaration locations
IdealClassQuantitativeAttachment.leanPaperX/
103 lines · 9 declaration locations
IdealClassQuantitativeConstant.leanPaperX/
62 lines · 5 declaration locations
IdealClassQuantitativeGeometry.leanPaperX/
48 lines · 4 declaration locations
IdealClassQuantitativeTheorem.leanPaperX/
58 lines · 3 declaration locations
IdealClassQuantitativeTransfer.leanPaperX/
115 lines · 6 declaration locations
IdealNormCharacterBound.leanPaperX/
93 lines · 3 declaration locations
IdealNormCharacterMellin.leanPaperX/
50 lines · 3 declaration locations
IdealNormFilterAttachment.leanPaperX/
135 lines · 7 declaration locations
IdealNormWeightedAttachment.leanPaperX/
160 lines · 15 declaration locations
IdealResidueUnitAction.leanPaperX/
106 lines · 7 declaration locations
IdealResidueUnitActionMean.leanPaperX/
80 lines · 6 declaration locations
IdempotentNewton.leanPaperX/
75 lines · 7 declaration locations
IndexedExistenceBoundary.leanPaperX/
51 lines · 1 declaration location
IntegerCellBounds.leanPaperX/
123 lines · 12 declaration locations
IntegerCellChartCounting.leanPaperX/
101 lines · 5 declaration locations
IntegerCellFiniteCharts.leanPaperX/
62 lines · 3 declaration locations
IntegralActionSpan.leanPaperX/
182 lines · 9 declaration locations
IntegralCharts.leanPaperX/
140 lines · 15 declaration locations
InverseLimitLocalConditions.leanPaperX/
147 lines · 12 declaration locations
IrreducibleCharacterRigidity.leanPaperX/
93 lines · 4 declaration locations
JointOccupancy.leanPaperX/
155 lines · 20 declaration locations
LatticeCountingDiscrepancy.leanPaperX/
84 lines · 9 declaration locations
LatticeCountingFull.leanPaperX/
79 lines · 3 declaration locations
LatticeCountingGrid.leanPaperX/
122 lines · 10 declaration locations
LatticeCountingInterface.leanPaperX/
54 lines · 6 declaration locations
LatticeCountingTransport.leanPaperX/
72 lines · 6 declaration locations
LocalComparisonCompletion.leanPaperX/
107 lines · 2 declaration locations
LogarithmTruncation.leanPaperX/
120 lines · 9 declaration locations
LogarithmicRecovery.leanPaperX/
124 lines · 11 declaration locations
MatrixProjector.leanPaperX/
137 lines · 21 declaration locations
MatrixSpanBound.leanPaperX/
196 lines · 9 declaration locations
MatrixSpanCompletion.leanPaperX/
84 lines · 3 declaration locations
MatrixSpanExamples.leanPaperX/
214 lines · 22 declaration locations
MatrixWitnessLimits.leanPaperX/
105 lines · 9 declaration locations
MonodromyData.leanPaperX/
119 lines · 18 declaration locations
MonodromyExamples.leanPaperX/
81 lines · 10 declaration locations
MonodromyKernels.leanPaperX/
74 lines · 7 declaration locations
MonodromyReconstruction.leanPaperX/
119 lines · 16 declaration locations
NilpotentExponential.leanPaperX/
90 lines · 12 declaration locations
NilpotentLogarithm.leanPaperX/
71 lines · 5 declaration locations
NilpotentSeries.leanPaperX/
56 lines · 6 declaration locations
NormResidueAlgebra.leanPaperX/
70 lines · 9 declaration locations
NormResidueArithmetic.leanPaperX/
85 lines · 9 declaration locations
NormResidueAutomaticCounting.leanPaperX/
63 lines · 3 declaration locations
NormResidueAutomaticPole.leanPaperX/
48 lines · 1 declaration location
NormResidueBoundary.leanPaperX/
29 lines · 3 declaration locations
NormResidueCharacter.leanPaperX/
74 lines · 5 declaration locations
NormResidueCharacterCounting.leanPaperX/
72 lines · 4 declaration locations
NormResidueCoprimeRepresentative.leanPaperX/
87 lines · 2 declaration locations
NormResidueExactScalarCriterion.leanPaperX/
78 lines · 3 declaration locations
NormResidueGeneratorAttachment.leanPaperX/
71 lines · 5 declaration locations
NormResidueGeneratorSum.leanPaperX/
62 lines · 4 declaration locations
NormResidueIdealFilter.leanPaperX/
78 lines · 9 declaration locations
NormResidueLatticeMap.leanPaperX/
65 lines · 7 declaration locations
NormResidueMellinAttachment.leanPaperX/
63 lines · 3 declaration locations
NormResidueMellinPole.leanPaperX/
50 lines · 1 declaration location
NormResidueRepresentative.leanPaperX/
50 lines · 2 declaration locations
NormResidueScalarCounting.leanPaperX/
51 lines · 2 declaration locations
NormResidueScalarObstruction.leanPaperX/
42 lines · 1 declaration location
NormResidueScalarPower.leanPaperX/
56 lines · 2 declaration locations
NormResidueScalarWitness.leanPaperX/
94 lines · 5 declaration locations
NormResidueTotientWitness.leanPaperX/
62 lines · 2 declaration locations
NormResidueUnitCounting.leanPaperX/
66 lines · 4 declaration locations
NormResidueWeightedCounting.leanPaperX/
79 lines · 4 declaration locations
NormSignArithmetic.leanPaperX/
70 lines · 6 declaration locations
NormSignDilation.leanPaperX/
72 lines · 7 declaration locations
NormSignFormula.leanPaperX/
81 lines · 5 declaration locations
NormSignGeometry.leanPaperX/
98 lines · 11 declaration locations
NormSignPartition.leanPaperX/
85 lines · 8 declaration locations
NormSignResidueCounting.leanPaperX/
79 lines · 7 declaration locations
NumberFieldFrobeniusRestriction.leanPaperX/
117 lines · 6 declaration locations
NumberFieldPrimeRestriction.leanPaperX/
92 lines · 14 declaration locations
NumberFieldWitnessIndependence.leanPaperX/
67 lines · 4 declaration locations
OccupancyBoundary.leanPaperX/
75 lines · 14 declaration locations
OccupancyExamples.leanPaperX/
128 lines · 20 declaration locations
OccupancyTransport.leanPaperX/
71 lines · 4 declaration locations
OrderPrecision.leanPaperX/
81 lines · 6 declaration locations
OrthogonalLifting.leanPaperX/
132 lines · 3 declaration locations
OrthogonalPartial.leanPaperX/
102 lines · 11 declaration locations
OrthogonalProjectors.leanPaperX/
42 lines · 3 declaration locations
PacketCohomology.leanPaperX/
203 lines · 17 declaration locations
PacketNaturality.leanPaperX/
55 lines · 3 declaration locations
PadicQuadraticSplitting.leanPaperX/
123 lines · 9 declaration locations
PrecisionAveraging.leanPaperX/
175 lines · 6 declaration locations
PrecisionBoundary.leanPaperX/
62 lines · 7 declaration locations
PrecisionCompletion.leanPaperX/
164 lines · 8 declaration locations
PrecisionExamples.leanPaperX/
260 lines · 36 declaration locations
PrecisionIdempotent.leanPaperX/
37 lines · 1 declaration location
PrimeDegreeFieldFrobenius.leanPaperX/
101 lines · 10 declaration locations
PrimeDegreeSummability.leanPaperX/
175 lines · 18 declaration locations
PrimeDegreeSummabilityFrobenius.leanPaperX/
67 lines · 4 declaration locations
PrimeDegreeSummabilityTower.leanPaperX/
71 lines · 5 declaration locations
PrimeDegreeUnramifiedFrobenius.leanPaperX/
85 lines · 5 declaration locations
PrimitiveMatrix.leanPaperX/
129 lines · 5 declaration locations
ProfiniteSeparation.leanPaperX/
45 lines · 3 declaration locations
ProjectorSummands.leanPaperX/
119 lines · 19 declaration locations
QuadraticAlgebra.leanPaperX/
86 lines · 16 declaration locations
QuadraticArithmeticCompletion.leanPaperX/
144 lines · 18 declaration locations
QuadraticCharacters.leanPaperX/
96 lines · 14 declaration locations
QuadraticGalois.leanPaperX/
96 lines · 14 declaration locations
QuadraticGaloisInertia.leanPaperX/
64 lines · 7 declaration locations
QuadraticGaloisPackets.leanPaperX/
149 lines · 23 declaration locations
QuadraticLocalArithmetic.leanPaperX/
120 lines · 13 declaration locations
QuadraticLocalCompletion.leanPaperX/
117 lines · 8 declaration locations
QuadraticLocalGalois.leanPaperX/
122 lines · 14 declaration locations
QuadraticLocalPackets.leanPaperX/
93 lines · 12 declaration locations
QuadraticPacketBoundary.leanPaperX/
67 lines · 12 declaration locations
QuadraticPadicInertia.leanPaperX/
63 lines · 7 declaration locations
QuadraticRootCompletion.leanPaperX/
167 lines · 21 declaration locations
QuadraticValuationInertia.leanPaperX/
80 lines · 7 declaration locations
RayCountingGeometry.leanPaperX/
134 lines · 11 declaration locations
RayCountingUnits.leanPaperX/
136 lines · 21 declaration locations
RealAxisEndpointIntegral.leanPaperX/
99 lines · 7 declaration locations
RealAxisMellinMoment.leanPaperX/
99 lines · 5 declaration locations
RealAxisMellinPole.leanPaperX/
35 lines · 2 declaration locations
RealAxisPoleBoundary.leanPaperX/
70 lines · 9 declaration locations
RealAxisPoleRigidity.leanPaperX/
120 lines · 5 declaration locations
Reconstruction.leanPaperX/
189 lines · 19 declaration locations
ReconstructionBoundary.leanPaperX/
64 lines · 11 declaration locations
ReconstructionExamples.leanPaperX/
80 lines · 13 declaration locations
ReconstructionLocal.leanPaperX/
46 lines · 5 declaration locations
ReconstructionRecovery.leanPaperX/
90 lines · 5 declaration locations
ReconstructionSummands.leanPaperX/
74 lines · 9 declaration locations
ReconstructionTopology.leanPaperX/
60 lines · 3 declaration locations
RepresentationClasses.leanPaperX/
132 lines · 24 declaration locations
RepresentationForests.leanPaperX/
118 lines · 12 declaration locations
RepresentationLimits.leanPaperX/
193 lines · 28 declaration locations
RepresentationTopology.leanPaperX/
124 lines · 11 declaration locations
RequiredPacketBoundary.leanPaperX/
82 lines · 13 declaration locations
RequiredPacketOccupancy.leanPaperX/
164 lines · 19 declaration locations
Residual.leanPaperX/
101 lines · 18 declaration locations
ResidueLatticeFibers.leanPaperX/
101 lines · 10 declaration locations
ResidueLatticeIdeal.leanPaperX/
56 lines · 5 declaration locations
ResidueLatticeIdealPoints.leanPaperX/
80 lines · 7 declaration locations
ResidueLatticeIdealWeights.leanPaperX/
36 lines · 4 declaration locations
ResidueLatticeNormCounts.leanPaperX/
67 lines · 6 declaration locations
ResidueLatticePointSums.leanPaperX/
77 lines · 6 declaration locations
ResidueLatticeWeights.leanPaperX/
97 lines · 8 declaration locations
RestrictionEmbeddingConjugacy.leanPaperX/
55 lines · 7 declaration locations
SeedBoundary.leanPaperX/
98 lines · 12 declaration locations
SeedCertificates.leanPaperX/
82 lines · 11 declaration locations
SeedConsequences.leanPaperX/
96 lines · 7 declaration locations
SeedExamples.leanPaperX/
108 lines · 26 declaration locations
SeparationForcesCoverage.leanPaperX/
90 lines · 5 declaration locations
SimpleModuleSeparation.leanPaperX/
104 lines · 7 declaration locations
Singular.leanPaperX/
101 lines · 10 declaration locations
SingularZeta.leanPaperX/
97 lines · 11 declaration locations
SmoothMaps.leanPaperX/
171 lines · 16 declaration locations
SmoothModels.leanPaperX/
92 lines · 8 declaration locations
SpecialMonodromy.leanPaperX/
165 lines · 16 declaration locations
SpectralProjectors.leanPaperX/
124 lines · 17 declaration locations
SpineCompletionBoundary.leanPaperX/
127 lines · 15 declaration locations
SpineExistenceCriterion.leanPaperX/
155 lines · 6 declaration locations
SplitTemplateRigidity.leanPaperX/
34 lines · 1 declaration location
SummandBoundary.leanPaperX/
141 lines · 18 declaration locations
SummandExamples.leanPaperX/
57 lines · 3 declaration locations
SurjectivePullbackBoundary.leanPaperX/
95 lines · 13 declaration locations
SurjectiveRepresentationPullback.leanPaperX/
116 lines · 12 declaration locations
SystemCompletion.leanPaperX/
82 lines · 6 declaration locations
TraceBoundaries.leanPaperX/
53 lines · 10 declaration locations
TraceExamples.leanPaperX/
123 lines · 29 declaration locations
TraceRecovery.leanPaperX/
96 lines · 11 declaration locations
UnipotentLogarithm.leanPaperX/
165 lines · 22 declaration locations
UnramifiedFrobeniusUniqueness.leanPaperX/
150 lines · 13 declaration locations
WeakCoverageBoundary.leanPaperX/
166 lines · 24 declaration locations
WeilCopies.leanPaperX/
82 lines · 8 declaration locations
WeilData.leanPaperX/
107 lines · 17 declaration locations
WeilEuler.leanPaperX/
61 lines · 7 declaration locations
WeilExamples.leanPaperX/
153 lines · 34 declaration locations
WeilMorphisms.leanPaperX/
83 lines · 8 declaration locations
WeilSmooth.leanPaperX/
71 lines · 5 declaration locations
WeilSpecialChain.leanPaperX/
124 lines · 13 declaration locations
Zeta.leanPaperX/
130 lines · 14 declaration locations
ScalarWitnessAttempt.lean
94 lines · 5 declaration locations