notion of direction and frame of reference

Stream: PhysLean

[ZhiKai Pong]

The context of this is for plane waves but I imagine this must be applicable to a wide range of physics.

Consider a plane wave of the form E(t, x) = E(x · n - ct) where n is a unit vector indicating the direction of propagation.

1. any ideas on how to define n?
2. to simplify the geometry we often want to "choose a set of cartesian axes where the z direction coincides with n". How should this idea be implemented?

my guess would be to use docs#OrthonormalBasis somehow and work in the new reference frame, then map everything back via some transformation? but I'm really not sure how this should work

[Joseph Tooby-Smith]

I think really n is corresponds to a difference between space points normalized to 1. But given we have chosen a 0 of Space, and you have already manifestly used this, since you have written the dot product, then I think it is sufficient to define n as

(n : Space) (hn : n  · n =  1)

For part 2, you can extend n to an orthonormal basis, maybe with docs#Orthonormal.exists_orthonormalBasis_extension. Then define the linear transformation taking the standard basis on Space to this new basis.
This linear transformation will be a rotation, and (if you are dealing with the wave-equation here), there should be some suitable property of the Laplacian which says that it is equivariant w.r.t. rotations.

Something like the following, if R is a rotation then and f : Space → EuclideanSpace ℝ (Fin d), and x : Space then

(Δ f) x = (Δ (fun y => f (R * y))) (R⁻¹ x)

[Joseph Tooby-Smith]

More generally I think we should define a MulAction of SO(d) on Space at somepoint.