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

tau19

show as:
view Lean formalization →

The declaration defines τ₁₉ as τ₀ multiplied by φ raised to the 19th power, locating the rung at -19 on the phi-ladder for biological timescales near 68 ps. Researchers deriving time hierarchies from Planck units to macroscopic scales would cite this rung. The definition is a direct scaling assignment using the imported base tick and self-similar factor.

claimDefine τ₁₉ := τ₀ ⋅ φ¹⁹, where τ₀ denotes the fundamental tick duration and φ is the golden-ratio fixed point of the Recognition Science scaling.

background

Recognition Science organizes time scales on a phi-ladder in which each rung multiplies the prior duration by φ. The base unit τ₀ is the fundamental tick duration, defined in Constants as the duration of one tick and derived in Derivation from Planck constants in RS-native units. The module on Planck Scale from φ relates these to l_P = c × τ₀ × φ^(-n) for suitable n, with upstream scale defined as φ^k.

proof idea

This is a direct definition that sets tau19 equal to tau0 multiplied by phi to the power 19. It applies the imported constants for tau0 and the phi scaling without invoking further lemmas or tactics.

why it matters in Recognition Science

The definition supplies rung -19 on the phi-ladder, extending the hierarchy from Planck time to biological timescales as stated in the module documentation. It supports the claim that the full ladder spans from t_P to cosmological times and aligns with the self-similar fixed point φ in the forcing chain. No downstream theorems are listed.

scope and limits

formal statement (Lean)

 129noncomputable def tau19 : ℝ := tau0 * phi^19

proof body

Definition body.

 130
 131/-! ## Quantum Gravity Predictions -/
 132
 133/-- RS predictions for quantum gravity:
 134
 135    1. **Minimum length = l_voxel**, not l_P
 136       - Below l_voxel, spacetime is discrete
 137       - l_P may be inaccessible
 138
 139    2. **φ-quantized energies** near Planck scale
 140       - Energies at φ^n × E_P
 141
 142    3. **No singularities**
 143       - Voxel structure prevents infinite densities
 144
 145    4. **Modified dispersion relations**
 146       - At high energy, E² = p²c² + m²c⁴ + corrections -/

depends on (11)

Lean names referenced from this declaration's body.