Reflections survive a change of scalar field

Submodule.reflection K x = 2 • K.starProjection x - x, and the 2 • is an ℕ-action: a reflection is built from the orthogonal projection and the additive group alone. TauCeti.ScalarTransport changes neither, so a reflection transports to the reflection of the transported subspace, and so does the image of a subspace under one.

This is what carries the Davis--Kahan double-angle objects — the mirror image of U in V and the projector differences built from it — across a change of scalar field.

Main results

• TauCeti.ScalarTransport.reflection_of.
• TauCeti.ScalarTransport.submodule_map_reflection.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti.
• Extraction class: authored in place for the Tau Ceti staging layer.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

theorem TauCeti.ScalarTransport.reflection_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] (x : E) : (submodule S).reflection (of x) = of (S.reflection x)

The reflection of a transported subspace is the transported reflection.

@[simp]

theorem TauCeti.ScalarTransport.submodule_map_reflection {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S T : Submodule 𝕜 E) [T.HasOrthogonalProjection] : submodule (Submodule.map (↑T.reflection.toLinearEquiv) S) = Submodule.map (↑(submodule T).reflection.toLinearEquiv) (submodule S)

The image of a subspace under a reflection transports.

@[simp] because the transported reflection image is the normal form: every consumer wants the two transports pushed inside, not a reflection of a transport.

theorem TauCeti.ScalarTransport.starProjection_map_reflection_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S T : Submodule 𝕜 E) [T.HasOrthogonalProjection] [(Submodule.map (↑T.reflection.toLinearEquiv) S).HasOrthogonalProjection] [(Submodule.map (↑(submodule T).reflection.toLinearEquiv) (submodule S)).HasOrthogonalProjection] (x : E) : (Submodule.map (↑(submodule T).reflection.toLinearEquiv) (submodule S)).starProjection (of x) = of ((Submodule.map (↑T.reflection.toLinearEquiv) S).starProjection x)

The projector onto the mirror image transports.