A.5 The rational signal and its filter
On this page · Permalink · Source line 101
The first layer uses literal rational lists. The chosen perturbation is \(r_n=3\cos(\pi n/2)+2\), whose displayed rational entries can be certified without numerical trigonometric evaluation. Its sum with \(c\) is the test signal.
Literal source. QuantumArithmeticBridge.lean, physical lines 51–61.
/-- Ramanujan sum c_12(n), n = 0,...,11. -/
def ramanujan12 : QVector :=
[4, 0, 2, 0, -2, 0, -4, 0, -2, 0, 2, 0]
/-- A deliberately off-band perturbation: 3 cos(pi n/2) + 2. -/
def noise12 : QVector :=
[5, 2, -1, 2, 5, 2, -1, 2, 5, 2, -1, 2]
/-- Signal used in the essay's filter demonstration. -/
def testSignal12 : QVector :=
[9, 2, 1, 2, 3, 2, -5, 2, 3, 2, 1, 2]The cyclic matrix has entry \(c_{(n-m)\bmod12}/12\). The original layer proves its symmetry, idempotence, preservation of \(c\), rejection of the chosen perturbation, and exact recovery from the displayed contaminated signal. The exact energy contract is \(150=48+102\).
Literal source. QuantumArithmeticBridge.lean, physical lines 92–126.
theorem projector12_idempotent :
matMulN 12 projector12 projector12 = projector12 := by
decide +kernel
/-- The arithmetic signal lies in the selected subspace. -/
theorem projector12_fixes_ramanujan :
matVec projector12 ramanujan12 = ramanujan12 := by
decide +kernel
/-- The chosen constant-plus-frequency-3 perturbation lies in the complementary subspace. -/
theorem projector12_kills_noise :
matVec projector12 noise12 = List.replicate 12 0 := by
decide +kernel
/-- Therefore the exact filter recovers the arithmetic component. -/
theorem projector12_recovers_test_signal :
matVec projector12 testSignal12 = ramanujan12 := by
decide +kernel
/-- The arithmetic amplitude vector has squared norm 48. -/
theorem ramanujan12_energy : sqEnergy ramanujan12 = 48 := by
decide +kernel
/-- The perturbation has squared norm 102. -/
theorem noise12_energy : sqEnergy noise12 = 102 := by
decide +kernel
/-- The full signal has squared norm 150. -/
theorem testSignal12_energy : sqEnergy testSignal12 = 150 := by
decide +kernel
/-- Exact orthogonal energy decomposition 150 = 48 + 102. -/
theorem energy_decomposition :
sqEnergy testSignal12 = sqEnergy ramanujan12 + sqEnergy noise12 := by
decide +kernelThe list operations use finite lists, including zero defaults and zip-based dot products. These facts are therefore claims about the supplied twelve-entry objects. They should not be silently interpreted as universal matrix theorems for arbitrary ragged lists. The later \(\operatorname{Fin}(12)\) layer supplies the typed matrix identities used in the publication.