Consequences of the quartic idempotence equation #
The nine-coordinate bridge is applied to an equation F * c = F, where
F is affine plus a Hankel target and c is affine plus a rational target.
Every summand except target times rational has degree at most three, so the
quartic equation is exactly the rational-annihilator probe.
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_eq_zero_of_mem_targetAmbient
{p : ANF 8}
(hp : p ∈ targetAmbient 8 (mulTarget 4))
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_affineANF
(a : F₂)
(ell : LinearForm)
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_targetANF
(c : TargetCoeff)
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_affine_mul_affine
(a b : F₂)
(ell m : LinearForm)
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_affine_mul_targetANF
(a : F₂)
(ell : LinearForm)
(c : TargetCoeff)
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_targetANF_mul_affine
(c : TargetCoeff)
(a : F₂)
(ell : LinearForm)
(k : Fin 9)
:
@[simp]
theorem
UnrestrictedBooleanMul.N4.anfQuarticAnnihilatorProbe_affine_mul_rationalANF
(a : F₂)
(ell : LinearForm)
(delta : Fin 3 → F₂)
(k : Fin 9)
:
theorem
UnrestrictedBooleanMul.N4.quartic_data_of_right_idempotence
{F c : ANF 8}
(hFAmbient : F ∈ targetAmbient 8 (mulTarget 4))
(hFNotLow : F ∉ rationalLowSpace)
(hcLow : c ∈ rationalLowSpace)
(hFc : F * c = F)
:
∃ (a : F₂) (b : F₂) (ell : LinearForm) (m : LinearForm) (C : TargetCoeff) (delta : Fin 3 → F₂),
F = affineANF a ell + targetANF C ∧ c = affineANF b m + rationalANF delta ∧ ¬IsRationalCoeff C ∧ VanishesOnQuarticAnnihilatorProbe C delta
Normal forms extracted from the right idempotence equation. The target
coefficient is nonrational because F lies outside the rational-low state,
and its quartic product with the rational part of c vanishes.