StepBounds
StepBounds packages the per-step time and radius increments for a discrete kinematics relation into a single predicate. Researchers establishing light-cone inequalities from reachability chains cite it when lifting local increments to global bounds. The structure is introduced by direct field definitions that encode the two universal quantifiers over steps.
claimLet $K$ be a kinematics structure on type $α$ equipped with a step relation, let $U$ be the RS units with fundamental tick duration $τ_0$ and voxel length $ℓ_0$, and let $t,r:α→ℝ$. The predicate StepBounds$(K,U,t,r)$ holds if and only if every step $y→z$ in $K$ satisfies $t(z)=t(y)+τ_0$ and $r(z)≤r(y)+ℓ_0$.
background
The LightCone.StepBounds module builds discrete causal bounds inside the Recognition Science framework. It imports the Kinematics structure from Causality.Basic (and its siblings in ConeBound and Reach), which consists solely of a binary step predicate on states of type $α$. Constants tau0 and ell0 supply the fundamental tick duration $τ_0$ and length unit $ℓ_0=1$ in RS-native units.
proof idea
This is a structure definition whose two fields directly encode the universal properties over steps. No lemmas or tactics are invoked; the declaration serves as a hypothesis interface for the induction arguments in sibling lemmas reach_time_eq and reach_rad_le.
why it matters in Recognition Science
StepBounds supplies the local increment assumptions that downstream lemmas cone_bound and cone_bound_export convert into the global light-cone inequality $r(y)-r(x)≤c(t(y)-t(x))$. It appears in the verification-level export cone_bound_export. In the framework it supports the causal structure underlying the eight-tick octave and spatial dimension $D=3$ by ensuring discrete steps respect the light-cone bound.
scope and limits
- Does not define the underlying kinematics relation or step predicate.
- Does not introduce the speed of light $c$ or other RS constants.
- Does not apply to continuous-time or non-discrete transitions.
- Does not prove saturation or equality cases for the bounds.
- Does not specify the concrete type $α$ or particular kinematics instance.
formal statement (Lean)
18structure StepBounds (K : Local.Kinematics α)
19 (U : IndisputableMonolith.Constants.RSUnits)
20 (time rad : α → ℝ) : Prop where
21 step_time : ∀ {y z}, K.step y z → time z = time y + U.tau0
22 step_rad : ∀ {y z}, K.step y z → rad z ≤ rad y + U.ell0
23
24namespace StepBounds
25
26variable {K : Local.Kinematics α}
27variable {U : IndisputableMonolith.Constants.RSUnits}
28variable {time rad : α → ℝ}
29