Pith. sign in
module module high

IndisputableMonolith.Constants

show as:
view Lean formalization →

The Constants module supplies the RS-native definitions of the fundamental time quantum τ₀ = 1 tick, the golden ratio φ, and the eight-tick octave. Researchers deriving acoustics or aesthetics results from J-cost import it to fix units and the self-similar scale factor. It consists entirely of definitions with no theorems.

claimThe module declares the RS time quantum $\tau_0 = 1$ tick, the golden ratio $\phi = (1 + \sqrt{5})/2$ satisfying the fixed-point equation of the Recognition Composition Law, and the octave period of eight ticks.

background

This module forms the base layer of the Recognition Science library and imports only the Cost module that supplies the J-cost function J(x). It introduces the time quantum τ₀ = 1 tick as the RS-native unit together with the golden ratio φ as the self-similar fixed point. The theoretical setting is the forcing chain T0–T8 in which T6 forces φ and T7 fixes the eight-tick octave period.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The constants anchor all downstream applications of J-cost. They feed MusicPitchJNDFromJCost (JND for pitch), RoomAcousticsFromPhiLadder (RT60 scaling by φ), RoomAcousticsSabineFromJCost (reverberation regimes), SpeechIntelligibilityFromJCost (intelligibility threshold at J(φ)), BerlyneInvertedU (inverted-U from reciprocal symmetry), and CulturalAestheticFromJCost (familiarity ratio).

scope and limits

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (67)