Affine restrictions of inversion in characteristic two

The reciprocal identity on a nondegenerate affine plane excludes affine restrictions with more than four points. Scaling one additive defect also rules out every nonzero additive component of inversion over a field larger than four.

The affine-plane obstruction is a special case of the inverse-function sum identities discussed by Claude Carlet, "On the vector subspaces of F₂ⁿ over which the multiplicative inverse function sums to zero", Designs, Codes and Cryptography 93 (2025), 1237–1254, https://doi.org/10.1007/s10623-024-01531-6.

theorem Algebraic.Aggregate.Geometry.Inversion.eq_of_inverse_three {K : Type u_1} [Field K] [CharP K 2] {a b c : K} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hs : a + b + c ≠ 0) (identity : (a + b + c)⁻¹ = a⁻¹ + b⁻¹ + c⁻¹) : a = b ∨ a = c ∨ b = c

A reciprocal ternary identity forces a repeated point or a zero entry.

theorem Algebraic.Aggregate.Geometry.Inversion.card_le_four_of_inverse_affine {K : Type u_1} [Field K] [CharP K 2] (S : Finset K) (affine : ∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, (a + b + c)⁻¹ = a⁻¹ + b⁻¹ + c⁻¹) : S.card ≤ 4

Inversion preserves ternary addition on at most four points of a binary field.

theorem Algebraic.Aggregate.Geometry.Inversion.exists_inverse_add_defect {K : Type u_1} [Field K] [CharP K 2] [Fintype K] (large : 4 < Fintype.card K) : ∃ (a : K) (b : K), (a + b)⁻¹ ≠ a⁻¹ + b⁻¹

A binary field with more than four elements has an additive inversion defect.

theorem Algebraic.Aggregate.Geometry.Inversion.eq_zero_of_additive_inverse_component {K : Type u_1} [Field K] [CharP K 2] [Fintype K] (large : 4 < Fintype.card K) (L R : K →+ ZMod 2) (component : ∀ (x : K), L x⁻¹ = R x) : L = 0

No nonzero additive component of inversion is additive over a field larger than four.