pith. sign in
module module high

IndisputableMonolith.Constants

show as:
view Lean formalization →

The Constants module supplies the RS-native time quantum τ₀ = 1 tick together with the golden ratio φ and the eight-tick octave. Acoustics and aesthetics derivations cite these constants to anchor J-cost calculations on physical ratios. It is a pure definition module containing no theorems or proofs.

claimThe module declares the fundamental time quantum $\tau_0 = 1$ tick, the golden ratio $\phi = (1 + \sqrt{5})/2$ with $\phi > 1.5$ and $\phi^2 = \phi + 1$, and the octave period of eight ticks.

background

The module imports Mathlib and the Cost module, which supplies the J-cost function used throughout Recognition Science. It introduces the tick as the indivisible RS time quantum and phi as the unique positive fixed point of the self-similar map J(x) = (x + 1/x)/2 - 1. Additional definitions establish positivity, irrationality, and ordering properties of phi together with the octave structure of period 2^3.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Constants are imported by MusicPitchJNDFromJCost, RoomAcousticsFromPhiLadder, RoomAcousticsSabineFromJCost, SpeechIntelligibilityFromJCost, BerlyneInvertedU, and CulturalAestheticFromJCost. These downstream modules apply the tick and phi to derive pitch JND, reverberation regimes on the phi-ladder, and aesthetic inverted-U curves from J-cost reciprocity. The definitions close the T6 phi fixed-point and T7 eight-tick octave steps of the forcing chain.

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)