module module moderate

`IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi`

The ContinuedFractionPhi module develops the continued fraction expansion of the golden ratio phi together with its Fibonacci approximations and fixed-point property. Researchers formalizing the RS-Ramanujan connection cite it to link classical number theory to the phi-ladder. The module supplies supporting definitions and a monotonicity lemma on x + x^{-1} that underpins later cost comparisons.

claimOn $[1,∞)$, the map $x ↦ x + x^{-1}$ is monotone increasing. The golden ratio satisfies the continued-fraction equation $ϕ = 1 + 1/ϕ$ and is the fixed point of the iteration $cfracIteration$, with Fibonacci ratios $fibRatio(n)$ converging to it.

background

Recognition Science obtains phi as the self-similar fixed point (T6) of the forcing chain. The module imports tau_0 = 1 tick from Constants and the J-cost machinery from Cost. It introduces cfracIteration, fib, fibRatio and the auxiliary result that x + x^{-1} is monotone on [1,∞), which directly supports Jcost_mono_on_one and the Recognition Composition Law.

proof idea

This is a definition module, no proofs. Supporting lemmas such as add_inv_mono_on_one and phi_is_cfrac_fixed_point are established by direct verification or recursion on the Fibonacci sequence.

why it matters in Recognition Science

The module supplies the continued-fraction and Fibonacci infrastructure required by the parent RamanujanBridge module, whose doc-comment states it provides the formal bridge between Ramanujan's mathematical structures and Recognition Science. It thereby connects the phi fixed point and eight-tick octave to Ramanujan's classical identities.

scope and limits

Does not prove convergence rates of the continued fraction beyond Fibonacci ratios.
Does not derive physical constants or the alpha band from these number-theoretic objects.
Does not treat continued fractions of other quadratic irrationals.

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