Reflection Character Preservation

Abstract

An equivariant real-linear bridge preserves both reflection characters and has no nonzero response of the opposite character.

Theorem 1.1 (Equivariant bridges preserve reflection characters).

$$\begin{array}{r}\forall C,Z:\mathrm{Type},\\ [\mathrm{AddCommGroup}\left(C\right)],[\mathrm{Module}\left(\mathbb{R},C\right)],[\mathrm{AddCommGroup}\left(Z\right)],[\mathrm{Module}\left(\mathbb{R},Z\right)],\\ configReflection:\mathrm{LinearMap}\left(\mathbb{R},C,C\right),responseReflection:\mathrm{LinearMap}\left(\mathbb{R},Z,Z\right),bridge:\mathrm{LinearMap}\left(\mathbb{R},C,Z\right),\\ Function.Semiconj\left(bridge,configReflection,responseReflection\right)\Rightarrow \\ (\forall x\in C,\mathrm{apply}\left(configReflection,x\right)=x\Rightarrow \mathrm{apply}\left(responseReflection,\mathrm{apply}\left(bridge,x\right)\right)=\mathrm{apply}\left(bridge,x\right))\wedge \\ (\forall x\in C,\mathrm{apply}\left(configReflection,x\right)=-x\Rightarrow \mathrm{apply}\left(responseReflection,\mathrm{apply}\left(bridge,x\right)\right)=-\mathrm{apply}\left(bridge,x\right))\wedge \\ (\forall x\in C,\mathrm{apply}\left(configReflection,x\right)=x\Rightarrow \left(\mathrm{apply}\left(responseReflection,\mathrm{apply}\left(bridge,x\right)\right)=-\mathrm{apply}\left(bridge,x\right)\Rightarrow \mathrm{apply}\left(bridge,x\right)=0\right))\wedge \\ (\forall x\in C,\mathrm{apply}\left(configReflection,x\right)=-x\Rightarrow \left(\mathrm{apply}\left(responseReflection,\mathrm{apply}\left(bridge,x\right)\right)=\mathrm{apply}\left(bridge,x\right)\Rightarrow \mathrm{apply}\left(bridge,x\right)=0\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/CharacterPreservation.character_preservation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let the configuration and response carriers be real modules. The two linear reflections act on their respective carriers, and the linear bridge intertwines those actions.

Fixed configurations map to fixed responses, while negated configurations map to negated responses. A response lying in the opposite character sector is therefore zero.

References

• Truth anchor: D5/S3/Observer/Bridges/CharacterPreservation.character_preservation
• Dependency: D5/S3/Observer/Bridges/FixedPointSemiconjugacy