Jet separation from a two-wedge shadow

This is the interface between the homogeneous bookkeeping of a cancelled low--low product and the coordinate jet_separation lemma. All terms wholly supported in K₀ disappear on the four outside slices; the two remaining wedge directions give a subspace of rank at most two.

def UnrestrictedBooleanMul.N4.SupportedK0Two (k : TwoForm) : Prop

Every row indexed outside the normalized first-jet coordinates vanishes.

Equations

• UnrestrictedBooleanMul.N4.SupportedK0Two k = ∀ (z j : Fin 8), UnrestrictedBooleanMul.N4.OutsideK0Index z → k z j = 0

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.zero : SupportedK0Two 0

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.add {k l : TwoForm} (hk : SupportedK0Two k) (hl : SupportedK0Two l) : SupportedK0Two (k + l)

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.smul (a : F₂) {k : TwoForm} (hk : SupportedK0Two k) : SupportedK0Two (a • k)

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.vectorWedge {u v : LinearForm} (hu : InK0Linear u) (hv : InK0Linear v) : SupportedK0Two (N4.vectorWedge u v)

theorem UnrestrictedBooleanMul.N4.jet_separation_of_twoWedge_shadow (M N p r : LinearForm) (k : TwoForm) (s d : TargetCoeff) (hM : InK0Linear M) (hN : InK0Linear N) (hk : SupportedK0Two k) (hs : s ∈ feedbackCoeffSpace) (hUne : Submodule.span F₂ (Set.range ![M, N]) ≠ anchorPlane) (hshadow : targetTwo d = targetTwo s + k + vectorWedge M p + vectorWedge N r) : d ∈ feedbackCoeffSpace

Coordinate wrapper for jet_separation: a target shadow consisting of a feedback term, a K₀ term, and two wedge directions is already feedback.