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

K_rs

show as:
view Lean formalization →

K_rs defines the K-gate ratio as π/(4 ln φ) inside the RS-native unit system. Researchers modeling coherence quanta or φ-ladder scalings in Recognition Science reference this constant for all dimensionless ratios. The definition is a direct one-line alias to the K_gate_ratio computation imported from KDisplayCore.

claim$K_{rs} := K = {π}/(4 ln φ)$

background

The RS-native units module sets up a measurement system with tick τ₀ as the discrete ledger time quantum and voxel ℓ₀ as the causal spatial step satisfying c = 1. Derived quantities are the coherence energy E_coh = φ^{-5} and action ħ = E_coh · τ₀, with all ratios fixed by φ on the φ-ladder for masses, energies, times, and lengths. This definition draws on the RSUnits structure (tau0, ell0, c with c · tau0 = ell0) and the K_gate_ratio computation π/(4 log φ) from KDisplayCore, plus the abstract Constants bundle containing Knet and related terms.

proof idea

The definition is a one-line alias that directly references the K_gate_ratio evaluation Real.pi / (4 * Real.log phi) from the imported KDisplayCore module. No lemmas or reductions are applied beyond the import and alias.

why it matters in Recognition Science

K_rs supplies the fixed K-gate ratio for RS-native constants, supporting coherence scaling E_coh = φ^{-5} and the φ-ladder organization in the Recognition framework. It aligns with the eight-tick octave and D = 3 spatial dimensions by providing a φ-derived dimensionless parameter without external anchors. No downstream uses appear in the graph, leaving its role as a foundational constant definition.

scope and limits

formal statement (Lean)

 269noncomputable def K_rs : ℝ := Constants.RSUnits.K_gate_ratio

proof body

Definition body.

 270
 271/-- Coherence scaling: E_coh = φ⁻⁵. -/

depends on (4)

Lean names referenced from this declaration's body.