import GroupApproximation.Algebra.CoweightCoinvariants
import GroupApproximation.Algebra.FaithfulRadicalCocycle
import GroupApproximation.Algebra.MappingTelescope
import GroupApproximation.Algebra.SemidirectProductAssoc
import GroupApproximation.Algebra.TwoGeneratedFreeQuotient
import GroupApproximation.Analysis.FaithfulTracialMatrix
import GroupApproximation.Analysis.FiniteMatrixPositiveSquareRoot
import GroupApproximation.Analysis.FiniteMatrixPositiveSquareRootUnit
import GroupApproximation.Analysis.FiniteMatrixCorrectedStarEquiv
import GroupApproximation.Analysis.FiniteProductCorrectedStarEquiv
import GroupApproximation.Analysis.ProperIsometryFromCompression
import GroupApproximation.Analysis.ExplicitReducedGroupCStarConsequences
import GroupApproximation.Analysis.MaximalGroupCStar
import GroupApproximation.Analysis.UniversalCStarHNN
import GroupApproximation.Analysis.MaximalCStarKazhdanAverage
import GroupApproximation.Analysis.QuasiRegularWitness
import GroupApproximation.Analysis.StateExtension
import GroupApproximation.Analysis.SpectralStateWitness
import GroupApproximation.Analysis.SpectralComponentDiameter
import GroupApproximation.Analysis.SpectralComponentMotion
import GroupApproximation.Analysis.ClopenSpectralProjection
import GroupApproximation.Analysis.GNSEigenvector
import GroupApproximation.Computability.AbelianEnumeratedPi02
import GroupApproximation.Computability.ArithmeticalLedgerEndpoint
import GroupApproximation.Computability.ElementaryEnumeratedHardness
import GroupApproximation.Computability.FreeSubgroupEnumeratedHardness
import GroupApproximation.Computability.HyperlinearEnumeratedHardness
import GroupApproximation.Computability.HyperlinearUndecidabilityRoute
import GroupApproximation.Computability.AmenableEnumeratedHardness
import GroupApproximation.Computability.IsoInvariantSwitchHardness
import GroupApproximation.Computability.LEFEnumeratedPi02
import GroupApproximation.Computability.MFEnumeratedMicrostate
import GroupApproximation.Computability.MFEnumeratedNormalForm
import GroupApproximation.Computability.MFEnumeratedPi02
import GroupApproximation.Computability.PerfectEnumeratedHardness
import GroupApproximation.Computability.PerfectEnumeratedPi02
import GroupApproximation.Computability.ProfinitelyClosedIndexSet
import GroupApproximation.Computability.RFEnumeratedHardness
import GroupApproximation.Computability.RFPresentationPi02
import GroupApproximation.Computability.RFRecognitionHierarchy
import GroupApproximation.Computability.SoficEnumeratedPi02
import GroupApproximation.Computability.SoficMicrostateNormalForm
import GroupApproximation.Computability.SoficRecognitionPi02
import GroupApproximation.Computability.TorsionFreeEnumeratedHardness
import GroupApproximation.Computability.TorsionFreeEnumeratedPi02
import GroupApproximation.Computability.TrivialEnumeratedPi02
import GroupApproximation.Kazhdan.KazhdanEigenvalueBound
import GroupApproximation.Analysis.AbstractSpectralGap
import GroupApproximation.Analysis.CStarSpectralProjection
import GroupApproximation.Analysis.KazhdanProjectionAbsorption
import GroupApproximation.Analysis.KazhdanProjectionOneSidedOrder
import GroupApproximation.Analysis.ProjectionOrbitCollapse
import GroupApproximation.Analysis.CollapseJoinNonvanishing
import GroupApproximation.Analysis.CollapseNormalizedSetup
import GroupApproximation.Analysis.CollapseUnitaryLift
import GroupApproximation.Analysis.GroupStandardFormInstance
import GroupApproximation.Analysis.GroupVonNeumannAlgebra
import GroupApproximation.Analysis.GroupVonNeumannTrace
import GroupApproximation.Analysis.LimitsTraceStandardForm
import GroupApproximation.Analysis.PrintedFiniteDimensionalUses
import GroupApproximation.Analysis.PermutationICC
import GroupApproximation.Analysis.ShiftIsometry
import GroupApproximation.Analysis.TwoSidedRegularCommutant
import GroupApproximation.Analysis.MaximalCStarProperCompression
import GroupApproximation.Analysis.AmenableQuasidiagonal
import GroupApproximation.Analysis.CStarExactness
import GroupApproximation.Analysis.NFAlgebra
import GroupApproximation.Analysis.CStarMatrixFactorization
import GroupApproximation.Analysis.LanceMatrixSubalgebra
import GroupApproximation.Analysis.LanceBlockOperator
import GroupApproximation.Analysis.LanceChoiFunctional
import GroupApproximation.Analysis.LanceHermitianFunctional
import GroupApproximation.Analysis.LanceMatrixArveson
import GroupApproximation.Analysis.LanceDayEngine
import GroupApproximation.Analysis.LanceMultiplicationOperator
import GroupApproximation.Analysis.LanceHypertrace
import GroupApproximation.Analysis.LanceCPApprox
import GroupApproximation.Analysis.LanceCPContractiveUnitalization
import GroupApproximation.Analysis.LanceNuclearity
import GroupApproximation.Kazhdan.KazhdanUniverseDescent
import GroupApproximation.Sofic.ChosenMaximalCStarInfinite
import GroupApproximation.Sofic.FreeGroupPFFInterface
import GroupApproximation.Analysis.TorsionFreeFullMFCStarConsequences
import GroupApproximation.Computability.MarkovMFConsequences
import GroupApproximation.Computability.MFRadicalComputer
import GroupApproximation.Computability.MFRadicalQuine
import GroupApproximation.Computability.MFRadicalQuineSource
import GroupApproximation.Computability.MFRadicalGodel
import GroupApproximation.Computability.MFObserverBlindPromise
import GroupApproximation.Endpoint.MFObserverBlindPromiseAudit
import GroupApproximation.Computability.OperatorMFMarkovWitness
import GroupApproximation.Computability.CStarRecognitionConsequences
import GroupApproximation.Computability.PresentationCodes
import GroupApproximation.Computability.PresentationCodeCompleteness
import GroupApproximation.Computability.PresentationCodeList
import GroupApproximation.Computability.RabinVariantCode
import GroupApproximation.Computability.CoprodCode
import GroupApproximation.Computability.AmalgamCode
import GroupApproximation.Computability.AmalgamCodeSemantics
import GroupApproximation.Computability.AmalgamCodePushout
import GroupApproximation.Computability.BenignMapEmbCode
import GroupApproximation.Computability.BenignInfCode
import GroupApproximation.Computability.BenignInfCodeSemantics
import GroupApproximation.Computability.BenignSupCode
import GroupApproximation.Computability.BenignComapCode
import GroupApproximation.Computability.BenignComapThreeCode
import GroupApproximation.Computability.CodedProfiniteWitnessThree
import GroupApproximation.Computability.BenignMapEmbRopeInput
import GroupApproximation.Computability.DirectProductCodeSemantics
import GroupApproximation.Computability.AdianRabinVariantTransform
import GroupApproximation.Computability.RawWord
import GroupApproximation.Computability.RawTransform
import GroupApproximation.Computability.RawTransformPrimrec
import GroupApproximation.Computability.OperatorMFMarkovAtCodes
import GroupApproximation.Computability.StringRewriting
import GroupApproximation.Computability.UniversalCodeHalting
import GroupApproximation.Computability.UniversalCode
import GroupApproximation.Computability.RewriteMonoid
import GroupApproximation.Computability.RewriteInvariants
import GroupApproximation.Computability.RewriteConfluence
import GroupApproximation.Computability.AdianRabinMarkovProperty
import GroupApproximation.Computability.WordProblemRE
import GroupApproximation.GroupTheory.FiniteWordAutomaton
import GroupApproximation.GroupTheory.FiniteRelatorQuotient
import GroupApproximation.GroupTheory.QuotientProtectedPair
import GroupApproximation.GroupTheory.TreeGraphGeometry
import GroupApproximation.Sofic.AdjointMatrix
import GroupApproximation.Sofic.HilbertUltraproductFaithful
import GroupApproximation.Sofic.HilbertUltraproductSeparating
import GroupApproximation.Sofic.KOmegaHilbert
import GroupApproximation.Sofic.OmegaOperatorUltraproduct
import GroupApproximation.Sofic.OmegaAlmostRepresentation
import GroupApproximation.Sofic.OmegaCoronaFinite
import GroupApproximation.Sofic.OmegaKazhdanCompression
import GroupApproximation.Sofic.OmegaWeightedAmbient
import GroupApproximation.Sofic.UltrafilterSubsequence
import GroupApproximation.Sofic.HilbertUltraproductSpace
import GroupApproximation.Sofic.ProjectionRankFlip
import GroupApproximation.Sofic.ExactInvolutionCut
import GroupApproximation.Sofic.InvolutiveTwoSheet
import GroupApproximation.Sofic.PauliBranchTransfer
import GroupApproximation.Sofic.DoublePauliCoefficient
import GroupApproximation.Sofic.TransitionGaugeInvariance
import GroupApproximation.Sofic.CoefficientAlternatingReynolds
import GroupApproximation.Sofic.MixedCommutatorDihedral
import GroupApproximation.Sofic.SpectralCapture
import GroupApproximation.Sofic.NegativeCornerModel
import GroupApproximation.Sofic.BlockCliffordLamp
import GroupApproximation.Sofic.BlockingFamilyRadical
import GroupApproximation.Sofic.CliffordLampGroup
import GroupApproximation.Monsters.AffineSL3Doubling
import GroupApproximation.Monsters.CliffordAlgebraLamp
import GroupApproximation.Monsters.CliffordLampLocallyFinite
import GroupApproximation.Monsters.AffineSL3Scaling
import GroupApproximation.Monsters.ExplicitLinearModel
import GroupApproximation.Monsters.ExplicitLinearModelScaling
import GroupApproximation.Monsters.CyclicBaseCalibration
import GroupApproximation.Monsters.LiteralCyclicCalibration
import GroupApproximation.Monsters.LiteralCyclicRelatorCount
import GroupApproximation.Monsters.LiteralP13MatrixModel
import GroupApproximation.Monsters.SL3ElementaryGeneration
import GroupApproximation.Monsters.P13SteinbergCalculus
import GroupApproximation.Monsters.P13UnipotentInjectivity
import GroupApproximation.Monsters.P13WeylCalculus
import GroupApproximation.Monsters.P13Weyl23Calculus
import GroupApproximation.Monsters.P13Weyl13Calculus
import GroupApproximation.Monsters.P13WeylFourthPowers
import GroupApproximation.Monsters.P13SL2ComparisonAll
import GroupApproximation.Monsters.SL3BlockEmbeddingAll
import GroupApproximation.Monsters.P13ParabolicKernel
import GroupApproximation.Monsters.P13ColumnLift
import GroupApproximation.Monsters.P13MonomialMachine
import GroupApproximation.Monsters.P13DescentCore
import GroupApproximation.Monsters.P13WordDescent
import GroupApproximation.Monsters.P13DescentCases
import GroupApproximation.Monsters.P13Completeness
import GroupApproximation.Monsters.P13DescentMaster
import GroupApproximation.Monsters.LiteralBaseResiduallyFinite
import GroupApproximation.Monsters.P13LowerUnipotentInjectivity
import GroupApproximation.Monsters.SL2BraidPresentation
import GroupApproximation.Monsters.P13SL2Comparison
import GroupApproximation.Monsters.SL3BlockEmbedding
import GroupApproximation.Monsters.SL2WeylRelations
import GroupApproximation.Monsters.MoebiusIrrationalAction
import GroupApproximation.GroupTheory.FiniteCyclicHom
import GroupApproximation.GroupTheory.HNNBrittonPinch
import GroupApproximation.GroupTheory.HNNBrittonSpelling
import GroupApproximation.GroupTheory.HNNBrittonCyclic
import GroupApproximation.GroupTheory.FiniteHNNFreeLabelAction
import GroupApproximation.GroupTheory.FiniteHNNFreeLabelFaithful
import GroupApproximation.GroupTheory.FiniteHNNResiduallyFinite
import GroupApproximation.Monsters.SL2PingPong
import GroupApproximation.Monsters.SL2Completeness
import GroupApproximation.Monsters.P13BlockSL2
import GroupApproximation.Monsters.CyclicBaseLEFObstruction
import GroupApproximation.Sofic.ScalingFamilyPresentation
import GroupApproximation.Sofic.ScalingFamilyRelatorCount
import GroupApproximation.Sofic.ScalingFamilyLinearWitness
import GroupApproximation.Sofic.ScalingFamilyEndpoint
import GroupApproximation.Sofic.LiteralNonMFLinearWitness
import GroupApproximation.Sofic.WitnessVerticalResiduallyFinite
import GroupApproximation.Sofic.AlternatingLampVisibleQuotient
import GroupApproximation.Sofic.LiteralNonMFEndpoint
import GroupApproximation.Sofic.LiteralBaseTranslationLattice
import GroupApproximation.Sofic.LiteralBaseDoublingIndex
import GroupApproximation.Sofic.LiteralBaseP13Replay
import GroupApproximation.Sofic.LiteralBasePropertyTBridge
import GroupApproximation.Sofic.LiteralBaseTwoGenerator
import GroupApproximation.Sofic.LiteralFiniteDimensionalObstruction
import GroupApproximation.Sofic.LiteralUniversalHorn
import GroupApproximation.Sofic.LiteralPresentationRadius
import GroupApproximation.Sofic.LiteralMarkedCylinderTopology
import GroupApproximation.Sofic.LiteralMarkedCylinder
import GroupApproximation.Sofic.LiteralSixGenerator
import GroupApproximation.Sofic.LiteralSignFreeQuotient
import GroupApproximation.Sofic.LiteralTietzePresentation
import GroupApproximation.Sofic.LiteralWitnessConsequences
import GroupApproximation.Sofic.MarkedCompressionInclusionData
import GroupApproximation.Sofic.CompressionDefectSquare
import GroupApproximation.Sofic.MarkedCompressionGroup
import GroupApproximation.Sofic.ChosenMarkedCylinder
import GroupApproximation.Sofic.ChosenUniversalHorn
import GroupApproximation.Sofic.KazhdanCompressorCorner
import GroupApproximation.Sofic.MarkedCompressionVectorChain
import GroupApproximation.Sofic.MarkedCompressionSequentialKill
import GroupApproximation.Sofic.MarkedCompressionRootCapture
import GroupApproximation.Sofic.FiniteNormalAverageCorner
import GroupApproximation.Sofic.FiniteNormalCompressionObstruction
import GroupApproximation.Sofic.FiniteNormalCoronaObstruction
import GroupApproximation.Sofic.OperatorMF
import GroupApproximation.Sofic.CDEOperatorMF
import GroupApproximation.Sofic.MFDefinitions
import GroupApproximation.Sofic.MFRepresentationVariants
import GroupApproximation.Sofic.CDEMFRadical
import GroupApproximation.Sofic.RadicalSeparation
import GroupApproximation.Sofic.NormMFUniversalQuotient
import GroupApproximation.Sofic.NormMFUniversalCorona
import GroupApproximation.Sofic.NormMFCoronaRadical
import GroupApproximation.Sofic.NormMFPrintedConsequences
import GroupApproximation.Sofic.NormallyGeneratedMFObstruction
import GroupApproximation.Sofic.OperatorMFPositiveControls
import GroupApproximation.Sofic.OperatorMFProduct
import GroupApproximation.Sofic.OperatorMFHNNCyclicBlocks
import GroupApproximation.Sofic.LocallyFiniteMF
import GroupApproximation.Sofic.CentralInvolutionFinite
import GroupApproximation.Sofic.OperatorMFQuotientNonclosure
import GroupApproximation.Sofic.OperatorMFFreeProductConsequences
import GroupApproximation.Computability.SeededSelfAwareMFCompiler
import GroupApproximation.Sofic.MarkedCompressionProperness
import GroupApproximation.Sofic.ChosenMarkedPresentation
import GroupApproximation.Sofic.ChosenNonMFTheorem
import GroupApproximation.Endpoint.ChosenNonMFAudit
import GroupApproximation.Endpoint.SignFreeCompressionAudit
import GroupApproximation.Sofic.ChosenNonMFEndpoint
import GroupApproximation.Sofic.NormUltraproductSequentialExtraction
import GroupApproximation.Sofic.NormMFConsequences
import GroupApproximation.Sofic.Asymptotics
import GroupApproximation.Sofic.ExteriorMFProfile
import GroupApproximation.Sofic.UnitaryProjectionBalance
import GroupApproximation.Sofic.ExplicitNonMFBase
import GroupApproximation.Steinberg.QuotientExactness
import GroupApproximation.Domination.Audit
import GroupApproximation.Sofic.AlmostAutomorphism
import GroupApproximation.PropertyT.A2System
import GroupApproximation.PropertyT.A2ClassTwoOrthogonality
import GroupApproximation.PropertyT.A2MagicGraph
import GroupApproximation.PropertyT.A2MagicGraphEstimates
import GroupApproximation.PropertyT.A2MagicLaplacian
import GroupApproximation.PropertyT.A2MagicEnergy
import GroupApproximation.PropertyT.A2MagicHilbert
import GroupApproximation.Kazhdan.PositiveOperatorGap
import GroupApproximation.Kazhdan.ExactHodgeCertificate
import GroupApproximation.Sofic.LiteralBaseP13RotationQuotient
import GroupApproximation.PropertyT.FreeAlgebraDegree
import GroupApproximation.PropertyT.FreeRootFiltration
import GroupApproximation.PropertyT.FreeRootActions
import GroupApproximation.PropertyT.FreeRootPlane
import GroupApproximation.PropertyT.FreeRootPlaneMassBase
import GroupApproximation.PropertyT.FreeRootPlaneMass
import GroupApproximation.PropertyT.FreeRootFunctionalValuation
import GroupApproximation.PropertyT.FreeRootPlaneFourier
import GroupApproximation.PropertyT.FreeRootCharacterValuationBase
import GroupApproximation.PropertyT.FreeRootCharacterValuation
import GroupApproximation.PropertyT.FiniteFieldElementaryPropertyT
import GroupApproximation.PropertyT.FreeElementaryPropertyT
import GroupApproximation.PropertyT.FiniteTypeCharacteristicTwoPropertyT
import GroupApproximation.Leavitt.FiniteFieldLeavitt
import GroupApproximation.PropertyT.A2Kazhdan
import GroupApproximation.PropertyT.ClassTwoNormalForm
import GroupApproximation.PropertyT.ClassTwoApproximation
import GroupApproximation.Matching.DirectedCoarea
import GroupApproximation.Kazhdan.KazhdanImprovement
import GroupApproximation.Kazhdan.Kazhdan
import GroupApproximation.Kazhdan.KazhdanDisplacementCriterion
import GroupApproximation.Kazhdan.HilbertComplexification
import GroupApproximation.Kazhdan.KazhdanComplex
import GroupApproximation.Kazhdan.KazhdanUniverse
import GroupApproximation.Kazhdan.KazhdanFiniteGeneration
import GroupApproximation.PropertyT.CharacterMass
import GroupApproximation.Leavitt.RankTwoCompression
import GroupApproximation.Kazhdan.KazhdanControl
import GroupApproximation.Kazhdan.AlmostMinimalDisplacement
import GroupApproximation.Kazhdan.DelormeFixedPoint
import GroupApproximation.Kazhdan.ShalomFinitePresentation
import GroupApproximation.Kazhdan.UltralimitGeometry
import GroupApproximation.Kazhdan.UltralimitGaussianBoundedness
import GroupApproximation.Kazhdan.GaussianPositiveDefinite
import GroupApproximation.Kazhdan.HilbertCircumcenter
import GroupApproximation.Kazhdan.KazhdanFixedSpace
import GroupApproximation.Kazhdan.HilbertConvexFixedPoint
import GroupApproximation.PropertyT.InvolutionSplitting
import GroupApproximation.PropertyT.FiniteInvolutionDecomposition
import GroupApproximation.Kazhdan.HilbertEpsilonOrthogonality
import GroupApproximation.PropertyT.FiniteGroupAverage
import GroupApproximation.PropertyT.FiniteOrbitRepresentation
import GroupApproximation.PropertyT.FiniteClassTwoOrthogonality
import GroupApproximation.PropertyT.OrthogonalRepresentationDecomposition
import GroupApproximation.PropertyT.FiniteClassTwoDecompositionBound
import GroupApproximation.PropertyT.ClassTwoOrthogonality
import GroupApproximation.PropertyT.NormalEdgeCodistance
import GroupApproximation.Kazhdan.KazhdanGenerators
import GroupApproximation.Kazhdan.KazhdanOrthogonal
import GroupApproximation.Kazhdan.FixedSpaceCompression
import GroupApproximation.Kazhdan.FixedSpaceStabilizer
import GroupApproximation.Kazhdan.FixedSpaceDefect
import GroupApproximation.Kazhdan.KazhdanProjection
import GroupApproximation.Kazhdan.InvariantDisplacement
import GroupApproximation.Kazhdan.KazhdanFiniteModel
import GroupApproximation.Kazhdan.KazhdanGNS
import GroupApproximation.Kun.KunFiniteMarkov
import GroupApproximation.Kun.KunBoundary
import GroupApproximation.Kun.KunRounding
import GroupApproximation.Kun.KunThreshold
import GroupApproximation.Kun.KunGeneratorGraph
import GroupApproximation.Kun.KunSupport
import GroupApproximation.Kun.KunIndicatorRounding
import GroupApproximation.Kun.KunQuantitativeRounding
import GroupApproximation.Kun.KunRemoval
import GroupApproximation.Kun.KunAsymptoticRemoval
import GroupApproximation.Kun.KunSmallBoundary
import GroupApproximation.Kun.KunPartition
import GroupApproximation.Kun.KunFinitePartition
import GroupApproximation.Kun.KunDiagonalPartition
import GroupApproximation.Kun.KunDecomposition
import GroupApproximation.Kun.KunFixedDecomposition
import GroupApproximation.KunThom.KunThomDiagonal
import GroupApproximation.KunThom.KunThomCorrelation
import GroupApproximation.KunThom.KunThomFiniteMarkov
import GroupApproximation.KunThom.KunThomRounding
import GroupApproximation.KunThom.KunThomParameters
import GroupApproximation.KunThom.KunThomTheorem
import GroupApproximation.Kun.KunSpectralCounterexample
import GroupApproximation.Matching.MaximalCutRepair
import GroupApproximation.Sofic.SoficRestriction
import GroupApproximation.Sofic.IntersectionReduction
import GroupApproximation.Sofic.RelativeIntersectionPermanence
import GroupApproximation.Matching.EssentialExpanderRepair
import GroupApproximation.KunThom.KunThomEssential
import GroupApproximation.Kun.KunPartitionBoundary
import GroupApproximation.Kun.KunPartitionCrossing
import GroupApproximation.Kun.KunBlockGraph
import GroupApproximation.Kun.KunRepairGraph
import GroupApproximation.Kun.KunMarkerSelection
import GroupApproximation.Kun.KunLocalNeighborhood
import GroupApproximation.Kun.KunBadBlocks
import GroupApproximation.Kun.KunSelectiveRepairGraph
import GroupApproximation.Kun.KunSelectiveRepairExpansion
import GroupApproximation.Kun.KunRefinedInvariance
import GroupApproximation.Kun.KunRepairExpansion
import GroupApproximation.Kun.KunUniformMovement
import GroupApproximation.Kun.KunUniformRemoval
import GroupApproximation.Kun.KunUniformRounding
import GroupApproximation.Kun.KunUniformDecompositionStep
import GroupApproximation.Criterion.CompressionSetup
import GroupApproximation.Criterion.ExactCompression
import GroupApproximation.Criterion.ChainConditionCompression
import GroupApproximation.Criterion.TensorInvariantRigidity
import GroupApproximation.Criterion.ClosedEnvelopeCompression
import GroupApproximation.Criterion.CommutantRigidity
import GroupApproximation.Criterion.CompressionCentralizerDefect
import GroupApproximation.Sofic.NormMFResidualExactQuotient
import GroupApproximation.Sofic.IntrinsicCompressionDefect
import GroupApproximation.Sofic.KazhdanAsymptoticCommutant
import GroupApproximation.Sofic.ScaledKazhdanTransport
import GroupApproximation.Sofic.IntertwinerKazhdanTransport
import GroupApproximation.Sofic.TorsionCompressionCollapse
import GroupApproximation.Sofic.MFRelationClosure
import GroupApproximation.Sofic.MFTraceRecognition
import GroupApproximation.Sofic.InvolutionRankMass
import GroupApproximation.Sofic.CollisionCapacityDetectors
import GroupApproximation.Sofic.ExactInvolutionLifts
import GroupApproximation.Kazhdan.ApproximateCircumcenter
import GroupApproximation.Sofic.InvolutionMicrostateTools
import GroupApproximation.Sofic.InvolutionOrbitMicrostates
import GroupApproximation.Sofic.InvolutionCollapseMetric
import GroupApproximation.Sofic.InvolutionCollapseProfile
import GroupApproximation.Sofic.InvolutionCollapseCocycle
import GroupApproximation.Sofic.InvolutionCollapseCenter
import GroupApproximation.Sofic.InvolutionCollapseIndexCapture
import GroupApproximation.Sofic.InvolutionCollapseEndpointPrep
import GroupApproximation.Sofic.InvolutionCollapseEndpoint
import GroupApproximation.Sofic.ProjectionCompressionCollapse
import GroupApproximation.Sofic.SpectralCompression
import GroupApproximation.Manuscript.SpectralPaper.MainTheorems
import GroupApproximation.Manuscript.SpectralPaper.Audit
import GroupApproximation.Sofic.TorsionSpectralCollapse
import GroupApproximation.Sofic.TorsionActiveCore
import GroupApproximation.Sofic.FiniteOrderRankMass
import GroupApproximation.Sofic.ActiveCoreAlmostRepresentation
import GroupApproximation.Sofic.FiniteOrderNormalGenerator
import GroupApproximation.Sofic.SimpleTorsionDichotomy
import GroupApproximation.Sofic.MatricialStabilityRadical
import GroupApproximation.Sofic.PropertyTFreeMFCollapse
import GroupApproximation.Sofic.CommutingLampCollapse
import GroupApproximation.Sofic.CommutingLampQuotientSofic
import GroupApproximation.Algebra.HNNTorsionFree
import GroupApproximation.Sofic.GreendlingerCombinatorics
import GroupApproximation.Sofic.GreendlingerConjugation
import GroupApproximation.Sofic.GreendlingerNormalForm
import GroupApproximation.Sofic.GreendlingerOneRelator
import GroupApproximation.Sofic.GreendlingerExpression
import GroupApproximation.Sofic.GreendlingerCancellation
import GroupApproximation.Sofic.GreendlingerDescent
import GroupApproximation.Sofic.GreendlingerPiece
import GroupApproximation.Sofic.IntegerLampSurvival
import GroupApproximation.Monsters.LiteralBaseCompleteness
import GroupApproximation.Sofic.LEFMarkedCompression
import GroupApproximation.Algebra.FinitePresentationTietze
import GroupApproximation.Algebra.PartialCommutationLamp
import GroupApproximation.Algebra.FiniteResidual
import GroupApproximation.Algebra.VisibleQuotient
import GroupApproximation.Algebra.FiniteResidualCommensurability
import GroupApproximation.Algebra.AlternatingLampNoncommensurable
import GroupApproximation.Algebra.TorsionFreeRank
import GroupApproximation.Algebra.AmenableMFProof
import GroupApproximation.Algebra.PermutationalWreath
import GroupApproximation.Algebra.PermutationalWreathSimple
import GroupApproximation.Algebra.PermutationalWreathAmenable
import GroupApproximation.Algebra.PermutationalWreathLinear
import GroupApproximation.Algebra.AbelianLampPushforward
import GroupApproximation.Algebra.AbelianLampTelescopeKernel
import GroupApproximation.Algebra.PermutationalWreathRadicalTame
import GroupApproximation.Algebra.WreathLampPushforward
import GroupApproximation.Algebra.WreathTelescopeUnion
import GroupApproximation.Algebra.IntJacobson
import GroupApproximation.Algebra.FiniteTypeField
import GroupApproximation.Algebra.Malcev
import GroupApproximation.Algebra.MalcevLinear
import GroupApproximation.Algebra.WreathSplitQuotient
import GroupApproximation.Algebra.PerfectLamp
import GroupApproximation.Algebra.ModTwoLampParity
import GroupApproximation.Sofic.FiniteDimensionalResidual
import GroupApproximation.Sofic.ThreeRadicalsCoincide
import GroupApproximation.Sofic.LinearResidual
import GroupApproximation.Sofic.FourRadicalsCoincide
import GroupApproximation.Sofic.FiveRadicalsCoincide
import GroupApproximation.Sofic.BlockAmplificationRepair
import GroupApproximation.Sofic.AmplifiedBlockNorms
import GroupApproximation.Sofic.InducedCoronaMF
import GroupApproximation.Sofic.SoficPiProduct
import GroupApproximation.Sofic.AmenableActionSofic
import GroupApproximation.Sofic.CoAmenableActionSofic
import GroupApproximation.Sofic.WreathPermLayer
import GroupApproximation.Sofic.WreathChartLamp
import GroupApproximation.Sofic.GeneralizedWreathSofic
import GroupApproximation.Sofic.AscendingHNNWreathSofic
import GroupApproximation.Sofic.RegularActionSofic
import GroupApproximation.Algebra.WreathTelescopeTower
import GroupApproximation.Algebra.WreathFunctor
import GroupApproximation.Algebra.GraphProduct
import GroupApproximation.Algebra.GraphProductAction
import GroupApproximation.Analysis.PeterWeylProfinite
import GroupApproximation.Analysis.CompactHaar
import GroupApproximation.Analysis.CompactIntegralOperator
import GroupApproximation.Algebra.TietzeFinitePresentation
import GroupApproximation.Algebra.FinitePresentationKernel
import GroupApproximation.Sofic.FiniteIndexRigidity
import GroupApproximation.Algebra.FreePermutationalPrecursor
import GroupApproximation.Algebra.FreePrecursorUniversal
import GroupApproximation.Algebra.FreePrecursorPresentation
import GroupApproximation.Sofic.UniversalFactorization
import GroupApproximation.Sofic.RadicalFunctoriality
import GroupApproximation.Algebra.SplitExtensionFailure
import GroupApproximation.Sofic.SplitExtensionEndpoint
import GroupApproximation.Sofic.CommensurabilityInvariance
import GroupApproximation.Sofic.Type0Transfer
import GroupApproximation.Sofic.FiniteIndexNonMF
import GroupApproximation.Sofic.DossierAuditAddenda
import GroupApproximation.Sofic.SoficNonMFAssembly
import GroupApproximation.Sofic.SoficActionOrbits
import GroupApproximation.Sofic.SoficActionApproximationBelow
import GroupApproximation.Sofic.AscendingHNNFolner
import GroupApproximation.Sofic.AscendingHNNDiagonalOrbits
import GroupApproximation.Sofic.TargetEquivalence
import GroupApproximation.Sofic.InducedFiniteDimensional
import GroupApproximation.Kazhdan.IntegerNotKazhdan
import GroupApproximation.Sofic.SoficAction
import GroupApproximation.Sofic.SoficActionEmbedding
import GroupApproximation.Sofic.AscendingHNNSoficDescent
import GroupApproximation.Sofic.SoficActionFiniteOrbits
import GroupApproximation.Sofic.SoficActionExamples
import GroupApproximation.Sofic.MaxDisplacement
import GroupApproximation.Sofic.CoronaSubsequence
import GroupApproximation.Sofic.CyclicStack
import GroupApproximation.Sofic.SoficActionCyclicExtension
import GroupApproximation.Sofic.AscendingHNNNotKazhdan
import GroupApproximation.Sofic.AscendingHNNCosetActionSofic
import GroupApproximation.Sofic.SoficActionChabauty
import GroupApproximation.Sofic.SoficActionSum
import GroupApproximation.Sofic.AscendingHNNStabilizer
import GroupApproximation.Sofic.AscendingHNNDoubleCosets
import GroupApproximation.Sofic.AscendingHNNWreathWitness
import GroupApproximation.Sofic.AscendingHNNSplitExtension
import GroupApproximation.Sofic.AscendingHNNTelescopeRadical
import GroupApproximation.Sofic.AscendingHNNFullTelescopeRadical
import GroupApproximation.Sofic.PerfectLampCompressionRadical
import GroupApproximation.Sofic.CompressionWreathFinitelyGenerated
import GroupApproximation.Sofic.AlternatingLampExactRadical
import GroupApproximation.Sofic.FinitePerfectLampExactRadical
import GroupApproximation.Sofic.AlternatingLampBohrResidual
import GroupApproximation.Manuscript.MFRadicals.Definitions
import GroupApproximation.Manuscript.MFRadicals.SemanticClosure
import GroupApproximation.Manuscript.MFRadicals.Compression
import GroupApproximation.Manuscript.MFRadicals.ExplicitSeed
import GroupApproximation.Manuscript.MFRadicals.FullRadical
import GroupApproximation.Manuscript.MFRadicals.SimpleSofic
import GroupApproximation.Manuscript.MFRadicals.PerfectLampExact
import GroupApproximation.Manuscript.MFRadicals.AlternatingFamily
import GroupApproximation.Manuscript.MFRadicals.RadicalComputer
import GroupApproximation.Manuscript.MFRadicals.FinitePerfectLamp
import GroupApproximation.Manuscript.MFRadicals.TargetEquivalence
import GroupApproximation.Manuscript.MFRadicals.MainTheorems
import GroupApproximation.Manuscript.OneSidedMFRadical.LiteralMFClosure
import GroupApproximation.Manuscript.OneSidedMFRadical.ResidualCalculus
import GroupApproximation.Manuscript.OneSidedMFRadical.FiniteDimensionalCommutant
import GroupApproximation.Manuscript.OneSidedMFRadical.StableFiniteness
import GroupApproximation.Manuscript.OneSidedMFRadical.UniversalFactorization
import GroupApproximation.Manuscript.OneSidedMFRadical.PrescribedQuotients
import GroupApproximation.Manuscript.OneSidedMFRadical.ClosurePullback
import GroupApproximation.Manuscript.OneSidedMFRadical.DefectHS
import GroupApproximation.Manuscript.OneSidedMFRadical.KazhdanTransport
import GroupApproximation.Manuscript.OneSidedMFRadical.NormalKazhdan
import GroupApproximation.Manuscript.OneSidedMFRadical.KazhdanProjectionOrder
import GroupApproximation.Manuscript.OneSidedMFRadical.KazhdanProjectionOrderLiteral
import GroupApproximation.Manuscript.OneSidedMFRadical.CentralCoronaCorner
import GroupApproximation.Manuscript.OneSidedMFRadical.CompressionCriterion
import GroupApproximation.Manuscript.OneSidedMFRadical.DefectSaturation
import GroupApproximation.Manuscript.OneSidedMFRadical.ShadowResidual
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedDefectShadow
import GroupApproximation.Manuscript.OneSidedMFRadical.Audit
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedDefect
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedCriterion
import GroupApproximation.Manuscript.OneSidedMFRadical.CurrentManuscriptDefinitionRepairs
import GroupApproximation.Manuscript.NonMF.LiteralEDirectCriterion
import GroupApproximation.Manuscript.NonMF.SimpleInDefect
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedAudit
import GroupApproximation.Manuscript.OneSidedMFRadical.RankTwelveConfiguration
import GroupApproximation.Manuscript.OneSidedMFRadical.RankTwelveEJZInstance
import GroupApproximation.Manuscript.OneSidedMFRadical.RankTwelveAudit
import GroupApproximation.Manuscript.OneSidedMFRadical.RankTwelveSimplicity
import GroupApproximation.Endpoint.MFRadicalPaperAudit
import GroupApproximation.Sofic.TelescopeLimitKernel
import GroupApproximation.Sofic.ProfiniteTwins
import GroupApproximation.Sofic.AlternatingLampLiteralPackage
import GroupApproximation.Sofic.LiteralDoublingWreathNonMF
import GroupApproximation.Sofic.CoronaRadicalPullback
import GroupApproximation.Sofic.MoverGeneration
import GroupApproximation.Sofic.HereditaryNonsoficDescent
import GroupApproximation.Sofic.SmallCancellationRouter
import GroupApproximation.Sofic.ConcreteCompressionSource
import GroupApproximation.Sofic.DefectSaturation
import GroupApproximation.Sofic.KazhdanSignCriterion
import GroupApproximation.Sofic.IntrinsicCompressionMFRadical
import GroupApproximation.Sofic.UltraproductAdjointAmbient
import GroupApproximation.Sofic.UltraproductDedekindFinite
import GroupApproximation.Sofic.UltraproductKazhdanProjection
import GroupApproximation.Sofic.UltraproductKazhdanTransport
import GroupApproximation.Sofic.ManuscriptKazhdanTransport
import GroupApproximation.Sofic.KazhdanTransportAnyUniverse
import GroupApproximation.Sofic.NormalKazhdanCompressionObstruction
import GroupApproximation.Sofic.KazhdanCompressionFunctorial
import GroupApproximation.Sofic.NormalKazhdanMFRadical
import GroupApproximation.Sofic.NormalKazhdanHyperlinearKilled
import GroupApproximation.Sofic.CoronaImageNormalKazhdan
import GroupApproximation.Sofic.QuestionTwoReduction
import GroupApproximation.Sofic.TorsionFreeFullMFRadical
import GroupApproximation.Sofic.OpToHSShadowResidual
import GroupApproximation.Sofic.TorsionFreeFullMFConsequences
import GroupApproximation.Sofic.TensorPowerAmplification
import GroupApproximation.Sofic.TensorPowerTransport
import GroupApproximation.Algebra.ProductFinitePresentation
import GroupApproximation.Algebra.Amenable
import GroupApproximation.Algebra.AmenableMean
import GroupApproximation.Algebra.AmenableInt
import GroupApproximation.Algebra.AmenableLocallyFiniteByInt
import GroupApproximation.Algebra.AmenableConstructions
import GroupApproximation.Algebra.AmenableRat
import GroupApproximation.Sofic.CliffordBSAmenable
import GroupApproximation.Sofic.ProductMultiplicity
import GroupApproximation.Sofic.ProductMultiplicityRank
import GroupApproximation.Sofic.ContinuumMultiplicity
import GroupApproximation.Sofic.ContinuumFamilyCriterion
import GroupApproximation.Sofic.ContinuumFromNormalSubgroups
import GroupApproximation.Sofic.OperatorMFPairAmplification
import GroupApproximation.Sofic.OperatorMFLocalNormalization
import GroupApproximation.Sofic.MarkedGroupTopology
import GroupApproximation.Sofic.MarkedMFClosed
import GroupApproximation.Criterion.FiniteQuotientBlindness
import GroupApproximation.Criterion.LocalCriterion
import GroupApproximation.Criterion.LocalizedApproximation
import GroupApproximation.Criterion.SelectionOutput
import GroupApproximation.Matching.Pinning
import GroupApproximation.Matching.Refinement
import GroupApproximation.Matching.Selection
import GroupApproximation.Matching.MedianNormalization
import GroupApproximation.Sofic.LEF
import GroupApproximation.Sofic.FinitelyPresentedLEF
import GroupApproximation.Sofic.ThompsonFObstruction
import GroupApproximation.Sofic.AugmentationExtension
import GroupApproximation.Criterion.Scheme
import GroupApproximation.Criterion.Criterion
import GroupApproximation.Matching.BlockEnumeration
import GroupApproximation.Matching.BlockIndex
import GroupApproximation.Matching.ComponentDivergence
import GroupApproximation.Matching.GeneratorWords
import GroupApproximation.Matching.BlockWordCrossing
import GroupApproximation.Matching.BlockTransport
import GroupApproximation.Matching.ComponentRefinement
import GroupApproximation.Matching.DecompositionRefinement
import GroupApproximation.Matching.FiniteGroupoidCounting
import GroupApproximation.Matching.FiniteGroupoidPresentation
import GroupApproximation.Matching.FinitePartialBijection
import GroupApproximation.Matching.AsymptoticPartialBijection
import GroupApproximation.Matching.AsymptoticPartialGroupoid
import GroupApproximation.Matching.AsymptoticBlockArrow
import GroupApproximation.Matching.FiniteGroupoidBisection
import GroupApproximation.Matching.PartialBijectionSandwich
import GroupApproximation.Matching.FinitePartialClusterGroupoid
import GroupApproximation.Matching.PartialEquivarianceBoundary
import GroupApproximation.Matching.PartialTaggedExpansion
import GroupApproximation.Matching.ComponentInvolutionRepair
import GroupApproximation.Matching.RepairedComponentBisection
import GroupApproximation.Matching.BlockPartialBijection
import GroupApproximation.Matching.EdgeEditing
import GroupApproximation.Matching.GeneratorCrossing
import GroupApproximation.Matching.ExternalCompressorCrossing
import GroupApproximation.Matching.CompressionRefinement
import GroupApproximation.Matching.FiniteMedian
import GroupApproximation.Matching.NormalizedComponents
import GroupApproximation.Matching.ComponentPinning
import GroupApproximation.Matching.NormalizedVariation
import GroupApproximation.Matching.InverseNormalization
import GroupApproximation.Matching.GlobalVariation
import GroupApproximation.Matching.SlowThreshold
import GroupApproximation.Matching.FiniteMarkov
import GroupApproximation.Matching.MatchingPreparation
import GroupApproximation.Matching.MatchingSelection
import GroupApproximation.Matching.EdgeWitnessDistance
import GroupApproximation.Matching.EdgeWitnessRestriction
import GroupApproximation.Matching.GeneratorGraphEditing
import GroupApproximation.Matching.CompletionGraphEditing
import GroupApproximation.Matching.SelectedGraphComparison
import GroupApproximation.Matching.ConservativeMatching
import GroupApproximation.Criterion.CriterionAssembly
import GroupApproximation.Leavitt.Leavitt
import GroupApproximation.Leavitt.FiniteModuleObstruction
import GroupApproximation.Leavitt.UnitAdditiveSpan
import GroupApproximation.Leavitt.FiniteDualOrbit
import GroupApproximation.Leavitt.ElementaryWeylBridge
import GroupApproximation.Leavitt.AtlasProperInfiniteCorner
import GroupApproximation.Leavitt.TwoChildFiniteObstruction
import GroupApproximation.Leavitt.FinitePairedQuotientObstruction
import GroupApproximation.Leavitt.RobustPairedQuotientFloor
import GroupApproximation.Leavitt.FiniteTreeCoupling
import GroupApproximation.Leavitt.NonincidentFlagGram
import GroupApproximation.Leavitt.RawWordReynoldsGap
import GroupApproximation.Leavitt.S3S4BranchingBalance
import GroupApproximation.Leavitt.AryCorner
import GroupApproximation.Leavitt.FamilyRankFour
import GroupApproximation.Leavitt.RawSwapCompressors
import GroupApproximation.Leavitt.LeavittOverCommRing
import GroupApproximation.Leavitt.IntegralGeneration
import GroupApproximation.Leavitt.ElementaryPerfect
import GroupApproximation.Leavitt.AryProfile
import GroupApproximation.Leavitt.SelfSimilarityAlgebra
import GroupApproximation.Leavitt.PlaneEmbedding
import GroupApproximation.Leavitt.GeneralRankWords
import GroupApproximation.Leavitt.Collision19243
import GroupApproximation.Leavitt.GeneralScheme
import GroupApproximation.Leavitt.GeneralCornerTheorem
import GroupApproximation.Sofic.LEFSofic
import GroupApproximation.Sofic.NotVirtuallyLinear
import GroupApproximation.Sofic.FreeGroupResiduallyFinite
import GroupApproximation.Sofic.FreeProductSignReflection
import GroupApproximation.Endpoint.QuotientNonclosure
import GroupApproximation.Leavitt.AryLeavitt
import GroupApproximation.Leavitt.AryCornerMatrix
import GroupApproximation.Leavitt.AryEndpoints
import GroupApproximation.Leavitt.UniversalLeavittOver
import GroupApproximation.Leavitt.LeavittNormalForm
import GroupApproximation.Leavitt.DiagonalClassGroup
import GroupApproximation.KOne.GLIsElementary
import GroupApproximation.Leavitt.LeavittDiagonalClass
import GroupApproximation.Leavitt.BinaryLeavittDiagonal
import GroupApproximation.KOne.StableUnitsGenerators
import GroupApproximation.Leavitt.FamilyDiagonalClass
import GroupApproximation.KOne.FieldMatrixReduction
import GroupApproximation.Leavitt.LeavittDegreeZero
import GroupApproximation.Leavitt.FamilyDescent
import GroupApproximation.Leavitt.LeavittGradingSpans
import GroupApproximation.Leavitt.LeavittBalancedUnits
import GroupApproximation.Leavitt.LeavittWindowReduction
import GroupApproximation.Leavitt.BinaryLeavittWindow
import GroupApproximation.KOne.ScaledStreamRepresentation
import GroupApproximation.KOne.VandermondeExtraction
import GroupApproximation.KOne.GradedIndependence
import GroupApproximation.KOne.BaseChangeIndependence
import GroupApproximation.KOne.StableRankOne
import GroupApproximation.KOne.BalancedStableRank
import GroupApproximation.Leavitt.WhiteheadFlip
import GroupApproximation.KOne.ResidualNormalForm
import GroupApproximation.KOne.ResidualMoves
import GroupApproximation.KOne.ResidualReduction
import GroupApproximation.KOne.BalancedRegularity
import GroupApproximation.KOne.WindowProductClosure
import GroupApproximation.KOne.NilpotentTailKill
import GroupApproximation.KOne.IncomparableUnipotents
import GroupApproximation.KOne.ShapeCalculus
import GroupApproximation.KOne.GradedComponents
import GroupApproximation.KOne.PureTailNilpotency
import GroupApproximation.Leavitt.RankNormalForm
import GroupApproximation.KOne.DegreeShapeBridge
import GroupApproximation.KOne.CylinderCornerRank
import GroupApproximation.KOne.ZeroKOne
import GroupApproximation.KOne.WidthTwoReduction
import GroupApproximation.KOne.WindowNonnegReduction
import GroupApproximation.KOne.OppositeTranspose
import GroupApproximation.KOne.ThetaStable
import GroupApproximation.KOne.WindowNonposReduction
import GroupApproximation.KOne.CodeChangeInfrastructure
import GroupApproximation.KOne.CodeChangeSwap
import GroupApproximation.KOne.CodeChangeUnits
import GroupApproximation.KOne.PencilCore
import GroupApproximation.KOne.PencilForm
import GroupApproximation.KOne.CodePairTransport
import GroupApproximation.KOne.CodeScalarMoves
import GroupApproximation.KOne.CodeRelativeFullness
import GroupApproximation.KOne.CodeChangeGlue
import GroupApproximation.KOne.AtomPeel
import GroupApproximation.KOne.MixedCodeMoves
import GroupApproximation.KOne.GLPairNormalization
import GroupApproximation.KOne.PencilEntryArith
import GroupApproximation.KOne.CompleteCodeSupply
import GroupApproximation.KOne.GLVectorNormalization
import GroupApproximation.KOne.RowClearMove
import GroupApproximation.KOne.FullExtraction
import GroupApproximation.KOne.MirrorExtraction
import GroupApproximation.KOne.EntryStrip
import GroupApproximation.KOne.EntrywiseKill
import GroupApproximation.KOne.StackDichotomy
import GroupApproximation.KOne.RefinedCodes
import GroupApproximation.KOne.BalancedCodePencil
import GroupApproximation.KOne.EntrywiseKillMirror
import GroupApproximation.KOne.RefineStep
import GroupApproximation.KOne.StrictNegativePencil
import GroupApproximation.KOne.CodeShapeSupply
import GroupApproximation.KOne.PencilReshape
import GroupApproximation.KOne.RefineLoopDischarge
import GroupApproximation.Leavitt.MatrixDiagonalization
import GroupApproximation.Leavitt.LeavittSimplicity
import GroupApproximation.Leavitt.LeavittRankEquivalence
import GroupApproximation.Matching.FiniteGraph
import GroupApproximation.Leavitt.LeavittCorner
import GroupApproximation.Leavitt.LeavittMatrixCompression
import GroupApproximation.Leavitt.DiagonalCornerCompression
import GroupApproximation.Leavitt.DiagonalElementary
import GroupApproximation.Leavitt.LeavittSelfSimilarity
import GroupApproximation.Matching.Localization
import GroupApproximation.Leavitt.MatrixSelfSimilarity
import GroupApproximation.Matching.PermutationConservation
import GroupApproximation.Sofic.Sofic
import GroupApproximation.Sofic.SoficAmplification
import GroupApproximation.Sofic.SoficUltraproduct
import GroupApproximation.Sofic.HyperlinearMetric
import GroupApproximation.Sofic.Hyperlinear
import GroupApproximation.Sofic.HyperlinearAmplification
import GroupApproximation.Quantum.FiniteMeasurement
import GroupApproximation.Sofic.HyperlinearNonScalar
import GroupApproximation.Sofic.HyperlinearScalar
import GroupApproximation.Sofic.AntipodalTraceExtraction
import GroupApproximation.Sofic.AntipodalRadicalCollision
import GroupApproximation.Sofic.CliffordPhaseExtraction
import GroupApproximation.Sofic.PhaseOrder
import GroupApproximation.Sofic.MonomialModel
import GroupApproximation.Sofic.PhasePropagation
import GroupApproximation.Sofic.LeavittTraceFloor
import GroupApproximation.Sofic.ScalarCocycle
import GroupApproximation.Sofic.CharacterCount
import GroupApproximation.Sofic.NoRounding
import GroupApproximation.Sofic.RootableGroupFiniteImages
import GroupApproximation.Sofic.PhaseCorrection
import GroupApproximation.Sofic.ScalarClass
import GroupApproximation.Sofic.RationalCharacter
import GroupApproximation.Sofic.UntwistSeparation
import GroupApproximation.Sofic.HeisenbergCentre
import GroupApproximation.Sofic.HyperlinearReduction
import GroupApproximation.Sofic.HyperlinearWeakBridge
import GroupApproximation.Sofic.HyperlinearUltraproductBridge
import GroupApproximation.Sofic.ImplementerCocycle
import GroupApproximation.Sofic.CoordinateTransfer
import GroupApproximation.Sofic.DivisibleInvisible
import GroupApproximation.Sofic.HyperlinearUltraproduct
import GroupApproximation.Sofic.NormTraceGap
import GroupApproximation.Sofic.FaithfullyTracedCoordinateNoGo
import GroupApproximation.Sofic.HilbertSchmidtAdjointGap
import GroupApproximation.Sofic.PermutationAdjointGap
import GroupApproximation.Sofic.AdjointOperatorNormRequirement
import GroupApproximation.Sofic.KazhdanTransportFiniteDimensionalInputs
import GroupApproximation.Sofic.WeakMFUltraproduct
import GroupApproximation.Sofic.OpAlmostRepresentation
import GroupApproximation.Sofic.NormMFResidualDetector
import GroupApproximation.Sofic.MarkedCompressionData
import GroupApproximation.Sofic.NormMFResidualFunctorial
import GroupApproximation.Sofic.ApproxInvolutionCorner
import GroupApproximation.Sofic.WeakMFTransfer
import GroupApproximation.Sofic.WeakMFRegularTrace
import GroupApproximation.Sofic.RegularCharacterGNS
import GroupApproximation.Sofic.KazhdanCorner
import GroupApproximation.Sofic.KazhdanCornerMatrices
import GroupApproximation.Sofic.WeakMFVectorGNS
import GroupApproximation.Sofic.KazhdanCornerModel
import GroupApproximation.Sofic.KazhdanCornerDiagonal
import GroupApproximation.Sofic.FreeLampReduction
import GroupApproximation.Sofic.PushoutEmbedding
import GroupApproximation.Sofic.SymmetricDoubleSubgroupReflection
import GroupApproximation.Sofic.FreeLampDoubleEmbedding
import GroupApproximation.Sofic.WeakMFNonsoficDouble
import GroupApproximation.Sofic.SoficFiniteSemidirect
import GroupApproximation.Sofic.SymmetricDoubleFlip
import GroupApproximation.Sofic.LineDouble
import GroupApproximation.Sofic.DoubleSoficTransfer
import GroupApproximation.Sofic.MFNonsoficDoubleEndpoint
import GroupApproximation.Sofic.FreeLampRigidity
import GroupApproximation.Sofic.ProfiniteClosure
import GroupApproximation.Sofic.CentralFreeLampCover
import GroupApproximation.Sofic.CentralCoverInheritance
import GroupApproximation.Sofic.CommutantPinning
import GroupApproximation.Sofic.NearAction
import GroupApproximation.Sofic.NearActionModel
import GroupApproximation.Sofic.LevelShiftObstruction
import GroupApproximation.Sofic.SoficPositiveControl
import GroupApproximation.Sofic.SemanticPositiveControls
import GroupApproximation.Sofic.SoficErrors
import GroupApproximation.Sofic.Normalization
import GroupApproximation.Sofic.InvolutiveCentralizerComponents
import GroupApproximation.Leavitt.Whitehead
import GroupApproximation.Covers.KazhdanCover
import GroupApproximation.Covers.PresentedEnlargement
import GroupApproximation.Covers.TableCover
import GroupApproximation.Covers.HyperlinearTableCover
import GroupApproximation.Leavitt.LeavittWords
import GroupApproximation.Leavitt.PrefixCode
import GroupApproximation.Leavitt.ElementaryGroup
import GroupApproximation.Leavitt.ElementaryRoots
import GroupApproximation.Leavitt.OuterRootLeavittRouting
import GroupApproximation.Leavitt.ElementaryStabilization
import GroupApproximation.Leavitt.RankFourCompressors
import GroupApproximation.Leavitt.RankTwelveCompressor
import GroupApproximation.Leavitt.ElementaryNormalGeneration
import GroupApproximation.Leavitt.RankTwelvePropertyT
import GroupApproximation.Leavitt.UniversalLeavitt
import GroupApproximation.Leavitt.UniversalRankFour
import GroupApproximation.Leavitt.UniversalPropertyT
import GroupApproximation.Leavitt.ZeroRangeObstruction
import GroupApproximation.PropertyTT.PaperStatements
import GroupApproximation.PropertyTT.NonsoficCorollary
import GroupApproximation.Leavitt.UniversalCompressionSetup
import GroupApproximation.Leavitt.ThompsonV
import GroupApproximation.Leavitt.ThompsonVEmbedding
import GroupApproximation.Leavitt.FamilyVEmbedding
import GroupApproximation.Leavitt.ThompsonVWitness
import GroupApproximation.Leavitt.ThompsonWitness
import GroupApproximation.Matching.MatchedComponents
import GroupApproximation.Sofic.SoficTransfer
import GroupApproximation.Sofic.SoficDirectedUnion
import GroupApproximation.Sofic.CliffordLampPermanence
import GroupApproximation.Sofic.IntegralLinearResiduallyFinite
import GroupApproximation.Sofic.SoficFiniteKernelSemidirect
import GroupApproximation.Sofic.SoficInvariantFiniteKernel
import GroupApproximation.Sofic.FiniteOrbitInvariantKernel
import GroupApproximation.Sofic.MappingTelescopeFiniteOrbits
import GroupApproximation.Sofic.SoficIntegerExtension
import GroupApproximation.Sofic.SoficTelescope
import GroupApproximation.Monsters.ExplicitIntegralLinearModel
import GroupApproximation.Endpoint.NonMFImpact
import GroupApproximation.Sofic.HyperlinearResidualDetector
import GroupApproximation.Sofic.FiniteLinearHammingGap
import GroupApproximation.Sofic.RelativeImplementerCentralizer
import GroupApproximation.Sofic.FiniteResidualKernel
import GroupApproximation.Sofic.InternalRadicalGap
import GroupApproximation.Sofic.AuxiliaryClassSeparation
import GroupApproximation.Sofic.StarGaussian
import GroupApproximation.Sofic.FermionicOptimality
import GroupApproximation.Endpoint.MainResults
import GroupApproximation.Endpoint.SimultaneousStability
import GroupApproximation.Endpoint.StructuralProfile
import GroupApproximation.Leavitt.UnitsGLProfile
import GroupApproximation.KOne.AllRanksElementary
import GroupApproximation.Kazhdan.KazhdanTextbook
import GroupApproximation.Monsters.Terminality
import GroupApproximation.Monsters.TwoConjugacyClasses
import GroupApproximation.Monsters.VerbalCompleteness
import GroupApproximation.Monsters.Protection
import GroupApproximation.Monsters.UniversalMFEventHorizon
import GroupApproximation.Monsters.UniversalFinitelyPresentedTorsionFreeGroup
import GroupApproximation.Monsters.TorsionFreeConjugacyExtension
import GroupApproximation.Monsters.HitchhikerPayload
import GroupApproximation.Endpoint.Audit
import GroupApproximation.Endpoint.Public
import GroupApproximation.Endpoint.ManuscriptStatements
import GroupApproximation.Sofic.SoficSequential
import GroupApproximation.KOne.WhiteheadQuotient
import GroupApproximation.KOne.ClassicalKOne
import GroupApproximation.KOne.FactorizationCertificate
import GroupApproximation.KOne.PaperStatements
import GroupApproximation.Leavitt.FiniteTypeCountable
import GroupApproximation.Leavitt.FiniteOutcomeCoarsening
import GroupApproximation.Leavitt.FiniteNoSignalingPairingBox
import GroupApproximation.Leavitt.FiniteBinaryFiberDecoder
import GroupApproximation.Leavitt.PauliCarrierBinaryGap
import GroupApproximation.Leavitt.ShiftEndomorphism
import GroupApproximation.Sofic.LocalCentralQuotientLifting
import GroupApproximation.Steinberg.KervaireSteinberg
import GroupApproximation.Criterion.FiniteDimensionalKill
import GroupApproximation.Sofic.KazhdanCliffordEpsilon
import GroupApproximation.Algebra.ZariskiClosedSubgroup
import GroupApproximation.Algebra.ZariskiDescendingChain
import GroupApproximation.Algebra.DyadicRationals
import GroupApproximation.Algebra.DiagonalCosetAction
import GroupApproximation.Algebra.WordMetric
import GroupApproximation.Monsters.LiteralDyadicCalibration
import GroupApproximation.Sofic.SoficByAmenablePermanence
import GroupApproximation.Analysis.PropertyTNonamenable
import GroupApproximation.Analysis.ResiduallyFiniteDimensional
import GroupApproximation.Analysis.MaximalCStarParagraphEndpoint
import GroupApproximation.Sofic.ManuscriptCentralSignCriterion
import GroupApproximation.Sofic.CollapseUniverseScopeDefs
import GroupApproximation.Sofic.CollapseUniverseScope
import GroupApproximation.Sofic.CollapseProfileBound
import GroupApproximation.Analysis.CStarTensorProductAdjointable
import GroupApproximation.Analysis.ExactnessPermanence
import GroupApproximation.Computability.SemigroupWordProblemRewriting
import GroupApproximation.Monsters.FournierFacioRealization
import GroupApproximation.Monsters.P13SpectralGap
import GroupApproximation.Sofic.CollapseProfileBoundNumeric
import GroupApproximation.Sofic.CollapseTransportDiagonalization
import GroupApproximation.Sofic.CollapseTransportDiagonalizationCommutant
import GroupApproximation.Sofic.CollapseWordMetric
import GroupApproximation.Sofic.GraphCliffordLamp
import GroupApproximation.Sofic.LiteralAffineCosetTransitivity
import GroupApproximation.Sofic.LiteralBlockGeometry
import GroupApproximation.Sofic.LiteralBlockNormalForm
import GroupApproximation.Sofic.LiteralLampKernelSplit
import GroupApproximation.Sofic.LiteralTelescopeCoreLEF
import GroupApproximation.Sofic.MatricialStabilityInstances
import GroupApproximation.Sofic.SimpleSoficEnvelope
import GroupApproximation.Sofic.SoficEnvelopeExistence
import GroupApproximation.Sofic.UltraproductIntertwinerTransport
import GroupApproximation.Sofic.UltraproductScaledTransport
import GroupApproximation.Sofic.MultiMoverUniversalUpgrade
import GroupApproximation.Sofic.AscendingHNNSeparableCosetAction
import GroupApproximation.Sofic.SimpleFullMFRadical
import GroupApproximation.Computability.RewriteDeterminism
import GroupApproximation.Analysis.NuclearityAmenability
import GroupApproximation.Computability.RewriteSimulation
import GroupApproximation.Monsters.NeumannContinuum
import GroupApproximation.Computability.UnaryCounterSimulation
import GroupApproximation.Computability.PostMachine
import GroupApproximation.Computability.PostMachineHalting
import GroupApproximation.Computability.HaltingReduction
import GroupApproximation.Computability.RewriteSimulationOn
import GroupApproximation.Sofic.SimpleLampNormalGeneration
import GroupApproximation.Sofic.UniversalVisibleQuotient
import GroupApproximation.Sofic.SimpleFactorRecovery
import GroupApproximation.Sofic.RadicalFiniteIndexTransfer
import GroupApproximation.Sofic.KazhdanCliffordConstruction
import GroupApproximation.Sofic.LiteralBaseP13PropertyTBridge
import GroupApproximation.Sofic.LiteralMFQuotientControls
import GroupApproximation.Sofic.LiteralNonMFConsequences
import GroupApproximation.Sofic.LiteralNonMFPresentation
import GroupApproximation.Sofic.LiteralUniformObstruction
import GroupApproximation.Sofic.RelatorDefectBudget
import GroupApproximation.Sofic.LiteralRelatorObstruction
import GroupApproximation.Sofic.ExactCoronaNegativeCorner
import GroupApproximation.Sofic.LiteralTheoremAPackage
import GroupApproximation.Sofic.ManuscriptExactWrappers
import GroupApproximation.Sofic.ManuscriptSubgroupSpecializations
import GroupApproximation.Sofic.TorsionFreeFiniteNormalLimit

-- Modules that until now compiled only in isolation.  Outside the root import
-- closure nothing in CI ever built them, so their proofs went unverified in every
-- run that mattered; `scripts/check.py --list-orphans` is the scan.  The rest of
-- the orphan set stays out on purpose: some of it is work other sessions have in
-- flight, and some has gone stale against renames upstream of it.  Wiring either
-- kind in here breaks the root build for everyone instead of getting it verified.
--
-- The four below are in because `Sofic/LiteralSoficAssembly.lean` is now cited by
-- Theorem `thm:Esofic` in the manuscript, and `check_non_mf_refs.py` rejects a
-- badge on an unbuilt module in as many words: outside the closure `lake build`
-- never compiles it, so the badge certifies nothing.  The other three are that
-- module's own dependencies, listed rather than left implicit so that dropping
-- one is a visible edit.  Every one of the four is tracked and fully proved.
import GroupApproximation.Sofic.BlockCliffordTowerSofic
import GroupApproximation.Sofic.LiteralSoficConsequences
import GroupApproximation.Sofic.LiteralSoficEndpoint
import GroupApproximation.Sofic.LiteralVerticalBridge

-- The modules below were kept out under the rule above, on the presumption that
-- they did not compile.  Each has now been compiled against the warm cache with
-- the pinned toolchain -- exit 0, no messages, olean emitted -- so the reason for
-- keeping them out no longer applies, and leaving them out would keep CI blind to
-- proofs that are in fact finished.  Several needed only a one-line repair to get
-- there: a missing `Mathlib.GroupTheory.FreeGroup.Reduce` import, a universe
-- declared `Type*` against a `Type` dependency, and two files that ended in
-- leaked tool markup.
--
-- The remaining orphans stay out for the original reason: they are either in
-- flight in another session or genuinely broken.
import GroupApproximation.Computability.FreeByRetraction
import GroupApproximation.Computability.HNNPresentedForward
import GroupApproximation.Computability.PresentedGroupBasisChange
import GroupApproximation.Computability.RabinBrittonFreeness
import GroupApproximation.Computability.RabinConstruction
import GroupApproximation.Computability.RabinConstructionMF
import GroupApproximation.Computability.RabinConstructionSource
import GroupApproximation.Computability.RabinFreeLetterOrder
import GroupApproximation.Computability.SemigroupWordProblemMachine
import GroupApproximation.Sofic.LiteralSoficSeparation
import GroupApproximation.Sofic.SimpleNotLEF
import GroupApproximation.Sofic.RationalEnvelope
import GroupApproximation.Sofic.RepresentationCategoryTwins

-- Restored 2026-08-16: a root-file sweep dropped these while wiring in others.
-- Each compiles and each was in the closure before, so the removal silently
-- un-verified them.
import GroupApproximation.Computability.ListBlankCanonical
import GroupApproximation.Computability.PostMachineTM0
import GroupApproximation.Computability.PostMachineTM0Canonical
import GroupApproximation.Computability.TM0WordProblem
import GroupApproximation.Sofic.ActionFormMoverEstimate
import GroupApproximation.Sofic.FullRadicalClosureProperties
import GroupApproximation.Sofic.WreathFinitePresentationObstruction
import GroupApproximation.Sofic.TelescopeLimitUnion

import GroupApproximation.Sofic.TelescopeRadicalInduction
import GroupApproximation.Sofic.BlockCliffordIndex
import GroupApproximation.Sofic.LiteralCosetBraid
import GroupApproximation.Computability.FreeGroupSquaring
import GroupApproximation.Computability.SemigroupWordProblemSimulation
import GroupApproximation.Computability.SemigroupWordProblemPresentation
import GroupApproximation.Computability.SemigroupWordProblem

-- Added by the 1:1 audit pass: modules that were outside the import closure,
-- so `lake build` never compiled them and no audit ever saw them.  Appended,
-- never regenerated -- a regenerated block has twice silently dropped modules.
import GroupApproximation.Analysis.FiniteCStarMurrayVonNeumann
import GroupApproximation.Analysis.MaximalCStarLiteralBase
import GroupApproximation.Analysis.MaximalGroupCStarUniqueness
import GroupApproximation.Analysis.PropertyAExtension
import GroupApproximation.Analysis.ExactnessGroupSideEndpoint
import GroupApproximation.Analysis.PropertyALocality
import GroupApproximation.Analysis.PropertyATelescope
import GroupApproximation.Analysis.PropertyAFiniteKernel
import GroupApproximation.Analysis.CStarTensorProductSeminorm
import GroupApproximation.Analysis.CStarTensorProductSpatial
import GroupApproximation.Analysis.CStarTensorProductConcrete
import GroupApproximation.Analysis.CStarTensorProductAlgebra
import GroupApproximation.Analysis.CStarStateSeparation
import GroupApproximation.Analysis.CStarStateGNS
import GroupApproximation.Analysis.CStarStatePullback
import GroupApproximation.Analysis.CStarMinTensorNorm
import GroupApproximation.Analysis.CStarSliceBound
import GroupApproximation.Analysis.CStarSliceCompletion
import GroupApproximation.Analysis.CStarSliceLeft
import GroupApproximation.Analysis.CStarExactnessSliceReduction
import GroupApproximation.Analysis.CStarSliceIdeal
import GroupApproximation.Analysis.CStarMaxTensorNorm
import GroupApproximation.Analysis.CStarTensorComparison
import GroupApproximation.Analysis.CStarNuclearity
import GroupApproximation.Analysis.CStarTensorComparisonRange
import GroupApproximation.Analysis.CStarMinTensorFunctorial
import GroupApproximation.Analysis.CStarMinTensorQuotient
import GroupApproximation.Analysis.CStarNonUnitalState
import GroupApproximation.Analysis.CStarCompletelyPositiveForm
import GroupApproximation.Analysis.CStarCompletelyPositiveStar
import GroupApproximation.Analysis.CStarStinespringForm
import GroupApproximation.Analysis.CStarStinespringSpace
import GroupApproximation.Analysis.CStarStinespringBound
import GroupApproximation.Analysis.CStarStinespringAct
import GroupApproximation.Analysis.CStarStinespringDefect
import GroupApproximation.Analysis.CStarStinespringMul
import GroupApproximation.Analysis.CStarStinespringRep
import GroupApproximation.Analysis.CStarStinespringLinear
import GroupApproximation.Analysis.CStarStinespringDilation
import GroupApproximation.Analysis.CStarStinespringHom
import GroupApproximation.Analysis.LanceReiterMean
import GroupApproximation.Analysis.CStarIdealQuotient
import GroupApproximation.Analysis.CStarQuotientIdentity
import GroupApproximation.Analysis.CStarIdealApproximateUnit
import GroupApproximation.Analysis.CStarProductCorona
import GroupApproximation.Analysis.CStarTensorProduct
import GroupApproximation.Algebra.ZariskiEnvelopeEndpoint
import GroupApproximation.Criterion.ClosedEnvelopeCompressionCore
import GroupApproximation.Monsters.RealizationEmbedding
import GroupApproximation.Monsters.FournierFacioUniversalRealization
import GroupApproximation.Monsters.P13InvariantProjection
import GroupApproximation.Sofic.CompressionUniverseTransfer
import GroupApproximation.Sofic.TransportVariantsAnyUniverse
import GroupApproximation.Sofic.ConjugationDatumAnyUniverse
import GroupApproximation.Sofic.FiniteNormalAnyUniverse
import GroupApproximation.Sofic.SoundIterateInstances
import GroupApproximation.Sofic.ContinuumMultiplicityCore
import GroupApproximation.Sofic.PrintedPreliminaryEstimates
import GroupApproximation.Sofic.PrintedCentralSignCriterion
import GroupApproximation.Sofic.PrintedNegativeCornerKill
import GroupApproximation.Sofic.PrintedReverseTransportRoute
import GroupApproximation.Sofic.LiteralSignFreeRadicalReduction
import GroupApproximation.Sofic.SoficEnvelopeSimplicity
import GroupApproximation.Sofic.BoundedConjProductAlgebra
import GroupApproximation.Sofic.SoficEnvelopeWitness
import GroupApproximation.Sofic.CollapsePrintedProfile
import GroupApproximation.Sofic.CliffordBSSixRelator
import GroupApproximation.Sofic.CliffordBSPrintedRoute
import GroupApproximation.Sofic.WreathWitnessGeneric
import GroupApproximation.Sofic.WreathWitnessW3
import GroupApproximation.Sofic.FiveConditionInsufficiency
import GroupApproximation.Sofic.Type0Corollaries
import GroupApproximation.Sofic.WreathWitnessSignFree
import GroupApproximation.Sofic.WeightedUltraproductModelConstruction
import GroupApproximation.Sofic.CollapseJointCornerRefinement
import GroupApproximation.Sofic.AmalgamQuestionEndpoint
import GroupApproximation.Sofic.LiteralBlockCliffordBridge
import GroupApproximation.Sofic.LiteralLampKernelAmalgam
import GroupApproximation.Sofic.DirectSumAmplification
import GroupApproximation.Sofic.CornerDilutionInvariance
import GroupApproximation.Sofic.LiteralBaseRotationMatrix
import GroupApproximation.Sofic.CollapseScaledStepSix
import GroupApproximation.Sofic.CollapseJointCorner
import GroupApproximation.Sofic.CollapseWordMetricBridge
import GroupApproximation.Analysis.MFStablyFinite
import GroupApproximation.Analysis.PreliminaryInequalitiesPrinted
import GroupApproximation.Analysis.StrictCompressionFromPrinted
import GroupApproximation.Criterion.StandardRepCommutant
import GroupApproximation.Monsters.NeumannNormalSubgroups
import GroupApproximation.Sofic.IntrinsicCompressionFiniteStage
import GroupApproximation.Computability.UniversalMachineInit
import GroupApproximation.Sofic.CollapseTransportEndpoint
import GroupApproximation.Sofic.CollapsePrintedDiagonalization
import GroupApproximation.Sofic.CollapsePrintedCorollary
import GroupApproximation.Computability.MachineRestrict
import GroupApproximation.Sofic.CliffordLampGraphLocalFiniteness
import GroupApproximation.Sofic.CliffordLampGraphFreeSubgroup
import GroupApproximation.Sofic.CliffordBSAmenableMF
import GroupApproximation.Sofic.CliffordQuotientMFUnconditional
import GroupApproximation.Sofic.DefectActionAnyUniverse
import GroupApproximation.Sofic.DefectRadicalAnyUniverse
import GroupApproximation.Sofic.InvolutionsAnyBase
import GroupApproximation.Sofic.NormalKazhdanAnyUniverse
import GroupApproximation.Sofic.TensorPowerAnyUniverse
import GroupApproximation.Computability.FiniteMachineWordProblem
import GroupApproximation.Computability.MarkovPost
import GroupApproximation.Computability.BooneGroupFreeBasis
import GroupApproximation.Computability.BooneGroupModularMachine
import GroupApproximation.Computability.BooneGroupBase
import GroupApproximation.Computability.BooneGroupPresentation
import GroupApproximation.Computability.BooneGroupTower
import GroupApproximation.Computability.BooneGroupGoodness
import GroupApproximation.Computability.BooneBaseWords
import GroupApproximation.Computability.BooneTowerPresentation
import GroupApproximation.Computability.QuadMachine
import GroupApproximation.Computability.QuadMachineTM0
import GroupApproximation.Computability.ModularMachineUndecidable
import GroupApproximation.Computability.ComputableConfigReduction
import GroupApproximation.Computability.BinaryDigitPrimrec
import GroupApproximation.Computability.TrNatRecurrence
import GroupApproximation.Computability.IndexMapComputable
import GroupApproximation.Computability.BooneWordProblem
import GroupApproximation.Computability.BooneGroupMachineIndex
import GroupApproximation.Computability.UniversalMachineUndecidable
import GroupApproximation.Computability.AdianRabinWordProblem
import GroupApproximation.Algebra.HNNFinitePresentation
import GroupApproximation.Algebra.HNNPresentation
import GroupApproximation.Algebra.HNNPresentationQuotient
import GroupApproximation.Algebra.RabinVariantPresentation
import GroupApproximation.Computability.RabinVariantMF
import GroupApproximation.Algebra.RabinVariantTower
import GroupApproximation.Algebra.HNNRetraction
import GroupApproximation.Algebra.HNNTrivialAssociated
import GroupApproximation.Algebra.PresentedGroupRelabel
import GroupApproximation.Algebra.HNNCongr
import GroupApproximation.Algebra.FreeProductOrder
import GroupApproximation.Computability.BooneGroupFinitePresentation
import GroupApproximation.Computability.NovikovBoone
import GroupApproximation.Computability.BooneGroupCode
import GroupApproximation.Computability.UniformWordProblemUndecidable
import GroupApproximation.Computability.CodedWordTriviality
import GroupApproximation.Computability.FreeGroupCheckerPrimrec
import GroupApproximation.Computability.FreeGroupDeletion
import GroupApproximation.Computability.FreeGroupDeletionPrimrec
import GroupApproximation.Computability.FreeGroupRedNil
import GroupApproximation.Computability.ModularMachineConfigHalting
import GroupApproximation.Computability.BooneWords
import GroupApproximation.Computability.BooneWordMapPrimrec
import GroupApproximation.Computability.BooneWordAgreement
import GroupApproximation.Computability.BooneWordProblemUndecidable
import GroupApproximation.Analysis.PrintedLiftingSteps
import GroupApproximation.Analysis.FiniteExceptionalPatch
import GroupApproximation.Kazhdan.PrintedComplexificationBridge
import GroupApproximation.Sofic.CentralSignAnyUniverse
import GroupApproximation.Analysis.OmegaHilbertComplete
import GroupApproximation.Analysis.RankFrobeniusBound
import GroupApproximation.Sofic.RealizationFromUniversalGroup
import GroupApproximation.Analysis.PrintedReverseTransport
import GroupApproximation.Algebra.AlternatingBoundedNormalGeneration
import GroupApproximation.Algebra.AlternatingDoubledTransport
import GroupApproximation.Analysis.CollapseCocycleAnalytic
import GroupApproximation.Analysis.MaximalCStarAnyUniverse
import GroupApproximation.Analysis.NormalKazhdanUltraproduct
import GroupApproximation.Analysis.OmegaConjugationOperators
import GroupApproximation.Analysis.OmegaCommutatorFixes
import GroupApproximation.Analysis.RankNormalizedHilbertization
import GroupApproximation.Analysis.RankNormalizedLambda
import GroupApproximation.Analysis.CollapseDisplacementIdeal
import GroupApproximation.Analysis.CollapseTransportEndpoint
import GroupApproximation.Analysis.CollapseCoronaIsometry
import GroupApproximation.Analysis.CollapseDelormeCorona
import GroupApproximation.Analysis.CollapseRouteJoin
import GroupApproximation.Analysis.CollapseCompressionBundle
import GroupApproximation.Analysis.CollapsePrintedContradiction
import GroupApproximation.Analysis.CollapsePrintedProjectionCollapse
import GroupApproximation.Analysis.PrintedFiniteException
import GroupApproximation.Analysis.CollapseDiscardCoordinates
import GroupApproximation.Analysis.CollapseLambdaCocycle
import GroupApproximation.Analysis.CollapseInvariantSubspace
import GroupApproximation.Analysis.CollapseKqTransport
import GroupApproximation.Analysis.CollapseProjectionLift
import GroupApproximation.Monsters.NeumannTwoGenerator
import GroupApproximation.Sofic.CollapseRankWeightTransport
import GroupApproximation.Sofic.FinitePacketCovariance
import GroupApproximation.Sofic.FinitePacketDelormeCenter
import GroupApproximation.Sofic.FiniteGroupUlamStep
import GroupApproximation.Sofic.FiniteGroupUlamIteration
import GroupApproximation.Sofic.FiniteGroupCoronaExactification
import GroupApproximation.Sofic.FinitePacketRankWeight
import GroupApproximation.Sofic.StarTranspositionRankMass
import GroupApproximation.Sofic.FinitePacketCollapseCore
import GroupApproximation.Endpoint.FinitePacketCollapseAudit
import GroupApproximation.Sofic.StableLetterLEFRoute
import GroupApproximation.Manuscript.NonMF.ClosedRows
import GroupApproximation.Analysis.MatrixReindexHilbertSchmidt
import GroupApproximation.Analysis.CollapseDelormeEndpoint
import GroupApproximation.Analysis.ProperIsometryStrictOrder
import GroupApproximation.Analysis.OmegaDefectExtraction
import GroupApproximation.Analysis.UltraproductRigidityRoute
import GroupApproximation.Manuscript.NonMF.QuestionAtoms
import GroupApproximation.Sofic.LiteralTraceConsequence
import GroupApproximation.Analysis.ShulmanTraceClasses
import GroupApproximation.Sofic.ShulmanMFTraceBridge
import GroupApproximation.Analysis.MaximalGroupCStarTrace
import GroupApproximation.Analysis.MaximalGroupCStarSubgroupReflection
import GroupApproximation.Analysis.ShulmanTraceNorms
import GroupApproximation.Analysis.TracialMatrixUltraproduct
import GroupApproximation.Analysis.ShulmanTraceFactorization
import GroupApproximation.Analysis.ShulmanTraceFromRepresentation
import GroupApproximation.Analysis.TracialUltraproductCStar
import GroupApproximation.Analysis.UltrafilterDiagonalExtraction
import GroupApproximation.Analysis.ShulmanTracePositiveControls
import GroupApproximation.Analysis.HilbertSchmidtApproximateUnit
import GroupApproximation.Sofic.MFTraceCoronaBridge
import GroupApproximation.Sofic.SoficPermutationTrace
import GroupApproximation.Analysis.TracialQuotientCStar
import GroupApproximation.Analysis.SoficHyperlinearTrace
import GroupApproximation.Analysis.TracialQuotientCStarIdentity
import GroupApproximation.Analysis.SoficHyperlinearBridge
import GroupApproximation.Analysis.PrintedUltrafilterHyperlinearTrace
import GroupApproximation.Sofic.TraceSeparationEndpoint

-- Modules that stood outside this root's import closure and were therefore
-- never compiled by an ordinary `lake build`: `scripts/check.py --list-orphans`
-- named twenty-eight of them, and ten did not elaborate at all.  They carry the
-- literal-route transport, the coordinate Hilbert ultraproduct `H_ω`, the
-- C*-completion chain, general polar lifting, stably finite amplification and
-- the unconditional simple sofic envelope -- the very files the manuscript
-- correspondence needs -- so an unbuilt module here reads as coverage that does
-- not exist.  They are wired in below.
import GroupApproximation.Algebra.AlternatingPairGeneration
import GroupApproximation.Algebra.GroupRingStar
import GroupApproximation.Algebra.PermutationTwoInvolutions
import GroupApproximation.Algebra.InvolutionBlocks
import GroupApproximation.Algebra.InvolutionBlockSplit
import GroupApproximation.Algebra.InvolutionBlockAssembly
import GroupApproximation.Analysis.CStarCompletion
import GroupApproximation.Analysis.CStarCompletionCoe
import GroupApproximation.Analysis.CStarCompletionHom
import GroupApproximation.Analysis.CStarSeminormQuotient
import GroupApproximation.Analysis.CStarNormBundled
import GroupApproximation.Analysis.CStarQuotientHom
import GroupApproximation.Analysis.CStarNormFromRepresentation
import GroupApproximation.Analysis.CStarSeminormCompletion
import GroupApproximation.Analysis.MaximalCStarAllUniverses
import GroupApproximation.Analysis.MaximalCStarPrintedCompletion
import GroupApproximation.Analysis.CollapseUltraproductRepresentation
import GroupApproximation.Analysis.OmegaActionLinear
import GroupApproximation.Analysis.OmegaIsometryRepresentation
import GroupApproximation.Analysis.OmegaConjQCompatibility
import GroupApproximation.Analysis.CollapseKqAlmostRep
import GroupApproximation.Analysis.OmegaFiniteComparison
import GroupApproximation.Analysis.OmegaFixRange
import GroupApproximation.Analysis.PolarLiftingGeneralCStar
import GroupApproximation.Analysis.FiniteBlockCoronaHilbert
import GroupApproximation.Analysis.PolarLiftingPrintedSequence
import GroupApproximation.Analysis.MFAlgebraDimensionNormalization
import GroupApproximation.Analysis.MatrixCoronaAmplificationEmbedding
import GroupApproximation.Analysis.CompatibleMatrixCoronaAmplification
import GroupApproximation.Analysis.NormCoronaAsymptoticLiftModel
import GroupApproximation.Analysis.NormCoronaAsymptoticLiftCore
import GroupApproximation.Analysis.NormCoronaAsymptoticLift
import GroupApproximation.Analysis.PolarLiftingHypothesisFree
import GroupApproximation.Analysis.StablyFiniteAmplification
import GroupApproximation.Analysis.MatrixCoronaDedekindFinite
import GroupApproximation.Analysis.MFAlgebraMatrixAmplification
import GroupApproximation.Analysis.ReducedProductMFPermanence
import GroupApproximation.Analysis.MFAlgebraAmalgamGenerated
import GroupApproximation.Analysis.MFAlgebraAmalgamCriterion
import GroupApproximation.Analysis.CoronaProjectionOrder
import GroupApproximation.Analysis.VectorHilbertUltraproduct
import GroupApproximation.Analysis.VectorHilbertComplete
import GroupApproximation.Analysis.VectorOmegaAction
import GroupApproximation.Analysis.VectorOmegaKazhdanGap
import GroupApproximation.Analysis.FilterMatrixCStarCorona
import GroupApproximation.Analysis.VectorOmegaCoronaAction
import GroupApproximation.Analysis.CoronaProjectionLifting
import GroupApproximation.Analysis.UnitaryAverageFixedVector
import GroupApproximation.Analysis.OmegaCoronaKazhdanProjection
import GroupApproximation.Analysis.PrintedDiagonalSubsequence
import GroupApproximation.Analysis.PrintedCornerCompression
import GroupApproximation.Analysis.PrintedCornerAssembly
import GroupApproximation.Analysis.FiniteDimensionalOperatorFinite
import GroupApproximation.Analysis.PrintedCornerRelabelling
import GroupApproximation.Analysis.PolarLiftingMatrixBlocks
import GroupApproximation.Sofic.OmegaRouteManuscriptTransport
import GroupApproximation.Sofic.LiteralProductMultiplicity
import GroupApproximation.Sofic.SimpleSoficEnvelopeAnyUniverse
import GroupApproximation.Sofic.PrintedTransportOpening
import GroupApproximation.Sofic.KazhdanTransportFailureExtraction
import GroupApproximation.Monsters.NeumannSimpleSocle
import GroupApproximation.Sofic.TransportShapeBridges
import GroupApproximation.Sofic.GeneralModelKazhdanTransport
import GroupApproximation.Sofic.LiteralRouteTransport
import GroupApproximation.Sofic.SimpleSoficEnvelopeUnconditional
import GroupApproximation.Sofic.ConsistencyDistance
import GroupApproximation.Analysis.CStarTakesakiCoefficient
import GroupApproximation.Analysis.LancePositiveDefinite
import GroupApproximation.Analysis.LanceReduction
import GroupApproximation.Analysis.LanceMultiplicativeDomain
import GroupApproximation.Analysis.CStarTakesakiDense
import GroupApproximation.Analysis.CStarTakesakiMinLe
import GroupApproximation.Analysis.CStarTakesakiCyclic
import GroupApproximation.Analysis.CStarTakesakiIdentification
import GroupApproximation.Analysis.TracialStandardFormCommutation
import GroupApproximation.Analysis.TracialConjugationExists
import GroupApproximation.Analysis.QuasidiagonalCompression
import GroupApproximation.Analysis.UniformRoeAlgebra
import GroupApproximation.Analysis.AmenableMFInput
import GroupApproximation.Sofic.CliffordAsideInert
import GroupApproximation.Sofic.ContainsSquareWitness
import GroupApproximation.Analysis.CStarMinTensorInjective
import GroupApproximation.Analysis.CStarExactComplex
import GroupApproximation.Algebra.WordMetricBall
import GroupApproximation.Analysis.CoarseCompression
import GroupApproximation.Analysis.SchoenbergKernel
import GroupApproximation.Analysis.GuentnerKaminker
import GroupApproximation.Analysis.PropertyASquareWitness
import GroupApproximation.Manuscript.NonMF.QuestionOneOpenness
import GroupApproximation.Manuscript.NonMF.QuestionTwoRemainder
import GroupApproximation.Sofic.FournierFacioUniversalGroup
import GroupApproximation.Sofic.GreendlingerInduction
import GroupApproximation.Sofic.GreendlingerIsoperimetric
import GroupApproximation.Sofic.GreendlingerMinimal
import GroupApproximation.Sofic.GreendlingerMirror
import GroupApproximation.Sofic.GreendlingerOverlap
import GroupApproximation.Sofic.GreendlingerRegime
import GroupApproximation.Sofic.GreendlingerSlide
import GroupApproximation.Sofic.GreendlingerWeight
import GroupApproximation.Sofic.SmallCancellationKazhdanEnvelope
import GroupApproximation.Analysis.OmegaUnitaryRepExists
import GroupApproximation.Sofic.HSDistVanishingWitness
import GroupApproximation.Analysis.L2KernelOperator
import GroupApproximation.Computability.AdianRabinGeneral
import GroupApproximation.Analysis.CStarChoiMap
import GroupApproximation.Algebra.CoprodIPresentation
import GroupApproximation.Algebra.FreeProductCyclicWord
import GroupApproximation.Algebra.FreeProductUnionNorm
import GroupApproximation.Algebra.HyperbolicGroup
import GroupApproximation.Algebra.HyperbolicInteger
import GroupApproximation.Algebra.HyperbolicQuasiIsometry
import GroupApproximation.Algebra.HyperbolicSlimFourPoint
import GroupApproximation.Algebra.HyperbolicSlimTriangles
import GroupApproximation.Algebra.TorsionFreeQuotient
import GroupApproximation.Algebra.TorsionFreeRadical
import GroupApproximation.Algebra.TorsionFreeRadicalTower
import GroupApproximation.Algebra.WordMetricComparison
import GroupApproximation.Analysis.CStarCorestrictCP
import GroupApproximation.Analysis.CStarFormCompletelyPositive
import GroupApproximation.Analysis.CStarUnitalCPContractive
import GroupApproximation.Analysis.CompressionTraceFolner
import GroupApproximation.Analysis.CompressionTraceLocallyFinite
import GroupApproximation.Analysis.CompressionTraceModel
import GroupApproximation.Analysis.CompressionTraceRigidity
import GroupApproximation.Analysis.GaussianRoeOperator
import GroupApproximation.Analysis.GuentnerKaminkerEndpoint
import GroupApproximation.Analysis.MFTracePullback
import GroupApproximation.Analysis.NuclearApproximationEstimate
import GroupApproximation.Analysis.QuasidiagonalTrace
import GroupApproximation.Analysis.ReducedGroupCStarSpan
import GroupApproximation.Analysis.RoeSquareRoot
import GroupApproximation.Analysis.TikuisisWhiteWinter
import GroupApproximation.Analysis.TikuisisWhiteWinterUnconditional
import GroupApproximation.Analysis.UCPContractiveMatrix
import GroupApproximation.Computability.OperatorMFMarkovData
import GroupApproximation.Computability.SoficMarkov
import GroupApproximation.Higman.Benign
import GroupApproximation.Higman.BenignClosure
import GroupApproximation.Kazhdan.TorsionFreeHyperbolicKazhdan
import GroupApproximation.Monsters.ChiodoFreeProductAbsorber
import GroupApproximation.Monsters.ChiodoTorsionFreeAbsorber
import GroupApproximation.Monsters.RecursiveCodeAbsorber
import GroupApproximation.Sofic.ChiodoBelegradekTheorem
import GroupApproximation.Sofic.ChiodoUniversalHost
import GroupApproximation.Sofic.ExplicitSuitableDefect
import GroupApproximation.Sofic.GreendlingerTwoPieceRegime
import GroupApproximation.Sofic.HullPrescribedSaturation
import GroupApproximation.Sofic.HullSuitableDefectSubgroup
import GroupApproximation.Sofic.FournierFacioHullBridge
import GroupApproximation.Sofic.InfranormalCompressionPair
import GroupApproximation.Sofic.KunThomDoubleWitness
import GroupApproximation.Sofic.TikuisisWhiteWinterSharpness
import GroupApproximation.Sofic.TikuisisWhiteWinterSites
import GroupApproximation.Algebra.CoprodIFinitePresentation
import GroupApproximation.Algebra.PushoutIFinitePresentation
import GroupApproximation.Analysis.LanceAmenableOverlap
import GroupApproximation.Analysis.LanceFolnerCPAP
import GroupApproximation.Analysis.LanceFolnerMaps
import GroupApproximation.Analysis.LanceNuclearAmenable
import GroupApproximation.Analysis.TikuisisWhiteWinterAmenableClass
import GroupApproximation.Kazhdan.SharpExistenceRoutes
import GroupApproximation.Algebra.FreeProductConjugacy
import GroupApproximation.Analysis.CStarOrderZero
import GroupApproximation.Higman.RopeTrick
import GroupApproximation.Sofic.GreendlingerThreeFactor
import GroupApproximation.Sofic.HullSuitabilityGeometry
import GroupApproximation.Algebra.CoprodIWordInverse
import GroupApproximation.Algebra.FiniteIndexQuasiIsometry
import GroupApproximation.Algebra.FiniteIndexTransversal
import GroupApproximation.Algebra.MorseLemma
import GroupApproximation.Algebra.ReidemeisterSchreier
import GroupApproximation.Algebra.SchreierGenerators
import GroupApproximation.Analysis.CStarOrderZeroSupport
import GroupApproximation.Analysis.DadarlatEilers
import GroupApproximation.Analysis.KKTheoryKGroups
import GroupApproximation.Analysis.KKTheoryKasparov
import GroupApproximation.Analysis.KirchbergRordamCorona
import GroupApproximation.Analysis.KirchbergRordamEpsilonTest
import GroupApproximation.Analysis.KirchbergRordamOrderZeroLift
import GroupApproximation.Analysis.TikuisisWhiteWinterProof
import GroupApproximation.Analysis.UniversalCoefficientTheorem
import GroupApproximation.Higman.AbsorberProgram
import GroupApproximation.Higman.BlockTower
import GroupApproximation.Higman.NormalClosureProduct
import GroupApproximation.Higman.RadicalDirectSum
import GroupApproximation.Higman.TowerBlockSearch
import GroupApproximation.Higman.TowerCert
import GroupApproximation.Higman.TowerComputable
import GroupApproximation.Higman.TowerDerivation
import GroupApproximation.Kazhdan.InducedRepresentation
import GroupApproximation.Kazhdan.KazhdanFiniteIndex
import GroupApproximation.Kazhdan.LatticeRouteRemainder
import GroupApproximation.Algebra.HyperbolicTransport
import GroupApproximation.Analysis.CStarCPStarTarget
import GroupApproximation.Analysis.QuasidiagonalTraceLocal
import GroupApproximation.Analysis.QuasidiagonalTraceProperties
import GroupApproximation.Analysis.TikuisisWhiteWinterCore
import GroupApproximation.Computability.TorsionFreeMarkov
import GroupApproximation.Computability.TorsionFreeMFMarkov
import GroupApproximation.Sofic.IteratedDoubleAmalgam
import GroupApproximation.Sofic.SymmetricDoubleCovering
import GroupApproximation.Sofic.CoveringWitness
import GroupApproximation.Sofic.DoubleFiniteDimensionalRigidity
import GroupApproximation.Sofic.DoubleInputsMinimal
import GroupApproximation.Sofic.KunThomShulmanDoubleConstruction
import GroupApproximation.Sofic.FreeLampKernelSplitting
import GroupApproximation.Stability.LinearMetricApproximation
import GroupApproximation.Stability.UnnormalizedSchattenApproximation
import GroupApproximation.Stability.SchattenNonapproximability
import GroupApproximation.Sofic.CentralizerNormalizationRefuted
import GroupApproximation.Sofic.GreendlingerDehn
import GroupApproximation.Sofic.GreendlingerDehnCritical
import GroupApproximation.Sofic.GreendlingerDehnFree
import GroupApproximation.Sofic.GreendlingerDehnSwap
import GroupApproximation.Algebra.CoprodITorsionFree
import GroupApproximation.Algebra.CoprodIWordLength
import GroupApproximation.Algebra.CoprodICyclicReduction
import GroupApproximation.Algebra.PushoutITorsionFree
import GroupApproximation.Algebra.FreeProductFactorQuotient
import GroupApproximation.Higman.AmalgamPresentation
import GroupApproximation.Higman.AmalgamPushout
import GroupApproximation.Higman.CoprodTorsion
import GroupApproximation.Higman.HNNCentralizer
import GroupApproximation.Higman.BenignAmbient
import GroupApproximation.Higman.BenignFamily
import GroupApproximation.Higman.BenignJoin
import GroupApproximation.Higman.Pinch
import GroupApproximation.Higman.Program
import GroupApproximation.Higman.EvalRaw
import GroupApproximation.Higman.QuotientPresentation
import GroupApproximation.Higman.AbsorberGenerators
import GroupApproximation.Higman.CodedAbsorber
import GroupApproximation.Higman.BlockDecomposition
import GroupApproximation.Higman.BlockWordProblem
import GroupApproximation.Higman.BlockSearch
import GroupApproximation.Higman.BlockComputable
import GroupApproximation.Higman.ConjugateBasis
import GroupApproximation.Higman.SequenceSpace
import GroupApproximation.Higman.BaseCases
import GroupApproximation.Higman.Operations
import GroupApproximation.Higman.TheoremFour
import GroupApproximation.Higman.ShiftOperation
import GroupApproximation.Higman.PinchGraph
import GroupApproximation.Higman.RopeTorsion
import GroupApproximation.Higman.BenignTorsionFree
import GroupApproximation.Higman.RowSubgroup
import GroupApproximation.Higman.RowBasis
import GroupApproximation.Higman.HNNEmbedding
import GroupApproximation.Higman.BridgeTorsion
import GroupApproximation.Higman.EmbeddingTheorem
import GroupApproximation.Higman.ChiodoReduction
import GroupApproximation.Higman.RowKernel
import GroupApproximation.Higman.HNNDescent
import GroupApproximation.Algebra.HNNSubextension
import GroupApproximation.Sofic.GreendlingerChunks
import GroupApproximation.Sofic.OsinRelativeSmallCancellation
import GroupApproximation.Analysis.CStarHilbertModule
import GroupApproximation.Analysis.CStarHilbertModuleNorm
import GroupApproximation.Analysis.CStarAdjointable
import GroupApproximation.Analysis.CStarAdjointableNorm
import GroupApproximation.Analysis.CStarPositiveOrder
import GroupApproximation.Analysis.PairSumIncidence
import GroupApproximation.Analysis.CStarUnitary
import GroupApproximation.Analysis.CStarFiniteRank
import GroupApproximation.Analysis.CStarCompactOperators
import GroupApproximation.Analysis.CStarDirectSumOperators
import GroupApproximation.Analysis.CStarModuleDirectSum
import GroupApproximation.Analysis.CStarStandardModule
import GroupApproximation.Analysis.CStarStandardModuleEquiv
import GroupApproximation.Analysis.CStarStabilization
import GroupApproximation.Analysis.KasparovBimodule
import GroupApproximation.Analysis.KasparovUnitaryEquivalence
import GroupApproximation.Sofic.FreeCancellationNesting
import GroupApproximation.Kazhdan.OrbitAverageSpectralGap
import GroupApproximation.Kazhdan.OrbitAverageFormGap
import GroupApproximation.Kazhdan.OrbitAverageFiniteControl
import GroupApproximation.Kazhdan.SharpExistenceSpectralRoute
import GroupApproximation.Kazhdan.CharTwoTorsionObstruction
import GroupApproximation.Kazhdan.SharpExistenceCertificateRoute
import GroupApproximation.Algebra.TreeLikeHyperbolic
import GroupApproximation.Algebra.BassSerreFreeProductAction
import GroupApproximation.Sofic.BassSerreHullGeometry
import GroupApproximation.Algebra.ListCommonPrefix
import GroupApproximation.Algebra.HyperbolicFreeGroup
import GroupApproximation.Kazhdan.FreeGroupSharpProfile
import GroupApproximation.Analysis.QuasidiagonalCoronaCriterion
import GroupApproximation.Analysis.QuasidiagonalMatricialTrace
import GroupApproximation.Analysis.TikuisisWhiteWinterDerivation
import GroupApproximation.Higman.HalfRowEndo
import GroupApproximation.Higman.IntPrimrec
import GroupApproximation.Higman.HigmanPrimitiveRecursion
import GroupApproximation.Sofic.BlockInfix
import GroupApproximation.Sofic.ConjExprMatching
import GroupApproximation.Sofic.MatchingSpine
import GroupApproximation.Sofic.NonCrossingMatching
import GroupApproximation.Sofic.RelatorBlock
import GroupApproximation.Algebra.HNNBridgeAmbient
import GroupApproximation.Algebra.HNNBridgeFamily
import GroupApproximation.Higman.AddRelators
import GroupApproximation.Higman.FinalReduction
import GroupApproximation.Higman.REPredNormalForm
import GroupApproximation.Higman.RecursivePresentationBridge
import GroupApproximation.Higman.RelatorEnumeration
import GroupApproximation.Higman.RelatorRE
import GroupApproximation.Sofic.GreendlingerBeyond
import GroupApproximation.Algebra.HNNBridgeFreeness
import GroupApproximation.Algebra.HNNBridgeTorsionFree
import GroupApproximation.Analysis.CStarCompactSelfModule
import GroupApproximation.Analysis.ConvexUnitVectorRigidity
import GroupApproximation.Sofic.GreendlingerMaxConjugator
import GroupApproximation.Sofic.OrderPreservingDegeneracy
import GroupApproximation.Sofic.BareDefectSource
import GroupApproximation.Sofic.SingleDefectSaturation
import GroupApproximation.Sofic.ArithmeticSingleDefectEndpoint
import GroupApproximation.Algebra.CongruenceTorsionFree
import GroupApproximation.Kazhdan.SL3Certificate
import GroupApproximation.Sofic.BespokeRouterConstruction
import GroupApproximation.Algebra.FreeGroupFiniteRank
import GroupApproximation.Kazhdan.TorsionFreeKazhdanPartner
import GroupApproximation.Algebra.SteinbergSL3
import GroupApproximation.Algebra.FinitePresentationFiniteIndex
import GroupApproximation.Sofic.PeriodicOverlap
import GroupApproximation.Sofic.FreeProductRouterObstruction
import GroupApproximation.Sofic.GreendlingerDeepestMatch
import GroupApproximation.Sofic.GreendlingerCoincidence
import GroupApproximation.Sofic.GreendlingerBetaBranch
import GroupApproximation.Sofic.GreendlingerAlphaPlumb
import GroupApproximation.Sofic.GreendlingerDeepArc
import GroupApproximation.Sofic.GreendlingerDeepVacuity
import GroupApproximation.Sofic.GreendlingerPieceOverlapProof
import GroupApproximation.Sofic.GreendlingerSharpTwins
import GroupApproximation.Sofic.GreendlingerDeepVacuitySharp
import GroupApproximation.Sofic.GreendlingerDeepThreeFactor
import GroupApproximation.Sofic.GreendlingerDeepInduction
import GroupApproximation.Sofic.GreendlingerDeepTailWindow
import GroupApproximation.Sofic.GreendlingerSharpWindow
import GroupApproximation.Sofic.GreendlingerSharpRigidity
import GroupApproximation.Sofic.GreendlingerSharpBackLoss
import GroupApproximation.Sofic.GreendlingerSharpReduction
import GroupApproximation.Sofic.GreendlingerSharpDropGate
import GroupApproximation.Sofic.GreendlingerSharpDeepArc
import GroupApproximation.Sofic.GreendlingerSharpChunks
import GroupApproximation.Sofic.GreendlingerSharpLandingAux
import GroupApproximation.Sofic.GreendlingerSharpThreeFactor
import GroupApproximation.Sofic.GreendlingerSharpInduction
import GroupApproximation.Sofic.GreendlingerSharpOverlap
import GroupApproximation.Sofic.GreendlingerSharpLandingProd
import GroupApproximation.Sofic.GreendlingerSharpInvariant
import GroupApproximation.Sofic.GreendlingerSharpWindowDrop
import GroupApproximation.Sofic.GreendlingerSharpDehn
import GroupApproximation.Sofic.GreendlingerSharpMinimal
import GroupApproximation.Sofic.GreendlingerSharpRegime
import GroupApproximation.Sofic.GreendlingerDeepInvariant
import GroupApproximation.Sofic.GreendlingerLandingConfined
import GroupApproximation.Sofic.GreendlingerRelativeTransfer
import GroupApproximation.Sofic.GreendlingerSharpResidualWiring
import GroupApproximation.Sofic.GreendlingerSharpResidualWiring2
import GroupApproximation.Sofic.GreendlingerDeepOverrunCount
import GroupApproximation.Sofic.GreendlingerLandingProd
import GroupApproximation.Sofic.GreendlingerSharpLandingProduction
import GroupApproximation.Sofic.GreendlingerSharpHeadLanding
import GroupApproximation.Sofic.GreendlingerCompositeWellPosed
import GroupApproximation.Sofic.GreendlingerNoDeepCollapse
import GroupApproximation.Sofic.GreendlingerEmptyConjCorner
import GroupApproximation.Sofic.GreendlingerCollapseInduction
import GroupApproximation.Sofic.GreendlingerCyclicTwoArc
import GroupApproximation.Sofic.SymmetricDoubleMF
import GroupApproximation.Sofic.LiteralAffineFreeProductSource
import GroupApproximation.Sofic.LiteralAffineHullCommonQuotientInput
import GroupApproximation.Sofic.LiteralAffineHullTwoStageBridge
import GroupApproximation.Sofic.LiteralAffineFreeProductBassSerre
import GroupApproximation.Sofic.LiteralAffineFreeProductBassSerreDisplacement
import GroupApproximation.Sofic.LiteralAffineFreeProductBassSerreIndependence
import GroupApproximation.Kazhdan.TriangularHodgeLayer
import GroupApproximation.Sofic.OsinWeightedDefectNoGo
import GroupApproximation.Sofic.OsinWeightedLeafNoGo
import GroupApproximation.Sofic.TorsionDescent
import GroupApproximation.Leavitt.HilbertHotelBlocks
import GroupApproximation.Leavitt.HilbertHotelSaturation
import GroupApproximation.Leavitt.HilbertHotelWhitehead
import GroupApproximation.Leavitt.HilbertHotelBinary
import GroupApproximation.Leavitt.HilbertHotelDefectNormal
import GroupApproximation.Leavitt.HilbertHotelCover
import GroupApproximation.Leavitt.ConjProductClosure
import GroupApproximation.Leavitt.HilbertHotelCoverDischarges
import GroupApproximation.Leavitt.HilbertHotelModelNonMF
import GroupApproximation.Leavitt.HilbertHotelCoverBlock
import GroupApproximation.Leavitt.HilbertHotelEndpoint
import GroupApproximation.Sofic.MFCamouflage
import GroupApproximation.Sofic.MFCamouflageRadical
import GroupApproximation.Sofic.MFCamouflageConsequences
import GroupApproximation.Higman.CoordCalculus
import GroupApproximation.Higman.SeqFilter
import GroupApproximation.Higman.AgreeClosure
import GroupApproximation.Higman.OmegaClosure
import GroupApproximation.Higman.OperationClosureRho
import GroupApproximation.Higman.TorsionFreeImageClosure
import GroupApproximation.Higman.ClosuresAssembly
import GroupApproximation.Higman.AmalgamTorsionDischarge
import GroupApproximation.Higman.TheoremThreeAssembly
import GroupApproximation.Higman.EnumeratedRange
import GroupApproximation.Higman.EnumeratedRangeTrace
import GroupApproximation.Higman.EnumeratedRangeTraceCorrectness
import GroupApproximation.Higman.EnumeratedRangeProjection
import GroupApproximation.Higman.EnumeratedRangeVerify
import GroupApproximation.Higman.TraceRelationRE
import GroupApproximation.Higman.HigmanCodingDictionary
import GroupApproximation.Higman.HigmanAtoms
import GroupApproximation.Higman.HigmanVariableCalculus
import GroupApproximation.Higman.TransportFive
import GroupApproximation.Higman.TransportStar
import GroupApproximation.Higman.TransportStarWitness
import GroupApproximation.Higman.MapEmbSharp
import GroupApproximation.Higman.BridgeEffectivity
import GroupApproximation.Higman.BridgeWordProblem
import GroupApproximation.Higman.CentralHNNFreeLabelAction
import GroupApproximation.Higman.CentralHNNFreeLabelFaithful
import GroupApproximation.Higman.CentralHNNFreeLabelKernel
import GroupApproximation.Higman.OmegaTower
import GroupApproximation.Higman.OmegaTowerStages
import GroupApproximation.Higman.OmegaTowerDescent
import GroupApproximation.Higman.OmegaTowerStageTwo
import GroupApproximation.Higman.OmegaTowerStageThree
import GroupApproximation.Higman.OmegaTowerClassifiedPinchStep
import GroupApproximation.Higman.OmegaTowerInterfaceCounterexample
import GroupApproximation.Higman.OmegaTowerRightTailCollapse
import GroupApproximation.Higman.OmegaTowerRightTailSubgroup
import GroupApproximation.Higman.OmegaTowerStaticSeamFreeCoordinates
import GroupApproximation.Higman.RowDeletionBenign
import GroupApproximation.Higman.SwapWitnessTower
import GroupApproximation.Higman.SwapCarrierFromTower
import GroupApproximation.Higman.SwapCarrierWitness
import GroupApproximation.Higman.TauRouteC
import GroupApproximation.Higman.SsetBaseCase
import GroupApproximation.Higman.CurrentOperationClosures
import GroupApproximation.Higman.CurrentREBenign
import GroupApproximation.Higman.OmegaDebt
import GroupApproximation.Higman.OperationClosureTheta
import GroupApproximation.Higman.OperationClosureTau
import GroupApproximation.Higman.FlipGroup
import GroupApproximation.Higman.AmalgamTorsion
import GroupApproximation.Higman.GeneratedBasic
import GroupApproximation.Higman.GeneratedCoords
import GroupApproximation.Higman.GeneratedPin
import GroupApproximation.Higman.GeneratedValue
import GroupApproximation.Higman.GeneratedTransition
import GroupApproximation.Higman.GeneratedEnumeration
import GroupApproximation.Sofic.LiteralTorsionFreeRouterSourceNoGo
import GroupApproximation.Sofic.LiteralAffineFreeProductAvatarBlueprint
import GroupApproximation.Higman.LiteralAffineFreeProductPaddedAvatarBlueprint
import GroupApproximation.Higman.LiteralAffineFreeProductAvatarChecks
import GroupApproximation.Sofic.AvatarRouterInstance
import GroupApproximation.Sofic.AvatarRunBound
import GroupApproximation.Sofic.BespokeRouterGateAssembly
import GroupApproximation.Sofic.GreendlingerFreeGate
import GroupApproximation.Sofic.GreendlingerReducedness
import GroupApproximation.Sofic.AmalgamMFTrace
import GroupApproximation.Sofic.TerminalQuotientPresentation
import GroupApproximation.Sofic.TerminalQuotientIso
import GroupApproximation.Sofic.SigmaGroupMF
import GroupApproximation.Sofic.SymmetricDoubleShulman
import GroupApproximation.Sofic.PushedDefectSaturation
import GroupApproximation.Sofic.ArithmeticAmplifiedEndpoint
import GroupApproximation.Sofic.MinimalNoCancellingPair
import GroupApproximation.Sofic.MinimalPalindromePair
import GroupApproximation.Sofic.MatchingReduced
import GroupApproximation.Sofic.MatchingPositions
import GroupApproximation.Sofic.MatchingBoundaryBlock
import GroupApproximation.Sofic.MatchingRunPiece
import GroupApproximation.Sofic.MatchingStemContraction
import GroupApproximation.Sofic.CurvatureAssembly
import GroupApproximation.Sofic.MatchingRunGap
import GroupApproximation.Sofic.ShellSingleRegion
import GroupApproximation.Sofic.RadicalAutomorphization
import GroupApproximation.Endpoint.ApproximationRadicals
import GroupApproximation.Sofic.MatchingSameBlock
import GroupApproximation.Sofic.MatchingRunStructure
import GroupApproximation.Sofic.MatchingStemFold
import GroupApproximation.Sofic.SigmaCompressionPair
import GroupApproximation.Computability.MFRecognitionImpossible
import GroupApproximation.Endpoint.MFRecognitionAudit
import GroupApproximation.Sofic.PalindromicMinimalExpr
import GroupApproximation.Sofic.MatchingFactorPair
import GroupApproximation.Sofic.NonCrossingEdgeBound
import GroupApproximation.Sofic.NonCrossingDegreeBound
import GroupApproximation.Sofic.MatchingChordGraph
import GroupApproximation.Sofic.CurvatureStemThreshold
import GroupApproximation.Sofic.MatchingFoldObstruction
import GroupApproximation.Sofic.MatchingBlockOrder
import GroupApproximation.Computability.CodedMicrostate
import GroupApproximation.Computability.MicrostateNormalForm
import GroupApproximation.Computability.RationalComplexCode
import GroupApproximation.Computability.EffectiveMatrixCode
import GroupApproximation.Analysis.OperatorNormCertificate
import GroupApproximation.Analysis.CayleyUnitary
import GroupApproximation.Analysis.UnitaryPerturbation
import GroupApproximation.Analysis.RationalHermitian
import GroupApproximation.Analysis.RatComplexSubfield
import GroupApproximation.Analysis.AdjointDefectEstimate
import GroupApproximation.Manuscript.OneSidedMFRadical.TransportAssembly
import GroupApproximation.Manuscript.OneSidedMFRadical.CanonicalSector
import GroupApproximation.Manuscript.OneSidedMFRadical.HeadlineTheorem
import GroupApproximation.Endpoint.OneSidedTransportAudit
import GroupApproximation.Leavitt.RankTwelveCorner
import GroupApproximation.Leavitt.LeavittMarkNontrivial
import GroupApproximation.Kazhdan.AmenableKazhdanFinite
import GroupApproximation.Kazhdan.KazhdanSeparableDescent
import GroupApproximation.Leavitt.BinaryLeavittSimple
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedLeavittEquations
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedDefinitions
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedRemarks
import GroupApproximation.Manuscript.OneSidedMFRadical.CountableNonMF
import GroupApproximation.Leavitt.ElementarySimplicity
import GroupApproximation.Manuscript.OneSidedMFRadical.CornerCoronaClass
import GroupApproximation.Leavitt.CongruenceSubgroups
import GroupApproximation.Leavitt.ElementaryTransvectionExtraction
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedSectorProof
import GroupApproximation.Leavitt.RootDetectionBinary
import GroupApproximation.Leavitt.DiagonalNormalExtraction
import GroupApproximation.Manuscript.OneSidedMFRadical.CornerCoordinatePassage
import GroupApproximation.Manuscript.OneSidedMFRadical.SentenceClosureAudit
import GroupApproximation.Manuscript.OneSidedMFRadical.SentenceCurrentLeavittCompressionClosure
import GroupApproximation.Manuscript.OneSidedMFRadical.HNNCoronaConjugatorSentenceAudit
import GroupApproximation.Manuscript.OneSidedMFRadical.HNNAmalgamCornerSentences
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFEndpoint
import GroupApproximation.Manuscript.OneSidedMFRadical.ComputabilityConstructionClosure
import GroupApproximation.Manuscript.OneSidedMFRadical.CompleteDefectSaturation
import GroupApproximation.Manuscript.OneSidedMFRadical.TransportCommutantEquality
import GroupApproximation.Leavitt.ExchangeRefinement
import GroupApproximation.Leavitt.RowAnnihilatorTransvection
import GroupApproximation.Leavitt.PreusserSandwichStep
import GroupApproximation.Leavitt.PreusserAssembly
import GroupApproximation.Leavitt.PreusserLevelUniqueness
import GroupApproximation.Leavitt.PreusserNormalizedByCore
import GroupApproximation.Leavitt.PreusserNormalizedByRowAnnihilator
import GroupApproximation.Leavitt.PreusserNormalizedBySandwich
import GroupApproximation.Leavitt.PreusserNormalizedBy
import GroupApproximation.Steinberg.GeneralRankElementaryPropertyT
import GroupApproximation.Steinberg.ElementaryIndexPadding
import GroupApproximation.Steinberg.GeneralRankFiniteFieldPropertyT
import GroupApproximation.PropertyT.A2MagicExponentFree
import GroupApproximation.PropertyT.FinitelyGeneratedRing
import GroupApproximation.PropertyT.FinitelyGeneratedRingPermanence
import GroupApproximation.PropertyT.EJZIntegralReduction
import GroupApproximation.PropertyT.EJZIntegralGeneralRankReduction
import GroupApproximation.Leavitt.RowAnnihilatorAlternate
import GroupApproximation.PropertyT.IntegralCharacterMass
import GroupApproximation.PropertyT.IntegralColumnPlaneReduction
import GroupApproximation.PropertyT.IntegralColumnPlaneRootReduction
import GroupApproximation.PropertyT.IntegralColumnPlaneSpectralShear
import GroupApproximation.PropertyT.IntegralColumnPlaneSpectralTorus
import GroupApproximation.PropertyT.IntegralColumnPlaneSpectralCoreBound
import GroupApproximation.PropertyT.IntegralColumnPlaneSpectralMassBound
import GroupApproximation.PropertyT.KassabovRankZeroTorusGeometry
import GroupApproximation.PropertyT.IntegralScalarRootDisplacement
import GroupApproximation.PropertyT.IntegralPolynomialDisplacement
import GroupApproximation.PropertyT.KassabovMeasureInequalities
import GroupApproximation.PropertyT.KassabovBorelMeasureInequalities
import GroupApproximation.PropertyT.KassabovTorusNumerics
import GroupApproximation.Analysis.CommutativeCStarCovariance
import GroupApproximation.Analysis.CommutativeStateSpectralMeasure
import GroupApproximation.Analysis.HilbertQuadraticTransport
import GroupApproximation.Analysis.RepresentedRootPlaneSpectralMeasure
import GroupApproximation.Kazhdan.RealToComplexUnitaryRepresentation
import GroupApproximation.PropertyT.ExponentFreeClassTwoOrthogonality
import GroupApproximation.PropertyT.HeisenbergAngleBound
import GroupApproximation.Computability.FiniteDimensionalApproximationIncomplete
import GroupApproximation.Computability.ArithmeticalHierarchy
import GroupApproximation.Computability.FixedMarkedQueryHierarchy
import GroupApproximation.Computability.FixedLiteralMarkedQuery
import GroupApproximation.Computability.ExactSwitchQueryCompleteness
import GroupApproximation.Computability.ExactSwitchAlgorithmicConsequences
import GroupApproximation.Computability.FixedLiteralMarkedQueryFiniteHardness
import GroupApproximation.Computability.EnumeratedFixedMarkedQueryConsequences
import GroupApproximation.Computability.MicrostateNaturalize
import GroupApproximation.Endpoint.MFComputabilityPaperAudit
import GroupApproximation.Sofic.SplitMFStability
import GroupApproximation.Sofic.MFBlackHoleAttachment
import GroupApproximation.Sofic.InvisibleExtensions
import GroupApproximation.Endpoint.InvisibleExtensionsAudit
import GroupApproximation.Analysis.KOmegaHilbertSpaceEndpoint
import GroupApproximation.Analysis.ReducedGroupCStarStablyFinite
import GroupApproximation.Analysis.ReducedGroupCStarMFAlgebra
import GroupApproximation.Analysis.ReducedGroupCStarDedekindFinite
import GroupApproximation.Analysis.BlackadarKirchbergFiniteDimensionalLift
import GroupApproximation.Analysis.BlackadarKirchbergFiniteDirectSumLift
import GroupApproximation.Analysis.BlackadarKirchbergStarEquivTransport
import GroupApproximation.Analysis.GoldbringHartRoute
import GroupApproximation.Manuscript.OneSidedMFRadical.ReducedCStarConsequence
import GroupApproximation.Manuscript.OneSidedMFRadical.ReducedCStarNotNuclear
import GroupApproximation.Computability.HereditaryPropertySwitchCompleteness
import GroupApproximation.Computability.HyperlinearMarkov
import GroupApproximation.Computability.HereditaryRecognitionPhaseDiagram
import GroupApproximation.Computability.HyperlinearRecognitionSecondLevel
import GroupApproximation.Computability.HyperlinearRecognitionHierarchy
import GroupApproximation.Computability.MarkovRecognitionHierarchy
import GroupApproximation.Analysis.FiniteMatrixAnisotropicSign
import GroupApproximation.Analysis.FiniteMatrixSignNormalization
import GroupApproximation.Computability.FreeEdgeTowerCodePrimrec
import GroupApproximation.Computability.FreeEdgeTowerSemantics
import GroupApproximation.Computability.FreeEdgeTowerIteration
import GroupApproximation.Computability.EffectiveMatrixVectorWitnessComplete
import GroupApproximation.Computability.MFRecognitionPi02
import GroupApproximation.Computability.MFRecognitionSecondLevel
import GroupApproximation.Endpoint.MFRecognitionSecondLevelAudit
import GroupApproximation.Endpoint.MFEnumeratedPi02Audit
import GroupApproximation.Computability.MicrostateGeneratorEncoding
import GroupApproximation.Computability.SoficPromiseMFRecognition
import GroupApproximation.External.TauCeti.RepresentationTheory.Compact.RepresentativeDensity
import GroupApproximation.Higman.InjectedCompilerTower
import GroupApproximation.Higman.MikhailovaFiberProduct
import GroupApproximation.Higman.MikhailovaFiberProductProfinite
import GroupApproximation.Higman.MikhailovaGraphProductWitness
import GroupApproximation.Higman.MikhailovaRankThreeWitness
import GroupApproximation.Higman.MikhailovaRopeCode
import GroupApproximation.Higman.MikhailovaRankThreeCode
import GroupApproximation.Higman.MikhailovaRopeCodeSemantics
import GroupApproximation.Higman.MikhailovaRopeCompiler
import GroupApproximation.Higman.PairedReturnCutterCode
import GroupApproximation.Higman.PairedReturnMapEmbCode
import GroupApproximation.Higman.TransportStarCode
import GroupApproximation.Endpoint.PairedReturnCutterCodeAudit
import GroupApproximation.Higman.FreeLampFinitePresentation
import GroupApproximation.Higman.PairedFoldKernel
import GroupApproximation.Higman.PairedReturnFirstIntersection
import GroupApproximation.Higman.PairedReturnGraphIntersection
import GroupApproximation.Higman.MatchedSubgroupAmalgam
import GroupApproximation.Higman.PairedReturnCutter
import GroupApproximation.Higman.PairedReturnEdgeGraph
import GroupApproximation.Higman.PairedReturnEdgeProfinite
import GroupApproximation.Higman.PairedReturnFirstRangeVirtualRetract
import GroupApproximation.Higman.PairedReturnAmbientResiduallyFinite
import GroupApproximation.Higman.TransportCodeRE
import GroupApproximation.Leavitt.LeavittModuleRank
import GroupApproximation.Manuscript.OneSidedMFRadical.CornerClassIdentificationAudit
import GroupApproximation.Computability.SoficRecognitionSecondLevel
import GroupApproximation.Manuscript.NonMF.AcylindricallyHyperbolic
import GroupApproximation.Manuscript.NonMF.HullSmallCancellation
import GroupApproximation.Manuscript.MFRecognition.MarkedHigmanOutput
import GroupApproximation.Manuscript.MFRecognition.EffectiveHigmanCompiler
import GroupApproximation.Manuscript.MFRecognition.LocalityAndCertificates
import GroupApproximation.Manuscript.MFRecognition.FinitelyGeneratedNonMFQuotient
import GroupApproximation.Manuscript.MFRecognition.SeedPresentation
import GroupApproximation.Manuscript.MFRecognition.ReducedProductsWiring
import GroupApproximation.Manuscript.NonMF.Saturation
import GroupApproximation.Manuscript.MFRecognition.MikhailovaConsequences
import GroupApproximation.Manuscript.OneSidedMFRadical.RankTwelveSimplicitySentences
import GroupApproximation.Manuscript.OneSidedMFRadical.LeavittSectionSentences
import GroupApproximation.Manuscript.MFRecognition.RopeObjects
import GroupApproximation.Manuscript.MFRecognition.CentralRope
import GroupApproximation.Manuscript.NonMF.PriorWorkBlackadarKirchberg
import GroupApproximation.Manuscript.NonMF.PriorWorkConnesEmbedding
import GroupApproximation.Manuscript.NonMF.PriorWorkErshovJaikinZapirain
import GroupApproximation.Manuscript.NonMF.PriorWorkShulmanAmalgam
import GroupApproximation.Manuscript.MFRecognition.TensorSynchronizationCoronaTrace
import GroupApproximation.Manuscript.OneSidedMFRadical.StableFinitenessSentencesCore
import GroupApproximation.Manuscript.OneSidedMFRadical.StableFinitenessSentences
import GroupApproximation.Manuscript.NonMF.FournierFacioDoubleHNN
import GroupApproximation.Manuscript.NonMF.FournierFacioInput
import GroupApproximation.Manuscript.NonMF.TorsionFreeTheoremC
import GroupApproximation.Manuscript.MFRecognition.FiniteRope
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgeRecursive
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgeInjective
import GroupApproximation.Manuscript.MFRecognition.RopeObjectsProfinite
import GroupApproximation.Manuscript.OneSidedMFRadical.NormalKazhdanSentences
import GroupApproximation.Manuscript.OneSidedMFRadical.RadicalCalculusSentences
import GroupApproximation.Manuscript.OneSidedMFRadical.IntroductionClaimSentences
import GroupApproximation.Manuscript.OneSidedMFRadical.KazhdanTransportSentences
import GroupApproximation.Manuscript.MFRecognition.ReducedProductsPermanenceWiring
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridge
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgeNormalCore
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgeQuotient
import GroupApproximation.Manuscript.MFRecognition.RecognitionInputs
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceDischarge
import GroupApproximation.Manuscript.MFRecognition.BridgeUniformPresentation
import GroupApproximation.Manuscript.MFRecognition.CentralRopeGenerators
import GroupApproximation.Manuscript.MFRecognition.PositiveBranchStableLetterRemark
import GroupApproximation.Manuscript.MFRecognition.SeedLemma
import GroupApproximation.Manuscript.MFRecognition.RopeRecognitionInputs
import GroupApproximation.Manuscript.MFRecognition.RecognitionAssembly
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerProof
import GroupApproximation.Manuscript.MFRecognition.RopeCodeFamilyConstruction
import GroupApproximation.Manuscript.MFRecognition.RopeCodeFamilySemantics
import GroupApproximation.Analysis.ShulmanFillTheorem16
import GroupApproximation.Analysis.ShulmanFillConjugatePair
import GroupApproximation.Analysis.MFAlgebraAmalgamFactorMap
import GroupApproximation.Analysis.MFAlgebraAmalgamFactorMapProperties
import GroupApproximation.Analysis.MFAlgebraAmalgamFactorRepresentation
import GroupApproximation.Analysis.MFAlgebraSymmetricDoubleIdentity
import GroupApproximation.Analysis.CompatibleCoronaSupportCorner
import GroupApproximation.Analysis.ShulmanFillConjugationEstimate
import GroupApproximation.Analysis.ShulmanFillModelDescent
import GroupApproximation.Analysis.ShulmanFillAsymptoticGlue
import GroupApproximation.Analysis.ShulmanFillCommutantExact
import GroupApproximation.Analysis.ShulmanFillSymmetricDoubleFlip
import GroupApproximation.Analysis.ShulmanFillDiagonalHom
import GroupApproximation.Analysis.ShulmanFillCommutantUnitary
import GroupApproximation.Analysis.ShulmanFillCoronaJoin
import GroupApproximation.Analysis.ShulmanFillCoronaPair
import GroupApproximation.Analysis.ShulmanFillUnitalCorner
import GroupApproximation.Analysis.ShulmanFillWordLimsup
import GroupApproximation.Analysis.ShulmanSymmetricDoubleRoute
import GroupApproximation.Analysis.ShulmanFillSymmetricDouble
import GroupApproximation.Analysis.ShulmanFillSymmetricDoubleEmbedTheorem13
import GroupApproximation.Analysis.ShulmanFillSymmetricDoubleEmbed
import GroupApproximation.Analysis.ShulmanFillTheorem13
import GroupApproximation.Analysis.ShulmanFillFaithfulPairCollapse
import GroupApproximation.Analysis.CalkinCompactIdeal
import GroupApproximation.Analysis.CalkinSchauder
import GroupApproximation.Analysis.CalkinSchauderProof
import GroupApproximation.Analysis.CStarQuotient
import GroupApproximation.Analysis.CalkinAlgebra
import GroupApproximation.Analysis.CalkinAlgebraStar
import GroupApproximation.Analysis.CalkinCStarAlgebra
import GroupApproximation.Analysis.StarStrongMatrixSequences
import GroupApproximation.Analysis.StarStrongMatrixSequencesAlgebra
import GroupApproximation.Analysis.StarStrongLimitNorm
import GroupApproximation.Analysis.StarStrongMatrixSequencesShulman
import GroupApproximation.Analysis.ArvesonBHTarget
import GroupApproximation.Analysis.VoiculescuPlan
import GroupApproximation.Analysis.StarStrongBlockModel
import GroupApproximation.Analysis.EllTwoBlockFamily
import GroupApproximation.Analysis.ArvesonWeakLimit
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceNonunital
import GroupApproximation.Manuscript.MFRecognition.EffectiveCompilerOfOmega
import GroupApproximation.Manuscript.OneSidedMFRadical.PrintedForms
import GroupApproximation.Manuscript.NonMF.TheoremCPrinted
import GroupApproximation.Manuscript.NonMF.HullBallForm
import GroupApproximation.Manuscript.NonMF.TheoremCDebts
import GroupApproximation.Manuscript.NonMF.ChiodoOfHigman
import GroupApproximation.Manuscript.NonMF.HullInputsProved
import GroupApproximation.Manuscript.NonMF.HullFillKernelRefutation
import GroupApproximation.Manuscript.NonMF.HullFillCorrectedInputs
import GroupApproximation.Manuscript.NonMF.HullFillTheoremCCorrected
import GroupApproximation.Manuscript.MFRecognition.SeedFromTheoremC
import GroupApproximation.Manuscript.MFRecognition.SeedRemarkTheoremC
import GroupApproximation.Manuscript.MFRecognition.RecognitionDebts
import GroupApproximation.Manuscript.MFRecognition.CentralRopeBritton
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceSetup
import GroupApproximation.Manuscript.MFRecognition.MarkedHigmanRopeInput
import GroupApproximation.Manuscript.MFRecognition.MarkedHigmanRopeProfinite
import GroupApproximation.Manuscript.MFRecognition.CentralRopeCore
import GroupApproximation.Manuscript.MFRecognition.NegativeBranch
import GroupApproximation.Manuscript.MFRecognition.PositiveBranchFiniteQuotients
import GroupApproximation.Analysis.ContinuousImageClosure
import GroupApproximation.Analysis.StarSubalgebraMapEquiv
import GroupApproximation.Manuscript.MFRecognition.TensorSynchronizationData
import GroupApproximation.Manuscript.MFRecognition.TensorSynchronizationConjugator
import GroupApproximation.Analysis.ContinuousAdjoinMapping
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceSetupPrelude
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceSetupEdges
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeConjugationDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientGenerators
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientContinuous
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientClosureForward
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientClosureBackward
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientClosure
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceBaseToCoronaInjective
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceSourceAmbientMap
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceTargetAmbientMap
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientMaps
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientRestriction
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceConstructedEdgeDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceConstructedEdgeConj
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceConstructedEdgeGenerator
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeAmbientEquiv
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeIso
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeCovariance
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceCoronaRepresentation
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUniversalDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUniversalMapping
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceSetupUniversal
import GroupApproximation.Manuscript.MFRecognition.SwitchGroupBCRRelators
import GroupApproximation.Manuscript.MFRecognition.CompilerIntroSentences
import GroupApproximation.Manuscript.MFRecognition.TensorSynchronization
import GroupApproximation.Manuscript.MFRecognition.SwitchGroupBCR
import GroupApproximation.Manuscript.MFRecognition.CoronaEmbeddingRemark
import GroupApproximation.Manuscript.MFRecognition.RegularRealizationSentences
import GroupApproximation.Manuscript.ClosureAssumptionAudit
import GroupApproximation.Manuscript.MFRecognition.PreliminarySentences
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGroupData
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMatrixCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationCoordinateCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationCoronaCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationCoordinateConjugatorCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationProductConjugatorCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationConjugatorCore
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaOperations
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaBasicMaps
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCoronaFactors
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCompatibility
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaFactorMaps
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaRepresentation
import GroupApproximation.Analysis.HNNTraceGeneratedDensity
import GroupApproximation.Analysis.HNNTraceStarAlgHomDescent
import GroupApproximation.Analysis.HNNTraceTracialStateContinuous
import GroupApproximation.Manuscript.MFRecognition.HNNTraceBaseTransport
import GroupApproximation.Manuscript.MFRecognition.TensorSynchronizationSentences
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceCitations
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceTraceBridge
import GroupApproximation.Manuscript.MFRecognition.HNNPermanence
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamPackage
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamLeft
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamRight
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamInjective
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamCommonImage
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaMatrixIdentities
import GroupApproximation.Manuscript.MFRecognition.HNNTraceBaseTrace
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedFactorization
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedAlongMap
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedAlongTrace
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedSurjection
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedSubgroupCore
import GroupApproximation.Manuscript.MFRecognition.HNNTraceReducedSubgroup
import GroupApproximation.Manuscript.MFRecognition.HNNTraceCovariantBase
import GroupApproximation.Manuscript.MFRecognition.PositiveBranch
import GroupApproximation.Manuscript.MFRecognition.RecognitionMainTheorem
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceEdgeDensity
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnit
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaMatrixUnitLeft
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaLeftMatrixIdentityEleven
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaElevenLeftInclusion
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaMatrixUnitRight
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaRightMatrixIdentityEleven
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaElevenRightInclusion
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitEleven
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitLeft
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerMatrixIdentity
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitLeftInclusion
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitLeftCommon
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitCommonImage
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaRightMatrixIdentity
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitRightInclusion
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerUnitRight
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerCommonImages
import GroupApproximation.Manuscript.NinetyNineProblems.StablyFinite
import GroupApproximation.Manuscript.NinetyNineProblems.ProblemX
import GroupApproximation.Manuscript.NinetyNineProblems.ProblemXImpliesIX
import GroupApproximation.Manuscript.NinetyNineProblems.FactorizationProperty
import GroupApproximation.Manuscript.NinetyNineProblems.ProblemXGroups
import GroupApproximation.Manuscript.NinetyNineProblems.FactorizationImpliesHyperlinear
import GroupApproximation.Analysis.MatrixAbsoluteValue
import GroupApproximation.Analysis.HilbertSchmidtPolarCorrection
import GroupApproximation.Analysis.CStarMatrixTwoCorner
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedConjugator
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedFactorDefs
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCovariance
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCompatibilityApply
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCompatibility
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedRepresentation
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedAmalgamMap
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedAmalgamProperties
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerWord
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaBaseCornerElement
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaBaseCornerMap
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerCovarianceAmbient
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerStableUnitary
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerCovariance
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerNontrivial
import GroupApproximation.Analysis.AmenableTraceHyperlinear
import GroupApproximation.Manuscript.NinetyNineProblems.FactorizationHyperlinearTheorem
import GroupApproximation.Manuscript.NinetyNineProblems.KazhdanQuasidiagonalTraces
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCornerDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCornerBase
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaUniversalMapDef
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaUniversalMapProperties
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedCornerStable
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaEvaluatedComposite
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaDirectEmbedding
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCitation
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceShulman
import GroupApproximation.Algebra.CoprodIAltWord
import GroupApproximation.Analysis.NormMatrixCoronaPolynomialLifts
import GroupApproximation.Analysis.RationalNoncommutativeStarPolynomial
import GroupApproximation.Analysis.RationalStarPolynomialBlockDiagonal
import GroupApproximation.Analysis.ReducedProductMFBlockDiagonal
import GroupApproximation.Analysis.ReducedProductMFDiagonalData
import GroupApproximation.Analysis.ReducedProductMFFiniteSelection
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationAssembly
import GroupApproximation.Analysis.BoundedCStarSequenceAlgebraEvaluation
import GroupApproximation.Analysis.BoundedCStarSequenceEvaluation
import GroupApproximation.Analysis.BoundedCStarSequenceEvaluationDef
import GroupApproximation.Analysis.CStarCountableAdjoinSeparable
import GroupApproximation.Analysis.CStarGeneratedClosureEquality
import GroupApproximation.Analysis.CStarGeneratedSeparable
import GroupApproximation.Analysis.CStarGeneratedSeparableCountable
import GroupApproximation.Analysis.CStarGeneratedSeparableUnion
import GroupApproximation.Analysis.DenseRationalStarPolynomialExtension
import GroupApproximation.Analysis.ReducedProductMFDesignatedCoordinate
import GroupApproximation.Analysis.ShulmanCoronaHalmosArgumentCommutator
import GroupApproximation.Analysis.ShulmanCoronaHalmosDef
import GroupApproximation.Analysis.ShulmanCoronaHalmosDefectRoot
import GroupApproximation.Analysis.ShulmanHalmosDilationAlgebra
import GroupApproximation.Analysis.ShulmanHalmosDilationBase
import GroupApproximation.Analysis.ShulmanHalmosDilationCommutator
import GroupApproximation.Analysis.ShulmanHalmosDilationDef
import GroupApproximation.Analysis.ShulmanHalmosDilationDefectPositive
import GroupApproximation.Analysis.ShulmanHalmosDilationDiagNonneg
import GroupApproximation.Analysis.ShulmanHalmosDilationEndpoint
import GroupApproximation.Analysis.ShulmanHalmosDilationUnitary
import GroupApproximation.Analysis.StarSubalgebraMapEquivDef
import GroupApproximation.Analysis.StarSubalgebraRestrictionEquiv
import GroupApproximation.Computability.BenignComapCodeSemantics
import GroupApproximation.Higman.OmegaTowerConjugateBasisCoordinates
import GroupApproximation.Higman.OmegaTowerConjugateBasisEdge
import GroupApproximation.Higman.OmegaTowerConjugateBasisInvariant
import GroupApproximation.Higman.OmegaTowerConjugateBasisPinch
import GroupApproximation.Higman.OmegaTowerConjugateBasisPinchRewrite
import GroupApproximation.Higman.OmegaTowerConjugateBasisShift
import GroupApproximation.Higman.OmegaTowerConjugateBasisUnshift
import GroupApproximation.Higman.OmegaTowerLocalGlobalCoordinates
import GroupApproximation.Higman.OmegaTowerShiftSeam
import GroupApproximation.Higman.OmegaTowerSignedShift
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaAmalgamPackageType
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgeEffectivity
import GroupApproximation.Manuscript.MFRecognition.ThreeGeneratorBridgePresentation
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedCovarianceCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedDefinitionCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedEndpointCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedInstanceCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedRestrictionCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedSeparableCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationGeneratedSubalgebraCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFCoordinateCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFCoordinateGeneratedCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFGeneratedCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFManuscriptCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationMFRepresentationCore
import GroupApproximation.Manuscript.OneSidedMFRadical.TensorSynchronizationTraceCore
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUniversalInstances
import GroupApproximation.Analysis.AsymptoticModelMFEmbedding
import GroupApproximation.Analysis.BlackadarKirchbergConvexSupportDensity
import GroupApproximation.Analysis.BlackadarKirchbergCoordinateSelection
import GroupApproximation.Analysis.MatrixCoronaAmplificationEquivAudit
import GroupApproximation.Analysis.UniversalCStarAmalgamLarge
import GroupApproximation.Computability.BenignSupCodeModelSemantics
import GroupApproximation.Endpoint.MFRecognitionFiniteCertificatesAudit
import GroupApproximation.GroupTheory.HNNFiniteQuotientCriterion
import GroupApproximation.Higman.BenignJoinFiniteQuotientMap
import GroupApproximation.Higman.CentralHNNFiniteQuotientMap
import GroupApproximation.Higman.CodedTransportStarProfinite
import GroupApproximation.Higman.ConjugatorGraphProfinite
import GroupApproximation.Higman.FreeGroupHall
import GroupApproximation.Higman.FreeLampFiniteBaseProfinite
import GroupApproximation.Higman.FreeLampProfiniteEmbedding
import GroupApproximation.Higman.HNNSubextensionFiniteBaseProfinite
import GroupApproximation.Higman.MatchedSubgroupAmalgamWordReflection
import GroupApproximation.Higman.OmegaHalfLineAscendingCriterion
import GroupApproximation.Higman.OmegaHalfLineFiniteCutter
import GroupApproximation.Higman.OmegaHalfLineFiniteHNN
import GroupApproximation.Higman.OmegaHalfLineGraphGate
import GroupApproximation.Higman.OmegaHalfLineLabelShift
import GroupApproximation.Higman.OmegaHalfLineMatchedFiniteCutter
import GroupApproximation.Higman.OmegaHalfLineReduction
import GroupApproximation.Higman.OmegaHalfLineRightInsertion
import GroupApproximation.Higman.OmegaHalfLineSemanticGraphWitness
import GroupApproximation.Higman.OmegaHalfLineTargetCutter
import GroupApproximation.Higman.PairedReturnCutterCentralHNN
import GroupApproximation.Higman.PairedReturnImageIntersectionRefinement
import GroupApproximation.Higman.PairedReturnLeftProduct
import GroupApproximation.Higman.PairedReturnLeftProductProfinite
import GroupApproximation.Higman.PairedReturnMatchedCutterProfinite
import GroupApproximation.Higman.PairedReturnProfiniteWitness
import GroupApproximation.Higman.PairedReturnQProfinite
import GroupApproximation.Higman.ProfiniteBenignFactorizationReflection
import GroupApproximation.Higman.ProfiniteBenignInfProductSeparable
import GroupApproximation.Higman.ProfiniteBenignProductSeparable
import GroupApproximation.Higman.ProfiniteCofinalClosedImage
import GroupApproximation.Higman.TransportStarProdBotProfinite
import GroupApproximation.Higman.TransportStarSourceProductSeparable
import GroupApproximation.Manuscript.MFRecognition.ConcreteQCodeFamily
import GroupApproximation.Manuscript.MFRecognition.FinitelyGeneratedNonMFQuotientAudit
import GroupApproximation.Manuscript.MFRecognition.FixedUniversalFamily
import GroupApproximation.Manuscript.MFRecognition.FixedUniversalFamilyRecursive
import GroupApproximation.Manuscript.MFRecognition.FixedUniversalHostCompiler
import GroupApproximation.Manuscript.MFRecognition.FixedUniversalHostOfOmega
import GroupApproximation.Manuscript.MFRecognition.TwoSidedBridgeRelatorCode
import GroupApproximation.Manuscript.MFRecognition.TwoSidedConcreteQCodeFamily
import GroupApproximation.Sofic.ProfiniteFiniteExtensionLERF
import GroupApproximation.Computability.BenignSupCodeSemantics
import GroupApproximation.Analysis.CStarMatrixTwoByTwo
import GroupApproximation.Analysis.RepresentedRootPlaneSpectralQuasiInvariant
import GroupApproximation.Computability.BenignSupCodeSubgroupSemantics
import GroupApproximation.Computability.ParametricRecursiveSwitchPresentation
import GroupApproximation.GGT.HyperbolicTreeMetric
import GroupApproximation.GGT.HyperbolicAdditiveTransfer
import GroupApproximation.GGT.HyperbolicFreeGroupAH
import GroupApproximation.GGT.HyperbolicTreeAction
import GroupApproximation.GGT.HyperbolicWPDTransfer
import GroupApproximation.GGT.HyperbolicTreeSegmentShift
import GroupApproximation.GGT.BassSerreHNNLength
import GroupApproximation.GGT.BassSerreHNNTree
import GroupApproximation.GGT.BassSerreHNNIsTree
import GroupApproximation.GGT.BassSerreHNNAction
import GroupApproximation.GGT.BassSerreDoubleHNN
import GroupApproximation.GGT.BassSerreHNNWPDInput
import GroupApproximation.GGT.BassSerreHNNAxisWPD
import GroupApproximation.GGT.TreeWPDAxis
import GroupApproximation.GGT.CayleyGeodesicModel
import GroupApproximation.GGT.CayleyGeodesicRealisation
import GroupApproximation.GGT.ElementaryBowditch
import GroupApproximation.GGT.ElementaryCentralizerAxis
import GroupApproximation.GGT.ElementaryClosure
import GroupApproximation.GGT.ElementaryCommonPower
import GroupApproximation.GGT.ElementaryFillCentralizer
import GroupApproximation.GGT.ElementaryFillConjugate
import GroupApproximation.GGT.ElementaryMorse
import GroupApproximation.GGT.ElementaryMorseChord
import GroupApproximation.GGT.ElementaryMorseOrbit
import GroupApproximation.GGT.ElementaryIndependence
import GroupApproximation.GGT.ElementaryBowditchProof
import GroupApproximation.GGT.ElementaryOsinNormalClosed
import GroupApproximation.GGT.ElementaryMorseAlphabet
import GroupApproximation.GGT.ElementaryMorseBiInfinite
import GroupApproximation.GGT.ElementaryHypEmbedded
import GroupApproximation.GGT.ElementaryProjectionCriterion
import GroupApproximation.GGT.ElementaryProperFromTransversal
import GroupApproximation.GGT.ElementaryOsinSNormal
import GroupApproximation.GGT.ElementaryProperClosure
import GroupApproximation.GGT.ElementaryTransfer
import GroupApproximation.GGT.HullSC
import GroupApproximation.GGT.HullSCCommonQuotient
import GroupApproximation.GGT.HullSCCommonQuotientCorrected
import GroupApproximation.GGT.HullSCConeOff
import GroupApproximation.GGT.HullSCConeOffSpace
import GroupApproximation.GGT.HullSCFilling
import GroupApproximation.GGT.HullSCInjectivityTransfer
import GroupApproximation.GGT.HullSCFreeProductFactor
import GroupApproximation.GGT.HullSCHypEmbedded
import GroupApproximation.GGT.HullSCRelatorFamily
import GroupApproximation.GGT.HullSCRelatorWord
import GroupApproximation.GGT.HullSCRotatingFamily
import GroupApproximation.GGT.HullSCDGO
import GroupApproximation.GGT.HullSCSmallCancellation
import GroupApproximation.GGT.HullSCTheorem51
import GroupApproximation.GGT.KazhdanHyp
import GroupApproximation.GGT.KazhdanHypGirthEight
import GroupApproximation.GGT.KazhdanHypLinkGap
import GroupApproximation.GGT.KazhdanHypPolygonal
import GroupApproximation.GGT.KazhdanHypQuadrangle
import GroupApproximation.GGT.KazhdanHypQuadrangleBridge
import GroupApproximation.GGT.KazhdanHypTable
import GroupApproximation.GGT.KazhdanHypTorsionCriterion
import GroupApproximation.GGT.RelHypDefinition
import GroupApproximation.GGT.PingPongFreeSubgroup
import GroupApproximation.GGT.RelHypLetterPieces
import GroupApproximation.GGT.RelHypAbelianPartnerNoGo
import GroupApproximation.GGT.RelHypOsinTheorem24Repaired
import GroupApproximation.GGT.PingPongReduction
import GroupApproximation.GGT.RelHypElementaryAmenable
import GroupApproximation.GGT.RelHypFournierFacio
import GroupApproximation.GGT.RelHypFreeProductPeripheral
import GroupApproximation.GGT.RelHypKazhdanNonElementary
import GroupApproximation.GGT.RelHypOsinTheorem24
import GroupApproximation.GGT.RelHypOsinTheorem24Refuted
import GroupApproximation.GGT.CayleyFourPointBridge
import GroupApproximation.GGT.RelHypRelativeCayley
import GroupApproximation.GGT.RelHypWithoutKazhdan
import GroupApproximation.GGT.WPDAcylindricalHyperbolicity
import GroupApproximation.GGT.WPDDGOReduction
import GroupApproximation.GGT.WPDElement
import GroupApproximation.GGT.WPDHyperbolicallyEmbedded
import GroupApproximation.GGT.WPDMinasyanOsinSkeleton
import GroupApproximation.GGT.WPDElementaryEmbedding
import GroupApproximation.GGT.OsinComponents
import GroupApproximation.GGT.OsinEnlargement
import GroupApproximation.GGT.OsinSeparatingCosets
import GroupApproximation.GGT.OsinPenetration
import GroupApproximation.GGT.OsinGeodesicWord
import GroupApproximation.Higman.OmegaFillLinkPreimage
import GroupApproximation.Higman.OmegaFatSlimCanonicalOne
import GroupApproximation.Higman.OmegaFatSlimCanonicalTwo
import GroupApproximation.Higman.OmegaFatSlimCanonicalThree
import GroupApproximation.Manuscript.NonMF.HullFillOsinNormalReduction
import GroupApproximation.Analysis.NormCoronaAsymptoticLiftRestriction
import GroupApproximation.GGT.HullSCUnionGeometryNormalForm
import GroupApproximation.Higman.OmegaTowerSelectedRowWord
import GroupApproximation.Higman.OmegaTowerSelectedAbstractEndpointFactors
import GroupApproximation.GGT.HullSCUnionGeometryFourPoint
import GroupApproximation.Higman.OmegaFatShearedLinkSemantic
import GroupApproximation.Higman.OmegaFatShearedLinkBase
import GroupApproximation.Higman.OmegaFatLinkEmbeddingObstruction
import GroupApproximation.Higman.OmegaTowerSelectedArbitraryReturnWitness
import GroupApproximation.Analysis.ShulmanFillNormingCoronaRoute
import GroupApproximation.Analysis.ShulmanFillNormingAmalgamWitness
import GroupApproximation.Analysis.ShulmanFillNormingAsymptotic
import GroupApproximation.Analysis.ShulmanFillNormingPrefixBlock
import GroupApproximation.Analysis.ShulmanFillNormingFactorImages
import GroupApproximation.Analysis.ShulmanFillNormingFamily
import GroupApproximation.Analysis.ShulmanFillNormingResiduallyFinite
import GroupApproximation.Higman.OmegaTowerSelectedArbitraryTargetClassifier
import GroupApproximation.GGT.CayleyGeodesicQuotient
import GroupApproximation.Higman.OmegaFillLeadLinkBenign
import GroupApproximation.Analysis.ShulmanFillNormingAsymptoticMF
import GroupApproximation.Analysis.ShulmanFillNormingBlockHilbert
import GroupApproximation.Analysis.ShulmanFillNormingConjugation
import GroupApproximation.Analysis.ShulmanFillNormingDCStar
import GroupApproximation.GGT.OsinTheorem54Lemma24
import GroupApproximation.GGT.OsinLemma512Torsion
import GroupApproximation.GGT.HullSCRelatorSeparationBall
import GroupApproximation.GGT.HullSCRelatorSeparationGaps
import GroupApproximation.GGT.HullSCRelatorSeparationBlock
import GroupApproximation.GGT.OsinTheorem54SeparatingCosets
import GroupApproximation.GGT.OsinTheorem54SepReversal
import GroupApproximation.GGT.OsinTheorem54SepComponents
import GroupApproximation.GGT.HullSCRelatorSeparationValues
import GroupApproximation.GGT.HullSCRelatorSeparationRefuted
import GroupApproximation.GGT.HullSCRelatorSeparationRepair
import GroupApproximation.GGT.OsinTheorem54SepRuns
import GroupApproximation.GGT.HullSCUnionGeometryCoprod
import GroupApproximation.GGT.HullSCUnionGeometryAcylindrical
import GroupApproximation.GGT.HullSCUnionGeometryConcat
import GroupApproximation.GGT.HullSCUnionGeometryCrossing
import GroupApproximation.GGT.HullSCUnionGeometryLineal
import GroupApproximation.GGT.HullSCUnionGeometryPrefix
import GroupApproximation.GGT.HullSCUnionGeometryElliptic
import GroupApproximation.GGT.HullSCUnionGeometryLongSyllable
import GroupApproximation.GGT.HullSCUnionGeometryFactorBranch
import GroupApproximation.GGT.HullSCUnionGeometryCyclic
import GroupApproximation.GGT.HullSCUnionGeometryTrichotomy
import GroupApproximation.GGT.HullSCUnionGeometryHyperbolicFactor
import GroupApproximation.GGT.OsinTheorem54SepTransport
import GroupApproximation.GGT.OsinTheorem54SepSplit
import GroupApproximation.GGT.OsinTheorem54SepFinite
import GroupApproximation.GGT.OsinTheorem54SepSymmetric
import GroupApproximation.GGT.HullSCRelatorSeparationLetters
import GroupApproximation.GGT.OsinTheorem54SepPolygon
import GroupApproximation.GGT.OsinTheorem54SepCommRefuted
import GroupApproximation.GGT.HullSCRelatorSeparationComponent
import GroupApproximation.GGT.HullSCRelatorSeparationSpacing
import GroupApproximation.GGT.HullSCRelatorSeparationConnector
import GroupApproximation.GGT.HullSCRelatorSeparationNotQG
import GroupApproximation.GGT.HullSCRelatorSeparationRotation
import GroupApproximation.Analysis.ShulmanFillNormingBlockHom
import GroupApproximation.Analysis.ShulmanFillNormingCoronaMap
import GroupApproximation.Analysis.ShulmanFillNormingSeqHom
import GroupApproximation.Analysis.ShulmanFillNormingProductMF
import GroupApproximation.GGT.HullSCRelatorSeparation2Word
import GroupApproximation.GGT.HullSCRelatorSeparation2Component
import GroupApproximation.GGT.HullSCRelatorSeparation2Gaps
import GroupApproximation.GGT.HullSCRelatorSeparation2Design
import GroupApproximation.GGT.HullSCRelatorSeparation2Rigid
import GroupApproximation.GGT.HullSCRelatorSeparation2Core
import GroupApproximation.GGT.HullSCRelatorSeparation2Statement
import GroupApproximation.GGT.HullSCUnionGeometrySyllableSplit
import GroupApproximation.GGT.HullSCUnionGeometryWitness
import GroupApproximation.GGT.HullSCUnionGeometryVirtuallyCyclic
import GroupApproximation.Analysis.ShulmanFillNormingConjugationLift
import GroupApproximation.GGT.HullSCRelatorSeparation2QuasiGeodesic
import GroupApproximation.GGT.HullSCRelatorSeparation2Theorem51
import GroupApproximation.GGT.HullSCRelatorSeparation2ConeOff
import GroupApproximation.GGT.HullSCUnionGeometrySyllableCount
import GroupApproximation.Analysis.ShulmanFillNormingBlockLimit
import GroupApproximation.Analysis.ShulmanFillNormingGluing
import GroupApproximation.Analysis.ShulmanFillNormingMatrixFlatten
import GroupApproximation.GGT.OsinTheorem54SepTransportFam
import GroupApproximation.GGT.OsinTheorem54SepFiniteFam
import GroupApproximation.GGT.OsinTheorem54SepSymmetricFam
import GroupApproximation.GGT.OsinTheorem54Family
import GroupApproximation.GGT.HullSCRelatorSeparation2ConeOffSpace
import GroupApproximation.GGT.HullSCRelatorSeparation2RotatingFamily
import GroupApproximation.GGT.HullSCUnionGeometryFactorDichotomy
import GroupApproximation.GGT.HullSCUnionGeometryBranchPoint
import GroupApproximation.GGT.HullSCUnionGeometryFactorInput
import GroupApproximation.GGT.HullSCUnionGeometryShortBranch
import GroupApproximation.GGT.HullSCUnionGeometryAssembly
import GroupApproximation.Analysis.ShulmanFillNormingDoubleMF
import GroupApproximation.GGT.HullSCRelatorSeparation2Filling
import GroupApproximation.Analysis.ShulmanFillNormingDoubledData
import GroupApproximation.Analysis.BlackadarKirchbergAbstractFiniteDimensionalLift
import GroupApproximation.Analysis.BlackadarKirchbergFiniteCoordinateUCP
import GroupApproximation.Analysis.BlackadarKirchbergFiniteCoordinateLinearFactorization
import GroupApproximation.Analysis.BlackadarKirchbergMFUCPApproximateInverse
import GroupApproximation.Analysis.MFAlgebraAmalgamFaithfulEval
import GroupApproximation.Analysis.MFAlgebraHNNPermanence
import GroupApproximation.Analysis.ShulmanCoronaContractionRepresentative
import GroupApproximation.Analysis.ShulmanCoronaBoundedRepresentative
import GroupApproximation.Analysis.ShulmanContractiveAsymptoticLift
import GroupApproximation.Analysis.ShulmanCoronaHalmosCommutator
import GroupApproximation.Analysis.ShulmanCoronaHalmosSequence
import GroupApproximation.Analysis.ShulmanDenseCompatibility
import GroupApproximation.Analysis.ShulmanDiagonalSelection
import GroupApproximation.Analysis.ShulmanUnitaryConjugationControl
import GroupApproximation.Analysis.ShulmanDiagonalConjugation
import GroupApproximation.Analysis.UniversalCStarAmalgamCoordinate
import GroupApproximation.Computability.FreeEdgeTowerExactEdgeData
import GroupApproximation.Computability.FreeEdgeTowerExactEdgeHom
import GroupApproximation.Computability.FreeEdgeTowerExactEdge
import GroupApproximation.Computability.FreeEdgeTowerExactIterationCore
import GroupApproximation.Computability.FreeEdgeTowerExactIteration
import GroupApproximation.Computability.FreeEdgeTowerMarkedCompiler
import GroupApproximation.Higman.CodedBenignWitness
import GroupApproximation.Higman.TransportStarCodeSemantics
import GroupApproximation.Higman.OmegaFiniteTower
import GroupApproximation.Higman.OmegaTowerBlockWindow
import GroupApproximation.Higman.OmegaTowerPinchRewrite
import GroupApproximation.Higman.OmegaTowerRightLabelInverseCanonical
import GroupApproximation.Higman.PairedReturnFiveCutterProfiniteReduction
import GroupApproximation.Higman.ReifiedHigmanWitnessAgreeCode
import GroupApproximation.Higman.ReifiedHigmanWitnessAgreeConstants
import GroupApproximation.Higman.ReifiedPrimitiveRecursiveProgram
import GroupApproximation.Higman.ReifiedPrimitiveRecursiveCode
import GroupApproximation.Higman.ReifiedPrimitiveRecursiveTowerBase
import GroupApproximation.Higman.ReifiedHigmanWitnessBaseCode
import GroupApproximation.Higman.ReifiedHigmanWitnessRhoCode
import GroupApproximation.Higman.ReifiedHigmanWitnessSigmaCode
import GroupApproximation.Higman.ReifiedHigmanWitnessThetaCode
import GroupApproximation.Higman.TransportStarSpecialJoinClosed
import GroupApproximation.Manuscript.MFRecognition.HNNTraceEdgeDensity
import GroupApproximation.Manuscript.MFRecognition.HNNTraceCovarianceGenerator
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCornerConcrete
import GroupApproximation.Manuscript.MFRecognition.PrintedTarskiCertificateDerivation
import GroupApproximation.Manuscript.MFRecognition.PrintedTarskiCertificateSyntax
import GroupApproximation.Manuscript.MFRecognition.PrintedTarskiCertificateDecision
import GroupApproximation.Manuscript.MFRecognition.PrintedTarskiCertificate
import GroupApproximation.GGT.RelHypOsin24CayleyLeaf
import GroupApproximation.GGT.RelHypOsin24CayleyEndpoint
import GroupApproximation.GGT.OsinTheorem54SepPolygonVertex
import GroupApproximation.GGT.RelHypOsin24CollapseModel
import GroupApproximation.GGT.OsinTheorem54SepFourGon
import GroupApproximation.GGT.OsinTheorem54SepFourGonSide
import GroupApproximation.Analysis.ShulmanFillNormingDoubledFlip
import GroupApproximation.Sofic.Osin24FoldWitnessLegality
import GroupApproximation.GGT.DGOCorollary612Malnormal
import GroupApproximation.GGT.HullSCRelatorSeparation2FillingData
import GroupApproximation.GGT.HullSCRelatorSeparation2Assembly
import GroupApproximation.GGT.HullSCRelatorSeparation2Quotient
import GroupApproximation.GGT.HullSCRelatorSeparation2ListFacts
import GroupApproximation.GGT.HullSCRelatorSeparation2Rotation
import GroupApproximation.Sofic.Osin24FactorEdgeBound
import GroupApproximation.GGT.OsinTheorem54SepFourGonCorner
import GroupApproximation.GGT.RelHypOsin24Collapse
import GroupApproximation.GGT.HullSCRelatorSeparation2Mirror
import GroupApproximation.GGT.HullSCRelatorSeparation2MirrorRun
import GroupApproximation.Higman.OmegaFatShearedCoordinateEdge
import GroupApproximation.GGT.DGOIsolatedComponentWitness
import GroupApproximation.GGT.DGOIsolatedComponentCoset
import GroupApproximation.GGT.RelHypOsin24CayleyWitness
import GroupApproximation.GGT.HullSCRelatorSeparation2Locate
import GroupApproximation.GGT.OsinTheorem54SepSmul
import GroupApproximation.Analysis.BlackadarKirchbergScalarCoordinateStateDensity
import GroupApproximation.Sofic.Osin24FoldedWalk
import GroupApproximation.GGT.OsinTheorem54SepFourGonGeneral
import GroupApproximation.GGT.OsinTheorem54SepFourGonPinning
import GroupApproximation.GGT.OsinTheorem54SepCommIndex
import GroupApproximation.GGT.HullSCRelatorSeparation2MirrorGap
import GroupApproximation.GGT.HullSCRelatorSeparation2Aligned
import GroupApproximation.Analysis.ShulmanFillNormingEllTwoModels
import GroupApproximation.GGT.HullSCRelatorSeparation2MixedCase
import GroupApproximation.GGT.DGOIsolatedComponentBridge
import GroupApproximation.Analysis.ShulmanFillNormingScalarMF
import GroupApproximation.Analysis.ShulmanFillNormingTheorem4Refuted
import GroupApproximation.GGT.OsinTheorem54SepFourGonQuasi
import GroupApproximation.Higman.CodedTransportStarRankThree
import GroupApproximation.GGT.HyperbolicThinTriangles
import GroupApproximation.GGT.DGOIsolatedComponentReduce
import GroupApproximation.GGT.HullSCRelatorSeparation2Cross
import GroupApproximation.GGT.OsinTheorem54SepFourGonInterface
import GroupApproximation.GGT.HullSCRelatorSeparation2Centralizer
import GroupApproximation.GGT.HullSCRelatorSeparation2Power
import GroupApproximation.GGT.OsinTheorem54SepCommSet
import GroupApproximation.GGT.DGOIsolatedComponentTransport
import GroupApproximation.GGT.OsinTheorem54SepFourGonMeet
import GroupApproximation.GGT.HullSCRelatorSeparation2Diagonal
import GroupApproximation.Manuscript.MFRecognition.PositiveBranchResidualFiniteness
import GroupApproximation.Higman.OmegaFatShearedCoordinateBase
import GroupApproximation.Higman.OmegaFatShearedCoordinateShift
import GroupApproximation.GGT.HullSCRelatorSeparation2Aperiodic
import GroupApproximation.Higman.OmegaFatShearedFirstCoordinateMatched
import GroupApproximation.GGT.OsinTheorem54SepElementaryBall
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCompatibleCorner
import GroupApproximation.Manuscript.MFRecognition.HNNPermanenceUedaCoordinateCorner
import GroupApproximation.GGT.OsinTheorem54SepLemma55
import GroupApproximation.GGT.OsinTheorem54SepLetterCount
import GroupApproximation.Higman.OmegaFatShearedFirstSemanticMatched
import GroupApproximation.GGT.OsinTheorem54SepOrder
import GroupApproximation.GGT.OsinTheorem54SepSubGeodesic
import GroupApproximation.GGT.HullSCRelatorSeparation2Diff
import GroupApproximation.GGT.HullSCRelatorSeparation2PowFam
import GroupApproximation.GGT.HullSCRelatorSeparation2Join
import GroupApproximation.GGT.OsinTheorem54SepSegmentComp
import GroupApproximation.GGT.HullSCRelatorSeparation2Tails
import GroupApproximation.GGT.HullSCRelatorSeparation2Window
import GroupApproximation.GGT.OsinTheorem54SepBlockConj
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLift
import GroupApproximation.GGT.HullSCRelatorSeparation2AlignedClose
import GroupApproximation.GGT.DGOThinPolygonVertex
import GroupApproximation.GGT.OsinTheorem54SepSegmentVertex
import GroupApproximation.GGT.OsinTheorem54SepLemma59
import GroupApproximation.GGT.HullSCRelatorSeparation2Segment
import GroupApproximation.GGT.HullSCRelatorSeparation2MirrorClose
import GroupApproximation.GGT.OsinTheorem54SepEnum
import GroupApproximation.GGT.OsinTheorem54SepGapY
import GroupApproximation.GGT.HullSCRelatorSeparation2Assemble
import GroupApproximation.GGT.DGOPolygonGeodesicChain
import GroupApproximation.GGT.HullSCRelatorSeparation2NoCommute
import GroupApproximation.GGT.HullSCRelatorSeparation2Ledger
import GroupApproximation.GGT.OsinTheorem54SepInhabit
import GroupApproximation.GGT.DGOShortIsolatingCycle
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftDouble
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftFlip
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftPair
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftTwoLeg
import GroupApproximation.GGT.OsinTheorem54SepRigidityReduction
import GroupApproximation.GGT.OsinTheorem54SepRigidityTrivial
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftFaithful
import GroupApproximation.GGT.DGOCycleSplice
import GroupApproximation.GGT.DGOCycleAssembly
import GroupApproximation.GGT.OsinTheorem54SepDistBase
import GroupApproximation.GGT.DGOIsolatedComponentVertexDist
import GroupApproximation.GGT.DGOIsolatedComponentRecut
import GroupApproximation.GGT.DGOIsolatedComponentSplit
import GroupApproximation.GGT.HullSCRelatorSeparation2Rigidity
import GroupApproximation.Analysis.ShulmanFillNormingEllTwoTheorem10
import GroupApproximation.GGT.DGOIsolatedComponentNormalise
import GroupApproximation.Analysis.ShulmanFillNormingExistentialLiftPrinted
import GroupApproximation.GGT.DGOFourGonThin
import GroupApproximation.GGT.DGOShortCycleIndices
import GroupApproximation.GGT.OsinTheorem54SepDistPrefix
import GroupApproximation.GGT.OsinTheorem54SepDistSuffix
import GroupApproximation.GGT.DGOIsolatedComponentCut
import GroupApproximation.Analysis.ShulmanFillNormingFactorMapComp
import GroupApproximation.GGT.DGOTwoConnectorSplice
import GroupApproximation.GGT.OsinTheorem54SepDistStep
import GroupApproximation.GGT.DGOIsolatedComponentStraddle
import GroupApproximation.GGT.OsinTheorem54SepDistLeSep
import GroupApproximation.GGT.OsinTheorem54SepLetterMult
import GroupApproximation.GGT.OsinTheorem54SepAssemble
import GroupApproximation.GGT.DGOIsolatedComponentRotate
import GroupApproximation.Analysis.ShulmanFillNormingFactorMapRange
import GroupApproximation.Analysis.ShulmanFillNormingRecognitionWiring
import GroupApproximation.GGT.OsinTheorem54SepLemma510Right
import GroupApproximation.GGT.OsinTheorem54SepAssembleFull
import GroupApproximation.GGT.DGOIsolatedComponentRotateCut
import GroupApproximation.GGT.DGOIsolatedComponentCollapseCut
import GroupApproximation.GGT.DGOIsolatedComponentSideForm
import GroupApproximation.GGT.OsinTheorem54SepFourGonOpposite
import GroupApproximation.GGT.OsinTheorem54SepDeepSixForm
import GroupApproximation.Analysis.CStarSeparableFaithfulRepresentation
import GroupApproximation.Analysis.CStarHilbertTransport
import GroupApproximation.GGT.HullSCRelatorSeparation2Ball
import GroupApproximation.GGT.HullSCRelatorSeparation2MirrorBall
import GroupApproximation.Analysis.CStarHilbertCountableBasis
import GroupApproximation.GGT.OsinTheorem54SepRotatePolygon
import GroupApproximation.GGT.HullSCRelatorSeparation2Span
import GroupApproximation.GGT.DGOReversedSplice
import GroupApproximation.GGT.DGOShortIsolatingCycleMain
import GroupApproximation.GGT.DGOIsolatedComponentBoundFourGon
import GroupApproximation.GGT.OsinTheorem54SepFourGonPolygon
import GroupApproximation.GGT.OsinTheorem54SepRotateComponent
import GroupApproximation.GGT.OsinTheorem54SepTwoBlockRot
import GroupApproximation.GGT.HullSCRelatorSeparation2Extract
import GroupApproximation.Analysis.CStarSeparableTypeZeroRepresentation
import GroupApproximation.GGT.HullSCRelatorSeparation2OtherArc
import GroupApproximation.GGT.DGOIsolatedComponentSideZero
import GroupApproximation.GGT.DGOGeodesicChainComponents
import GroupApproximation.GGT.DGOSafeBlock
import GroupApproximation.GGT.DGOPolygonJoin
import GroupApproximation.GGT.DGOPolygonCutFourGon
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyNamed
import GroupApproximation.GGT.HullSCRelatorSeparation2Apply
import GroupApproximation.GGT.DGOPolygonFarGon
import GroupApproximation.Analysis.ShulmanFillNormingTailAsymptotic
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyComp
import GroupApproximation.Analysis.ShulmanFillNormingTailAsymptoticMF
import GroupApproximation.Analysis.ShulmanFillNormingTailPrinted
import GroupApproximation.Analysis.ShulmanFillNormingPrintedPairRefuted
import GroupApproximation.Analysis.ShulmanFillNormingPrintedPairCharacter
import GroupApproximation.GGT.DGOPolygonEdgeGon
import GroupApproximation.GGT.DGOPolygonLemma417
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyBlock
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplySpelling
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyGap
import GroupApproximation.GGT.DGOPolygonBaseCaseTower
import GroupApproximation.Analysis.ShulmanFillNormingTailTruncation
import GroupApproximation.Analysis.ShulmanFillNormingTailPair
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplySide
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyPair
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyClose
import GroupApproximation.Analysis.ShulmanFillNormingTailCorner
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyRotate
import GroupApproximation.Analysis.ShulmanFillNormingTailShift
import GroupApproximation.Analysis.ShulmanFillNormingTailShiftLimit
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyPin
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyAssemble
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyDispatch
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyExp
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyMatch
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyMixed
import GroupApproximation.Analysis.ShulmanFillNormingTailSeqHom
import GroupApproximation.Analysis.ShulmanFillNormingTailGlueAlign
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyMixedClose
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyMixedInv
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyNarrow
import GroupApproximation.Analysis.ShulmanFillNormingTailGluing
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyNarrowGap
import GroupApproximation.Analysis.ShulmanFillNormingTailDoubleMF
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyNarrowPair
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyPiece
import GroupApproximation.Analysis.ShulmanFillNormingTailPrintedPair
import GroupApproximation.Analysis.ShulmanFillNormingTailRecognition
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyIface
import GroupApproximation.Analysis.CStarInfiniteDimensionalGNS
import GroupApproximation.Analysis.CStarInfiniteFaithfulRepresentation
import GroupApproximation.Analysis.ShulmanFillNormingTailRoute
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyTwoBlock
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyFourWay
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyShortSide
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyLoxGap
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyCompose
import GroupApproximation.GGT.HullSCRelatorSeparation2ApplyQuantified

/-!
# An unconditional construction of a finitely presented nonsofic group

This library proves that a nonsofic group exists, and that a finitely
presented one does.  Both are closed theorems: neither takes a hypothesis
standing in for a construction, and neither is a parameterized implication
advertised as an existence result.

**Start at `GroupApproximation.Public`.**  It is the reading path -- the
declarations a referee needs, each named against the theorem it establishes.

The statement-by-statement correspondence between this construction and its
manuscript is `notes/CLAIM_MAP.md`, generated from the paper's own margin notes;
the manuscript itself is no longer kept in the repository.  The two manuscripts
here are `property_tt_leavitt.tex`, on coordinate-block
factorization and `(TT)/T`, and `non_mf_groups_exist.tex`, on operator-norm
matrix approximation; neither states the nonsofic theorems.

## What is proved here rather than assumed

Every theorem the paper cites for its own proofs is proved in this library,
in the exact form used, so each is an input to the manuscript and not to the
development: Kun's expander decomposition (`KunDecomposition`), the Kun--Thom
centralizer obstruction (`KunThomTheorem`), Shalom's finitely presented
Kazhdan covers (`ShalomFinitePresentation`), and property `(T)` for
elementary groups over finite-type algebras over finite fields
(`FiniteFieldElementaryPropertyT`, with the explicit Kazhdan pair of
`FreeElementaryPropertyT`).  The Ershov--Jaikin-Zapirain theorem over an
arbitrary finitely generated ring is not formalized, and nothing here needs
it.

The `K₁`-theoretic input is likewise eliminated: `BinaryLeavitt.K1_trivial`
proves `K₁(L_k(1,2)) = 0` in Whitehead form by an elementary two-exit
elimination, so the localization-sequence citation is confirmation rather than
dependency.

## The construction

The coefficient ring is the actual universal binary Leavitt algebra, defined
as the presented quotient of the free algebra; its stream-operator
representation proves that quotient nontrivial, so no faithfulness claim is
needed.  `UniversalRankFour.compressionSetup` constructs the algebraic setup
rather than accepting it from a caller, and the corner subgroup carrying the
non-LEF obstruction is identified with Thompson's group `V`
(`ThompsonVWitness.thompsonV_not_isLEF`), proved non-LEF unconditionally with
no Higman presentation input.

`MainResults.universalLeavittEL4_not_isSofic` supplies the initial nonsofic
group; `TableCover` builds its finitely presented cover, and `KazhdanCover`
the Kazhdan one.

## Trust surface

`GroupApproximation.Audit` prints the dependency report for the public results on
an ordinary build.  `scripts/Audit.lean` independently walks the transitive
dependency closure of the whole namespace and fails on anything beyond `propext`,
`Classical.choice`, and `Quot.sound`; `scripts/check.py` scans the source text
for what the kernel cannot see, including files that are never compiled.
-/