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

IndisputableMonolith.Cost.FixedPoint

show as:
view Lean formalization →

Cost.FixedPoint establishes that the golden ratio φ is the positive solution to the fixed-point equation x = 1 + 1/x. Researchers deriving the phi-ladder mass formulas or the eight-tick octave cite this lemma to anchor the self-similar scale. The module imports Constants and consists of one sibling declaration whose proof reduces directly to the quadratic x² - x - 1 = 0.

claimThe golden ratio satisfies the equation $x = 1 + x^{-1}$.

background

Recognition Science builds the J-cost function J(x) = (x + x^{-1})/2 - 1 from the Recognition Composition Law. The module imports the base time quantum τ₀ = 1 tick from Constants. It isolates the fixed-point condition that forces φ as the self-similar scale factor in the T0-T8 chain.

proof idea

The module declares the single lemma phi_is_cost_fixed_point. Its proof is a direct algebraic verification that the positive root of x² - x - 1 = 0 satisfies the fixed-point equation using field arithmetic on the reals.

why it matters in Recognition Science

The lemma supplies the T6 fixed-point step in the UnifiedForcingChain. It supports downstream derivations of ħ = φ^{-5}, G = φ^5 / π, and the mass formula on the phi-ladder. The result closes the self-similarity requirement before the eight-tick octave and D = 3 are forced.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)