Binary Character Uniform Information Exactness

Abstract

Uniform finite-group inputs yield exact binary-character information in bits.

Definition 1.1 (Joint binary-character profile).

Lean statement: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterProfileHom

Formalization. D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterProfileHom (✓ std3).

Source. Repository-derived.

Commentary.

The named profile homomorphism evaluates every binary character on the canonical quotient class of the same group element.

Definition 1.2 (Binary-character span).

Lean statement: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterSpan

Formalization. D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterSpan (✓ std3).

Source. Repository-derived.

Commentary.

The named span is the binary-linear subspace generated by the character family.

Definition 1.3 (Binary-character rank).

Lean statement: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterRank

Formalization. D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterRank (✓ std3).

Source. Repository-derived.

Commentary.

The named rank is the finite dimension of the binary-character span.

Theorem 1.4 (A uniform character profile carries exactly its rank in bits).

$$\frac{H\left(\mathrm{profileLaw}\left(chi,\mathrm{Uniform}\left(G\right)\right)\right)}{\log \left(2\right)}=\mathrm{finrank}\left(\mathrm{span}\left(\mathrm{range}\left(chi\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The joint profile of a uniform input is uniform on the realized image. Its image has cardinality two to the character-span rank, so its Shannon entropy divided by log two is exactly that rank.

Theorem 1.5 (The residual entropy is group-size bits minus character rank).

$$\frac{\mathrm{conditionalEntropy}\left(\mathrm{Uniform}\left(G\right),\mathrm{profile}\left(chi\right)\right)}{\log \left(2\right)}={\log }_2\left(\mathrm{card}\left(G\right)\right)-\mathrm{finrank}\left(\mathrm{span}\left(\mathrm{range}\left(chi\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The deterministic profile decomposition subtracts the realized profile entropy from the uniform source entropy. This is the second boxed conclusion of FPOD Corollary 90.1.

Theorem 1.6 (A zero character family carries no profile information).

$$\frac{H\left(\mathrm{profileLaw}\left(\mathrm{zeroFamily}\left(I\right),\mathrm{Uniform}\left(G\right)\right)\right)}{\log \left(2\right)}=0\wedge \frac{\mathrm{conditionalEntropy}\left(\mathrm{Uniform}\left(G\right),\mathrm{profile}\left(\mathrm{zeroFamily}\left(I\right)\right)\right)}{\log \left(2\right)}={\log }_2\left(\mathrm{card}\left(G\right)\right)$$

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

Source. Repository-derived.

Commentary.

For any finite index type, an all-zero family has span rank zero. Its profile entropy vanishes and the full uniform source entropy remains in the conditional term.

Theorem 1.7 (The empty character family retains all source entropy).

$$\frac{H\left(\mathrm{profileLaw}\left(\mathrm{emptyFamily}\left(G\right),\mathrm{Uniform}\left(G\right)\right)\right)}{\log \left(2\right)}=0\wedge \frac{\mathrm{conditionalEntropy}\left(\mathrm{Uniform}\left(G\right),\mathrm{profile}\left(\mathrm{emptyFamily}\left(G\right)\right)\right)}{\log \left(2\right)}={\log }_2\left(\mathrm{card}\left(G\right)\right)$$

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

Source. Repository-derived.

Commentary.

The empty family is the explicit zero-index degeneracy. Its profile has zero bits and conditioning on that profile leaves log base two of the group cardinality.

Theorem 1.8 (Every character family on the singleton group carries zero bits).

$$\frac{H\left(\mathrm{profileLaw}\left(chi,\mathrm{Uniform}\left(Unit\right)\right)\right)}{\log \left(2\right)}=0\wedge \frac{\mathrm{conditionalEntropy}\left(\mathrm{Uniform}\left(Unit\right),\mathrm{profile}\left(chi\right)\right)}{\log \left(2\right)}=0$$

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

Source. Repository-derived.

Commentary.

Every binary character on the singleton group is zero. For every finite character index type, both the profile entropy and its conditional residual therefore vanish.

References

• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterProfileHom
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterRank
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binaryCharacterSpan
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binary_character_uniform_conditional_entropy_bits
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.binary_character_uniform_profile_entropy_bits
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.empty_character_family_information_bits
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.singleton_group_character_information_bits
• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterUniformInformationExactness.zero_character_family_information_bits
• Dependency: D5/S3/Entropy/EntropyEquality
• Dependency: D5/S3/Entropy/Fusion/QuotientFiberDecomposition
• Dependency: D5/S3/Fourier/CharacterSelection/BinaryCharacterRankAndRedundancy