reach_rad_le
plain-language theorem explainer
The lemma establishes that under a StepBounds hypothesis the radial coordinate grows by at most ell0 per step along any finite causal chain: rad(y) ≤ rad(x) + n ⋅ ℓ₀ whenever y is reachable from x in exactly n steps. Light-cone derivations in Recognition Science cite it when controlling spatial propagation from discrete kinematics. The proof is by induction on the ReachN inductive predicate, applying the step_rad axiom at each successor and reassociating the arithmetic bound.
Claim. Let $H$ satisfy the StepBounds axioms for kinematics $K$, units $U$, time map and radial map. Then for every natural number $n$ and points $x,y$, if $y$ is reachable from $x$ in exactly $n$ steps under the ReachN relation for $K$, one has $rad(y) ≤ rad(x) + n · ℓ₀$, where $ℓ₀$ is the fundamental length unit supplied by $U$.
background
StepBounds is the structure requiring that each kinematic step advances time by exactly τ₀ and radius by at most ℓ₀. ReachN is the inductive definition of n-step reachability: the zero constructor connects a point to itself, while succ appends one step via the kinematics relation. The module imports Constants for ℓ₀ (set to 1 in RS-native units) and Causality.Basic/Reach for the ReachN inductive. Upstream results include the CostAlgebra definition of the shifted cost H(x) = J(x) + 1, though this lemma uses only the kinematic bounds.
proof idea
Proof by induction on the ReachN hypothesis h. The zero case is discharged by simp. In the succ case, the step_rad field of H yields rad(z) ≤ rad(y) + ℓ₀; the inductive hypothesis bounds rad(y) by rad(x) + n · ℓ₀; the two inequalities are added and the sum is reassociated to (n+1) · ℓ₀ via add_le_add_left, add_assoc and Nat.cast lemmas.
why it matters
The lemma is invoked inside cone_bound to pair with the corresponding time bound and obtain the light-cone inequality rad(y) - rad(x) ≤ c (time(y) - time(x)). It supplies the radial half of the causal bound derivation in LightCone.StepBounds, supporting the T7 eight-tick octave and D = 3 spatial dimensions in the T0-T8 forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.