pith. sign in
module module high

IndisputableMonolith.Quantum.PlanckScale

show as:
view Lean formalization →

The Quantum.PlanckScale module supplies definitions for Planck units expressed via RS-native constants. Physicists modeling discrete spacetime or quantum gravity would cite these to link the phi-forced ledger to standard scales. The module consists entirely of definitions and algebraic relations with no proofs, importing directly from Constants and PhiForcing.

claim$l_P = √(ℏG/c³) ≈ 1.616 × 10^{-35} m$, together with the companion Planck mass, time, energy, and temperature expressed in the same RS units.

background

The module resides in the Quantum domain and imports Constants (setting the fundamental RS time quantum τ₀ = 1 tick) and PhiForcing (establishing that φ is forced by self-similarity in a discrete ledger with J-cost). The supplied doc-comment states the classical Planck length formula. Sibling declarations include planckLength, planckMass, tau0_tP_ratio, voxelLength, lengthHierarchy, and phiLadderRung, which relate these quantities to the phi-ladder and the eight-tick octave.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Planck-scale bridge that connects RS constants (τ₀, φ, ħ = φ^{-5}, G = φ^5/π) to conventional quantum-gravity scales. It feeds the lengthHierarchy and phiLadderRung siblings and supports the D = 3 spatial dimensions and eight-tick octave steps of the forcing chain (T7–T8). No downstream uses are listed in the current graph.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)