RealizationBoundaries.lean

1 import RealizationBoundaries.Ambient
2 import RealizationBoundaries.Quotient
3 import RealizationBoundaries.Preimages
4 import RealizationBoundaries.FiniteQuotients
5 import RealizationBoundaries.Extensions
6 import RealizationBoundaries.Sections
7 import RealizationBoundaries.Cocycle
8 import RealizationBoundaries.PairedPrimes
9 import RealizationBoundaries.NormalForms
10 import RealizationBoundaries.PureCorrespondence
11 import RealizationBoundaries.Countability
12 import RealizationBoundaries.ProductTopology
13 import RealizationBoundaries.FiniteTargets
14 import RealizationBoundaries.ProfiniteCompletion
15 import RealizationBoundaries.CompletionConsequences
16 import RealizationBoundaries.TailSignature
17 import RealizationBoundaries.SelectorClassification
18 import RealizationBoundaries.HomomorphismObstruction
19 import RealizationBoundaries.NormalFormTransport
20 import RealizationBoundaries.ClassificationConsequences
21 import RealizationBoundaries.DiagonalHomomorphisms
22 import RealizationBoundaries.DiagonalRealization
23 import RealizationBoundaries.EndomorphismScalars
24 import RealizationBoundaries.DiagonalAutomorphisms
25 import RealizationBoundaries.CompletionReflection
26 import RealizationBoundaries.DirectSumEndomorphisms
27 import RealizationBoundaries.SeedGeneration
28 import RealizationBoundaries.SeedObstructions
29 import RealizationBoundaries.GenerationRanks
30 import RealizationBoundaries.Procyclic
31 import RealizationBoundaries.GenerationConsequences
32 import RealizationBoundaries.RootFibers
33 import RealizationBoundaries.RadicalCounts
34 import RealizationBoundaries.CyclicQuotients
35 import RealizationBoundaries.CyclicFiniteTargets
36 import RealizationBoundaries.RootConsequences
37 
38 import RealizationBoundaries.Reachability
39 import RealizationBoundaries.SubgroupSpectrum
40 import RealizationBoundaries.UnarySelectors
41 import RealizationBoundaries.ObservationPatternClosure
42 import RealizationBoundaries.GrammarEscape
43 import RealizationBoundaries.RationalFG
44 import RealizationBoundaries.StructuralClosure
45 import RealizationBoundaries.PrimeComputability
46 import RealizationBoundaries.ComputablePresentations
47 import RealizationBoundaries.RootAlgorithm
48 import RealizationBoundaries.ObservationSystems
49 
50 import RealizationBoundaries.RootAlgorithmCost
51 import RealizationBoundaries.SubgroupTopology
52 import RealizationBoundaries.RationalComputability
53 import RealizationBoundaries.ComputableQuotientCodes
54 import RealizationBoundaries.OracleCopyOperations
55 
56 import RealizationBoundaries.SpectrumComputability
57 import RealizationBoundaries.DirectSumPresentation
58 import RealizationBoundaries.ComputableNormalCodes
59 import RealizationBoundaries.SearchEnumerableSpectrum
60 import RealizationBoundaries.ListingSearchEquivalence
61 import RealizationBoundaries.OraclePartialRecursionTraces
62 import RealizationBoundaries.OraclePartialMinimizationTraces
63 import RealizationBoundaries.OracleEnumerationNormalForm
64 import RealizationBoundaries.EnumerationClosure
65 import RealizationBoundaries.ComputableFiniteObservations
66 import RealizationBoundaries.DegreeVariation
67 import RealizationBoundaries.CanonicalOperationDegree
68 
69 import RealizationBoundaries.AdditionGraphDegree
70 
71 import RealizationBoundaries.LocalCocycleQueries

Back to source controls