Documentation

LeanPool.BooleanMultiplication.N4.SliceGeometry

Exterior geometry for the zero-place slice argument #

The quartic exclusion leaves two six-variable complementary quadratic geometries. The type-A form is decomposable and its linear annihilator is exactly its two-dimensional support. The type-B form has alternating rank four and therefore has no nonzero linear annihilator. Everything below is proved from fixed exterior coordinates; no circuits or truth tables are enumerated.

source
noncomputable def UnrestrictedBooleanMul.N4.sliceX :
LinearForm

The two anchor variables used to slice the Boolean identities.

Equations
Instances For
    source
    noncomputable def UnrestrictedBooleanMul.N4.sliceY :
    LinearForm

    The second polynomial constant coefficient, used as a slice anchor.

    Equations
    Instances For
      source
      noncomputable def UnrestrictedBooleanMul.N4.sliceU :
      LinearForm

      The first complementary target directions.

      Equations
      Instances For
        source
        noncomputable def UnrestrictedBooleanMul.N4.sliceV :
        LinearForm

        The second polynomial linear coefficient, complementary to its slice anchor.

        Equations
        Instances For
          source
          def UnrestrictedBooleanMul.N4.sliceABar :
          LinearForm

          Sums of the three variables complementary to the zero place.

          Equations
          Instances For
            source
            def UnrestrictedBooleanMul.N4.sliceBBar :
            LinearForm

            The sum of the three second-polynomial input variables away from the zero-place anchor.

            Equations
            Instances For
              source
              def UnrestrictedBooleanMul.N4.sliceQuadraticA :
              TwoForm

              Type A complementary quadratic part.

              Equations
              Instances For
                source
                def UnrestrictedBooleanMul.N4.sliceInfinityQuadratic :
                TwoForm

                The extra infinity-place term producing type B.

                Equations
                Instances For
                  source
                  def UnrestrictedBooleanMul.N4.sliceQuadraticB :
                  TwoForm

                  Type B complementary quadratic part.

                  Equations
                  Instances For
                    source
                    def UnrestrictedBooleanMul.N4.InSliceComplementPlane (ell : LinearForm) :
                    Prop

                    The plane spanned by the complementary evaluation-at-one input directions.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[instance_reducible]
                      instance UnrestrictedBooleanMul.N4.instDecidableInSliceComplementPlane (ell : LinearForm) :
                      Decidable (InSliceComplementPlane ell)
                      Equations
                      source
                      theorem UnrestrictedBooleanMul.N4.sliceQuadraticA_ne_zero :
                      sliceQuadraticA ≠ 0
                      source
                      theorem UnrestrictedBooleanMul.N4.sliceQuadraticA_annihilator {ell : LinearForm} (h : vectorWedgeTwo ell sliceQuadraticA = 0) :
                      InSliceComplementPlane ell

                      The annihilator of the decomposable type-A quadratic is its support plane.

                      source
                      theorem UnrestrictedBooleanMul.N4.sliceQuadraticB_annihilator {ell : LinearForm} (h : vectorWedgeTwo ell sliceQuadraticB = 0) :
                      ell = 0

                      The type-B form has alternating rank four. The selected triples expose two independent cross blocks and force every coordinate of an annihilating linear form to vanish.

                      source
                      theorem UnrestrictedBooleanMul.N4.sliceU_not_in_complement_plane :
                      ¬InSliceComplementPlane sliceU
                      source
                      theorem UnrestrictedBooleanMul.N4.sliceV_not_in_complement_plane :
                      ¬InSliceComplementPlane sliceV
                      source
                      theorem UnrestrictedBooleanMul.N4.sliceUV_combination_not_in_complement_plane (a b : F₂) (hne : a ≠ 0 ∨ b ≠ 0) :
                      ¬InSliceComplementPlane (a • sliceU + b • sliceV)

                      A nonzero combination of the two target difference directions cannot lie in the type-A support plane.