Boolean coordinates for binary-field inversion

A linear coordinate equivalence supplies an arbitrary basis over the two-element field. Encoding and decoding use actual Boolean bits, and inversion fixes zero.

def Algebraic.Aggregate.Geometry.Inversion.bitEquiv : Bool ≃ ZMod 2

The two Boolean values as elements of the prime field.

Equations

• Algebraic.Aggregate.Geometry.Inversion.bitEquiv = { toFun := fun (b : Bool) => if b = true then 1 else 0, invFun := fun (a : ZMod 2) => decide (a = 1), left_inv := ⋯, right_inv := ⋯ }

theorem Algebraic.Aggregate.Geometry.Inversion.bitEquiv_xor (a b : Bool) : bitEquiv (a ^^ b) = bitEquiv a + bitEquiv b

Boolean XOR is addition in the two-element field.

noncomputable def Algebraic.Aggregate.Geometry.Inversion.encode {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) : (Fin n → Bool) ≃ K

Encode the Boolean cube in an arbitrary linear basis of a binary field.

Equations

• Algebraic.Aggregate.Geometry.Inversion.encode e = (Equiv.piCongrRight fun (x : Fin n) => Algebraic.Aggregate.Geometry.Inversion.bitEquiv).trans e.toEquiv

theorem Algebraic.Aggregate.Geometry.Inversion.encode_xorThree {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x y z : Fin n → Bool) : (encode e) (xorThree x y z) = (encode e) x + (encode e) y + (encode e) z

Encoding converts the affine ternary operation into field addition.

noncomputable def Algebraic.Aggregate.Geometry.Inversion.inverseFunction {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x : Fin n → Bool) : Fin n → Bool

Finite-field inversion expressed in Boolean coordinates, with zero fixed.

Equations

• Algebraic.Aggregate.Geometry.Inversion.inverseFunction e x = (Algebraic.Aggregate.Geometry.Inversion.encode e).symm ((Algebraic.Aggregate.Geometry.Inversion.encode e) x)⁻¹

theorem Algebraic.Aggregate.Geometry.Inversion.inverseFunction_bijective {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) : Function.Bijective (inverseFunction e)

The encoded inversion map is a permutation.

theorem Algebraic.Aggregate.Geometry.Inversion.encode_inverseFunction {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x : Fin n → Bool) : (encode e) (inverseFunction e x) = ((encode e) x)⁻¹

Decoding inversion recovers exactly the field inverse.