module module moderate

`IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi`

The ContinuedFractionPhi module develops the continued fraction expansion of the golden ratio phi together with Fibonacci ratio recursions and associated monotonicity results for the map x + x^{-1}. Researchers formalizing the Ramanujan Bridge between classical number theory and Recognition Science would cite these lemmas. The module proceeds by defining iteration and ratio functions then applying monotonicity of the inversion map on [1,∞) to reach the fixed-point equation.

claimOn $[1,\infty)$ the map $x\mapsto x+x^{-1}$ is monotone; the golden ratio satisfies $\phi=[1;\overline{1}]$ as the fixed point of continued-fraction iteration, with Fibonacci ratios $F_{n+1}/F_n$ converging to $\phi$ and J-cost monotonicity holding on the same interval.

background

Recognition Science works in RS-native units with time quantum $\tau_0=1$ tick supplied by the Constants module. The Cost module supplies the J-cost function $J(x)=(x+x^{-1})/2-1$ that quantifies multiplicative deviation from unity and obeys the Recognition Composition Law. The present module introduces the continued-fraction iterator cfracIteration and the auxiliary objects fib, fibRatio, fibRatio_recursion, and cfracLevelCost to connect these structures to the self-similar fixed point phi.

proof idea

The module first records the elementary monotonicity lemma add_inv_mono_on_one for the map $x+x^{-1}$ on $[1,\infty)$, lifts it to Jcost_mono_on_one, then defines the iteration and ratio functions. It concludes with the direct algebraic verification phi_continued_fraction_eq and the fixed-point statement phi_is_cfrac_fixed_point.

why it matters in Recognition Science

This module supplies the continued-fraction and Fibonacci machinery required by the parent RamanujanBridge module, whose doc-comment states it provides the formal bridge between Ramanujan's deepest mathematical structures and Recognition Science. It thereby populates the self-similar fixed-point step (T6) of the forcing chain with concrete number-theoretic content.

scope and limits

Does not treat continued fractions of other quadratic irrationals.
Does not derive the fine-structure constant or mass ladder from these identities.
Does not quantify approximation error beyond the fixed-point relation.
Does not address multidimensional 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