pith. sign in
module module moderate

IndisputableMonolith.Constants.RSUnitsHelpers

show as:
view Lean formalization →

RSUnitsHelpers supplies auxiliary definitions and equalities for constants in Recognition Science native units, centered on the time quantum τ₀. Researchers deriving unit conversions or phi-ladder masses cite it when working with the base Constants module. The module consists of simple definitions and one-line wrappers with no complex proofs.

claimThe module provides relations such as $c · τ₀ = ℓ₀$ where τ₀ = 1 tick in RS-native units with c = 1.

background

The upstream module IndisputableMonolith.Constants states that the fundamental RS time quantum (RS-native) is τ₀ = 1 tick. RSUnitsHelpers extends this with helper lemmas for unit scaling. In the Recognition Science setting, constants are fixed as c = 1, ħ = φ^{-5}, G = φ^5 / π, supporting the mass formula yardstick · φ^(rung - 8 + gap(Z)) on the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supports constant definitions that feed the forcing chain T0 to T8, particularly T7 eight-tick octave and T8 D = 3. It supplies the auxiliary relations needed for downstream mass and alpha-band calculations in the parent Constants module.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)