pq_one_minimal_cost
plain-language theorem explainer
The partial quotient 1 minimizes J-cost among positive integer choices in continued fraction levels. Researchers tracing φ as the ground state of sequential cost optimization cite this to anchor the Ramanujan bridge. The tactic proof establishes the ordering 1 + 1/φ ≤ k + 1/φ on the reals and invokes monotonicity of J on [1, ∞) via a direct application of the sibling lemma Jcost_mono_on_one.
Claim. For every positive integer $k$, the J-cost of the continued-fraction level with partial quotient 1 satisfies $J(1 + 1/φ) ≤ J(k + 1/φ)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module treats continued fractions as sequential J-cost geodesics. The functional $J(x) = ½(x + x^{-1}) - 1$ attains its global minimum at $x = 1$ and possesses the unique positive fixed point $φ = 1 + 1/φ$. The level cost cfracLevelCost n is defined to be $J(n + 1/φ)$. Upstream ledger factorization supplies the calibration of J on the positive reals, while the multiplicative recognizer encodes the underlying cost structure.
proof idea
The tactic proof introduces $k$ and the hypothesis $0 < k$. It casts the inequality $1 ≤ k$ into the reals, verifies $0 < 1/φ$, and obtains $1 + 1/φ ≤ k + 1/φ$ by linarith. The final step unfolds cfracLevelCost and applies the monotonicity lemma Jcost_mono_on_one via simpa.
why it matters
The result confirms that the integer partial quotient 1 realizes the global J-cost minimum on the positive integers, a prerequisite for identifying φ as the attractor of the infinite recursion. It supplies the base case for the Rogers-Ramanujan continued-fraction analysis in the same module and aligns with T5 uniqueness of J together with T6 forcing of φ. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.