cone_bound_saturates
The lemma establishes saturation of the light-cone bound: under exact per-step increments of time by tau0 and radius by ell0, any n-step reachability chain yields equality between radial separation and c times temporal separation. Researchers deriving causal bounds from Recognition Science kinematics would cite this result. The proof obtains the inequality from the prior cone lemma, computes exact differences by congruence and induction on reachability, then substitutes the identity ell0 equals c tau0.
claimLet K be a kinematics structure on a set, with time and radius maps to the reals, and let U be the RS units. Assume the step-increment bounds hold and that every step of K increases time by exactly tau0 and radius by exactly ell0. Then for any natural number n and points x, y reachable from x to y in exactly n steps under K, the difference rad(y) minus rad(x) equals c times (time(y) minus time(x)).
background
StepBounds is the predicate requiring that each kinematics step advances time by exactly tau0 while advancing radius by at most ell0. ReachN is the inductive relation capturing n-step reachability: the base case is the zero-step identity, and the successor case appends one step relation. The module works inside local kinematics equipped with RS units, where the constants satisfy the light-cone identity ell0 equals c tau0.
proof idea
The proof first applies the cone_bound lemma to obtain the inequality version. It derives the exact time difference time(y) minus time(x) equals n tau0 by congruence from the reach_time_eq fact. For the radius difference it inducts on the ReachN hypothesis, using the exact step equality at each successor and the inductive hypothesis. The final calculation substitutes the identity ell0 equals c tau0 to obtain equality.
why it matters in Recognition Science
This saturation lemma completes the light-cone analysis by showing the bound is attained precisely when steps saturate the radius increment. It refines the cone_bound result and supports derivations of causal structure from the Recognition Science forcing chain, particularly the emergence of light-cone geometry. No downstream uses are recorded yet, but the result closes a key equality case in the StepBounds development.
scope and limits
- Does not prove the inequality direction of the light-cone bound.
- Does not apply when radius increments are strictly less than ell0.
- Does not extend to non-discrete or continuous-time kinematics.
- Does not derive the numerical value of c or other constants.
formal statement (Lean)
94lemma cone_bound_saturates
95 (H : StepBounds K U time rad)
96 (ht : ∀ {y z}, K.step y z → time z = time y + U.tau0)
97 (hr : ∀ {y z}, K.step y z → rad z = rad y + U.ell0)
98 {n x y} (h : Local.ReachN K n x y) :
99 rad y - rad x = U.c * (time y - time x) := by
proof body
Tactic-mode proof.
100 have hineq := cone_bound (K:=K) (U:=U) (time:=time) (rad:=rad) H h
101 have ht' : time y - time x = (n : ℝ) * U.tau0 := by
102 have := H.reach_time_eq (K:=K) (U:=U) (time:=time) (rad:=rad) h
103 have := congrArg (fun t => t - time x) this
104 simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this
105 have hr' : rad y - rad x = (n : ℝ) * U.ell0 := by
106 induction h with
107 | zero => simp
108 | @succ n x y z hxy hyz ih =>
109 have hineq_y : rad y - rad x ≤ U.c * (time y - time x) := H.cone_bound hxy
110 have ht_y : time y - time x = (n : ℝ) * U.tau0 := by
111 have := H.reach_time_eq hxy
112 have := congrArg (fun t => t - time x) this
113 simp [sub_eq_add_neg, add_comm, add_left_comm] at this
114 exact this
115 have ih_applied := ih hineq_y ht_y
116 have hz := hr hyz
117 calc
118 rad z - rad x = (rad y + U.ell0) - rad x := by rw [hz]
119 _ = (rad y - rad x) + U.ell0 := by ring
120 _ = (n : ℝ) * U.ell0 + U.ell0 := by rw [ih_applied]
121 _ = ((n : ℝ) + 1) * U.ell0 := by ring
122 _ = ((Nat.succ n : ℝ)) * U.ell0 := by simp [Nat.cast_add, Nat.cast_one]
123 have hcτ : U.ell0 = U.c * U.tau0 := by simpa using (U.c_ell0_tau0).symm
124 calc
125 rad y - rad x = (n : ℝ) * U.ell0 := hr'
126 _ = (n : ℝ) * (U.c * U.tau0) := by rw [hcτ]
127 _ = U.c * ((n : ℝ) * U.tau0) := by ring
128 _ = U.c * (time y - time x) := by rw [ht']
129
130end StepBounds
131end LightCone
132end IndisputableMonolith