pith. sign in
module module high

IndisputableMonolith.Cost.FrequencyLadder

show as:
view Lean formalization →

FrequencyLadder module defines the J-cost of a frequency ratio r = f₂/f₁ using the core cost function. Researchers building harmonic or self-similar analyses in Recognition Science cite these objects when constructing ladders or fixed-point arguments. The module supplies definitions together with unit and nonnegativity properties.

claimFor frequency ratio $r = f_2/f_1$, the cost is given by frequencyRatioCost$(r) := J(r)$ where $J$ satisfies the Recognition Composition Law; the module also records that this cost is nonnegative and equals zero precisely at $r=1$.

background

Constants supplies the RS time quantum $ au_0 = 1$ tick. JcostCore defines the underlying J-cost function obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. FrequencyLadder specializes this cost to ratios of frequencies, introducing frequencyRatioCost together with the predicate IsSelfSimilarRatio and the fixed-point statement phi_cost_fixed_point.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The objects defined here supply the cost layer required by the self-similar ratio theorems (phi_is_self_similar, phi_unique_self_similar, phi_cost_fixed_point) that realize T6 in the forcing chain and prepare the eight-tick octave of T7.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)