pith. sign in
module module high

IndisputableMonolith.Constants.KDisplayCore

show as:
view Lean formalization →

This module defines the clock-side display time τ_rec(display) as (2π τ₀)/(8 ln φ) using the fundamental RS time quantum τ₀. Researchers modeling recognition processes in native units cite it to link periodic displays to the eight-tick octave. It is a definition module consisting solely of the stated formula with no proofs.

claim$τ_{rec}(display) = (2π · τ_0) / (8 ln φ)$ where τ_0 denotes the fundamental RS time quantum of one tick.

background

The upstream Constants module sets τ_0 as the fundamental RS time quantum equal to one tick. KDisplayCore introduces the display-specific form of the recognition time τ_rec, expressed for clock-side presentations. The formula incorporates the factor 8 in the denominator to reflect the period-2^3 octave structure and the logarithm of φ drawn from the self-similar fixed point.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the display definition that feeds the dimensionless bridge ratio K and display equalities in KDisplay. It also supports the RS-native unit system in RSNativeUnits, which treats ledger primitives as base standards so that all physics can be expressed without reference to SI.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)