Binary Character Profile Rank Cardinality

Abstract

The binary-character span rank determines the realized profile count and every realized fiber size.

Theorem 1.1 (Character rank controls profiles and fibers).

$$\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)(c):=chi(c)(\mathrm{mkQ}(2,g)),H:=\mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi)),r:=\mathrm{finrank}(\mathrm{ZMod}(2),H))\\ \ker (Phi)=\mathrm{iInf}(c,I,\ker (chi(c)\circ \mathrm{mkQ}(2))),\mathrm{card}(\mathrm{range}(Phi))=2^r,\forall b:\mathrm{range}(Phi),\mathrm{card}(\{g:G\mid Phi(g)=b\})=\frac{\mathrm{card}(G)}{2^r}.\end{array}$$

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

Source. Repository-derived.

Commentary.

The group is finite abelian. Each binary character is a linear functional on the canonical quotient by doubles and is evaluated back on the original group.

The joint profile is constructed componentwise from those characters. Its rank is the finite dimension of their linear span.

All three conclusions are public: the kernel intersection, the power-of-two realized image count, and the uniform cardinality of every realized profile fiber.

References

• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterProfileRankCardinality.binary_character_profile_rank_cardinality
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/Fourier/BinaryCharacterBasisMinimality