pith. machine review for the scientific record. sign in
def definition def or abbrev high

c_RS

show as:
view Lean formalization →

RS-native units set the gravitational propagation speed c_RS to exactly 1, matching the electromagnetic speed because both signals traverse the same ledger substrate at one cell per tick. Cosmologists and gravity modelers cite this normalization when computing prefactors such as the eta_B correction or black-hole entropy coefficients. The declaration is a direct constant assignment with no lemmas or reduction steps.

claimIn RS-native units the gravitational signal speed satisfies $c_{RS} = 1$.

background

The module addresses G-007 on whether gravity propagates at exactly the speed of light. Recognition Science places both electromagnetic and gravitational signals on the same simplicial ledger, so they inherit the identical tick rate and therefore the same limiting speed; the definition normalizes this common speed to 1, meaning one ledger cell per tick.

proof idea

The declaration is a direct definition that assigns the real number 1 to c_RS. No lemmas are applied and no tactics are used.

why it matters in Recognition Science

This definition anchors the structural equality of gravitational and electromagnetic speeds and is referenced by twenty-eight downstream declarations, chiefly the eta_B prefactor derivations in cosmology. It implements the module claim that identical tick rates force identical speed limits, consistent with the eight-tick octave of the forcing chain. The choice closes the unit system for propagation questions in the Recognition Science framework.

scope and limits

formal statement (Lean)

  27def c_RS : ℝ := 1

proof body

Definition body.

  28
  29/-- Gravitational "signal" speed in RS-native units.
  30    Same as c: both use the ledger as substrate. -/

used by (28)

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

depends on (3)

Lean names referenced from this declaration's body.