Collatz.lean

import Collatz.Basic
import Collatz.Accelerated
import Collatz.Core.Arith
import Collatz.Core.Minimum
import Collatz.Core.Pigeonhole
import Collatz.Core.Sum
import Collatz.Core.Reach
import Collatz.Search.Descent
import Collatz.Search.StoppingTime
import Collatz.Search.Sieved
import Collatz.Search.Verify
import Collatz.Search.Verified768000
import Collatz.Structure.AccCycle
import Collatz.Structure.AccDivergence
import Collatz.Structure.AffineBound
import Collatz.Structure.AffineBoundSharp
import Collatz.Structure.CycleLength
import Collatz.Structure.CycleLengthSharp
import Collatz.Structure.CycleModThree
import Collatz.Structure.CycleMinClass
import Collatz.Structure.CycleMaxClass
import Collatz.Structure.CycleSum
import Collatz.Structure.CycleValuation
import Collatz.Structure.CycleOddCount
import Collatz.Structure.CycleExtremes
import Collatz.Structure.Congruence
import Collatz.Structure.Cycle
import Collatz.Structure.Density
import Collatz.Structure.Divergence
import Collatz.Structure.Minimal
import Collatz.Structure.MinimalHeavy
import Collatz.Structure.OrbitMin
import Collatz.Structure.HeavySet
import Collatz.Structure.OrbitMinSieve
import Collatz.Structure.ForcedSteps
import Collatz.Structure.Records
import Collatz.Structure.OddRuns
import Collatz.Structure.RunBounds
import Collatz.Structure.RunValue
import Collatz.Structure.RunDescent
import Collatz.Structure.SieveDensity
import Collatz.Structure.DensitySharp
import Collatz.Structure.DensityRate
import Collatz.Structure.Predecessors
import Collatz.Structure.Obstruction
import Collatz.Structure.Predecessor
import Collatz.Structure.ShortCycles
import Collatz.Strategy.Pillars
import Collatz.Strategy.Reductions
import Collatz.Strategy.Terras
import Collatz.Chains.Descent
import Collatz.Chains.Targets
import Collatz.Chains.Cycles
import Collatz.Chains.Modular
import Collatz.Chains.Parity
import Collatz.Chains.Index
import Collatz.Chains.CycleTargets
import Collatz.Chains.Arithmetic
import Collatz.Chains.Sharp
import Collatz.Chains.MinClass
import Collatz.Chains.Valuation
import Collatz.Chains.OddCount
import Collatz.Chains.MaxClass
import Collatz.Chains.Heavy
import Collatz.Chains.OrbitMin
import Collatz.Chains.OrbitSieve
import Collatz.Chains.Runs
import Collatz.Strategy.NeverDrops
import Collatz.Structure.VerifiedSharp
import Collatz.Strategy.Descent
import Collatz.Strategy.ThreeObstruction
import Collatz.Strategy.OrbitDescent
import Collatz.Strategy.BackwardRun
import Collatz.Strategy.ThreeAdic
import Collatz.Strategy.OrbitWindows
import Collatz.Strategy.RunInvariance
import Collatz.Strategy.OneRunCycle
import Collatz.Strategy.Mirror
import Collatz.Strategy.Denominator
import Collatz.Strategy.DenominatorScalar
import Collatz.Strategy.CycleProduct
import Collatz.Strategy.AffineExact
import Collatz.Strategy.AccumulatorArith
import Collatz.Strategy.AccumulatorClass
import Collatz.Strategy.AccumulatorValuation
import Collatz.Strategy.CycleAccumulator
import Collatz.Strategy.GapOne
import Collatz.Strategy.CycleCriterion
import Collatz.Strategy.OneRunOrder
import Collatz.Strategy.HeavyWord
import Collatz.Strategy.HeavyResidue
import Collatz.Strategy.ValuationBudget
import Collatz.Strategy.ArchimedeanCeiling
import Collatz.Strategy.Rotation
import Collatz.Strategy.GapSandwich
import Collatz.Strategy.RunAlgebra
import Collatz.Strategy.Bootstrap
import Collatz.Strategy.CycleLanguage
import Collatz.Strategy.MinimalCycle
import Collatz.Strategy.SUnitRelation
import Collatz.Strategy.NewModels
import Collatz.Strategy.ExpSum
import Collatz.Strategy.GapPrimes
import Collatz.Search.VerifiedExtended
import Collatz.Strategy.RealizableFrontier6809
import Collatz.Strategy.JointRank
import Collatz.Strategy.PAdicJoint
import Collatz.Strategy.PrimeLedge
import Collatz.Strategy.ReverseTree
import Collatz.Strategy.InfiniteWord
import Collatz.Strategy.RunRefined
import Collatz.Strategy.RepetitionDescent
import Collatz.Strategy.SpreadFloor
import Collatz.Strategy.SinkStructure
import Collatz.Strategy.ExtremalWord
import Collatz.Strategy.DeltaSpectrum
import Collatz.Strategy.WindowCollapse
import Collatz.Strategy.BackwardRange
import Collatz.Strategy.HighPart
import Collatz.Strategy.ImageDensity
import Collatz.Strategy.FiniteInfinite
import Collatz.Strategy.ForwardReverse
import Collatz.Strategy.AccumulatorAutomaton
import Collatz.Strategy.OrderBox
import Collatz.Strategy.OrderAutomaton
import Collatz.Strategy.CyclicOrder
import Collatz.Strategy.Discrepancy
import Collatz.Strategy.Height
import Collatz.Strategy.TransferOperator
import Collatz.Strategy.Rewriting
import Collatz.Strategy.Complexity
import Collatz.Strategy.CycleCode
import Collatz.Strategy.LatticeGeometry
import Collatz.Strategy.ExtensionClass
import Collatz.Strategy.MachineModel
import Collatz.Strategy.DigitAutomaton
import Collatz.Strategy.PhantomMediant
import Collatz.Strategy.Coupling
import Collatz.Strategy.Linearizing
import Collatz.Strategy.FloorSchedule
import Collatz.Strategy.GroundState
import Collatz.Strategy.CutGame
import Collatz.Strategy.TropicalDefect
import Collatz.Strategy.Escape
import Collatz.Strategy.EscapeCertificate
import Collatz.Strategy.DivergenceAudit
import Collatz.Strategy.GlobalHeight
import Collatz.Strategy.ScaleRecord
import Collatz.Strategy.ScaleLadder
import Collatz.Strategy.CouplingNormal
import Collatz.Strategy.SegmentMonoid
import Collatz.Strategy.ScaleFibre
import Collatz.Strategy.FilterDecomposition
import Collatz.Strategy.CoupledCycle
import Collatz.Strategy.CouplingDecay
import Collatz.Strategy.BottomUnreachable
import Collatz.Strategy.OctaveWord
import Collatz.Strategy.HighScaleWord
import Collatz.Strategy.OctaveOrder
import Collatz.Strategy.HarmonicCoupling
import Collatz.Strategy.PrefixLP
import Collatz.Strategy.MinimumInterval
import Collatz.Strategy.BcapSharp
import Collatz.Strategy.BeattyStability
import Collatz.Strategy.GapVector
import Collatz.Strategy.RotationSystem
import Collatz.Strategy.FamilyFlatness
import Collatz.Strategy.GapRotation
import Collatz.Strategy.DeltaAdversaryXIV
import Collatz.Strategy.UniformCovering
import Collatz.Strategy.ValuationBeatty
import Collatz.Strategy.ReversePinch
import Collatz.Strategy.ValuationTransition
import Collatz.Strategy.MixWitnessXV
import Collatz.Strategy.SieveGrowth
import Collatz.Strategy.Profile
import Collatz.Strategy.ExchangeRate
import Collatz.Strategy.TwoRunOrder
import Collatz.Strategy.RealizableBound
import Collatz.Strategy.AccumulatorSharp
import Collatz.Strategy.AccumulatorLocal
import Collatz.Strategy.AccumulatorCap
import Collatz.Strategy.DensitySharper
import Collatz.Strategy.ClassCap
import Collatz.Strategy.ThreeResidue
import Collatz.Strategy.HeavyState
import Collatz.Strategy.NoFiniteRanking
import Collatz.Strategy.AnyModulusRanking
import Collatz.Strategy.TransitionInvariant
import Collatz.Strategy.CycleLength520
import Collatz.Strategy.CycleLength1539
import Collatz.Strategy.CycleLength2593
import Collatz.Strategy.LiftExponent
import Collatz.Strategy.ValuationBridge
import Collatz.Strategy.Frontier
import Collatz.Strategy.Master
import Collatz.Chains.SumChains
import Collatz.Registry
import Collatz.Papers.Lagarias1985
import Collatz.Papers.Lagarias2003Bibliography
import Collatz.Papers.Everett1977
import Collatz.Papers.Terras1976
import Collatz.Papers.Tao2022
import Collatz.Papers.KrasikovLagarias2003
import Collatz.Papers.Conway1972
import Collatz.Papers.Template