Vectors in the same ray: partitions, sums, finite orbits, and durations of segments

Mathlib's SameRay.trans chains two ray relations SameRay R x y and SameRay R y z into SameRay R x z, provided the middle vector y vanishes only when x or z does. TauCeti.sameRay_of_partition iterates this step along a finite ordered partition of an interval in a linear order: if a map w into an ordered scalar module lies, on each piece of the partition, on the ray of its value at the end of that piece, and w vanishes at a point of the interval only if it vanishes at every earlier point, then every value of w lies on the ray of the final value. The explicit-partition induction follows the pattern of the Apache-2.0 frenzymath/Poincare-Conjecture formalization, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, as used in TauCeti/Geometry/Manifold/Riemannian/EDistComparison.lean.

Negating a ray twice gives it back (Module.Ray.neg_neg), in a form that rw and simp find on orientations. Scaling a ray by a unit commutes with negating it (Module.Ray.units_smul_neg), complementing Mathlib's Module.Ray.neg_units_smul, and with transporting it along a linear equivalence (Module.Ray.map_units_smul). Over a linearly ordered ring, any map of rays commuting with negation also commutes with scaling by units (Module.Ray.units_smul_of_map_neg).

Two nonzero vectors in the same ray cannot cancel: their sum is again nonzero. This is the non-degeneracy needed to merge adjacent segments of a piecewise-linear path that point in the same direction. A vector lies in the same ray as such a sum exactly when it lies in the same ray as the summands, since SameRay is transitive through a nonzero vector.

Two distinct points of a finite orbit of a linear group action never lie in the same ray. This is what makes the velocity of each segment of a path with velocities in a Weyl orbit recoverable from the segment alone: if no two distinct points of a set S ∌ 0 lie in the same ray, a segment v traversed in a positive time d at a velocity d⁻¹ • v ∈ S determines d (Set.Pairwise.eq_of_snd_eq_of_inv_smul_mem), and a list of such segments determines its list of durations (Set.Pairwise.eq_of_map_snd_eq_of_inv_smul_mem). Two pairs (d, v) and (e, w) of positive durations lie in the same ray exactly when they have the same velocity (Prod.sameRay_iff_inv_fst_smul_snd_eq).

theorem SameRay.trans_of_ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] {x y z : M} (hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y ≠ 0) : SameRay R x z

SameRay is transitive through a nonzero vector.

@[simp]

theorem Module.Ray.map_units_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) (u : Rˣ) (v : Ray R M) : (map f) (u • v) = u • (map f) v

Transporting a ray along a linear equivalence commutes with scaling it by a unit.

theorem TauCeti.sameRay_of_partition {R : Type u_1} {α : Type u_2} {M : Type u_3} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [LinearOrder α] [AddCommMonoid M] [Module R M] {w : α → M} {k : ℕ} (τ : Fin (k + 2) → α) (hτ : ∀ (i : Fin (k + 1)), τ i.castSucc ≤ τ i.succ) (hpiece : ∀ (i : Fin (k + 1)), ∀ t ∈ Set.Icc (τ i.castSucc) (τ i.succ), SameRay R (w t) (w (τ i.succ))) (hzero : ∀ ⦃s : α⦄, s ∈ Set.Icc (τ 0) (τ (Fin.last (k + 1))) → ∀ ⦃u : α⦄, u ∈ Set.Icc (τ 0) (τ (Fin.last (k + 1))) → s ≤ u → w u = 0 → w s = 0) {t : α} (ht : t ∈ Set.Icc (τ 0) (τ (Fin.last (k + 1)))) : SameRay R (w t) (w (τ (Fin.last (k + 1))))

Rays chain through a partition. If a map w into an ordered scalar module lies, on each piece of an ordered partition, on the ray of its value at the end of that piece, and w vanishes at a point of the interval only if it vanishes at every earlier point of the interval, then every value lies on the ray of the final value.

theorem Module.Ray.neg_neg {R : Type u_1} {M : Type u_2} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (v : Ray R M) : - -v = v

Negating a ray twice produces the original ray. This is Mathlib's neg_neg stated with the instance Neg (Module.Ray R M), so that rw and simp also find it on orientations, where the generic lemma does not match.

theorem Module.Ray.units_smul_neg {R : Type u_1} {M : Type u_2} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (u : Rˣ) (v : Ray R M) : u • -v = -(u • v)

Scaling a ray by a unit commutes with negating it.

theorem Module.Ray.units_smul_of_map_neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {F : Ray R M → Ray R N} (hF : ∀ (v : Ray R M), F (-v) = -F v) (u : Rˣ) (v : Ray R M) : F (u • v) = u • F v

A map of rays commuting with negation commutes with scaling by units, since a unit acts on rays as the identity or as negation according to its sign.

theorem SameRay.add_ne_zero {R : Type u_1} {M : Type u_2} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {x y : M} (h : SameRay R x y) (hx : x ≠ 0) : x + y ≠ 0

The sum of two vectors in the same ray, the first of them nonzero, is nonzero.

theorem SameRay.sameRay_add_left_iff {R : Type u_1} {M : Type u_2} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {x y z : M} (h : SameRay R x y) (hy : y ≠ 0) : SameRay R (x + y) z ↔ SameRay R y z

If x and y lie in the same ray and y is nonzero, then a vector lies in the same ray as x + y exactly when it lies in the same ray as y.

theorem SameRay.eq_of_mem_orbit {R : Type u_3} {M : Type u_4} {G : Type u_5} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [Group G] [MulAction G M] [SMulCommClass G R M] {x y z : M} (h : SameRay R y z) (hy : y ∈ MulAction.orbit G x) (hz : z ∈ MulAction.orbit G x) (hfin : (MulAction.orbit G x).Finite) : y = z

Two points of a finite orbit of a group acting by maps commuting with scalar multiplication are equal as soon as they lie in the same ray. If g moved a nonzero point y of the orbit to r • y with 0 < r, the powers of g would move y to the points r ^ n • y of the orbit, which are pairwise distinct unless r = 1.

theorem Set.Pairwise.eq_of_snd_eq_of_inv_smul_mem {R : Type u_3} {M : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] {S : Set M} (hS : S.Pairwise fun (u v : M) => ¬SameRay R u v) (h0 : 0 ∉ S) {x y : R × M} (hx : 0 < x.1 ∧ x.1⁻¹ • x.2 ∈ S) (hy : 0 < y.1 ∧ y.1⁻¹ • y.2 ∈ S) (h : x.2 = y.2) : x = y

If no two distinct points of a set S ∌ 0 lie in the same ray, a pair (d, v) with 0 < d and d⁻¹ • v ∈ S is determined by v: a segment traversed at a velocity in S determines its duration.

theorem Set.Pairwise.eq_of_map_snd_eq_of_inv_smul_mem {R : Type u_3} {M : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] {S : Set M} (hS : S.Pairwise fun (u v : M) => ¬SameRay R u v) (h0 : 0 ∉ S) {p q : List (R × M)} (hp : ∀ x ∈ p, 0 < x.1 ∧ x.1⁻¹ • x.2 ∈ S) (hq : ∀ x ∈ q, 0 < x.1 ∧ x.1⁻¹ • x.2 ∈ S) (h : List.map Prod.snd p = List.map Prod.snd q) : p = q

If no two distinct points of a set S ∌ 0 lie in the same ray, a list of pairs (d, v) with 0 < d and d⁻¹ • v ∈ S is determined by its second components: segments traversed at velocities in S determine their durations.

theorem Prod.inv_fst_smul_snd_smul {R : Type u_3} {M : Type u_4} [Field R] [AddCommGroup M] [Module R M] {a : R} (ha : a ≠ 0) (z : R × M) : (a • z).1⁻¹ • (a • z).2 = z.1⁻¹ • z.2

Rescaling a pair (d, v) by a nonzero factor does not change the velocity d⁻¹ • v.

theorem Prod.sameRay_iff_inv_fst_smul_snd_eq {R : Type u_3} {M : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] {y z : R × M} (hy : 0 < y.1) (hz : 0 < z.1) : SameRay R y z ↔ y.1⁻¹ • y.2 = z.1⁻¹ • z.2

Two pairs (d, v) and (e, w) with 0 < d and 0 < e lie in the same ray exactly when they have the same velocity, d⁻¹ • v = e⁻¹ • w.