cone_bound_export
The theorem exports a light-cone inequality that holds for any causally reachable pair without explicit dependence on the number of steps. Researchers modeling discrete spacetime or causal sets would cite it to obtain n-independent bounds from per-step assumptions. The proof is a one-line wrapper that invokes the cone_bound lemma from the StepBounds structure.
claimAssume $H$ satisfies the step bounds for kinematics $K$, constants $U$, and functions time, rad. If $x$ reaches $y$ in $n$ steps under $K$, then $rad(y) - rad(x) ≤ U.c · (time(y) - time(x))$.
background
ReachN is the inductive definition of n-step reachability: zero steps stay at x, and each successor applies a kinematics step. LightCone.StepBounds encodes per-step constraints on time and radial increments. The module provides a verification-level export of the discrete light-cone bound, removing the step count n from the final statement. Upstream, H from CostAlgebra shifts the J-cost to satisfy d'Alembert form, while K is defined as phi to the power 1/2.
proof idea
The proof applies simpa to the term LightCone.StepBounds.cone_bound instantiated with the given H and reachability hypothesis h. This reduces the n-dependent reach to the desired bound directly.
why it matters in Recognition Science
This declaration removes the step parameter from the cone bound, enabling direct use in continuous limits or entropy calculations. It supports the cone entropy bound axiom by providing the geometric constraint. In the Recognition framework it aligns with the discrete causality structure leading to light-cone propagation at c=1.
scope and limits
- Does not establish the per-step bounds; those remain an assumption.
- Does not derive the entropy bound; that is stated separately as an axiom.
- Does not apply to non-causal pairs.
- Does not quantify over specific values of n.
formal statement (Lean)
33theorem cone_bound_export
34 (H : LightCone.StepBounds K U time rad)
35 {n x y} (h : Causality.ReachN K n x y) :
36 rad y - rad x ≤ U.c * (time y - time x) := by
proof body
Term-mode proof.
37 simpa using (LightCone.StepBounds.cone_bound (K:=K) (U:=U) (time:=time) (rad:=rad) H h)
38
39end
40
41/-- Cone entropy bound: Entropy in a cone is bounded by area over 4 λ_rec².
42
43 This is currently an axiom (typeclass assumption). A full proof would require:
44 - Voxel counting: number of voxels ~ area / λ_rec²
45 - Entropy per voxel: ~ ln φ from ledger structure
46 - Holographic principle: caps total at area/(4λ_rec²)
47
48 See docs/Assumptions.md for the status of this assumption.
49-/