Parity-Conditioned Product Moments

Abstract

Uniform laws on the two parity fibers of a binary cube agree on every proper marginal and differ exactly at the full product.

Definition 1.1 (Binary coordinates as signs).

$$\forall b:\mathrm{Fin}(2),\mathrm{paritySign}(b)=\mathrm{ite}(b=0,-1,1).$$

Formalization. D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.paritySign (✓ std3).

Source. Repository-derived.

Commentary.

The binary value zero represents minus one and the binary value one represents plus one.

Definition 1.2 (The fiber of a prescribed total sign).

$$\begin{gathered} \forall d\in \mathbb{N},\epsilon \in \mathbb{Z}, \\ \mathrm{parityFiber}(d,\epsilon )=\mathrm{filter}(\mathrm{univ}(\mathrm{Fin}(2{)}^{\mathrm{Fin}(d)}),x\mapsto \prod _{i\in \mathrm{Fin}(d)}\mathrm{paritySign}(x\left(i\right))=\epsilon ). \end{gathered}$$

Formalization. D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityFiber (✓ std3).

Source. Repository-derived.

Commentary.

The fiber consists of all binary strings whose coordinate-sign product equals the specified integer parity.

Definition 1.3 (The uniform rational law on a parity fiber).

$$\begin{gathered} \forall d\in \mathbb{N},\epsilon \in \mathbb{Z},x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(d)}, \\ \mathrm{parityLaw}(d,\epsilon ,x)=\mathrm{ite}(x\in \mathrm{parityFiber}(d,\epsilon ),{2^{d-1}}^{-1},0). \end{gathered}$$

Formalization. D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityLaw (✓ std3).

Source. Repository-derived.

Commentary.

A point in the selected fiber receives mass 2 to the negative (d minus 1), and every point outside receives zero.

Definition 1.4 (Mass of a coordinate restriction).

$$\begin{gathered} \forall d\in \mathbb{N},\epsilon \in \mathbb{Z},A:\mathrm{Finset}(\mathrm{Fin}(d)),y\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(d)}, \\ \mathrm{parityMarginalMass}(d,\epsilon ,A,y)=\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(d)}}\mathrm{ite}(\forall i\in A,x\left(i\right)=y\left(i\right),\mathrm{parityLaw}(d,\epsilon ,x),0). \end{gathered}$$

Formalization. D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityMarginalMass (✓ std3).

Source. Repository-derived.

Commentary.

This finite sum is the mass of the event that a binary string agrees with y at every coordinate in A.

Theorem 1.5 (Cardinality and product moments on one parity fiber).

$$\begin{array}{r}\forall k\in \mathbb{N},\epsilon \in \mathbb{Z},\\ (\epsilon =-1)\vee (\epsilon =1)\Rightarrow \\ \mathrm{card}(\mathrm{parityFiber}(k+1,\epsilon ))=2^k\wedge \\ (\forall A:\mathrm{Finset}(\mathrm{Fin}(k+1)),A\ne \varnothing \Rightarrow A\ne univ\Rightarrow \\ \sum _{x\in \mathrm{parityFiber}(k+1,\epsilon )}\prod _{i\in A}\mathrm{paritySign}(x\left(i\right))=0)\wedge \\ \sum _{x\in \mathrm{parityFiber}(k+1,\epsilon )}\prod _{i\in \mathrm{Fin}(k+1)}\mathrm{paritySign}(x\left(i\right))=\epsilon \cdot \mathrm{card}(\mathrm{parityFiber}(k+1,\epsilon )).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parity_conditioned_moments (✓ std3). ∎

Source. Repository-derived.

Commentary.

For d = k+1 and parity epsilon equal to minus one or plus one, the fiber has 2^k elements. Every nonempty proper-coordinate product sums to zero, while every full-coordinate product equals epsilon.

The proper-moment cancellation pairs each string with the result of flipping one coordinate in A and one outside A. This is a fixed-point-free involution of the same parity fiber and negates the A-product. A single-coordinate flip bijects the two fibers, giving the cardinality after partitioning the full cube.

Theorem 1.6 (The two parity laws have identical proper marginals).

$$\begin{array}{r}\forall k\in \mathbb{N},\\ ((\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,-1,x)=1)\wedge (\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,1,x)=1))\wedge \\ (\forall A:\mathrm{Finset}(\mathrm{Fin}(k+1)),A\ne \varnothing \Rightarrow A\ne univ\Rightarrow \\ (\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,-1,x)\cdot \prod _{i\in A}\mathrm{paritySign}(x\left(i\right))=0)\wedge \\ (\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,1,x)\cdot \prod _{i\in A}\mathrm{paritySign}(x\left(i\right))=0))\wedge \\ (\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,-1,x)\cdot \prod _{i\in \mathrm{Fin}(k+1)}\mathrm{paritySign}(x\left(i\right))=-1)\wedge \\ (\sum _{x\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)}}\mathrm{parityLaw}(k+1,1,x)\cdot \prod _{i\in \mathrm{Fin}(k+1)}\mathrm{paritySign}(x\left(i\right))=1)\wedge \\ (\forall A:\mathrm{Finset}(\mathrm{Fin}(k+1)),A\ne univ\Rightarrow \forall y\in \mathrm{Fin}(2{)}^{\mathrm{Fin}(k+1)},\\ \mathrm{parityMarginalMass}(k+1,-1,A,y)=\mathrm{parityMarginalMass}(k+1,1,A,y)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parity_conditioned_probability_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both rational laws have total mass one. Every nonempty proper product has expectation zero under both laws, their full-product expectations are respectively minus one and plus one, and every proper marginal, including the empty marginal, is identical.

The mass and moment clauses use the preceding parity-fiber calculation. For marginal equality, flipping one coordinate outside A is a bijection between the two fibers and preserves the restriction event on A.

References

• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityFiber
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityLaw
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parityMarginalMass
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.paritySign
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parity_conditioned_moments
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/ParityConditionedMoments.parity_conditioned_probability_form