Completed Scalar Odd Coupling

Abstract

A reflection-invariant analytic scalar has no linear or odd homogeneous response.

Theorem 1.1 (A completed scalar has no linear odd coupling).

$$\begin{array}{c}\forall E:Type,\\ \mathrm{NormedAddCommGroup}(E)\wedge \mathrm{NormedSpace}(\mathbb{R},E)\Rightarrow \\ \forall completedScalar:E\to \mathbb{R},series:\mathrm{FormalMultilinearSeries}(\mathbb{R},E,\mathbb{R}),\\ \mathrm{HasFPowerSeriesAt}(completedScalar,series,0)\wedge (\forall u:E,completedScalar\left(u\right)=completedScalar\left(-u\right))\Rightarrow \\ \mathrm{fderiv}(\mathbb{R},completedScalar,0)=0\wedge \\ (\forall n:\mathbb{N},\mathrm{Odd}(n)\Rightarrow \forall u:E,\left(serie{s}_n\right)\left(\lambda i:\mathrm{Fin}(n)\mapsto u\right)=0)\wedge \\ (\forall n:\mathbb{N},0<n\wedge (\exists u:E,\left(serie{s}_n\right)\left(\lambda i:\mathrm{Fin}(n)\mapsto u\right)\ne 0)\Rightarrow \mathrm{Even}(n)\wedge 2\le n).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/ObserverJet/CompletedScalarOddCoupling.completed_scalar_has_no_linear_odd_coupling (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a scalar readout on a real normed space admit a formal power series at zero and be invariant under reflection of its input.

Restricting the readout to every real line gives two equal one-variable power series, one in each orientation. Uniqueness then forces every odd diagonal coefficient to vanish.

The linear coefficient is the Frechet derivative. Consequently the derivative is zero, and every positive degree with a nonzero homogeneous diagonal term is even and at least two.

References

• Truth anchor: D5/S3/CompletionDynamics/ObserverJet/CompletedScalarOddCoupling.completed_scalar_has_no_linear_odd_coupling