First-jet separation

This is the coordinate-linear heart of the manuscript's jet-separation lemma. Modulo the feedback state S = ⟨E₀,E₁,E₆,r₁⟩, a target has only three coordinates A E₂ + B E₃ + C E₄. One outside--outside coefficient kills C; the four remaining outside slices force A = B = 0 unless the auxiliary two-plane is exactly the anchor plane.

def UnrestrictedBooleanMul.N4.anchorPlane : Submodule F₂ LinearForm

The plane spanned by the constant-coefficient inputs of the two polynomials.

Equations

• UnrestrictedBooleanMul.N4.anchorPlane = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range ![UnrestrictedBooleanMul.N4.aLinear 0, UnrestrictedBooleanMul.N4.bLinear 0])

def UnrestrictedBooleanMul.N4.feedbackCoeffSpace : Submodule F₂ TargetCoeff

The target subspace spanned by the first two coefficients, the last, and evaluation at one.

Equations

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

def UnrestrictedBooleanMul.N4.jetA (c : TargetCoeff) : F₂

The second coefficient relative to the evaluation-at-one component.

Equations

• UnrestrictedBooleanMul.N4.jetA c = c 2 + c 5

def UnrestrictedBooleanMul.N4.jetB (c : TargetCoeff) : F₂

The third coefficient relative to the evaluation-at-one component.

Equations

• UnrestrictedBooleanMul.N4.jetB c = c 3 + c 5

def UnrestrictedBooleanMul.N4.jetC (c : TargetCoeff) : F₂

The fourth coefficient relative to the evaluation-at-one component.

Equations

• UnrestrictedBooleanMul.N4.jetC c = c 4 + c 5

noncomputable def UnrestrictedBooleanMul.N4.feedbackBasePart (c : TargetCoeff) : TargetCoeff

The feedback-subspace component in the chosen target decomposition.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.jetResidualCoeff (c : TargetCoeff) : TargetCoeff

The three remaining target coordinates after removing the feedback component.

Equations

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

theorem UnrestrictedBooleanMul.N4.feedback_decomposition (c : TargetCoeff) : c = feedbackBasePart c + jetResidualCoeff c

theorem UnrestrictedBooleanMul.N4.feedbackBasePart_mem (c : TargetCoeff) : feedbackBasePart c ∈ feedbackCoeffSpace

theorem UnrestrictedBooleanMul.N4.anchorPlane_linearIndependent : LinearIndependent F₂ ![aLinear 0, bLinear 0]

theorem UnrestrictedBooleanMul.N4.anchorPlane_finrank : Module.finrank F₂ ↥anchorPlane = 2

theorem UnrestrictedBooleanMul.N4.anchorPlane_le_of_generators_mem {U : Submodule F₂ LinearForm} (hx : aLinear 0 ∈ U) (hy : bLinear 0 ∈ U) : anchorPlane ≤ U

theorem UnrestrictedBooleanMul.N4.submodule_eq_anchorPlane_of_generators_mem {U : Submodule F₂ LinearForm} (hUdim : Module.finrank F₂ ↥U ≤ 2) (hx : aLinear 0 ∈ U) (hy : bLinear 0 ∈ U) : U = anchorPlane

noncomputable def UnrestrictedBooleanMul.N4.jetSliceA2 (c : TargetCoeff) : LinearForm

The second first-input slice of the residual jet coefficients.

Equations

• UnrestrictedBooleanMul.N4.jetSliceA2 c = UnrestrictedBooleanMul.N4.jetA c • UnrestrictedBooleanMul.N4.bLinear 0 + UnrestrictedBooleanMul.N4.jetB c • UnrestrictedBooleanMul.N4.bLinear 1

noncomputable def UnrestrictedBooleanMul.N4.jetSliceA3 (c : TargetCoeff) : LinearForm

The third first-input slice of the residual jet coefficients.

Equations

• UnrestrictedBooleanMul.N4.jetSliceA3 c = UnrestrictedBooleanMul.N4.jetB c • UnrestrictedBooleanMul.N4.bLinear 0

noncomputable def UnrestrictedBooleanMul.N4.jetSliceB2 (c : TargetCoeff) : LinearForm

The second second-input slice of the residual jet coefficients.

Equations

• UnrestrictedBooleanMul.N4.jetSliceB2 c = UnrestrictedBooleanMul.N4.jetA c • UnrestrictedBooleanMul.N4.aLinear 0 + UnrestrictedBooleanMul.N4.jetB c • UnrestrictedBooleanMul.N4.aLinear 1

noncomputable def UnrestrictedBooleanMul.N4.jetSliceB3 (c : TargetCoeff) : LinearForm

The third second-input slice of the residual jet coefficients.

Equations

• UnrestrictedBooleanMul.N4.jetSliceB3 c = UnrestrictedBooleanMul.N4.jetB c • UnrestrictedBooleanMul.N4.aLinear 0

theorem UnrestrictedBooleanMul.N4.jet_separation (U : Submodule F₂ LinearForm) (hUdim : Module.finrank F₂ ↥U ≤ 2) (hUne : U ≠ anchorPlane) (c : TargetCoeff) (hOutside : targetTwo (jetResidualCoeff c) (aCoord 2) (bCoord 2) = 0) (hA2 : jetSliceA2 c ∈ U) (hA3 : jetSliceA3 c ∈ U) (hB2 : jetSliceB2 c ∈ U) (hB3 : jetSliceB3 c ∈ U) : c ∈ feedbackCoeffSpace

Jet separation in the exact algebraic interface used later: the outside--outside part vanishes and all four outside slice vectors lie in a subspace of dimension at most two different from the anchor plane.