reach_time_eq
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.