cone_bound
plain-language theorem explainer
cone_bound establishes that any n-step causal reach in a kinematics obeying per-step time and radius increments satisfies the light-cone inequality rad(y) - rad(x) ≤ c (time(y) - time(x)). Discrete causality researchers in Recognition Science cite it to enforce relativistic bounds from local rules alone. The proof extracts the exact time increment n τ₀ and the radius upper bound n ℓ₀ from the StepBounds assumptions, then substitutes the identity ℓ₀ = c τ₀.
Claim. Let $K$ be a kinematics, $U$ a set of RS units, and time, rad maps from states to reals. If StepBounds $K$ $U$ time rad holds and ReachN $K$ $n$ $x$ $y$ is true, then rad$(y)$ - rad$(x)$ ≤ $U.c$ ⋅ (time$(y)$ - time$(x)$).
background
StepBounds is the structure requiring that every local step of $K$ advances time by exactly $U.τ₀$ and radius by at most $U.ℓ₀$. ReachN is the inductive predicate for finite causal reachability: zero steps stay at the same point, and each successor applies one $K.step$ transition. The module LightCone.StepBounds develops discrete light-cone bounds inside the Recognition Science units system. It imports the identity $c ⋅ τ₀ = ℓ₀$ from Constants, which states that the fundamental length and time scales are related by the speed of light in RS-native units.
proof idea
The tactic proof first calls reach_time_eq on the ReachN hypothesis to obtain time(y) - time(x) = n τ₀. It then calls reach_rad_le to obtain rad(y) - rad(x) ≤ n ℓ₀. Explicit rewriting produces the time difference as a multiple of τ₀ and converts the radius inequality via sub_le_iff_le_add'. The final step substitutes the lemma c_ell0_tau0 (ℓ₀ = c τ₀) and simplifies the product.
why it matters
This lemma supplies the core inequality used by cone_bound_export to state the light-cone bound without an explicit step count n, and by cone_bound_saturates to characterize the equality case when every step saturates both bounds. It closes the discrete-to-continuous bridge in the causality chain of the Recognition Science framework, ensuring models respect the light cone with the supplied constants c, τ₀ and ℓ₀.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.