The Complete SU(N) Index Argument

Exact root statement

∀ {Volume : Type u} {Regime : Type v} (system : PeriodicIndexData Volume Regime ℝ) (colors : ℕ)
  (frame : Matrix (Fin colors) (Fin (colors - 1)) ℂ) (character : CartanFock.VacuumCharacter)
  (largeVolume : Filter Volume) (Hilbert : Type uHilbert) [inst : NormedAddCommGroup Hilbert]
  [inst_1 : InnerProductSpace ℂ Hilbert]
  (operators :
    (volume : Volume) →
      SpectralOperatorData (system.regulatedSpectralReadout (system.periodic volume)).spectrum Hilbert),
  system.PureN1SUTheory colors →
    system.PeriodicWeakCouplingReduction →
      system.PeriodicCartanGaugeConstraintData →
        system.PeriodicZeroModeFermionicData colors →
          CartanFock.IsSUCartanFrame frame →
            Submodule.span ℂ (Set.range (CartanFock.candidate (colors - 1) character)) =
                CartanFock.physicalSpace frame character →
              system.PhysicalCartanZeroModeTraceAt colors frame character →
                (∀ (volume : Volume),
                    system.SupersymmetricFiniteVolumeSetup (system.periodic volume) ∧
                      0 < (system.regulatedSpectralReadout (system.periodic volume)).regulator ∧
                        (system.regulatedSpectralReadout
                              (system.periodic volume)).spectrum.AllPositiveBetaTracesDefinedAt) →
                  system.IndexInvariantUnderAdmissibleDeformation →
                    system.EveryPeriodicVolumeConnectsToCalculation →
                      (∀ (volume : Volume), (operators volume).RepresentsSpectrumAt) →
                        (∀ (volume : Volume),
                            (operators volume).GroundEnergyInfimumAt
                              (system.groundStateEnergy (system.periodic volume))) →
                          system.CofinalPeriodicBoxGroundEnergyLimit largeVolume →
                            (∀ (volume : Volume),
                                ∃ states,
                                  (Orthonormal ℂ fun label => ↑(states label)) ∧
                                    (∀ (label : Fin colors),
                                        (operators volume).operators.energyData.NonvacuousUnbrokenChargeVacuumAt
                                          (states label)) ∧
                                      system.groundStateEnergy (system.periodic volume) = 0 ∧
                                        (operators volume).operators.energyData.AttainedGroundEnergyAt
                                          (system.groundStateEnergy (system.periodic volume))) ∧
                              system.infiniteVolumeGroundStateEnergyFor SpatialBoundaryCondition.periodic = 0 ∧
                                ¬system.InfiniteVolumeSupersymmetryBroken