pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants

show as:
view Lean formalization →

The Constants module supplies the RS-native time quantum τ₀ equal to one tick and the golden ratio φ as the self-similar fixed point. Acoustics and aesthetics researchers cite these definitions to normalize J-cost on dimensionless ratios. It is a definition module with no proofs, importing the Cost framework to support scaling in forty downstream modules.

claim$τ_0 = 1$ tick and $φ = (1 + √5)/2$ with $φ > 1$, $φ^2 = φ + 1$, and $φ$ irrational.

background

Recognition Science starts from the J-cost functional equation in the Cost module. The Constants module fixes the base units: the tick as the indivisible time quantum τ₀ = 1 and the golden ratio φ as the self-similar fixed point forced by T6. These enable the eight-tick octave (T7) and the φ-ladder for scaling recognition costs.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds forty downstream results including MusicPitchJNDFromJCost (pitch JND from J-cost), RoomAcousticsFromPhiLadder (φ-ladder regimes with RT60 ratios = φ), RoomAcousticsSabineFromJCost (Sabine formula via J-cost on absorption ratio), and BerlyneInvertedU (aesthetic pleasure = 1 - J(r)/J(φ)_max). It anchors the T0-T8 chain by defining τ₀ and φ for the alpha band and mass ladder.

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)