Changing the reference frame II: aligning the spin with the -axis
ProvedNoHair.spin_alignmentFor every vector there is a rotation with
This is the step of the source's frame argument that orients the spin angular momentum along the positive -axis, leaving only its magnitude.
import Mathlib import Definitions.Def_NoHair_kerrNewman open scoped ContDiff Manifold BigOperators open Set Matrix
namespace NoHair
/-- **Milestone (changing the reference frame II): spin alignment.** Every angular-momentum
vector `J ∈ ℝ³` is rotated by some `R ∈ SO(3)` onto the positive `z`-axis: `R J = (0, 0, |J|)`. -/
theorem spin_alignment (J : Fin 3 → ℝ) :
∃ R ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ,
R *ᵥ J = ![0, 0, Real.sqrt (J 0 ^ 2 + J 1 ^ 2 + J 2 ^ 2)] := by
sorry
end NoHairRead-back
What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind
Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare it against the Lean code themselves or obtain an independent read-back.
For every there is a real matrix in the special orthogonal group (, ) with . The case is included (any rotation works).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.