Documentation

LeanPool.ConnesRigidity.Foundation.LinearAlgebra.ArithmeticSymplectic

The arithmetic symplectic component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.OpenAIPort.SymplecticIndex :
Type

The SymplecticIndex construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.OpenAIPort.IntegralLattice :
    Type

    The IntegralLattice construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Connes.OpenAIPort.ModTwoSpace :
      Type

      The ModTwoSpace construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Connes.OpenAIPort.IntegralSymplecticGroup :
        Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) ℤ)

        The IntegralSymplecticGroup construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          instance Connes.OpenAIPort.instCountableSubtypeMatrixSumFinOfNatNatIntMemSubmonoidIntegralSymplecticGroup :
          Countable ↥IntegralSymplecticGroup
          source
          @[instance_reducible]
          instance Connes.OpenAIPort.instDistribMulActionSubtypeMatrixSumFinOfNatNatIntMemSubmonoidIntegralSymplecticGroupIntegralLattice :
          DistribMulAction (↥IntegralSymplecticGroup) IntegralLattice
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def Connes.OpenAIPort.reducedMatrixHom :
          ↥IntegralSymplecticGroup →* Matrix SymplecticIndex SymplecticIndex (ZMod 2)

          The reducedMatrixHom construction used in the Connes rigidity formalization.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Connes.OpenAIPort.instDistribMulActionSubtypeMatrixSumFinOfNatNatIntMemSubmonoidIntegralSymplecticGroupModTwoSpace :
            DistribMulAction (↥IntegralSymplecticGroup) ModTwoSpace
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def Connes.OpenAIPort.reduceVector :
            IntegralLattice →+ ModTwoSpace

            Coordinatewise reduction. Paper: §2.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Connes.OpenAIPort.reduceVector_apply (v : IntegralLattice) (i : SymplecticIndex) :
              reduceVector v i = ↑(v i)

              Evaluation of coordinatewise reduction. Paper: §2.

              source
              def Connes.OpenAIPort.liftVector (w : ModTwoSpace) :
              IntegralLattice

              The liftVector construction used in the Connes rigidity formalization.

              Equations
              Instances For
                source
                @[simp]
                theorem Connes.OpenAIPort.reduceVector_liftVector (w : ModTwoSpace) :
                reduceVector (liftVector w) = w

                Reduction recovers the canonical lift. Paper: §2.

                source
                @[simp]
                theorem Connes.OpenAIPort.liftVector_zero :
                liftVector 0 = 0
                source
                theorem Connes.OpenAIPort.reduceVector_smul (g : ↥IntegralSymplecticGroup) (v : IntegralLattice) :
                reduceVector (g • v) = g • reduceVector v
                source
                theorem Connes.OpenAIPort.modTwoSpace_exponent_two (w : ModTwoSpace) :
                2 • w = 0
                source
                theorem Connes.OpenAIPort.exists_half_of_reduceVector_eq_zero (v : IntegralLattice) (hv : reduceVector v = 0) :
                ∃ (u : IntegralLattice), 2 • u = v
                source
                theorem Connes.OpenAIPort.two_nsmul_integralLattice_injective :
                Function.Injective fun (v : IntegralLattice) => 2 • v
                source
                def Connes.OpenAIPort.modTwoSymplecticForm (x y : ModTwoSpace) :
                ZMod 2

                The modTwoSymplecticForm construction used in the Connes rigidity formalization.

                Equations
                Instances For
                  source
                  def Connes.OpenAIPort.standardQuadraticForm (x : ModTwoSpace) :
                  ZMod 2

                  The standard quadratic refinement. Paper: §2.

                  Equations
                  Instances For
                    source
                    theorem Connes.OpenAIPort.standardQuadraticForm_add (x y : ModTwoSpace) :
                    standardQuadraticForm (x + y) = standardQuadraticForm x + standardQuadraticForm y + modTwoSymplecticForm x y