cfracLevelCost
plain-language theorem explainer
This definition assigns to each natural number partial quotient the J-cost of the ratio formed by that quotient plus the reciprocal of the golden ratio. Researchers analyzing minimal-cost continued fraction expansions for phi would cite it when quantifying strain per level in the phi geodesic. The definition is a direct one-line application of the Jcost functional to the expression k + 1/phi.
Claim. For each natural number $n$, the level cost is $J(n + 1/phi)$ where $J(x) = (x + x^{-1})/2 - 1$ and $phi = (1 + sqrt(5))/2$.
background
The J-cost functional $J(x) = (x + x^{-1})/2 - 1$ measures recognition strain on positive ratios and attains its unique minimum at $x=1$, with strict increase for $x>1$ (T5 J-uniqueness). In the continued fraction setting, each partial quotient $n$ produces the local ratio $n + 1/phi$, and the module treats the infinite nesting for phi as sequential minimization of this cost subject to the self-similar fixed-point constraint $phi = 1 + 1/phi$ (T6). Upstream results establish that recognition-event cost equals Jcost of the state and that derived cost from a multiplicative recognizer is likewise Jcost on ratios.
proof idea
One-line wrapper that applies Jcost directly to the ratio (partialQuotient + 1/phi).
why it matters
The definition supplies the per-level cost used by the downstream theorem establishing that partial quotient 1 is minimal, thereby confirming phi as the ground-state attractor of the continued-fraction recursion. It fills the concrete cost assignment in the Ramanujan-bridge module that links classical continued-fraction identities to the RS forcing chain (T5-T6). The construction touches the open question of whether all optimal geodesics in the framework reduce to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.