Pith. sign in
module module high

IndisputableMonolith.Quantum.PlanckScale

show as:
view Lean formalization →

This module defines Planck-scale quantities in Recognition Science, expressing them via the fundamental tick τ₀ and golden ratio φ. Quantum gravity researchers would cite it to link discrete RS units to standard Planck length, mass, and time. The module consists entirely of definitions and algebraic relations drawn from its two imports.

claimPlanck length $\ell_P = \sqrt{\hbar G / c^3}$, Planck mass $m_P = \sqrt{\hbar c / G}$, Planck time $t_P$, energy, and temperature, together with the ratios $\tau_0 / t_P$ and voxel length, all expressed in RS-native units where $c=1$, $\hbar=\phi^{-5}$, $G=\phi^5/\pi$.

background

The module resides in the Quantum domain. It imports Constants, which fixes the RS time quantum as $\tau_0 = 1$ tick, and PhiForcing, whose doc-comment states: "This module proves that φ is forced by self-similarity in a discrete ledger with J-cost." The supplied module doc-comment recalls the classical Planck length formula. Sibling declarations implement the concrete mappings from these constants onto the Planck hierarchy and the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the Planck-scale interface that subsequent quantum constructions require. It connects the phi-forcing result (T5–T6) and the RS constants directly to observable length and mass scales, preparing the ground for the eight-tick octave and D=3 spatial structure. No downstream uses are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)