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

IndisputableMonolith.RecogSpec.Scales

show as:
view Lean formalization →

The RecogSpec.Scales module supplies definitions for the binary scale factor B(k) = 2^k as a real and the companion PhiPow(k) = phi^k. Modelers of discrete growth or octave hierarchies in Recognition Science cite these for monotonicity facts. The module consists of inductive definitions plus elementary lemmas on zero, successor, and addition cases.

claimDefines the binary scale $B : ℤ → ℝ$ by $B(k) = 2^k$ together with the phi-power map $Φ : ℤ → ℝ$ by $Φ(k) = φ^k$.

background

Recognition Science builds scales on the phi-ladder inside the eight-tick octave. The module introduces B as the real-valued binary scale factor B = 2^k and PhiPow as the corresponding power of the golden ratio. It imports the RS time quantum τ₀ = 1 tick from Constants and supplies the supporting facts B_of_zero, B_of_succ, PhiPow_add.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The scale definitions feed directly into URCAdapters.TcGrowth, which exports a Prop that holds because PhiPow is strictly increasing for φ > 1. This supplies the discrete scale infrastructure required for growth computations under the Recognition Composition Law.

scope and limits

used by (1)

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 (42)