Three-term tail geometry at a rational anchor

After wedging by the zero-place form a₀ ∧ b₀, only the six tail variables remain. This file gives that quotient its own small coordinate model. The rank-one classification is proved from minors, so the annihilator argument does not enumerate the 128 target words or build a large exterior basis.

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.TailCoeff : Type

The five product coefficient coordinates of the three-term tail.

Equations

• UnrestrictedBooleanMul.N4.TailCoeff = (Fin 5 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.TailLinear : Type

The six linear input coordinates of the three-term tail.

Equations

• UnrestrictedBooleanMul.N4.TailLinear = (Fin 6 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.TailTwo : Type

Two-index coordinate arrays for exterior forms on the six tail inputs.

Equations

• UnrestrictedBooleanMul.N4.TailTwo = (Fin 6 → Fin 6 → UnrestrictedBooleanMul.F₂)

def UnrestrictedBooleanMul.N4.tailACoord (i : Fin 3) : Fin 6

Coordinate of a coefficient of the first tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailACoord i = ⟨↑i, ⋯⟩

def UnrestrictedBooleanMul.N4.tailBCoord (i : Fin 3) : Fin 6

Coordinate of a coefficient of the second tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailBCoord i = ⟨3 + ↑i, ⋯⟩

def UnrestrictedBooleanMul.N4.tailHankelMatrix (c : TailCoeff) : Matrix (Fin 3) (Fin 3) F₂

The three-by-three Hankel matrix of the five tail coefficients.

Equations

• UnrestrictedBooleanMul.N4.tailHankelMatrix c i j = c ⟨↑i + ↑j, ⋯⟩

def UnrestrictedBooleanMul.N4.TailHankelRankLEOne (c : TailCoeff) : Prop

Every two-by-two minor of the tail Hankel matrix vanishes.

Equations

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

def UnrestrictedBooleanMul.N4.tailZeroCoeff : TailCoeff

The tail coefficient vector for evaluation at zero.

Equations

• UnrestrictedBooleanMul.N4.tailZeroCoeff = ![1, 0, 0, 0, 0]

def UnrestrictedBooleanMul.N4.tailOneCoeff : TailCoeff

The tail coefficient vector for evaluation at one.

Equations

• UnrestrictedBooleanMul.N4.tailOneCoeff = ![1, 1, 1, 1, 1]

def UnrestrictedBooleanMul.N4.tailInfinityCoeff : TailCoeff

The tail coefficient vector for evaluation at infinity.

Equations

• UnrestrictedBooleanMul.N4.tailInfinityCoeff = ![0, 0, 0, 0, 1]

theorem UnrestrictedBooleanMul.N4.tail_rankOne_classification {c : TailCoeff} (h : TailHankelRankLEOne c) (hc : c ≠ 0) : c = tailZeroCoeff ∨ c = tailOneCoeff ∨ c = tailInfinityCoeff

The nonzero rank-one 3 × 3 Hankel tails are the three rational places.

def UnrestrictedBooleanMul.N4.tailTargetTwo (c : TailCoeff) : TailTwo

The alternating two-form whose mixed block is the tail Hankel matrix.

Equations

• UnrestrictedBooleanMul.N4.tailTargetTwo c i j = if hi : ↑i < 3 then if hj : 3 ≤ ↑j then c ⟨↑i + (↑j - 3), ⋯⟩ else 0 else if hj : ↑j < 3 then c ⟨↑j + (↑i - 3), ⋯⟩ else 0

def UnrestrictedBooleanMul.N4.tailAPart (u : TailLinear) : Fin 3 → F₂

Restrict a tail linear form to the first polynomial input.

Equations

• UnrestrictedBooleanMul.N4.tailAPart u i = u (UnrestrictedBooleanMul.N4.tailACoord i)

def UnrestrictedBooleanMul.N4.tailBPart (u : TailLinear) : Fin 3 → F₂

Restrict a tail linear form to the second polynomial input.

Equations

• UnrestrictedBooleanMul.N4.tailBPart u i = u (UnrestrictedBooleanMul.N4.tailBCoord i)

def UnrestrictedBooleanMul.N4.IsDecomposableTailTarget (c : TailCoeff) : Prop

The tail target is a mixed exterior product with both same-input blocks zero.

Equations

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

theorem UnrestrictedBooleanMul.N4.decomposableTailTarget_rankOne {c : TailCoeff} (h : IsDecomposableTailTarget c) : TailHankelRankLEOne c

theorem UnrestrictedBooleanMul.N4.decomposableTailTarget_classification {c : TailCoeff} (h : IsDecomposableTailTarget c) (hc : c ≠ 0) : c = tailZeroCoeff ∨ c = tailOneCoeff ∨ c = tailInfinityCoeff

def UnrestrictedBooleanMul.N4.tailEmbed : Fin 6 → Fin 8

Quotient coordinates obtained by deleting the anchor variables a₀,b₀.

Equations

• UnrestrictedBooleanMul.N4.tailEmbed = ![1, 2, 3, 5, 6, 7]

def UnrestrictedBooleanMul.N4.tailVectorOf (M : LinearForm) : TailLinear

Restrict an eight-variable linear form to the six tail inputs.

Equations

• UnrestrictedBooleanMul.N4.tailVectorOf M i = M (UnrestrictedBooleanMul.N4.tailEmbed i)

def UnrestrictedBooleanMul.N4.tailCoeffOf (c : TargetCoeff) : TailCoeff

Drop the first two coefficients of a four-term product target.

Equations

• UnrestrictedBooleanMul.N4.tailCoeffOf c i = c ⟨↑i + 2, ⋯⟩

theorem UnrestrictedBooleanMul.N4.tailTargetOf_apply (c : TargetCoeff) (i j : Fin 6) : targetTwo c (tailEmbed i) (tailEmbed j) = tailTargetTwo (tailCoeffOf c) i j

theorem UnrestrictedBooleanMul.N4.anchoredAnnihilator_tailEquation (M : LinearForm) (c : TargetCoeff) (hc : c ∈ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))) : vectorWedgeTwoN (tailVectorOf M) (tailTargetTwo (tailCoeffOf c)) = 0

The five-form annihilator equation descends to the three-form equation on the six-dimensional tail quotient.

theorem UnrestrictedBooleanMul.N4.tailVector_ne_zero_of_anchored_ne_zero (M : LinearForm) (hM : vectorWedgeTwo M (rationalPlaceTwo 0) ≠ 0) : tailVectorOf M ≠ 0

theorem UnrestrictedBooleanMul.N4.tailTarget_decomposable_of_annihilates (u : TailLinear) (c : TailCoeff) (hu : u ≠ 0) (h : vectorWedgeTwoN u (tailTargetTwo c) = 0) : IsDecomposableTailTarget c

theorem UnrestrictedBooleanMul.N4.anchored_annihilator_tail_classification (M : LinearForm) (hM : vectorWedgeTwo M (rationalPlaceTwo 0) ≠ 0) (c : TargetCoeff) (hc : c ∈ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))) : tailCoeffOf c = 0 ∨ tailCoeffOf c = tailZeroCoeff ∨ tailCoeffOf c = tailOneCoeff ∨ tailCoeffOf c = tailInfinityCoeff

Exterior core of the tail-place table: after quotienting by the two baseline annihilators, the only possible nonzero annihilator directions are the three rank-one three-term places.

def UnrestrictedBooleanMul.N4.tailZeroA : TailLinear

Evaluation at zero on the first tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailZeroA = ![1, 0, 0, 0, 0, 0]

def UnrestrictedBooleanMul.N4.tailZeroB : TailLinear

Evaluation at zero on the second tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailZeroB = ![0, 0, 0, 1, 0, 0]

def UnrestrictedBooleanMul.N4.tailInfinityA : TailLinear

Evaluation at infinity on the first tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailInfinityA = ![0, 0, 1, 0, 0, 0]

def UnrestrictedBooleanMul.N4.tailInfinityB : TailLinear

Evaluation at infinity on the second tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailInfinityB = ![0, 0, 0, 0, 0, 1]

def UnrestrictedBooleanMul.N4.tailOneA : TailLinear

Evaluation at one on the first tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailOneA = ![1, 1, 1, 0, 0, 0]

def UnrestrictedBooleanMul.N4.tailOneB : TailLinear

Evaluation at one on the second tail polynomial.

Equations

• UnrestrictedBooleanMul.N4.tailOneB = ![0, 0, 0, 1, 1, 1]

def UnrestrictedBooleanMul.N4.InTailPlane (u a b : TailLinear) : Prop

Membership in the span of two specified tail linear forms.

Equations

• UnrestrictedBooleanMul.N4.InTailPlane u a b = ∃ (α : UnrestrictedBooleanMul.F₂) (β : UnrestrictedBooleanMul.F₂), u = α • a + β • b

@[simp]

theorem UnrestrictedBooleanMul.N4.tailTargetTwo_zero_place : tailTargetTwo tailZeroCoeff = vectorWedgeN tailZeroA tailZeroB

@[simp]

theorem UnrestrictedBooleanMul.N4.tailTargetTwo_infinity_place : tailTargetTwo tailInfinityCoeff = vectorWedgeN tailInfinityA tailInfinityB

@[simp]

theorem UnrestrictedBooleanMul.N4.tailTargetTwo_one_place : tailTargetTwo tailOneCoeff = vectorWedgeN tailOneA tailOneB

theorem UnrestrictedBooleanMul.N4.tailVector_mem_zeroPlane_of_wedge (u : TailLinear) (h : vectorWedgeTwoN u (tailTargetTwo tailZeroCoeff) = 0) : InTailPlane u tailZeroA tailZeroB

theorem UnrestrictedBooleanMul.N4.tailVector_mem_infinityPlane_of_wedge (u : TailLinear) (h : vectorWedgeTwoN u (tailTargetTwo tailInfinityCoeff) = 0) : InTailPlane u tailInfinityA tailInfinityB

theorem UnrestrictedBooleanMul.N4.tailVector_mem_onePlane_of_wedge (u : TailLinear) (h : vectorWedgeTwoN u (tailTargetTwo tailOneCoeff) = 0) : InTailPlane u tailOneA tailOneB

theorem UnrestrictedBooleanMul.N4.anchored_annihilator_tail_table (M : LinearForm) (hM : vectorWedgeTwo M (rationalPlaceTwo 0) ≠ 0) (c : TargetCoeff) (hc : c ∈ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))) : tailCoeffOf c = 0 ∨ tailCoeffOf c = tailZeroCoeff ∧ InTailPlane (tailVectorOf M) tailZeroA tailZeroB ∨ tailCoeffOf c = tailOneCoeff ∧ InTailPlane (tailVectorOf M) tailOneA tailOneB ∨ tailCoeffOf c = tailInfinityCoeff ∧ InTailPlane (tailVectorOf M) tailInfinityA tailInfinityB

Full tail-place incidence table, stated in quotient coordinates.