Binary Character Basis Minimality

Abstract

Binary-character bases are exactly minimum complete observation families.

Theorem 1.1 (Character-span bases are minimum complete observation families).

$$\begin{array}{c}\forall G,I,J,B,\\ [\mathrm{AddCommGroup}(G)],[\mathrm{Finite}(G)],[\mathrm{Finite}(I)],\\ [\mathrm{Fintype}(J)],[\mathrm{Fintype}(B)],\\ chi:I\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),psi:J\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),\\ H:=\mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(chi)),r:=\mathrm{finrank}(\mathrm{ZMod}(2),H),\\ beta:\mathrm{Basis}(B,\mathrm{ZMod}(2),H),\\ (\forall g\in G,(\forall i\in I,chi(i)(\mathrm{mkQ}(2,g))=0)⟺(\forall j\in J,psi(j)(\mathrm{mkQ}(2,g))=0))\Rightarrow \\ \mathrm{IsLeast}(\{kappa\mid \exists S,S\subseteq \mathrm{range}(chi)\wedge \mathrm{span}(\mathrm{ZMod}(2),S)=H\wedge \mathrm{card}(S)=kappa\},\mathrm{rank}(\mathrm{ZMod}(2),H))\wedge r\le \mathrm{card}(J)\wedge \\ (\exists sigma:\mathrm{Fin}(r)\to \mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2)),(\forall k\in \mathrm{Fin}(r),sigma(k)\in \mathrm{range}(chi))\wedge \mathrm{LinearIndependent}(\mathrm{ZMod}(2),sigma)\wedge \\ \mathrm{span}(\mathrm{ZMod}(2),\mathrm{range}(sigma))=H\wedge \forall g\in G,(\forall k\in \mathrm{Fin}(r),sigma(k)(\mathrm{mkQ}(2,g))=0)⟺(\forall i\in I,chi(i)(\mathrm{mkQ}(2,g))=0))\wedge \\ ((\forall g\in G,(\forall j\in B,beta(j)(\mathrm{mkQ}(2,g))=0)⟺(\forall i\in I,chi(i)(\mathrm{mkQ}(2,g))=0))\wedge \mathrm{card}(B)\le \mathrm{card}(J)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let G be a finite abelian group. Binary characters are represented additively as linear functionals on the canonical quotient of G by doubles, so evaluation remains on the original group through the canonical quotient map.

The character space H is constructed as the binary-field span of the given character family, and r is its finite dimension. The displayed same-kernel premise is pointwise on G, not an abstract replacement definition of sufficiency.

The minimum same-span cardinality is inherited from the frozen binary role theorem. Equality of actual joint kernels forces the competitor span to equal H, giving the lower bound r.

A linearly independent Fin(r)-indexed family is extracted from the original characters, spans H, and has their joint kernel. The last public clause quantifies over an arbitrary supplied basis of H and proves both kernel sufficiency and minimum cardinality.

References

• Truth anchor: D5/S3/Fourier/BinaryCharacterBasisMinimality.binary_character_basis_minimality
• Dependency: D5/S3/ConceptDynamics/LinearSufficiency/BinaryRoleMinimumCardinality