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