pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.LightCone.StepBounds

show as:
view Lean formalization →

The LightCone.StepBounds module collects saturation lemmas showing that light-cone reach equalities hold exactly when every discrete step attains its individual bound. Researchers proving causal structure and propagation limits in Recognition Science cite these results to close the light-cone construction. The argument reduces directly to the imported time quantum τ₀ = 1 tick together with the reach_time_eq and reach_rad_le relations from sibling modules.

claimSaturation holds: reach_time(steps) equals the bound and reach_rad(steps) ≤ bound, with equality in the radial component if and only if each step saturates its per-step limit, where the bound is set by the number of steps times the RS time quantum τ₀ = 1.

background

The LightCone domain models discrete causal propagation at unit speed in RS-native units. It imports the fundamental time quantum τ₀ = 1 tick from IndisputableMonolith.Constants, which fixes the minimal duration of any step. Sibling modules Kinematics and ReachN supply the underlying reach_time and reach_rad functions; StepBounds isolates the saturation case in which those functions attain their upper limits.

proof idea

This module organizes saturation lemmas rather than a single long proof. The central result applies reach_time_eq to equate total elapsed time with the bound, then invokes reach_rad_le to cap the radial distance, with equality following once every step is shown to saturate its individual allowance.

why it matters in Recognition Science

StepBounds supplies the saturation case required to obtain sharp light-cone bounds. It feeds the cone_bound and cone_bound_saturates declarations that close the causal-structure layer of the Recognition framework, linking directly to the eight-tick octave and the D = 3 spatial dimensions enforced by the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)