GQ2.lean

/-
Copyright (c) 2026 David Roe. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Roe, roed@mit.edu, using Claude Opus-4.8 and Fable-5
-/
import GQ2.Sanity
import GQ2.Words
import GQ2.Omega2
import GQ2.AppendixB
import GQ2.Zhat
import GQ2.DiscreteModule
import GQ2.Cohomology
import GQ2.CupProduct
import GQ2.CupSymmetry
import GQ2.FreeProfinite
import GQ2.ProfiniteQuotient
import GQ2.ProfinitePresentation
import GQ2.Tame
import GQ2.FiniteGroupLemmas
import GQ2.Subdirect
import GQ2.Reconstruction
import GQ2.Statement
import GQ2.GammaA
import GQ2.Foundations
import GQ2.Foundations.Axioms
import GQ2.Foundations.Interfaces
import GQ2.EulerCharacteristic
import GQ2.MaxProP
import GQ2.Demushkin
import GQ2.HilbertSymbol
import GQ2.DyadicSquares
import GQ2.HilbertSymbolDyadic
import GQ2.HilbertSymbolNecessity
import GQ2.HilbertSymbolSufficiency
import GQ2.HilbertSymbolDyadicClose
import GQ2.Kummer
import GQ2.Reciprocity
import GQ2.MuN
import GQ2.TateDuality
import GQ2.EvensKahn
import GQ2.KummerSurjectivity
import GQ2.Orientation
import GQ2.FinitelyGenerated
import GQ2.BoundaryFrame
import GQ2.TameQuotient
import GQ2.SectionThree
import GQ2.Prop32
import GQ2.TameTwoQuotient
import GQ2.TameOrientationWitness
import GQ2.SectionThreeMarked
import GQ2.AdmissibleLimit
import GQ2.Prop23
import GQ2.FoxHeisenberg
import GQ2.FoxHeisenberg.Basic
import GQ2.FoxHeisenberg.Heisenberg
import GQ2.FoxHeisenberg.Traced
import GQ2.FoxHeisenberg.WildRow
import GQ2.FoxHeisenberg.HessianRow
import GQ2.Devissage
import GQ2.Devissage.Naturality
import GQ2.Devissage.ElemDualPack
import GQ2.Devissage.EvalPairings
import GQ2.Devissage.Chi1
import GQ2.Devissage.SelfDual
import GQ2.Devissage.LESCore
import GQ2.Devissage.LESExact
import GQ2.Devissage.LESMaster
import GQ2.Devissage.GeneratesBridge
import GQ2.QuadraticFp2
import GQ2.GaussCount
import GQ2.GaussSigns
import GQ2.GaussSignsRamified
import GQ2.TameSimple
import GQ2.Corestriction
import GQ2.OrbitData
import GQ2.Block.Module
import GQ2.SectionSix
import GQ2.HilbertLedger
import GQ2.Transgression
import GQ2.LocalLiftingDuality
import GQ2.SectionSeven
import GQ2.SectionSeven.Basic
import GQ2.SectionSeven.Decorations
import GQ2.SectionSeven.Prop74Step1
import GQ2.SectionSeven.ModuleCore
import GQ2.SectionSeven.Prop74
import GQ2.SectionEight
import GQ2.SectionEight.Fourier
import GQ2.SectionEight.Covers
import GQ2.SectionEight.ScalarCount
import GQ2.SectionEight.Partition
import GQ2.SectionEight.Recursion
import GQ2.AffineTLift
import GQ2.VCocycle
import GQ2.RadicalEdge.Bridge
import GQ2.Phase140.Obstruction
import GQ2.VLiftCount
import GQ2.KeystoneDelta
import GQ2.KeystoneDelta.AtomCalculus
import GQ2.KeystoneDelta.ThetaExtraction
import GQ2.KeystoneDelta.AffineAssembly
import GQ2.KeystoneDelta.Keystone
import GQ2.GaussZ.Reduction
import GQ2.GaussZ.Local
import GQ2.Shapiro.Deepness
import GQ2.Phase140.Assembly
import GQ2.Prop89Close
import GQ2.MStageCount
import GQ2.MStageCountGammaA
import GQ2.MStageCountGammaR
import GQ2.SectionNine
import GQ2.Block.Enrichment
import GQ2.Block.HeadDat
import GQ2.GaussZ.FinalD
import GQ2.SourceData
import GQ2.ThmFourTwo
import GQ2.DeepPart
import GQ2.DeepPart.QuadraticFp2
import GQ2.DeepPart.MuTwoPolarDual
import GQ2.DeepPart.Q0locLayer
import GQ2.DeepPart.HermitianCount
import GQ2.LocalKummer
import GQ2.RegularSummand
import GQ2.KappaNormalForm
import GQ2.HomCounting
import GQ2.UnitFiltration
import GQ2.UnitFiltrationTop
import GQ2.KummerFiltration
import GQ2.AdmissibleCount
import GQ2.DeepDuality
import GQ2.DeepDualityK
import GQ2.DeepCount
import GQ2.UnramifiedNorm
import GQ2.GaloisCosetNorm
import GQ2.UnitNormIndex
import GQ2.DimAssembly
import GQ2.DimClose
import GQ2.ResidueLift
import GQ2.UnramifiedBridge
import GQ2.CorestrictionCohomology
import GQ2.OrbitVanish
import GQ2.RegularIsometry
import GQ2.OrbitDecomp
import GQ2.Shapiro.Read
import GQ2.VanishClose
import GQ2.DetRamified
import GQ2.PropOneOne
import GQ2.ZtwoPowering
import GQ2.FrattiniCriterion
import GQ2.AnabelianBridge
import GQ2.PropOneOneAssembly
import GQ2.Shapiro.Ledger
import GQ2.WordCohBridge
import GQ2.RadicalEdge.GammaA
import GQ2.SectionTen
import GQ2.SectionTenSources
import GQ2.PresentationLiteral
import GQ2.RStage.GammaA
import GQ2.CardH2GammaA
import GQ2.Phase140.GammaA
import GQ2.QuadraticAdjoin
import GQ2.InvolutionVanish
import GQ2.InvolutionSplice
import GQ2.GaussZ.Final
import GQ2.GaussZ.CoordGammaA
import GQ2.IotaBridge
import GQ2.IotaGammaA
import GQ2.GaussZ.RelatorGammaA
import GQ2.GaussZ.FinalGammaA
import GQ2.GaussZ.GammaAD
import GQ2.RamifiedPack
import GQ2.UnramifiedQuadraticNorms
import GQ2.UnitFiltrationCounts
-- Roe-candidate verification (GQ2/Roe/, see docs/orchestration/roe-verification-plan.md)
import GQ2.Roe.Words
import GQ2.Roe.GammaR
import GQ2.Roe.AdmissibleLimit
import GQ2.Roe.Tame
import GQ2.Roe.Prop23
import GQ2.Roe.Stokes
import GQ2.Roe.OrientationRoot
import GQ2.Roe.Sanity
import GQ2.Roe.DRPresentation
import GQ2.Roe.DRAbelianization
import GQ2.Roe.CrossedDerivation
import GQ2.Roe.DRWordCoh
import GQ2.Roe.DRDemushkin
import GQ2.Roe.MarkedMatching
import GQ2.Roe.MarkedPro2
import GQ2.Roe.MaxPro2Bridge
import GQ2.Roe.FoxBasic
import GQ2.Roe.WildRow
import GQ2.Roe.NormalForms
import GQ2.Roe.Hessian
import GQ2.Roe.ChiR
import GQ2.Roe.Labute.TwoCentralTower
import GQ2.Roe.Labute.Levelwise
import GQ2.Roe.Labute.SpanFoundation
import GQ2.Roe.Labute.GradedLie.SpanIdentities
import GQ2.Roe.Labute.GradedLie.SpanStep
import GQ2.Roe.Labute.GradedLie.SpanBase
import GQ2.Roe.Labute.GradedLie.SpanAssembly
import GQ2.Roe.Labute.GradedLie.Magnus
import GQ2.Roe.Labute.StageLemma.Congruence
import GQ2.Roe.Labute.StageLemma.Defect
import GQ2.Roe.Labute.StageLemma.DigitToolkit
import GQ2.Roe.Labute.StageLemma.CrossedDerivation
import GQ2.Roe.Labute.StageLemma.StageOne
import GQ2.Roe.Labute.StageLemma.StageTwo
import GQ2.Roe.Labute.StageLemma
import GQ2.Roe.Labute.Assembly
import GQ2.Roe.Gauss
import GQ2.Roe.TrivialSelfDual
import GQ2.Roe.Devissage.TracedRows
import GQ2.Roe.Devissage.Naturality
import GQ2.Roe.Devissage.EvalPairings
import GQ2.Roe.Devissage.Chi1
import GQ2.Roe.Devissage.SelfDual
import GQ2.Roe.Devissage.LESCore
import GQ2.Roe.Devissage.LESExact
import GQ2.Roe.Devissage.LESMaster
import GQ2.Roe.Devissage.GeneratesBridge
import GQ2.Roe.Devissage
import GQ2.Roe.DevissageInduction
import GQ2.Roe.DualityAssembly
import GQ2.Roe.Supply
import GQ2.RStage.GammaR
import GQ2.WordCohBridgeR
import GQ2.Roe.CorrectionR
import GQ2.Roe.CoverLiftR
import GQ2.WordCoh2R
import GQ2.MixedBObsR
import GQ2.IotaGammaR
import GQ2.LedgerGammaR
import GQ2.HalfTorsorGammaR
import GQ2.Phase140.GammaR
import GQ2.GaussZ.KappaR
import GQ2.GaussZ.RelatorGammaR
import GQ2.GaussZ.CoordGammaR
import GQ2.GaussZ.GammaRD
import GQ2.Roe.Main