Fourier-Mode Determination

Abstract

Finite Fourier data leave regulator measures nonunique; the complete profile is exact.

Theorem 1.1 (Every finite Fourier table has distinct realizations).

$$\begin{array}{r}\forall S:\mathrm{Finset}\left(\mathbb{Z}\right),\\ \exists mu:\mathrm{Measure}\left(\mathrm{AddCircle}\left(2\cdot \pi \right)\right),\exists nu:\mathrm{Measure}\left(\mathrm{AddCircle}\left(2\cdot \pi \right)\right),\\ \mathrm{IsProbabilityMeasure}\left(mu\right)\wedge \mathrm{IsProbabilityMeasure}\left(nu\right)\wedge mu\ne nu\wedge \\ \forall n\in S,\mathrm{fourierMoment}\left(mu,n\right)=\mathrm{fourierMoment}\left(nu,n\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MeasureSeparation/FourierModeDetermination.finite_fourier_modes_do_not_determine_measure (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite mode set, choose a positive integer k beyond every listed absolute frequency. The construction compares normalized circle Haar measure with its density 1 + Re(fourier k)/2 perturbation.

Fourier orthogonality makes the two probability measures agree on every listed mode. Their moments at the unused mode -k differ by one quarter, which proves that the measures themselves are distinct.

The explicit nonnegative density and the unused-mode discrepancy are the constructive escape witness for finite non-clonability.

Theorem 1.2 (The complete Fourier profile determines the measure).

$$\begin{array}{r}\forall mu:\mathrm{Measure}\left(\mathrm{AddCircle}\left(2\cdot \pi \right)\right),nu:\mathrm{Measure}\left(\mathrm{AddCircle}\left(2\cdot \pi \right)\right),\\ [\mathrm{IsFiniteMeasure}\left(mu\right)],[\mathrm{IsFiniteMeasure}\left(nu\right)],\\ (\forall n:\mathbb{Z},\mathrm{fourierMoment}\left(mu,n\right)=\mathrm{fourierMoment}\left(nu,n\right))\Rightarrow mu=nu.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MeasureSeparation/FourierModeDetermination.all_fourier_modes_determine_measure (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Fourier characters generate a star subalgebra that separates points of the additive circle.

Equality on every character extends by linearity to that algebra. The pinned Mathlib finite-measure extensionality theorem then identifies the two finite regulator measures.

References

• Truth anchor: D5/S3/Observer/MeasureSeparation/FourierModeDetermination.all_fourier_modes_determine_measure
• Truth anchor: D5/S3/Observer/MeasureSeparation/FourierModeDetermination.finite_fourier_modes_do_not_determine_measure