Circuit hardness properties of binary-field inversion

The actual coordinate permutation has no projection coordinate, and every flat on which all of its output coordinates are affine contains at most four points.

theorem Algebraic.Aggregate.Geometry.Inversion.card_field {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) : Fintype.card K = 2 ^ n

A coordinate basis records the exact finite-field cardinality.

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

Decoding a field value recovers its original prime-field coordinates.

theorem Algebraic.Aggregate.Geometry.Inversion.inverseFunction_nonprojection {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) : (fun (x : Fin n → Bool) => inverseFunction e x i) ≠ fun (x : Fin n → Bool) => x j

In dimension at least three, no coordinate of inversion is a primary projection.

theorem Algebraic.Aggregate.Geometry.Inversion.card_flat_le_four {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (S : AffineFlat n) (affine : ∀ (i : Fin n), AffineOn S fun (x : Fin n → Bool) => inverseFunction e x i) : S.carrier.card ≤ 4

Every simultaneous affine restriction of inversion contains at most four points.