OAI/NumberTheory/TwoPoint/Walks/
960 declarations, 0 contain sorry, 0 declared as axioms; 203 files
Files
- AttachedCatalogAvoidance.lean 3 declarations
- AttachedResidueLift.lean 1 declarations
- AttachedWitnessCatalog.lean 5 declarations
- BlockEdgeForm.lean 2 declarations
- BlockEndpointSum.lean 4 declarations
- BlockFamilyDecoding.lean 6 declarations
- BlockFormPrefixBound.lean 2 declarations
- BlockGeometry.lean 12 declarations
- BlockOperatorSpectrum.lean 5 declarations
- BlockTestNormalization.lean 1 declarations
- BlockTesting.lean 7 declarations
- CanonicalBinSummation.lean 3 declarations
- CanonicalCenteringBins.lean 3 declarations
- CanonicalColumnEncoding.lean 2 declarations
- CanonicalColumnNames.lean 11 declarations
- CanonicalComplexBin.lean 2 declarations
- CanonicalComplexLimits.lean 2 declarations
- CanonicalComplexPrefix.lean 1 declarations
- CanonicalComplexTesting.lean 1 declarations
- CanonicalCorrelationDeletion.lean 4 declarations
- CanonicalForest.lean 7 declarations
- CanonicalPartialCentering.lean 3 declarations
- CanonicalPartialWindows.lean 2 declarations
- CanonicalRareDeletion.lean 2 declarations
- CanonicalRawSelection.lean 1 declarations
- CanonicalRetainedMass.lean 1 declarations
- CanonicalRoughScale.lean 7 declarations
- CanonicalShiftedDeletion.lean 3 declarations
- CanonicalTupleSlices.lean 6 declarations
- CanonicalTupleSmooth.lean 3 declarations
- ClosedPathProduct.lean 4 declarations
- ClosedTraceEncoding.lean 4 declarations
- ClosedTraceSummation.lean 4 declarations
- ClosedVertexMask.lean 2 declarations
- ClosedWalkNormalization.lean 6 declarations
- ClosedWordPadding.lean 8 declarations
- ClosedWordStateMask.lean 4 declarations
- ColumnBlockGeometry.lean 2 declarations
- ColumnBoundaryEncoding.lean 4 declarations
- ColumnBudget.lean 2 declarations
- ColumnChunkBudgets.lean 7 declarations
- ColumnChunks.lean 13 declarations
- ColumnClosedEncoding.lean 7 declarations
- ColumnCode.lean 5 declarations
- ColumnCodeUniverse.lean 11 declarations
- ColumnCoefficientBounds.lean 8 declarations
- ColumnDecoder.lean 19 declarations
- ColumnDecoderAsymptotics.lean 1 declarations
- ColumnEncodingRealization.lean 6 declarations
- ColumnForestAssembly.lean 1 declarations
- ColumnGeometryEncoding.lean 4 declarations
- ColumnHarmonicSum.lean 5 declarations
- ColumnHighRankTraceTotal.lean 1 declarations
- ColumnManyUnlitDecay.lean 1 declarations
- ColumnMatrixTrace.lean 2 declarations
- ColumnNameTransport.lean 6 declarations
- ColumnPaddingBridge.lean 10 declarations
- ColumnPatternRecovery.lean 3 declarations
- ColumnPieceMembership.lean 5 declarations
- ColumnRankRelations.lean 9 declarations
- ColumnRepresentatives.lean 9 declarations
- ColumnRunEncoding.lean 13 declarations
- ColumnSingletonDecay.lean 1 declarations
- ColumnTraceTotal.lean 1 declarations
- ColumnWordGeometry.lean 3 declarations
- ColumnWordSlices.lean 4 declarations
- DisjointCoordinates.lean 8 declarations
- FiveColorBilinear.lean 10 declarations
- FiveColorOrientation.lean 7 declarations
- ForestCode.lean 10 declarations
- ForestCodeAsymptotics.lean 3 declarations
- ForestGeometry.lean 2 declarations
- ForestLeaves.lean 1 declarations
- ForestPathCode.lean 3 declarations
- ForestPathCounting.lean 12 declarations
- ForestPathRealization.lean 4 declarations
- ForestRepresentation.lean 2 declarations
- GoodWordForest.lean 2 declarations
- GoodWordHybrid.lean 1 declarations
- GoodWordWeightedSum.lean 3 declarations
- HighRankActualDecay.lean 1 declarations
- HighRankCatalogCost.lean 1 declarations
- HighRankColumns.lean 2 declarations
- HighRankFixedPadding.lean 2 declarations
- HighRankMinor.lean 9 declarations
- HighRankPaddingSum.lean 2 declarations
- HighRankTraceSlices.lean 3 declarations
- HighRankTraceTotal.lean 1 declarations
- HighRankWeightedWords.lean 1 declarations
- HighRankWordEvents.lean 2 declarations
- IncidenceDecoding.lean 3 declarations
- IncidenceForest.lean 8 declarations
- IndexedBlockFamily.lean 8 declarations
- IndexedQuotientPaths.lean 2 declarations
- IndexedRuns.lean 11 declarations
- ManyUnlitCatalog.lean 2 declarations
- ManyUnlitDecay.lean 2 declarations
- ManyUnlitNumericalWords.lean 4 declarations
- ManyUnlitWeightedWords.lean 1 declarations
- PartialTupleProfiles.lean 4 declarations
- ProhibitedCatalogEncoding.lean 6 declarations
- ProhibitedCircuit.lean 25 declarations
- ProhibitedCircuitBounds.lean 2 declarations
- ProhibitedCostComparison.lean 6 declarations
- ProhibitedDensity.lean 9 declarations
- ProhibitedFamilyWitnesses.lean 6 declarations
- ProhibitedHighRankDecay.lean 1 declarations
- ProhibitedManyUnlitDecay.lean 1 declarations
- ProhibitedNumericalSingletonDecay.lean 1 declarations
- ProhibitedPrimeEncoding.lean 2 declarations
- ProhibitedRowComparison.lean 5 declarations
- ProhibitedSingletonCatalog.lean 1 declarations
- ProhibitedSingletonDecay.lean 1 declarations
- ProhibitedTraceTerms.lean 4 declarations
- ProhibitedWeightIndependence.lean 5 declarations
- ProhibitedWeightSupport.lean 4 declarations
- ProhibitedWordCircuit.lean 8 declarations
- ProhibitedWordIdentity.lean 5 declarations
- ProhibitedWords.lean 45 declarations
- RankDecay.lean 9 declarations
- RankEnumeration.lean 3 declarations
- RankProbability.lean 4 declarations
- RankSliceCost.lean 2 declarations
- ReducedIncidenceWalk.lean 10 declarations
- RetainedActiveEdges.lean 7 declarations
- RetainedBinSummation.lean 2 declarations
- RetainedBlockIdentity.lean 5 declarations
- RetainedBoundaryScale.lean 1 declarations
- RetainedComplexBlock.lean 6 declarations
- RetainedComplexEdges.lean 4 declarations
- RetainedComplexMatrix.lean 3 declarations
- RetainedComplexRows.lean 2 declarations
- RetainedDeletionBridge.lean 9 declarations
- RetainedDivisorMass.lean 6 declarations
- RetainedEdgeRows.lean 2 declarations
- RetainedEligibility.lean 4 declarations
- RetainedFinalScale.lean 3 declarations
- RetainedGraphOrientation.lean 3 declarations
- RetainedLiouvilleEdges.lean 4 declarations
- RetainedMainProbability.lean 1 declarations
- RetainedNumericalPrefix.lean 5 declarations
- RetainedRowScale.lean 4 declarations
- RetainedWitnessProbability.lean 4 declarations
- ReversedSegments.lean 7 declarations
- SegmentedWitnessDecay.lean 1 declarations
- SelectedBinEligibility.lean 4 declarations
- SelectedCenteringIdentity.lean 2 declarations
- SelectedGoodHybrid.lean 3 declarations
- SelectedPairBins.lean 2 declarations
- SelectedPairCosts.lean 3 declarations
- SelectedPairRank.lean 2 declarations
- SelectedRawBinsLower.lean 1 declarations
- SelectedRawComparison.lean 4 declarations
- SelectedRawLowerBound.lean 1 declarations
- SelectedWitnesses.lean 2 declarations
- TupleCenterExpansion.lean 5 declarations
- TupleColumnCover.lean 2 declarations
- TupleColumnResampling.lean 5 declarations
- TupleColumnWords.lean 10 declarations
- TupleDegreeDeletion.lean 1 declarations
- TupleDeletionNormalizer.lean 4 declarations
- TupleLitOrigins.lean 1 declarations
- TupleOccurrences.lean 4 declarations
- TuplePaddingDeletion.lean 1 declarations
- TuplePerfectRows.lean 5 declarations
- TuplePrimeArithmetic.lean 5 declarations
- TuplePrimeCosts.lean 3 declarations
- TupleRankCoordinate.lean 1 declarations
- TupleRankFiberSum.lean 1 declarations
- TupleRankWitness.lean 4 declarations
- TupleResidueLabels.lean 3 declarations
- TupleSlice.lean 7 declarations
- TupleSliceSupport.lean 5 declarations
- TupleSmoothCost.lean 3 declarations
- TupleWordPrimeSupport.lean 6 declarations
- WeightedWordBudget.lean 2 declarations
- WeightedWordCircuit.lean 6 declarations
- WeightedWordCoefficient.lean 5 declarations
- WeightedWordComparison.lean 1 declarations
- WeightedWordEnvelope.lean 5 declarations
- WitnessCatalogCost.lean 3 declarations
- WitnessCodeBounds.lean 2 declarations
- WitnessCover.lean 12 declarations
- WitnessMetadata.lean 2 declarations
- WitnessMetadataBounds.lean 2 declarations
- WitnessOrdering.lean 2 declarations
- WitnessPrimeSystems.lean 2 declarations
- WitnessProbabilityWeight.lean 4 declarations
- WitnessReciprocalUnion.lean 3 declarations
- WitnessRecordBounds.lean 4 declarations
- WitnessRecordBudget.lean 5 declarations
- WitnessRelabel.lean 1 declarations
- WitnessScaleParameters.lean 1 declarations
- WitnessSegmentation.lean 4 declarations
- WitnessSelection.lean 16 declarations
- WitnessSupport.lean 8 declarations
- WitnessSystemCodes.lean 8 declarations
- WitnessSystemDecoding.lean 15 declarations
- WordBlockGeometry.lean 9 declarations
- WordDegreeSupport.lean 4 declarations
- WordRelations.lean 16 declarations
- WordResampling.lean 11 declarations
- WordSegments.lean 15 declarations