Realization Boundaries · Lean sources

Realization Boundaries

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.

Source files 67

Source locations and editions

Files are shown relative to ./.

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

67 files

RealizationBoundaries.lean
71 lines · 0 declaration locations
AdditionGraphDegree.leanRealizationBoundaries/
64 lines · 6 declaration locations
Ambient.leanRealizationBoundaries/
122 lines · 20 declaration locations
CanonicalOperationDegree.leanRealizationBoundaries/
35 lines · 3 declaration locations
ClassificationConsequences.leanRealizationBoundaries/
103 lines · 11 declaration locations
Cocycle.leanRealizationBoundaries/
147 lines · 18 declaration locations
CompletionConsequences.leanRealizationBoundaries/
155 lines · 20 declaration locations
CompletionReflection.leanRealizationBoundaries/
152 lines · 12 declaration locations
ComputableFiniteObservations.leanRealizationBoundaries/
364 lines · 59 declaration locations
ComputableNormalCodes.leanRealizationBoundaries/
471 lines · 44 declaration locations
ComputablePresentations.leanRealizationBoundaries/
493 lines · 50 declaration locations
ComputableQuotientCodes.leanRealizationBoundaries/
282 lines · 35 declaration locations
Countability.leanRealizationBoundaries/
103 lines · 15 declaration locations
CyclicFiniteTargets.leanRealizationBoundaries/
115 lines · 13 declaration locations
CyclicQuotients.leanRealizationBoundaries/
123 lines · 14 declaration locations
DegreeVariation.leanRealizationBoundaries/
87 lines · 10 declaration locations
DiagonalAutomorphisms.leanRealizationBoundaries/
189 lines · 18 declaration locations
DiagonalHomomorphisms.leanRealizationBoundaries/
153 lines · 23 declaration locations
DiagonalRealization.leanRealizationBoundaries/
166 lines · 15 declaration locations
DirectSumEndomorphisms.leanRealizationBoundaries/
80 lines · 7 declaration locations
DirectSumPresentation.leanRealizationBoundaries/
153 lines · 18 declaration locations
EndomorphismScalars.leanRealizationBoundaries/
165 lines · 16 declaration locations
EnumerationClosure.leanRealizationBoundaries/
30 lines · 3 declaration locations
Extensions.leanRealizationBoundaries/
92 lines · 10 declaration locations
FiniteQuotients.leanRealizationBoundaries/
127 lines · 19 declaration locations
FiniteTargets.leanRealizationBoundaries/
99 lines · 10 declaration locations
GenerationConsequences.leanRealizationBoundaries/
80 lines · 8 declaration locations
GenerationRanks.leanRealizationBoundaries/
113 lines · 20 declaration locations
GrammarEscape.leanRealizationBoundaries/
327 lines · 40 declaration locations
HomomorphismObstruction.leanRealizationBoundaries/
107 lines · 10 declaration locations
ListingSearchEquivalence.leanRealizationBoundaries/
138 lines · 12 declaration locations
LocalCocycleQueries.leanRealizationBoundaries/
203 lines · 22 declaration locations
NormalFormTransport.leanRealizationBoundaries/
82 lines · 9 declaration locations
NormalForms.leanRealizationBoundaries/
58 lines · 8 declaration locations
ObservationPatternClosure.leanRealizationBoundaries/
59 lines · 5 declaration locations
ObservationSystems.leanRealizationBoundaries/
346 lines · 37 declaration locations
OracleCopyOperations.leanRealizationBoundaries/
97 lines · 16 declaration locations
OracleEnumerationNormalForm.leanRealizationBoundaries/
420 lines · 47 declaration locations
OraclePartialMinimizationTraces.leanRealizationBoundaries/
50 lines · 1 declaration location
OraclePartialRecursionTraces.leanRealizationBoundaries/
53 lines · 3 declaration locations
PairedPrimes.leanRealizationBoundaries/
91 lines · 17 declaration locations
Preimages.leanRealizationBoundaries/
92 lines · 10 declaration locations
PrimeComputability.leanRealizationBoundaries/
76 lines · 10 declaration locations
Procyclic.leanRealizationBoundaries/
117 lines · 11 declaration locations
ProductTopology.leanRealizationBoundaries/
80 lines · 13 declaration locations
ProfiniteCompletion.leanRealizationBoundaries/
174 lines · 23 declaration locations
PureCorrespondence.leanRealizationBoundaries/
128 lines · 14 declaration locations
Quotient.leanRealizationBoundaries/
109 lines · 16 declaration locations
RadicalCounts.leanRealizationBoundaries/
121 lines · 18 declaration locations
RationalComputability.leanRealizationBoundaries/
261 lines · 40 declaration locations
RationalFG.leanRealizationBoundaries/
65 lines · 5 declaration locations
Reachability.leanRealizationBoundaries/
252 lines · 24 declaration locations
RootAlgorithm.leanRealizationBoundaries/
306 lines · 31 declaration locations
RootAlgorithmCost.leanRealizationBoundaries/
292 lines · 34 declaration locations
RootConsequences.leanRealizationBoundaries/
115 lines · 13 declaration locations
RootFibers.leanRealizationBoundaries/
125 lines · 16 declaration locations
SearchEnumerableSpectrum.leanRealizationBoundaries/
370 lines · 30 declaration locations
Sections.leanRealizationBoundaries/
129 lines · 18 declaration locations
SeedGeneration.leanRealizationBoundaries/
106 lines · 15 declaration locations
SeedObstructions.leanRealizationBoundaries/
102 lines · 10 declaration locations
SelectorClassification.leanRealizationBoundaries/
164 lines · 13 declaration locations
SpectrumComputability.leanRealizationBoundaries/
407 lines · 42 declaration locations
StructuralClosure.leanRealizationBoundaries/
314 lines · 25 declaration locations
SubgroupSpectrum.leanRealizationBoundaries/
276 lines · 23 declaration locations
SubgroupTopology.leanRealizationBoundaries/
107 lines · 13 declaration locations
TailSignature.leanRealizationBoundaries/
129 lines · 13 declaration locations
UnarySelectors.leanRealizationBoundaries/
160 lines · 18 declaration locations