Pith. sign in
module module high

IndisputableMonolith.Constants.RSUnitsHelpers

show as:
view Lean formalization →

RSUnitsHelpers supplies auxiliary lemmas relating the speed of light c, fundamental time quantum τ₀, and length scale ℓ₀ in RS-native units. Researchers deriving or checking constant consistency in the Recognition Science framework would cite it when extending the base Constants module. The module consists of direct algebraic identities with no complex derivations.

claim$c au_0 = \ell_0$ and related unit-conversion identities in RS-native units.

background

The upstream Constants module defines the fundamental RS time quantum (RS-native) as τ₀ = 1 tick. RSUnitsHelpers operates inside the Constants domain where c = 1, supplying helper relations among time, length, and derived scales without introducing new physical content.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supports unit relations inside the Constants section of the Recognition Science framework and feeds downstream constant derivations that rely on τ₀ as the base tick.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)