cone_bound_export
plain-language theorem explainer
Verification of the light cone bound in discrete causality shows that radial separation is bounded by light travel time for any reachability chain when per-step constraints are met. Researchers in discrete spacetime models would cite it to confirm the bound holds independently of step count. The proof reduces directly to the core step-bound result from the light cone structure via simplification.
Claim. Assuming step bounds $H$ hold for kinematics $K$, units $U$, time and radial functions, if $x$ reaches $y$ via the $n$-step reachability relation under $K$, then $rad(y) - rad(x) ≤ U.c · (time(y) - time(x))$.
background
The module contains the verification-level cone bound theorem that exports the discrete light-cone bound without the step count parameter. The local theoretical setting is the export of this bound for causality verification as described in the module documentation.
proof idea
The proof is a one-line wrapper that applies the cone_bound from LightCone.StepBounds to the hypotheses H and h, discharging the goal with the simpa tactic.
why it matters
This theorem earns its place by providing the n-independent form of the cone bound, supporting causality and light-cone arguments in Recognition Science. It fills the verification-level export step in the module and connects to forcing chain landmarks including the eight-tick octave and three spatial dimensions. The module notes that a full cone entropy bound remains an axiom requiring voxel counting and holographic principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.