Binary Character Semantic Redundancy

Abstract

Character-span rank separates semantic profile bits from dependent parity checks.

Theorem 1.1 (Semantic information and transmission redundancy separate).

$$\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)),eta:\mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),\\ eta\in \mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi))\Rightarrow \\ \mathrm{let}(chiPlus:\mathrm{Option}(I)\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),chiPlus(none):=eta,\forall i:I,chiPlus(some(i)):=chi(i),\\ Phi(g)(i):=chi(i)(\mathrm{mkQ}(2,g)),PhiPlus(g)(j):=chiPlus(j)(\mathrm{mkQ}(2,g)),\\ H:=\mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi)),r:=\mathrm{finrank}(\mathrm{ZMod}(2),H),R:=\ker (\mathrm{linearCombination}(\mathrm{ZMod}(2),chi)),\\ RPlus:=\ker (\mathrm{linearCombination}(\mathrm{ZMod}(2),chiPlus)))\\ \mathrm{card}(\mathrm{range}(Phi))=2^r\wedge \\ \mathrm{finrank}(\mathrm{ZMod}(2),R)=\mathrm{card}(I)-r\wedge \\ \mathrm{card}(\mathrm{range}(PhiPlus))=\mathrm{card}(\mathrm{range}(Phi))\wedge \\ \mathrm{finrank}(\mathrm{ZMod}(2),RPlus)=\mathrm{finrank}(\mathrm{ZMod}(2),R)+1\wedge \\ \exists a:\mathrm{Option}(I)\to \mathrm{ZMod}(2),a\in RPlus\wedge a(none)=1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Fourier/CharacterSelection/BinaryCharacterSemanticRedundancy.binary_character_semantic_redundancy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Binary characters are linear functionals on the canonical quotient of a finite abelian group by doubles. Their joint profile and coefficient relation space are constructed from that family.

The character-span rank counts independent profile bits, while the kernel of coefficient synthesis counts role relations.

Adjoining a character already in the span preserves the realized profile count, adds one independent relation, and exposes a parity check with coefficient one on the new coordinate.

References

• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterSemanticRedundancy.binary_character_semantic_redundancy
• Dependency: D5/S3/Fourier/CharacterSelection/BinaryCharacterProfileRankCardinality