StepBounds
plain-language theorem explainer
StepBounds encodes the local increment rules that time advances by exactly τ₀ and radius grows by at most ℓ₀ on every kinematic step. Cone-bound derivations in the LightCone and ConeExport modules cite it to obtain the global light-cone inequality. The structure is a direct packaging of two universal quantifiers over the step relation supplied by Kinematics.
Claim. Let $K$ be a kinematics structure on type $α$ equipped with a step relation, let $U$ be the RS units, and let $t,r:α→ℝ$. The predicate holds when every step $y→z$ in $K$ satisfies $t(z)=t(y)+τ₀$ and $r(z)≤r(y)+ℓ₀$.
background
Kinematics supplies the binary step relation on the underlying type $α$. The constants τ₀ and ℓ₀ are the fundamental tick duration and voxel length in RS-native units. This structure lives inside the LightCone module, which assembles per-step bounds into reachability statements that feed the cone inequality.
proof idea
The declaration is a structure definition that directly encodes the two per-step increment properties; no tactics or lemmas are applied.
why it matters
It supplies the hypothesis for the cone_bound and reach_time_eq lemmas, which in turn discharge cone_bound_export. The export theorem states that any n-step reach obeys rad(y)−rad(x)≤U.c·(time(y)−time(x)) with no n appearing in the final statement, closing a local-to-global step in the causality chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.