coordRay_zero
The coordinate ray starting at a point x in direction e_μ evaluates to x itself at parameter zero. Researchers deriving directional derivatives of radial functions along coordinate lines in four-dimensional spacetime cite this as the base evaluation. The proof is a one-line term-mode application of function extensionality followed by simplification from the ray definition.
claimFor any point $x : ℝ^4$ and index $μ ∈ {0,1,2,3}$, the affine line $x + t e_μ$ evaluated at $t=0$ equals $x$, where $e_μ$ is the standard basis vector with 1 in position $μ$.
background
The Derivatives module develops directional calculus along coordinate rays in Minkowski space. The coordinate ray is the affine line sending parameter $t$ to $x + t e_μ$, with $e_μ$ the standard basis vector. This lemma records the evaluation at $t=0$, which serves as the origin point in all subsequent differentiability statements for functions such as spatial radius and radial inverses.
proof idea
One-line term proof that applies function extensionality to reduce the function equality to pointwise equality on components, then simplifies directly from the definition of the coordinate ray, which adds zero times the basis vector.
why it matters in Recognition Science
This base evaluation anchors the differentiability chain for radialInv and spatialRadius along coordinate rays. It is invoked in differentiableAt_coordRay_radialInv, partialDeriv_v2_radialInv, and the six related lemmas that close the remaining calculus axioms for Recognition Science derivative machinery in four spacetime dimensions.
scope and limits
- Does not address behavior for nonzero parameter values.
- Does not treat differentiability or analytic properties.
- Applies only to standard coordinate rays, not arbitrary directions.
- Does not reference Recognition Science constants, J-cost, or the phi-ladder.
formal statement (Lean)
26@[simp] lemma coordRay_zero (x : Fin 4 → ℝ) (μ : Fin 4) : coordRay x μ 0 = x := by
proof body
Term-mode proof.
27 funext ν; simp [coordRay]
28
used by (12)
-
differentiableAt_coordRay_partialDeriv_v2_radialInv -
differentiableAt_coordRay_radialInv -
differentiableAt_coordRay_spatialRadius -
partialDeriv_v2_mul -
partialDeriv_v2_radialInv -
partialDeriv_v2_spatialRadius -
secondDeriv_radialInv -
spatialRadius_coordRay_ne_zero_eventually -
differentiableAt_coordRay_partialDeriv_v2_radialInv_proved -
partialDeriv_v2_radialInv_proved -
partialDeriv_v2_spatialRadius_proved -
secondDeriv_radialInv_proved