Algebraic alignment of two quartic factor bases

Equality of two nonzero rational quartic wedges says that the two ordered quadratic pairs are bases of the same plane. The explicit inverse minor below produces the basis-change coefficients. Applying the same change to the affine and linear parts preserves the cubic projection; its quadratic projection changes only by an explicitly rational form.

def UnrestrictedBooleanMul.N4.basisChangeP (β γ : Fin 3 → F₂) (i j : Fin 3) : F₂

The minor computing the first coefficient in a rational-plane basis change.

Equations

• UnrestrictedBooleanMul.N4.basisChangeP β γ i j = γ i * β j + γ j * β i

def UnrestrictedBooleanMul.N4.basisChangeQ (α γ : Fin 3 → F₂) (i j : Fin 3) : F₂

The minor computing the second coefficient in a rational-plane basis change.

Equations

• UnrestrictedBooleanMul.N4.basisChangeQ α γ i j = α i * γ j + α j * γ i

def UnrestrictedBooleanMul.N4.coeffCombination (p q : F₂) (α β : Fin 3 → F₂) : Fin 3 → F₂

A two-term linear combination of rational-place coefficient vectors.

Equations

• UnrestrictedBooleanMul.N4.coeffCombination p q α β = p • α + q • β

def UnrestrictedBooleanMul.N4.SameRationalMinors (α β γ δ : Fin 3 → F₂) : Prop

The two pairs of rational coefficient vectors have the same three exterior minors.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableSameRationalMinors (α β γ δ : Fin 3 → F₂) : Decidable (SameRationalMinors α β γ δ)

Equations

• UnrestrictedBooleanMul.N4.instDecidableSameRationalMinors α β γ δ = id inferInstance

theorem UnrestrictedBooleanMul.N4.rationalTwo_coeffCombination (p q : F₂) (α β : Fin 3 → F₂) : rationalTwo (coeffCombination p q α β) = p • rationalTwo α + q • rationalTwo β

theorem UnrestrictedBooleanMul.N4.rational_basis_change_certificate (α β γ δ : Fin 3 → F₂) (pair : Fin 3) (hminor : rationalCoeffMinor α β (quarticSupportPair pair).1 (quarticSupportPair pair).2 = 1) (hsame : SameRationalMinors α β γ δ) : have i := (quarticSupportPair pair).1; have j := (quarticSupportPair pair).2; have p := basisChangeP β γ i j; have q := basisChangeQ α γ i j; have r := basisChangeP β δ i j; have s := basisChangeQ α δ i j; γ = coeffCombination p q α β ∧ δ = coeffCombination r s α β ∧ p * s + q * r = 1

theorem UnrestrictedBooleanMul.N4.same_rational_minors_of_wedge_eq (α β γ δ : Fin 3 → F₂) (h : wedgeTwo (rationalTwo α) (rationalTwo β) = wedgeTwo (rationalTwo γ) (rationalTwo δ)) : SameRationalMinors α β γ δ

def UnrestrictedBooleanMul.N4.changedFirstLinear (s q : F₂) (ell m : LinearForm) : LinearForm

The first linear factor after applying the inverse two-dimensional basis change.

Equations

• UnrestrictedBooleanMul.N4.changedFirstLinear s q ell m = s • ell + q • m

def UnrestrictedBooleanMul.N4.changedSecondLinear (r p : F₂) (ell m : LinearForm) : LinearForm

The second linear factor after applying the inverse two-dimensional basis change.

Equations

• UnrestrictedBooleanMul.N4.changedSecondLinear r p ell m = r • ell + p • m

def UnrestrictedBooleanMul.N4.basisChangeEta (p q r s : F₂) (γ δ : Fin 3 → F₂) : Fin 3 → F₂

The rational correction arising in the quadratic part of a basis change.

Equations

• UnrestrictedBooleanMul.N4.basisChangeEta p q r s γ δ = (s * r) • γ + (q * p) • δ

theorem UnrestrictedBooleanMul.N4.rationalProductCubic_basis_change (α β γ δ : Fin 3 → F₂) (p q r s : F₂) (ell m : LinearForm) (hγ : γ = coeffCombination p q α β) (hδ : δ = coeffCombination r s α β) : rationalProductCubic ell m γ δ = rationalProductCubic (changedFirstLinear s q ell m) (changedSecondLinear r p ell m) α β

theorem UnrestrictedBooleanMul.N4.rationalProductQuadratic_basis_change (α β γ δ : Fin 3 → F₂) (p q r s a b : F₂) (ell m : LinearForm) (hγ : γ = coeffCombination p q α β) (hδ : δ = coeffCombination r s α β) (hdet : p * s + q * r = 1) : rationalProductQuadratic a b ell m γ δ = rationalTwo (basisChangeEta p q r s γ δ) + rationalProductQuadratic (s * a + q * b) (r * a + p * b) (changedFirstLinear s q ell m) (changedSecondLinear r p ell m) α β

theorem UnrestrictedBooleanMul.N4.lowLow_quartic_collision_target_is_rational (α β γ δ : Fin 3 → F₂) (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) ≠ 0) (hquarticEq : wedgeTwo (rationalTwo α) (rationalTwo β) = wedgeTwo (rationalTwo γ) (rationalTwo δ)) (hcubic : rationalProductCubic ell₀ m₀ α β = rationalProductCubic ell₁ m₁ γ δ) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ α β + rationalProductQuadratic a₁ b₁ ell₁ m₁ γ δ) : IsRationalCoeff t

Arbitrary low--low collision with the same nonzero quartic part has only a rational target quadratic shadow.