coordRay_coordRay
Coordinate rays compose additively under successive displacements in the same direction: applying the ray map twice along index μ adds the parameters s and t. Derivative calculations in coordinate-based relativity rely on this property when chaining flows or verifying Lie derivatives. The term-mode proof reduces the equality to componentwise ring arithmetic after extensionality.
claimFor any point $x : Fin 4 → ℝ$, index $μ : Fin 4$, and scalars $s, t : ℝ$, the coordinate ray satisfies ray_μ(ray_μ(x, s), t) = ray_μ(x, s + t), where ray_μ(x, t) := x + t ⋅ e_μ and e_μ denotes the standard basis vector.
background
The module supplies basic calculus operators on Minkowski space using the standard basis vectors e_μ in four dimensions. The coordinate ray is the affine line obtained by adding a scalar multiple of e_μ to a point x, defined componentwise via basisVec as ray(x, μ, t)(ν) = x(ν) + t ⋅ basisVec(μ, ν). This lemma records the elementary semigroup property of these translations along a fixed axis. It rests directly on the ray definition and on the algebraic structure of ℝ^4.
proof idea
One-line term proof: apply funext to reduce to pointwise equality on components, simplify by unfolding the ray definition, then normalize the resulting linear expressions with ring.
why it matters in Recognition Science
The result supplies the additive flow property required by directional derivative operators such as partialDeriv_v2 and secondDeriv in the same module. It closes a basic algebraic step in the coordinate calculus that supports later constructions of derivatives along rays. Within the Recognition framework it aligns with the eight-tick octave and D = 3 spatial structure by ensuring consistent translation behavior in the underlying four-dimensional representation.
scope and limits
- Does not treat non-coordinate directions or general vector fields.
- Does not incorporate metric structure or curvature.
- Does not address continuity, differentiability, or convergence questions.
- Does not extend beyond flat Minkowski space.
formal statement (Lean)
29@[simp] lemma coordRay_coordRay (x : Fin 4 → ℝ) (μ : Fin 4) (s t : ℝ) :
30 coordRay (coordRay x μ s) μ t = coordRay x μ (s + t) := by
proof body
Term-mode proof.
31 funext ν; simp [coordRay]; ring
32
33/-- Directional derivative `∂_μ f(x)` via real derivative along the coordinate ray. -/