OAI/NumberTheory/Jacobsthal/Paths/
1109 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- ActualEffectiveWitness.lean 1 declarations
- ActualFirstTagExistence.lean 11 declarations
- ActualFlaggedCompact.lean 6 declarations
- ActualNearFullStopGroup.lean 1 declarations
- ActualOwnerLocalComparison.lean 4 declarations
- ActualPrefixClearance.lean 3 declarations
- ActualSampleWitness.lean 9 declarations
- ActualTagFreezing.lean 76 declarations
- ActualThresholdArrival.lean 33 declarations
- ActualWordSelection.lean 5 declarations
- AdmittedHarmonicPaths.lean 15 declarations
- AffineBranch.lean 1 declarations
- BranchWordEndpoint.lean 10 declarations
- CanonicalHighRatioVisit.lean 8 declarations
- CanonicalKeyWitness.lean 18 declarations
- CanonicalPairVisitCompletion.lean 3 declarations
- CanonicalUniformMissingVisit.lean 27 declarations
- CanonicalWordPrefix.lean 8 declarations
- ConsecutivePairStop.lean 30 declarations
- ContinuousArrivalSupport.lean 6 declarations
- CorrectSearchTags.lean 38 declarations
- CostPrefixTransport.lean 17 declarations
- ExpandedHardCapture.lean 10 declarations
- FiniteBoxWordMass.lean 54 declarations
- FiniteHistorySupport.lean 115 declarations
- FiniteVisitMass.lean 33 declarations
- FirstVisitRatioTail.lean 4 declarations
- FlagMeasurePartition.lean 4 declarations
- FlaggedHarmonicPaths.lean 17 declarations
- FlaggedHarmonicTransform.lean 9 declarations
- FlaggedSourceStart.lean 55 declarations
- FullBoxPrefixLower.lean 6 declarations
- FullPathCompactSelection.lean 4 declarations
- FullWordHighAlignment.lean 27 declarations
- GeometricEdgeWitness.lean 2 declarations
- GeometricRegularWords.lean 8 declarations
- GeometricWords.lean 2 declarations
- GlobalFiniteBranches.lean 17 declarations
- HighPrefixBounds.lean 9 declarations
- HighPrefixState.lean 22 declarations
- HistoryRestrictionAlgebra.lean 17 declarations
- MovingStopBandParameters.lean 3 declarations
- MovingStopMargins.lean 19 declarations
- NearPrefixOccurrence.lean 9 declarations
- OneStepHistoryReconstruction.lean 5 declarations
- OutsideExceptionsWitness.lean 16 declarations
- PairBranchFullProjection.lean 11 declarations
- PairCaptureProjection.lean 15 declarations
- PairedHitting.lean 18 declarations
- PrefixCompletions.lean 5 declarations
- QuantitativeOrdinaryHit.lean 5 declarations
- RawBoxRationalWitness.lean 9 declarations
- RawFullHitIncreasing.lean 7 declarations
- RawIncreasingPrefix.lean 17 declarations
- RawPhysicalHit.lean 13 declarations
- RawStableHistory.lean 16 declarations
- RawWordBridgeInputs.lean 9 declarations
- RawWordSpaces.lean 31 declarations
- ReferenceHistoryAdmission.lean 7 declarations
- ReferencePrefixRecurrence.lean 6 declarations
- RepeatedWordData.lean 6 declarations
- RepresentativeStopGeometry.lean 8 declarations
- ResidualHistoryGeometry.lean 2 declarations
- SampleWitnessAverage.lean 8 declarations
- SourceStopWindow.lean 2 declarations
- SourceStoppedCorrection.lean 1 declarations
- SourceWitnessSeries.lean 14 declarations
- StopLengthBandGeometry.lean 3 declarations
- StoppedErrorReduction.lean 1 declarations
- StoppedReferenceFinite.lean 8 declarations
- TagAffineConditions.lean 7 declarations
- TagCutoffSeparation.lean 8 declarations
- TagIntersectionError.lean 2 declarations
- TagPairBinding.lean 9 declarations
- TagRelativeAlgebra.lean 4 declarations
- TagSubbinWidths.lean 22 declarations
- TwoSidedThresholdArrival.lean 8 declarations
- WeightedIsolatedWords.lean 1 declarations
- WeightedRepeatedWords.lean 1 declarations
- WindowHitWords.lean 12 declarations
- WordIntervalGeometry.lean 4 declarations
- WrongOwnerBoxMass.lean 12 declarations