module module

`IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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