J_at_phi
plain-language theorem explainer
Verification shows that the cost function J applied to the golden ratio φ equals exactly (√5 − 2)/2. Researchers modeling self-similar quantization cite this to fix the base coherence cost on the φ-ladder. The value is identified as the minimum nonzero cost arising from self-similarity. The derivation unfolds the cost definition then reduces via field simplification and arithmetic on √5 positivity.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then $J(φ) = (√5 - 2)/2$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The J-cost is the function J(x) = (x + x^{-1})/2 − 1 drawn from the CostAlgebra module; it quantifies coherence cost for positive reals. The PhiRing module adjoins φ to the integers, with φ satisfying φ² = φ + 1 and serving as the self-similar fixed point. The doc-comment calls J(φ) the coherence cost of self-similarity and the minimum nonzero cost on the φ-ladder. Upstream results supply multiplicativity of J-automorphisms and positivity of √5 to license the algebraic steps.
proof idea
The term proof unfolds CostAlgebra.J and the definition of φ. It introduces a nonzeroness hypothesis for φ from phi_pos and the identity (√5)² = 5. Field simplification cancels the denominator, after which nlinarith closes the equality using sqrt5_pos and the square identity.
why it matters
The result supplies the explicit base value that feeds canonicalLayerSysPlus in RecognitionCategory and the H_StableIffPhiLadder hypothesis in PhiEmergence. It realizes the J-uniqueness step (T5) at the self-similar point φ (T6) inside the φ-ring certificate. The module summary lists this computation as the final verified link between cost algebra and the ring structure before octave and ledger layers are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.