J_phi
plain-language theorem explainer
The result gives the explicit value of the recognition cost function J at the golden ratio: J(φ) equals φ minus 3/2. Researchers deriving coherence costs or self-similar scales in discrete ledger models cite this identity when closing the forcing argument from J-cost to the golden ratio. The proof is a one-line algebraic reduction that unfolds the definition of J, substitutes the inverse identity for φ, and simplifies by ring arithmetic.
Claim. $J(φ) = φ - 3/2$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost and $φ = (1 + √5)/2$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module establishes that self-similarity in a discrete ledger equipped with J-cost forces the scale ratio to be the golden ratio. The cost function is taken from the Law of Existence and satisfies the Recognition Composition Law. Upstream results supply the key algebraic identity $φ^{-1} = φ - 1$, proved in both the PhiRing and Inequalities modules by direct expansion of the defining equation $φ^2 = φ + 1$. The local setting is a ledger whose cost is invariant under self-similar rescaling, so that only the fixed point of the J-equation yields a non-trivial solution.
proof idea
The term proof unfolds the definition of J from LawOfExistence, rewrites the inverse term via the phi_inv identity, and closes with ring normalization. No additional lemmas or case splits are required.
why it matters
The identity supplies the concrete cost at the self-similar fixed point and is invoked directly by SpectralEmergence to define the fundamental coherence cost and to prove its positivity. It also discharges the cost-equality step in StillnessGenerative. Within the framework it realizes the T5–T6 segment of the forcing chain: J-uniqueness selects the unique non-trivial scale ratio φ whose cost is equivalent to the unit scale. The result closes one link in the derivation of D = 3 and the eight-tick octave from self-similarity alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.