Binary Character Redundancy Criterion

Abstract

A binary character is redundant exactly when it lies in the existing span.

Theorem 1.1 (Kernel preservation, span membership, and output recovery are equivalent).

$$\begin{array}{c}\forall G,I:\mathrm{Type},\\ [\mathrm{AddCommGroup}(G)],[\mathrm{Finite}(I)],\\ chi:I\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),\\ eta:\mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),\\ \mathrm{ListTFAE}([\forall g\in G,(\forall i\in I,chi(i)(\mathrm{mkQ}(2,g))=0)\Rightarrow eta(\mathrm{mkQ}(2,g))=0,eta\in \mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi)),\exists a:\mathrm{Finsupp}(I,\mathrm{ZMod}(2)),\forall g\in G,\mathrm{ofAdd}(eta(\mathrm{mkQ}(2,g)))=\prod _{i\in \mathrm{support}(a)}\mathrm{ofAdd}(a(i)\cdot chi(i)(\mathrm{mkQ}(2,g)))]).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Fourier/BinaryCharacterRedundancyCriterion.binary_character_redundancy_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be an abelian group and let I be a finite role-index type. Every binary character is a linear functional on the canonical quotient of G by doubles, evaluated on G through the quotient map.

The first public clause says that the new character vanishes whenever all existing characters vanish. The second says directly that it belongs to the binary-field span of the existing character range.

The third clause exposes finite coefficients. At every group element, the multiplicative output of the new character is recovered as the finite product of the corresponding weighted existing outputs.

The proof applies the pinned library kernel-span criterion and finite-span coefficient theorem, then uses ofAdd_sum for the product formula.

References

• Truth anchor: D5/S3/Fourier/BinaryCharacterRedundancyCriterion.binary_character_redundancy_criterion
• Dependency: D5/S3/Fourier/BinaryCharacterBasisMinimality