OAI/Computability/PerfectCompleteness/Construction/
899 declarations, 0 contain sorry, 0 declared as axioms; 52 files
Files
- AscendingBranchingLemmas.lean 15 declarations
- BucketFullAgreement.lean 5 declarations
- BucketQuotientAgreement.lean 9 declarations
- CanonicalLocalCompletion.lean 30 declarations
- ChildCallNumbering.lean 15 declarations
- ChildUnmarkedSpace.lean 12 declarations
- CutBucketTransportLemmas.lean 6 declarations
- CutChildGrouping.lean 13 declarations
- CutNodeRows.lean 18 declarations
- DescendantSpacesLemmas.lean 21 declarations
- FactoredFunctionsLemmas.lean 24 declarations
- FlexibleLocalCompletionLemmas.lean 24 declarations
- HiddenBucketBias.lean 39 declarations
- HiddenChildMixture.lean 10 declarations
- HierarchicalAdviceFromBuckets.lean 7 declarations
- HierarchicalBucketFamily.lean 11 declarations
- LocalCompletionFamily.lean 22 declarations
- LocalCompletionOutput.lean 8 declarations
- LocalCompletionSerializedOutput.lean 7 declarations
- LocalReconstruction.lean 13 declarations
- MixedSourceLocalOddLists.lean 20 declarations
- NativeLeafAlphabet.lean 5 declarations
- NodeEmbedding.lean 28 declarations
- OriginalChildBlockProducts.lean 5 declarations
- OriginalChildBlocks.lean 17 declarations
- OriginalChildScalarAssemblyLemmas.lean 52 declarations
- OriginalChildScalars.lean 19 declarations
- OriginalCutBucketReplacement.lean 12 declarations
- OriginalHiddenChild.lean 17 declarations
- OriginalOwnBucketSplit.lean 47 declarations
- OwnBucketBias.lean 3 declarations
- ProjectedNodeEmbedding.lean 16 declarations
- RelativeDescendantProductsLemmas.lean 25 declarations
- SourceChildKernelLemmas.lean 61 declarations
- SourceLocalOddLists.lean 20 declarations
- SourcePhysicalChildExpectation.lean 5 declarations
- SourcePhysicalTaggedChildren.lean 9 declarations
- SourceQuestionCutSplit.lean 16 declarations
- SourceQuestionKernelJoint.lean 9 declarations
- SourceQuestionOrderLemmas.lean 54 declarations
- SourceQuestionPairPullback.lean 8 declarations
- SourceQuestionPhysicalHigh.lean 7 declarations
- SourceQuestionPositionSplit.lean 13 declarations
- SourceQuestionRawSwap.lean 11 declarations
- SourceQuestionReconstruction.lean 12 declarations
- SourceQuestionUnmarkedRange.lean 4 declarations
- StoppedBucketRows.lean 3 declarations
- StoppedProjectedBucketIndex.lean 12 declarations
- StoppedProjectedBuckets.lean 18 declarations
- TreeCanonical.lean 19 declarations
- TreeSourceSpaces.lean 27 declarations
- WholeCutLocalityLemmas.lean 16 declarations