Binary Character Rank And Redundancy

Abstract

Binary-character span rank counts independent joint outputs and identifies redundant roles.

Theorem 1.1 (Rank counts profiles and span dependence gives product recovery).

$$\begin{array}{c}\forall G,I:\mathrm{Type},\\ [\mathrm{AddCommGroup}(G)],[\mathrm{Fintype}(G)],[\mathrm{Fintype}(I)],\\ chi:I\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),\\ \mathrm{let}(Phi(g):=chi(i)(\mathrm{mkQ}(2,g){)}_{i\in I},H:=\mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi)),r:=\mathrm{finrank}(\mathrm{ZMod}(2),H))\\ \mathrm{card}(\mathrm{range}(Phi))=2^r\wedge \\ \forall j\in I,chi(j)\in \mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(\mathrm{restrict}(chi,I\setminus \{j\})))\Rightarrow \exists a:\mathrm{Finsupp}(I\setminus \{j\},\mathrm{ZMod}(2)),\forall g\in G,\mathrm{ofAdd}(chi(j)(\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/CharacterSelection/BinaryCharacterRankAndRedundancy.binary_character_rank_and_redundancy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each role is a binary linear character on the canonical quotient of a finite abelian group by doubles. Their joint profile is evaluated back on the original group.

The realized profile count is two raised to the finite dimension of the character span. A role lying in the span of all other roles has a finite coefficient witness whose multiplicative output is their product.

References

• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterRankAndRedundancy.binary_character_rank_and_redundancy
• Dependency: D5/S3/Fourier/BinaryCharacterRedundancyCriterion
• Dependency: D5/S3/Fourier/CharacterSelection/BinaryCharacterProfileRankCardinality