Every nonzero inversion component is nonaffine

The reciprocal scaling-defect argument applies to every nonzero linear output functional, rather than just individual coordinate projections. This supplies the nonlinear-generator rank hypothesis for arbitrary coordinate bases.

theorem Algebraic.Aggregate.Geometry.Inversion.encode_false {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) : ((encode e) fun (x : Fin n) => false) = 0

The coordinate encoding sends the all-false input to the field zero.

theorem Algebraic.Aggregate.Geometry.Inversion.inverseFunction_false {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) : (inverseFunction e fun (x : Fin n) => false) = fun (x : Fin n) => false

Binary-field inversion fixes the all-false input.

theorem Algebraic.Aggregate.Geometry.Inversion.bitVector_decode {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x : K) : bitVector ((encode e).symm x) = e.symm x

The prime-field input vector agrees with the chosen coordinate encoding.

theorem Algebraic.Aggregate.Geometry.Inversion.inverseFunction_nonaffineComponents {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (dimension : 3 ≤ n) : NonaffineComponents (inverseFunction e)

Every nonzero linear output component of inversion is nonaffine.

theorem Algebraic.Aggregate.Geometry.Inversion.inverseFunction_nonliteral {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (dimension : 3 ≤ n) (i j : Fin n) (b : Bool) : (fun (x : Fin n → Bool) => inverseFunction e x i) ≠ fun (x : Fin n → Bool) => b ^^ x j

No inverse output is a signed primary literal.