Paper XI · Lean source

PaperXI.lean

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.

Local imports (423)

PaperXI.lean423 lines

Original source pathformalization/PaperXI.lean

Skip source text

1 import PaperXI.AbstractHeisenberg
2 import PaperXI.AbstractHeisenbergExtension
3 import PaperXI.ActualCartanCandidate106
4 import PaperXI.ActualCharacterCandidate108
5 import PaperXI.ActualCharacterData108
6 import PaperXI.ActualCharacterIdentification61
7 import PaperXI.ActualCharacterResidue61
8 import PaperXI.ActualCharacterType61
9 import PaperXI.ActualCompactTypeCompletion58
10 import PaperXI.ActualCoordinateDeepIdeal111
11 import PaperXI.ActualCuspidalCandidate105
12 import PaperXI.ActualDepthZeroExtension
13 import PaperXI.ActualELatticeFieldJoin59
14 import PaperXI.ActualELatticeFreeness59
15 import PaperXI.ActualELatticeNormalizer59
16 import PaperXI.ActualELatticeQuotient59
17 import PaperXI.ActualELatticeResidue59
18 import PaperXI.ActualELatticeScalarPeriod60
19 import PaperXI.ActualELatticeTopology60
20 import PaperXI.ActualELatticeTypeGroup59
21 import PaperXI.ActualEmbeddedUniformizer58
22 import PaperXI.ActualFieldTypeQuotient69
23 import PaperXI.ActualGroupIndex111
24 import PaperXI.ActualHeisenbergCandidate107
25 import PaperXI.ActualIntegerTower111
26 import PaperXI.ActualIntegralGeneralLinear
27 import PaperXI.ActualIntersection108
28 import PaperXI.ActualLocalCartan106
29 import PaperXI.ActualLocalUnitDecomposition
30 import PaperXI.ActualLocalUnitTopology
31 import PaperXI.ActualNormalizerTypeExtension58
32 import PaperXI.ActualOnePlusTopology111
33 import PaperXI.ActualPacketTypeRealization70
34 import PaperXI.ActualProfileCandidate110
35 import PaperXI.ActualResidueGeneralLinear
36 import PaperXI.ActualScalarLift113
37 import PaperXI.ActualSourceCandidate111
38 import PaperXI.ActualUnramifiedBaseChange
39 import PaperXI.AlgebraActionModule
40 import PaperXI.ArithmeticAttachment110
41 import PaperXI.ArithmeticFieldInduction69
42 import PaperXI.ArithmeticTypeCertificate69
43 import PaperXI.AtomicMultiset
44 import PaperXI.AtomicNaturality
45 import PaperXI.AtomicReconstruction
46 import PaperXI.BilinearHeisenberg
47 import PaperXI.BoundaryExamples
48 import PaperXI.BreakBridge
49 import PaperXI.BreakBridgeAlong
50 import PaperXI.BreakDyadicPhase
51 import PaperXI.BreakHeisenbergSum
52 import PaperXI.BreakMoving
53 import PaperXI.BreakOddPhase
54 import PaperXI.BreakQuadratic
55 import PaperXI.BreakTensorFactorization
56 import PaperXI.BreakTensorMap
57 import PaperXI.CanonicalDVRValuation
58 import PaperXI.CentralCharacterAction
59 import PaperXI.CentralCharacterInduction
60 import PaperXI.CentralCharacterIrreducible
61 import PaperXI.CentralCharacterRepresentation
62 import PaperXI.CentralExtension
63 import PaperXI.CentralExtensionCocycle
64 import PaperXI.CentralExtensionComparison
65 import PaperXI.CentralExtensionExistence
66 import PaperXI.CentralExtensionInducing
67 import PaperXI.CentralExtensionInductionConsequences
68 import PaperXI.CentralExtensionSectionChange
69 import PaperXI.CentralExtensionStructure
70 import PaperXI.CentralExtensionUniqueness
71 import PaperXI.CentralProduct
72 import PaperXI.CentralProductCommutator
73 import PaperXI.CentralProductComparison
74 import PaperXI.CentralProductFactors
75 import PaperXI.CentralProductMap
76 import PaperXI.ChainSharpness
77 import PaperXI.CharacterAttachment108
78 import PaperXI.CharacterGenerators
79 import PaperXI.CharacterNormalizer61
80 import PaperXI.CharacterPairing108
81 import PaperXI.CharacterProjector
82 import PaperXI.CharacterSupport108
83 import PaperXI.CharacterTwist
84 import PaperXI.CliffordAction
85 import PaperXI.CliffordChoices
86 import PaperXI.CliffordCocycle
87 import PaperXI.CliffordCocycleChoices
88 import PaperXI.CliffordCocycleClass
89 import PaperXI.CliffordDatum
90 import PaperXI.CliffordEnvelope
91 import PaperXI.CliffordEvaluation
92 import PaperXI.CliffordHeisenbergAttachment
93 import PaperXI.CliffordIrreducible
94 import PaperXI.CliffordMultiplicity
95 import PaperXI.CliffordPacket
96 import PaperXI.CliffordSource
97 import PaperXI.CliffordStabilizer
98 import PaperXI.CliffordTransport
99 import PaperXI.CocycleBasis
100 import PaperXI.CocycleClass
101 import PaperXI.CocycleCommutator
102 import PaperXI.CocycleQuotient
103 import PaperXI.CommutatorEnvelope
104 import PaperXI.CompactDegreeSeparation
105 import PaperXI.CompactIntersection108
106 import PaperXI.CompactModCenterInduction68
107 import PaperXI.CompactQuotientPeriod69
108 import PaperXI.CompactSmoothSemisimple
109 import PaperXI.CompactTypeTensor58
110 import PaperXI.CompactTypeTensorNormalizer58
111 import PaperXI.ConditionalAtomicComparison
112 import PaperXI.ConstructedFieldFrobenius
113 import PaperXI.ContinuousHolonomyResidual
114 import PaperXI.CoordinateDeepIdeal111
115 import PaperXI.CuspidalAnnihilation
116 import PaperXI.CuspidalCartan105
117 import PaperXI.CuspidalContraction105
118 import PaperXI.CycleCoordinates
119 import PaperXI.CycleFixed
120 import PaperXI.CycleSpan
121 import PaperXI.CyclicAction
122 import PaperXI.CyclicBridge
123 import PaperXI.CyclicDefect113
124 import PaperXI.CyclicFrobeniusCount
125 import PaperXI.CyclicInducedBasis
126 import PaperXI.CyclicInducedCharacter
127 import PaperXI.CyclicInducedCoordinates
128 import PaperXI.CyclicInducedDegree
129 import PaperXI.CyclicInducedWrap
130 import PaperXI.CyclicLinearization
131 import PaperXI.CyclicNormalization113
132 import PaperXI.CyclicPolynomial
133 import PaperXI.DVRCartan106
134 import PaperXI.DegreeIndex110
135 import PaperXI.DerivedCentralCharacter69
136 import PaperXI.DiscrepancyCharacter
137 import PaperXI.DualCharacterSums
138 import PaperXI.DualityLinear
139 import PaperXI.DyadicAbstract
140 import PaperXI.DyadicAbstractOrthogonal
141 import PaperXI.DyadicAffine
142 import PaperXI.DyadicBasis
143 import PaperXI.DyadicBasisConsequences
144 import PaperXI.DyadicBasisCounts
145 import PaperXI.DyadicCoordinates
146 import PaperXI.DyadicCounts
147 import PaperXI.DyadicDimension
148 import PaperXI.DyadicExtensionClass
149 import PaperXI.DyadicGauss
150 import PaperXI.DyadicHeisenbergLift
151 import PaperXI.DyadicIsometry
152 import PaperXI.DyadicOrthogonal
153 import PaperXI.DyadicRefinement
154 import PaperXI.DyadicRefinementCounts
155 import PaperXI.DyadicTorsor
156 import PaperXI.DyadicTranslation
157 import PaperXI.ElementaryEnvelope
158 import PaperXI.ElementaryEnvelopeForm
159 import PaperXI.ElementaryEnvelopeTransport
160 import PaperXI.EquivariantRepresentation113
161 import PaperXI.EquivariantSplitting68
162 import PaperXI.FiniteAverage
163 import PaperXI.FiniteBreakAssembly
164 import PaperXI.FiniteFieldAverage
165 import PaperXI.FiniteFieldOrbitCount
166 import PaperXI.FiniteFreeCompletion
167 import PaperXI.FiniteFunctionAverage
168 import PaperXI.FiniteIntersectionCriterion108
169 import PaperXI.FiniteJointQuotient108
170 import PaperXI.FiniteOrbitAverage68
171 import PaperXI.FiniteProductDeterminant
172 import PaperXI.FiniteProfileBridge109
173 import PaperXI.FiniteRepresentation
174 import PaperXI.FiniteResidueBaseChange
175 import PaperXI.FiniteResidueSubgroup
176 import PaperXI.FiniteTameComparison
177 import PaperXI.FiniteTensor
178 import PaperXI.FiniteUnramifiedWeil
179 import PaperXI.FixedMoving
180 import PaperXI.FixedMovingSource
181 import PaperXI.FourierCovariance
182 import PaperXI.FourierPackets
183 import PaperXI.FourierProjectors
184 import PaperXI.FractionMatrix106
185 import PaperXI.FreeLatticeCard110
186 import PaperXI.FrobeniusOrbit
187 import PaperXI.FrobeniusPeriod
188 import PaperXI.FrobeniusPeriodCount
189 import PaperXI.FullBridgeTransport
190 import PaperXI.FullIntertwiningLocus69
191 import PaperXI.FullTypeIntertwining105
192 import PaperXI.GallagherTensorIrreducibility58
193 import PaperXI.GaussCharacters
194 import PaperXI.GaussSums
195 import PaperXI.GeneralChain
196 import PaperXI.GeneratedIrreducibility
197 import PaperXI.GlobalHeisenbergBridge112
198 import PaperXI.GluedPacketSections
199 import PaperXI.GraphChordCharacters
200 import PaperXI.GraphGauge
201 import PaperXI.GraphLoop
202 import PaperXI.GraphLoopRepresentation
203 import PaperXI.GraphResidual
204 import PaperXI.GraphTransport
205 import PaperXI.GraphTree
206 import PaperXI.GraphTreePaths
207 import PaperXI.GroupFixed
208 import PaperXI.HeisenbergCardinality
209 import PaperXI.HeisenbergCenter
210 import PaperXI.HeisenbergCharacterProfile111
211 import PaperXI.HeisenbergCochain
212 import PaperXI.HeisenbergComparison
213 import PaperXI.HeisenbergDimension
214 import PaperXI.HeisenbergFinite
215 import PaperXI.HeisenbergForm
216 import PaperXI.HeisenbergFrequency
217 import PaperXI.HeisenbergGeometry
218 import PaperXI.HeisenbergGroup
219 import PaperXI.HeisenbergNormalForm
220 import PaperXI.HeisenbergPrime
221 import PaperXI.HeisenbergProjector
222 import PaperXI.HeisenbergReduction107
223 import PaperXI.HeisenbergRepresentation
224 import PaperXI.HeisenbergSelector
225 import PaperXI.HeisenbergSource
226 import PaperXI.HeisenbergSourceProjector
227 import PaperXI.HeisenbergTensor
228 import PaperXI.HeisenbergTensorComparison
229 import PaperXI.HeisenbergTensorFactorization
230 import PaperXI.HeisenbergTrace108
231 import PaperXI.HeisenbergTransport
232 import PaperXI.HenselianConductorTransport
233 import PaperXI.HenselianFieldLift
234 import PaperXI.HenselianGaloisResidue
235 import PaperXI.HenselianLiftTower
236 import PaperXI.HenselianResidueLift
237 import PaperXI.HenselianWeilAttachment
238 import PaperXI.HolonomyResidual
239 import PaperXI.HyperbolicDeterminant
240 import PaperXI.HyperbolicPhase
241 import PaperXI.HyperbolicSpace
242 import PaperXI.InducedClassification
243 import PaperXI.InducedCycleInvariants
244 import PaperXI.InducedDual
245 import PaperXI.InducedTameProfile
246 import PaperXI.InducedTwist
247 import PaperXI.InducedTypeSpace68
248 import PaperXI.InductionIrreducibility
249 import PaperXI.InertiaFixed
250 import PaperXI.InertiaQuotient
251 import PaperXI.IntegerRingComparison
252 import PaperXI.InteractionPolynomial
253 import PaperXI.IntersectionModel108
254 import PaperXI.IntertwiningAlong105
255 import PaperXI.IntertwiningSpace107
256 import PaperXI.InvariantAssembly
257 import PaperXI.InvariantPolynomial
258 import PaperXI.IsotypicEvaluation
259 import PaperXI.LatticeCongruenceTopology60
260 import PaperXI.LatticeMatrixTopology60
261 import PaperXI.LiftedEtale
262 import PaperXI.LiftedFullResidue
263 import PaperXI.LiftedResidueDegree
264 import PaperXI.LiftedResidueFrobenius
265 import PaperXI.LiftedValuationFinite
266 import PaperXI.LiftedValuationInertia
267 import PaperXI.LineCharacter
268 import PaperXI.LocalFactorIdentification
269 import PaperXI.LocalFieldResidueExtension
270 import PaperXI.LocalResidueRank
271 import PaperXI.LocallyFiniteSemisimple
272 import PaperXI.MonicResidueAlgebra
273 import PaperXI.MonodromyAtom
274 import PaperXI.MonodromyChain
275 import PaperXI.MonomialAction
276 import PaperXI.MonomialDual
277 import PaperXI.MonomialInduction
278 import PaperXI.MonomialInductionSubgroup
279 import PaperXI.MonomialInductionTransitive
280 import PaperXI.MonomialOrbit
281 import PaperXI.MoritaActualCartan110
282 import PaperXI.MoritaCartanTransport110
283 import PaperXI.MoritaCornerRank110
284 import PaperXI.MoritaEndomorphismCoordinates111
285 import PaperXI.MoritaIndex110
286 import PaperXI.MoritaLattice110
287 import PaperXI.MoritaPairIndex110
288 import PaperXI.MoritaQuotient110
289 import PaperXI.MoritaRadicalDictionary110
290 import PaperXI.MoritaScalarUpgrade110
291 import PaperXI.MoritaUniformizer110
292 import PaperXI.MovingPhase
293 import PaperXI.NormalInertia
294 import PaperXI.NormalizedFrobeniusQuotient
295 import PaperXI.NormalizerDictionary110
296 import PaperXI.NormalizerExtensionInducing58
297 import PaperXI.NormalizerIntertwining60
298 import PaperXI.OddEnvelopeHeisenberg
299 import PaperXI.OddPhase
300 import PaperXI.OddPhaseCertificate
301 import PaperXI.OddPhaseSum
302 import PaperXI.OddPhaseTransport
303 import PaperXI.OddSymplectic
304 import PaperXI.OnePlusIndex110
305 import PaperXI.OnePlusIntersection110
306 import PaperXI.OpenSubgroupSmoothInduction
307 import PaperXI.OrbitSpan
308 import PaperXI.OrthogonalPhase
309 import PaperXI.OrthogonalSummands
310 import PaperXI.PacketBasis
311 import PaperXI.PacketCycle
312 import PaperXI.PacketLines
313 import PaperXI.PacketReturn
314 import PaperXI.PacketSupport
315 import PaperXI.PacketTransport
316 import PaperXI.PacketTypeAttachment70
317 import PaperXI.PairIndex110
318 import PaperXI.PeriodicLatticeReduction60
319 import PaperXI.PiPolynomial
320 import PaperXI.PolynomialAssembly
321 import PaperXI.PrescribedFieldType70
322 import PaperXI.PrimitiveCharacterBlock
323 import PaperXI.ProductNormalizerQuotient59
324 import PaperXI.ProjectiveCocycle
325 import PaperXI.ProjectiveHolonomy
326 import PaperXI.ProjectorTransport
327 import PaperXI.QuotientRepresentation
328 import PaperXI.RadicalOnePlus111
329 import PaperXI.RamificationPolyphase
330 import PaperXI.RamificationPolyphaseBaseChange
331 import PaperXI.RamificationPolyphaseDimensions
332 import PaperXI.RamificationSeparation
333 import PaperXI.RamifiedUnramifiedQuotient
334 import PaperXI.RankOneEulerFactor
335 import PaperXI.RankOneSourceCandidate110
336 import PaperXI.RegularCyclic
337 import PaperXI.RepresentationGraph
338 import PaperXI.RepresentationStability
339 import PaperXI.ResidueDegreeBaseChange
340 import PaperXI.ResidueExtensionRealization
341 import PaperXI.ResidueFrobeniusAttachment
342 import PaperXI.ResidueRestriction107
343 import PaperXI.ResidueWeil
344 import PaperXI.RestrictedHeisenbergBridge
345 import PaperXI.ScalarCocycle112
346 import PaperXI.ScalarCovariance
347 import PaperXI.ScalarGluing
348 import PaperXI.ScalarHolonomy
349 import PaperXI.ScalarRepresentation112
350 import PaperXI.SchrodingerConsequences
351 import PaperXI.SchrodingerFourier
352 import PaperXI.SchrodingerIrreducible
353 import PaperXI.SchrodingerOperator
354 import PaperXI.SchrodingerSeparation
355 import PaperXI.SchrodingerTrace
356 import PaperXI.SchrodingerUnitary
357 import PaperXI.SchrodingerUniversal
358 import PaperXI.SchurHom
359 import PaperXI.SchurScalar
360 import PaperXI.SemisimpleDetection
361 import PaperXI.SemisimpleProjection
362 import PaperXI.SimpleModuleClassification
363 import PaperXI.SmithMatrix106
364 import PaperXI.SmoothDegreeQuotient
365 import PaperXI.SmoothHomOrbit68
366 import PaperXI.SpectralGeometricFrobenius
367 import PaperXI.SpectralLocalField
368 import PaperXI.SplitRadical105
369 import PaperXI.SymplecticAssembly
370 import PaperXI.SymplecticCentralExtension
371 import PaperXI.SymplecticCoordinates
372 import PaperXI.SymplecticHeisenbergUniqueness
373 import PaperXI.SymplecticSplit
374 import PaperXI.TameConductor
375 import PaperXI.TameDegree
376 import PaperXI.TameExponent
377 import PaperXI.TameGaussNaturality
378 import PaperXI.TameHomCriterion
379 import PaperXI.TameNorm
380 import PaperXI.TameNormPacket
381 import PaperXI.TameOrbitTransitivity
382 import PaperXI.TameProjectors
383 import PaperXI.TameTensorInduction
384 import PaperXI.TameTensorOrbits
385 import PaperXI.TameTensorPackets
386 import PaperXI.TameTensorSource
387 import PaperXI.TensorFixed
388 import PaperXI.TensorIntertwining107
389 import PaperXI.TensorIrreducible
390 import PaperXI.TensorPolynomial
391 import PaperXI.TensorSlices107
392 import PaperXI.TensorSubspace
393 import PaperXI.TensorTypeOperators70
394 import PaperXI.TraceDiscrepancy
395 import PaperXI.TranslationAverage
396 import PaperXI.TwistedAction
397 import PaperXI.TwistedActionEquivalence
398 import PaperXI.TwistedAlgebra
399 import PaperXI.TwistedMatrix
400 import PaperXI.TwistedModules
401 import PaperXI.TwistedRegular
402 import PaperXI.TwistedRescaling
403 import PaperXI.TwistedSimple
404 import PaperXI.TypeNormalizerAction
405 import PaperXI.TypeNormalizerForm
406 import PaperXI.TypeNormalizerPairing
407 import PaperXI.TypeProjectiveImplementation
408 import PaperXI.TypeSideDescent
409 import PaperXI.TypeSideExtension
410 import PaperXI.TypeSideUniqueness
411 import PaperXI.UnramifiedBaseChangeFactor
412 import PaperXI.UnramifiedConductor
413 import PaperXI.UnramifiedConductorZero
414 import PaperXI.UnramifiedFieldTower
415 import PaperXI.UnramifiedLocalFactor
416 import PaperXI.UnramifiedPolynomial
417 import PaperXI.UnramifiedValuation
418 import PaperXI.ValuationConductor
419 import PaperXI.ValuationFixingField
420 import PaperXI.ValuationIntegralModel
421 import PaperXI.ValuationRamification
422 import PaperXI.ValuationResidueEmbedding
423 import PaperXI.ValuationTameEndpoint

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 751886f79ab5cbae124e56031bd938ea0b132e146f7732e30023dbb696134160

Original source on GitHub

Back to Paper XI: Packets, Arithmetic Realization, and Conditional Comparison