module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi`

ContinuedFractionPhi develops the continued fraction theory for the golden ratio phi inside Recognition Science. It proves monotonicity of the map x to x plus x inverse on the interval from one to infinity, defines Fibonacci sequences and their ratios, and shows phi as the fixed point of the continued fraction iteration. Researchers working on the Ramanujan Bridge would cite these lemmas to anchor self-similar structures from the forcing chain in classical analysis. The module proceeds via recursive definitions, algebraic verification of the J-

claimThe map $xmapsto x+x^{-1}$ is strictly increasing on $[1,infty)$. The golden ratio $phi$ satisfies $phi=1+1/phi$, equivalently the infinite continued fraction $[1;overline{1}]$.

background

Recognition Science places phi as the self-similar fixed point forced at step T6 of the UnifiedForcingChain. The J-cost function is built from the expression (x + x inverse)/2 minus one, drawn from the imported Cost module. Constants supplies the base time quantum tau zero equal to one tick. This module introduces the continued fraction expansion of phi together with the Fibonacci sequence (via fib and fibRatio) and the iteration map cfracIteration. The supplied doc-comment records the monotonicity of the add-inv map on [1, infinity), which directly supports J-cost monotonicity lemmas in the same file.

proof idea

The module interleaves definitions and short supporting lemmas. Monotonicity of the add-inv map is shown by algebraic comparison or derivative sign. Fibonacci numbers and their ratios are introduced recursively, with fibRatio_recursion proved by direct induction. The central statements phi_continued_fraction_eq and phi_is_cfrac_fixed_point follow by substituting the fixed-point equation and invoking uniqueness from the monotonicity result. All steps are direct computation or recursion; no external lemmas beyond the imported Cost and Constants properties are required.

why it matters in Recognition Science

These results supply the continued-fraction machinery imported by the parent RamanujanBridge module, whose doc-comment describes the formal bridge between Ramanujan's structures and Recognition Science. The lemmas close the link to T6 (phi forced as self-similar fixed point) and prepare the phi-ladder used for mass formulas and the alpha inverse band. The module therefore sits at the interface between classical number theory and the RS-native constants c=1, hbar=phi to the minus five.

scope and limits

Does not derive error bounds or convergence rates for the approximants.
Does not extend the analysis to other quadratic irrationals.
Does not connect directly to mass formulas or Berry thresholds.
Does not treat higher-dimensional or matrix continued fractions.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Mathematics.RamanujanBridge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

lemma add_inv_mono_on_one L73
lemma Jcost_mono_on_one L94
theorem phi_continued_fraction_eq L103
def cfracIteration L112
theorem phi_is_cfrac_fixed_point L115
def fib L122
theorem fib_values L128
theorem fib_pos L133
def fibRatio L146
theorem fibRatio_recursion L150
theorem phi_worst_approximable_core L192
def cfracLevelCost L206
theorem pq_one_minimal_cost L214
structure RogersRamanujanSpecialValue L240
def rr_special_values L247
theorem sequential_optimization_forces_phi L254
theorem sequential_optimization_forces_phi_strong L271
theorem cfrac_ground_state_is_phi L305