reach_time_eq
reach_time_eq shows that under the StepBounds hypothesis the time coordinate increases exactly by tau0 per step along any finite ReachN chain. Derivations of light-cone inequalities in the Recognition framework cite it to convert discrete kinematics into a linear time bound. The proof is a direct induction on the ReachN inductive definition that applies the step_time field at each successor and reassociates the arithmetic.
claimLet $K$ be a kinematics structure on a type $α$, let $U$ be an RS-units record, and let $time, rad : α → ℝ$. If $H$ witnesses that $time$ and $rad$ satisfy the StepBounds conditions for $K$ and $U$, then for every $n ∈ ℕ$ and points $x, y ∈ α$, whenever $y$ is reachable from $x$ in exactly $n$ steps under the ReachN relation generated by $K$, one has $time(y) = time(x) + n · τ₀$ where $τ₀$ is the fundamental tick duration supplied by $U$.
background
StepBounds is the structure that packages two properties: every kinematics step increases the time coordinate by exactly τ₀ and the radial coordinate by at most ℓ₀. ReachN is the inductive predicate whose constructors are the zero-step identity and the successor that appends one step; it therefore encodes finite causal chains of arbitrary length. The lemma lives inside the LightCone module, whose purpose is to extract metric bounds on the light cone from the discrete step relation together with the RS constants (including τ₀ defined as the native tick duration).
proof idea
The proof is by induction on the ReachN hypothesis. The zero case collapses by simplification. In the successor case the inductive hypothesis supplies the time up to the predecessor point, the step_time field of StepBounds adds one further τ₀, and a short calc block reassociates the sum to obtain the formula for n+1, using only commutativity and associativity of addition together with the definition of Nat.cast.
why it matters in Recognition Science
The lemma supplies the exact time increment required by the downstream cone_bound lemma, which converts the discrete reachability relation into the inequality Δrad ≤ c Δtime. It therefore forms the bridge between the inductive definition of causal reachability and the continuous light-cone structure used throughout the Recognition Science derivation. Both cone_bound and cone_bound_saturates depend on it directly; the latter further shows that equality is attained precisely when every step saturates the radial bound.
scope and limits
- Does not establish the corresponding radial increment bound.
- Does not depend on concrete values of the bridge ratio K or the golden ratio phi.
- Does not apply to reachability relations other than those generated by the kinematics step predicate.
- Does not address continuous or differential versions of the reachability relation.
Lean usage
have ht := H.reach_time_eq hformal statement (Lean)
30lemma reach_time_eq
31 (H : StepBounds K U time rad) :
32 ∀ {n x y}, Local.ReachN K n x y → time y = time x + (n : ℝ) * U.tau0 := by
proof body
Tactic-mode proof.
33 intro n x y h
34 induction h with
35 | zero => simp
36 | @succ n x y z hxy hyz ih =>
37 have ht := H.step_time hyz
38 calc
39 time z = time y + U.tau0 := ht
40 _ = (time x + (n : ℝ) * U.tau0) + U.tau0 := by simpa [ih]
41 _ = time x + ((n : ℝ) * U.tau0 + U.tau0) := by simp [add_comm, add_left_comm, add_assoc]
42 _ = time x + (((n : ℝ) + 1) * U.tau0) := by
43 have : (n : ℝ) * U.tau0 + U.tau0 = ((n : ℝ) + 1) * U.tau0 := by
44 calc
45 (n : ℝ) * U.tau0 + U.tau0
46 = (n : ℝ) * U.tau0 + 1 * U.tau0 := by simpa [one_mul]
47 _ = ((n : ℝ) + 1) * U.tau0 := by simpa [add_mul, one_mul]
48 simp [this]
49 _ = time x + ((Nat.succ n : ℝ) * U.tau0) := by
50 simpa [Nat.cast_add, Nat.cast_one]
51