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

IndisputableMonolith.LightCone

show as:
view Lean formalization →

The LightCone module defines the discrete light-cone bound in the Recognition Science framework. Researchers formalizing causal structure in phi-discretized spacetime cite it to obtain the bound independent of explicit step counts. The module assembles definitions and lemmas that feed directly into the export theorem.

claimThe discrete light-cone bound states that spatial separation satisfies $|Δx| ≤ B(Δt)$ where $B$ is the phi-ladder radius at unit speed $c=1$ and $Δt$ is measured in eight-tick intervals.

background

Recognition Science derives spacetime from the forcing chain T0-T8, with J-uniqueness $J(x)=(x+x^{-1})/2-1$, phi the self-similar fixed point, and the eight-tick octave fixing $D=3$. The LightCone module introduces the light cone as the causal boundary using J-cost and defectDist on the phi-ladder. It prepares the discrete geometry before the bound is exported without step-count dependence.

proof idea

This is a definition module, no proofs. It structures the argument by defining the light cone via the phi-ladder, then supplying lemmas that remove the explicit step-count parameter for export.

why it matters in Recognition Science

The module supplies the core light-cone construction to the Cone Bound Export Theorem. That theorem exports the discrete light-cone bound without the step count parameter, completing the causal-structure step in the T0-T8 chain. It anchors the discrete spacetime used for the alpha band and mass ladder.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.