Binary Character Subfamily Criterion

Abstract

A binary-character subfamily is sufficient exactly when it spans the full role space.

Theorem 1.1 (Observation kernels, expressible targets, and character spans agree).

$$\begin{array}{c}\forall G,E,B,\\ [\mathrm{AddCommGroup}(G)],[\mathrm{Finite}(G)],\\ E,B:\mathrm{Set}(\mathrm{Dual}(\mathrm{ZMod}(2),\mathrm{ModN}(G,2))),\\ B\subseteq E\Rightarrow \\ \mathrm{let}(profile(S)(g)(chi):=chi(\mathrm{mkQ}(2,g)),H:=\mathrm{span}(\mathrm{ZMod}(2),E))\\ \mathrm{ListTFAE}([\ker (profile(B))=\ker (profile(E)),\forall Y:\mathrm{Type},\{K:G\to Y\mid \mathrm{Refines}(K,\mathrm{effectiveReadout}(profile(B)))\}=\{K:G\to Y\mid \mathrm{Refines}(K,\mathrm{effectiveReadout}(profile(E)))\},\mathrm{span}(\mathrm{ZMod}(2),B)=H]).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let E be a set of binary characters on a finite abelian group and let B be a subset. Each character is evaluated on the original group through the canonical quotient by doubles.

The displayed profile is the canonical joint readout of a character set. Expressibility uses its canonical effective-image readout and the repository refinement relation.

The public three-way equivalence states equality of observation kernels, equality of expressible target families for every target type, and equality of binary-character spans.

References

• Truth anchor: D5/S3/Fourier/CharacterSelection/BinaryCharacterSubfamilyCriterion.binary_character_subfamily_sufficiency_tfae
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/QuestionAlgebraDuality
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/Fourier/BinaryCharacterRedundancyCriterion