first_excited_cost
plain-language theorem explainer
The result shows that Jcost attains its maximum on (1, phi] at the upper endpoint phi. Researchers modeling the first excited state on the phi-ladder cite this bound to establish the minimal positive cost of any non-trivial excitation. The proof is a one-line wrapper that invokes the monotonicity lemma Jcost_mono_on_one after weakening the strict lower bound via le_of_lt.
Claim. For all real numbers $x$ with $1 < x ≤ ϕ$, the J-cost satisfies $J(x) ≤ J(ϕ)$, where $J$ is the cost function $J(y) = (y + y^{-1})/2 - 1$.
background
The φ-ladder places admissible ratios at powers φ^n. The J-cost of a ratio x > 0 is the derived cost J(x) = (x + x^{-1})/2 - 1, vanishing only at the identity x = 1. Module documentation states that adjacent rungs at ratio φ produce positive J-cost and therefore collapse under the golden recurrence, forcing the “differ by ≥ 2” rule of the Rogers-Ramanujan identities. Upstream, ObserverForcing.cost records that every recognition event carries exactly this J-cost, while MultiplicativeRecognizerL4.cost supplies the underlying comparator.
proof idea
The proof is a one-line wrapper. It converts the hypothesis 1 < x into 1 ≤ x by le_of_lt, then feeds the resulting pair of bounds directly into the sibling monotonicity statement Jcost_mono_on_one.
why it matters
The declaration supplies the lower bound on excitation cost required by the φ-ladder stability argument. It thereby anchors the claim that the first excited state sits at ratio φ with cost J(φ) = φ − 3/2 > 0, the minimal positive value on the ladder. This step supports the module’s link between Zeckendorf representations and the Rogers-Ramanujan “differ by ≥ 2” constraint, and it sits inside the chain that forces D = 3 and the eight-tick octave from the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.