module module moderate

`IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi`

This module formalizes the continued fraction expansion of the golden ratio phi via Fibonacci ratios and proves monotonicity of x + x^{-1} on [1, infinity). Researchers connecting Ramanujan's classical results to Recognition Science's phi-ladder would cite these lemmas when building the self-similar fixed point. The module proceeds through recursive definitions of the Fibonacci sequence and direct algebraic verification of the fixed-point equation.

claimOn the interval $[1,\infty)$, the map $x \mapsto x + x^{-1}$ is monotone increasing. The golden ratio $\phi$ satisfies $\phi = [1;\overline{1}]$ and is the fixed point of the continued fraction iteration whose convergents are the Fibonacci ratios.

background

Recognition Science obtains phi as the self-similar fixed point (T6) from the forcing chain. The module imports the fundamental time quantum $\tau_0 = 1$ tick from Constants and the cost machinery from the Cost module. It introduces the Fibonacci sequence, its positivity and explicit values, the ratio recursion, and the continued fraction iteration map whose fixed point is phi.

The local theoretical setting is the Ramanujan Bridge, whose module documentation states that it provides the formal bridge between Srinivasa Ramanujan's deepest mathematical structures and Recognition Science.

proof idea

This module mixes definitions (fib, fibRatio, cfracIteration) with supporting lemmas. The core arguments use recursion on the Fibonacci sequence to establish fibRatio_recursion, direct substitution to obtain phi_is_cfrac_fixed_point, and algebraic comparison to prove add_inv_mono_on_one together with phi_continued_fraction_eq.

why it matters in Recognition Science

The module supplies the continued fraction foundation for phi that is imported by the RamanujanBridge module. That parent module uses these results to decipher Ramanujan's mathematical discoveries within the Recognition Science framework, particularly the self-similar properties tied to the phi-ladder and the eight-tick octave.

scope and limits

Does not treat continued fractions for quadratic irrationals other than phi.
Does not supply Diophantine approximation error bounds.
Does not connect the continued fraction directly to the Recognition Composition Law.
Does not address physical interpretations such as spatial dimension D=3.

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