Documentation

LeanPool.BooleanMultiplication.N4.QuarticIdempotence

ANF bridge for the quartic idempotence equation #

Only the nine quartic coordinates used by the rational-annihilator certificate are projected. Their product formula is proved on the 7 × 3 target/rational basis and extended bilinearly. This avoids a dense representation of all 210 coordinates of Λ⁴(F₂⁸).

source
def UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe (p : ANF 8) (k : Fin 9) :
F₂

Extract a designated quartic-annihilator coefficient from an ANF.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbeLinear (k : Fin 9) :
    ANF 8 →ₗ[F₂] F₂

    One quartic-annihilator coefficient projection as a linear map.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbeLinear_apply (k : Fin 9) (p : ANF 8) :
      (anfQuarticAnnihilatorProbeLinear k) p = anfQuarticAnnihilatorProbe p k
      source
      @[simp]
      theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_add (p q : ANF 8) (k : Fin 9) :
      anfQuarticAnnihilatorProbe (p + q) k = anfQuarticAnnihilatorProbe p k + anfQuarticAnnihilatorProbe q k
      source
      @[simp]
      theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_smul (a : F₂) (p : ANF 8) (k : Fin 9) :
      anfQuarticAnnihilatorProbe (a • p) k = a • anfQuarticAnnihilatorProbe p k
      source
      def UnrestrictedBooleanMul.N4.quarticAnnihilatorSet (k : Fin 9) :
      Finset (Fin 8)

      The squarefree monomial underlying a quartic-annihilator coordinate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem UnrestrictedBooleanMul.N4.quarticAnnihilatorSet_card (k : Fin 9) :
        (quarticAnnihilatorSet k).card = 4
        source
        @[simp]
        theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_monomial (s : Finset (Fin 8)) (k : Fin 9) :
        anfQuarticAnnihilatorProbe (monomial s) k = if s = quarticAnnihilatorSet k then 1 else 0
        source
        theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_monomial_mul (s t : Finset (Fin 8)) (k : Fin 9) :
        anfQuarticAnnihilatorProbe (monomial s * monomial t) k = if s ∪ t = quarticAnnihilatorSet k then 1 else 0
        source
        theorem UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_target_mul_rational (c : TargetCoeff) (delta : Fin 3 → F₂) (k : Fin 9) :
        anfQuarticAnnihilatorProbe (targetANF c * rationalANF delta) k = quarticAnnihilatorCoeffProbe c delta k