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

planckLength_rs

show as:
view Lean formalization →

The definition sets the Planck length in RS-native units to the product of the speed of light and the Planck time. Researchers expressing gravitational and quantum scales inside the Recognition Science framework cite this when working exclusively in tick and voxel units. It is realized as a direct one-line multiplication that reuses the already-defined Planck time.

claimIn RS-native units the Planck length satisfies $ℓ_P = c · τ_P$, where $τ_P$ is the Planck time expressed in the same system and $c = 1$.

background

The RS-Native Measurement System module defines base units tick (τ₀, one discrete ledger posting interval) and voxel (ℓ₀, one causal spatial step). Derived quanta are coh = φ^{-5} (energy) and act = ħ (action). All measures sit on the φ-ladder with integer powers of φ supplying natural scalings; the module fixes c = 1 and treats SI conversion as optional. This declaration reuses the upstream planckTime_rs, whose doc-comment states τ_P = √(ħG/c⁵) and notes that the expression becomes a dimensionless φ-structure once G and c are taken in RS units.

proof idea

The definition is a one-line wrapper that multiplies the speed of light by the Planck time supplied by the sibling declaration planckTime_rs.

why it matters in Recognition Science

The declaration supplies the length member of the Planck triad inside the RS unit system, completing the set of scales needed to express the gravitational constant G and the forcing-chain results T5–T8 without external anchors. It supports the module’s claim that all physics can be written in ledger primitives alone and aligns with the fixed α^{-1} band and the eight-tick octave. No open scaffolding questions are closed by this definition.

scope and limits

formal statement (Lean)

 249noncomputable def planckLength_rs : Length :=

proof body

Definition body.

 250  c * planckTime_rs
 251
 252/-- Planck mass in RS units: m_P = √(ħc/G).
 253    This is the mass at which gravitational and quantum scales meet. -/

depends on (11)

Lean names referenced from this declaration's body.