reach_time_eq
plain-language theorem explainer
The lemma establishes that StepBounds implies exact time advance of n times the base tick duration along any n-step causal path in ReachN. It would be cited when deriving discrete light-cone inequalities from step-wise kinematics in Recognition Science. The proof proceeds by induction on ReachN, applying the step_time axiom at each successor and rearranging the accumulated multiples of tau0 via associativity and commutativity.
Claim. Assume StepBounds$(K, U, \text{time}, \text{rad})$ holds, so that each kinematics step advances time by exactly $U.\tau_0$. Then for the inductive reachability ReachN$(K, n, x, y)$ (base case $x=y$ at $n=0$, successor by one additional step), one has $\text{time}(y) = \text{time}(x) + n \cdot U.\tau_0$.
background
The StepBounds structure requires that every single step in the kinematics relation $K$ increases the time coordinate by precisely the fundamental tick duration $\tau_0$ (from Constants.tau0) while increasing radius by at most $\ell_0$. ReachN is the inductive predicate whose constructors are the zero-step identity and the successor that appends one $K$-step; it therefore counts exact discrete causal distance. The module LightCone.StepBounds works inside the discrete causal layer that precedes continuous light-cone statements, importing the RS units $U$ whose $\tau_0$ is the base time unit.
Upstream, the same ReachN inductive appears in Causality.Basic and Causality.Reach; the CostAlgebra.H definition is unrelated here. The constant $K = \varphi^{1/2}$ enters only as a parameter of the kinematics and is not used in this timing lemma.
proof idea
Induction on the ReachN hypothesis. The zero constructor is discharged by simp. For the successor constructor, step_time from the StepBounds hypothesis supplies time $z =$ time $y + U.\tau_0$; the induction hypothesis rewrites time $y$, after which three applications of add_assoc/add_comm together with the algebraic identity $n\cdot\tau_0 + \tau_0 = (n+1)\cdot\tau_0$ (proved by distributivity) finish the step. The final Nat.succ cast is handled by simpa.
why it matters
The result is invoked directly by the downstream cone_bound lemma (which combines it with the radial bound to obtain the light-cone inequality) and by cone_bound_saturates (which recovers equality under saturation). It therefore supplies the exact timing ingredient for the discrete causality bounds that sit beneath the Recognition Science light-cone construction, consistent with the fundamental tick duration $\tau_0$ and the eight-tick octave. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.