Deterministic refinement by binary idempotents

def MIPRE.LowDegree.splitComponent {R : Type u_1} [CommRing R] [DecidableEq R] (e b : R) : List R

Split a component by a fixed idempotent and omit its zero children.

Equations

• MIPRE.LowDegree.splitComponent e b = List.filter (fun (x : R) => decide (x ≠ 0)) [e * b, e * (1 - b)]

theorem MIPRE.LowDegree.mem_splitComponent {R : Type u_1} [CommRing R] [DecidableEq R] (e b x : R) : x ∈ splitComponent e b ↔ (x = e * b ∨ x = e * (1 - b)) ∧ x ≠ 0

theorem MIPRE.LowDegree.splitComponent_sum {R : Type u_1} [CommRing R] [DecidableEq R] (e b : R) : (splitComponent e b).sum = e

theorem MIPRE.LowDegree.splitComponent_factor {R : Type u_1} [CommRing R] [DecidableEq R] {e b x : R} (hx : x ∈ splitComponent e b) : ∃ (c : R), x = e * c

theorem MIPRE.LowDegree.one_sub_idempotent {R : Type u_1} [CommRing R] [DecidableEq R] {b : R} (hb : b * b = b) : (1 - b) * (1 - b) = 1 - b

theorem MIPRE.LowDegree.mul_idempotent {R : Type u_1} [CommRing R] [DecidableEq R] {e b : R} (he : e * e = e) (hb : b * b = b) : e * b * (e * b) = e * b

theorem MIPRE.LowDegree.splitComponent_idempotent {R : Type u_1} [CommRing R] [DecidableEq R] {e b : R} (he : e * e = e) (hb : b * b = b) {x : R} (hx : x ∈ splitComponent e b) : x * x = x

theorem MIPRE.LowDegree.splitComponent_pairwise {R : Type u_1} [CommRing R] [DecidableEq R] (e : R) {b : R} (hb : b * b = b) : List.Pairwise (fun (x y : R) => x * y = 0) (splitComponent e b)

structure MIPRE.LowDegree.ComponentFamily {R : Type u_1} [CommRing R] (l : List R) : Prop

A finite complete family of nonzero orthogonal idempotents.

• nonzero (e : R) : e ∈ l → e ≠ 0
• idempotent (e : R) : e ∈ l → e * e = e
• orthogonal : List.Pairwise (fun (e f : R) => e * f = 0) l
• sum_eq_one : l.sum = 1

def MIPRE.LowDegree.splitComponents {R : Type u_1} [CommRing R] [DecidableEq R] (l : List R) (b : R) : List R

Refine all current components in the fixed input order.

Equations

• MIPRE.LowDegree.splitComponents l b = List.flatMap (fun (e : R) => MIPRE.LowDegree.splitComponent e b) l

theorem MIPRE.LowDegree.ComponentFamily.split {R : Type u_1} [CommRing R] [DecidableEq R] {l : List R} (hl : ComponentFamily l) {b : R} (hb : b * b = b) : ComponentFamily (splitComponents l b)

def MIPRE.LowDegree.DecidesComponent {R : Type u_1} [CommRing R] (e b : R) : Prop

A component is wholly inside or outside a supplied idempotent.

Equations

• MIPRE.LowDegree.DecidesComponent e b = (e * b = 0 ∨ e * b = e)

theorem MIPRE.LowDegree.splitComponent_decides {R : Type u_1} [CommRing R] [DecidableEq R] {e b x : R} (hb : b * b = b) (hx : x ∈ splitComponent e b) : DecidesComponent x b

theorem MIPRE.LowDegree.splitComponent_preserves {R : Type u_1} [CommRing R] [DecidableEq R] {e b c x : R} (hc : DecidesComponent e c) (hx : x ∈ splitComponent e b) : DecidesComponent x c

def MIPRE.LowDegree.splitAllComponents {R : Type u_1} [CommRing R] [DecidableEq R] (l bs : List R) : List R

Iterate the deterministic refinement over a fixed generating family.

Equations

• MIPRE.LowDegree.splitAllComponents l bs = List.foldl MIPRE.LowDegree.splitComponents l bs

theorem MIPRE.LowDegree.ComponentFamily.splitAll {R : Type u_1} [CommRing R] [DecidableEq R] {l bs : List R} (hl : ComponentFamily l) (hb : ∀ b ∈ bs, b * b = b) : ComponentFamily (splitAllComponents l bs)

theorem MIPRE.LowDegree.splitAllComponents_preserves {R : Type u_1} [CommRing R] [DecidableEq R] {l bs : List R} {c : R} (hc : ∀ e ∈ l, DecidesComponent e c) (e : R) : e ∈ splitAllComponents l bs → DecidesComponent e c

theorem MIPRE.LowDegree.splitAllComponents_decides {R : Type u_1} [CommRing R] [DecidableEq R] {l bs : List R} (hb : ∀ b ∈ bs, b * b = b) (e : R) : e ∈ splitAllComponents l bs → ∀ b ∈ bs, DecidesComponent e b

theorem MIPRE.LowDegree.instFactPrimeOfNatNat_mIPRE : Fact (Nat.Prime 2)

theorem MIPRE.LowDegree.decidesComponent_of_mem_span {R : Type u_1} [CommRing R] [DecidableEq R] [Algebra (ZMod 2) R] (e : R) (bs : List R) (hb : ∀ b ∈ bs, DecidesComponent e b) (z : R) (hz : z ∈ Submodule.span (ZMod 2) {b : R | b ∈ bs}) : DecidesComponent e z

Deciding each generator means deciding every binary linear combination.

theorem MIPRE.LowDegree.splitAllComponents_primitive {R : Type u_1} [CommRing R] [DecidableEq R] [Algebra (ZMod 2) R] {l bs : List R} (hl : ComponentFamily l) (hb : ∀ b ∈ bs, b * b = b) (hspan : ∀ (z : R), z * z = z → z ∈ Submodule.span (ZMod 2) {b : R | b ∈ bs}) (e : R) : e ∈ splitAllComponents l bs → PrimitiveBinaryComponent e

Separating a spanning family of fixed vectors makes every remaining component primitive.

theorem MIPRE.LowDegree.ComponentFamily.linearIndependent {R : Type u_1} [CommRing R] [DecidableEq R] [Algebra (ZMod 2) R] {l : List R} (hl : ComponentFamily l) : LinearIndependent (ZMod 2) fun (i : Fin l.length) => l.get i

Nonzero orthogonal idempotents are linearly independent over the binary base field.

theorem MIPRE.LowDegree.ComponentFamily.length_le_finrank {R : Type u_1} [CommRing R] [DecidableEq R] [Algebra (ZMod 2) R] [Module.Finite (ZMod 2) R] {l : List R} (hl : ComponentFamily l) : l.length ≤ Module.finrank (ZMod 2) R

Thus refinement can retain at most the ambient vector-space dimension.