The Speed of Light

1. Setting

Recognition Science begins with discrete primitives: a tick, written $\tau_0$, is one posting interval of the ledger; a voxel, written $\ell_0$, is the distance a unit of information traverses in one tick along a single causal step. These are not analogies, they are the chosen base units of the RS-native measurement system. Once those units exist, the propagation speed of light is fixed by construction:

$$c ;=; \frac{\ell_0}{\tau_0} ;=; 1\ \text{voxel/tick}.$$

In Lean, the unit pack U : RSUnits carries U.tau0 = 1, U.ell0 = 1, and U.c = 1. The lemma U_c : U.c = 1 is a one-liner reflexivity proof, because the speed of light in this gauge is not an empirical input, it is the unit ratio itself.

2. Why this is not circular

A reader meeting RS for the first time might object that defining the voxel as "one tick of light propagation" makes $c = 1$ tautological. The honest answer is yes, in the RS-native gauge it is tautological, and that is the point. The empirical content of "the speed of light" lives not in the dimensionless number 1 but in the calibration between the RS-native frame and any external frame such as SI. The non-trivial empirical claim is that the same calibration constants serve every process that runs on the ledger, electromagnetism, gravity, recognition flow, identity ticks, without any process-specific corrections.

The Lean structure ExternalCalibration captures exactly this. It packs the three positive scalars

$$\mathtt{seconds_per_tick},\quad \mathtt{meters_per_voxel},\quad \mathtt{joules_per_coh},$$

together with the consistency law

$$\frac{\mathtt{meters_per_voxel}}{\mathtt{seconds_per_tick}} ;=; 299{,}792{,}458.$$

The field speed_consistent of ExternalCalibration is precisely this equation. The theorem

theorem c_in_si (cal : ExternalCalibration) :
    to_m_per_s cal c = 299792458

then follows by unfolding to_m_per_s and applying cal.speed_consistent, six lines of Lean, no fitting parameter, no numerical input beyond the SI definition itself.

3. Same substrate forces gravity = light

Gravity in RS rides the same ledger that carries electromagnetism. There is no "gravitational medium" with a separate tick rate. The Lean module Gravity.PropagationSpeed makes this explicit:

def c_RS      : ℝ := 1
def c_grav_RS : ℝ := 1
theorem c_grav_eq_c_RS : c_grav_RS = c_RS := rfl

The proof is rfl, reflexivity, because both speeds are defined as 1 voxel/tick in the same gauge. The empirical content is the prediction that any measurement of $c_{\text{grav}} / c_{\text{EM}}$ at any frequency, in any local inertial frame, returns exactly 1. The 2017 binary-neutron-star merger GW170817 confirmed this to one part in $10^{15}$; RS predicts the structural equality at any precision the experiment can reach.

4. Light-cone causality

The corollary is that information propagation in RS is bounded by a light cone with $c$ at its boundary. The Lean module Physics.LightConeCausalityFromRS enumerates five canonical causal relations between events: timelike, spacelike, lightlike, past-boundary, and future-boundary. The certificate lightConeCausalityCert records the decidable count Fintype.card CausalRelation = 5. This finite count is itself a consequence of the 8-tick cycle and of the spatial dimension $D = 3$. Both upstream facts are proved in the same module: the theorem eight_tick_is_2_cubed checks $2^3 = 8$ by rfl, and the theorem eight_tick_forces_D3 shows that any dimension $D$ with $2^D = 8$ must equal $3$. The cone structure is what one gets once those are forced.

5. What the SI number reduces to

Recognition Science does not predict the SI integer 299,792,458 as a separate physical claim; that integer is the 2019 SI definition of the metre in terms of the second. Once the second is fixed by the Cs-133 hyperfine transition, the metre is defined so that c takes that exact integer value in m/s. RS's prediction is that this conversion is self-consistent at every frequency, in every inertial frame, and across every process that runs on the ledger, including gravity. If a future experiment measured any process propagating faster than c, or measured $c_{\text{grav}} \neq c_{\text{EM}}$, the single-substrate claim of RS would be refuted.

6. Where the derivation stops

The derivation stops at the RS-native gauge where c is defined to be 1. Below that level, the existence of a fundamental tick and a fundamental voxel rests on the discreteness theorem in Foundation.DiscretenessForcing. The dimension count $D = 3$ and the 8-tick cycle are upstream consequences of the same forcing argument that produces the cost function $J$ and the golden ratio $\varphi$ (see Foundation.PhiForcingDerived.phi_forcing_complete). The whole chain is checked in Lean. The SI integer 299,792,458 lives one level below, inside the ExternalCalibration structure, and is an empirical seam by design.