module module

`IndisputableMonolith.Mathematics.RamanujanBridge.PhiLadderStability`

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 (23)

lemma add_inv_mono_on_one L68
lemma Jcost_mono_on_one L89
lemma phi_pow_ge_one L96
lemma phi_pow_mono L111
def phiLadderPosition L125
theorem phiLadderPosition_pos L128
theorem adjacent_phi_ratio L132
theorem adjacent_collapses L143
theorem adjacent_Jcost_eq L160
theorem adjacent_Jcost_positive L167
theorem identity_Jcost_zero L178
def gapCost L184
theorem gap0_cost_zero L187
theorem gap1_cost_positive L191
theorem gap2_cost_eq L197
theorem gapCost_nonneg L200
theorem gapCost_mono L205
def PhiLadderAdmissible L216
theorem adjacent_absorptive L221
theorem rogers_ramanujan_stability L236
theorem ground_state_is_identity L255
theorem first_excited_cost L259
theorem coherence_cost_aperiodicity L267