module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.PhiLadderStability`

PhiLadderStability supplies monotonicity and positivity lemmas for the phi ladder within the Ramanujan bridge. The central result establishes that the map sending x to x plus its inverse is increasing on the closed interval from 1 to infinity, with parallel statements for J-cost and phi powers. Researchers formalizing links between Ramanujan's identities and Recognition Science cite these to secure ladder stability before mass or defect calculations. The module assembles direct algebraic proofs from the imported Cost and Constants modules.

claimOn the interval $[1,∞)$, the map $x ↦ x + x^{-1}$ is monotone increasing. Parallel statements assert monotonicity of the associated J-cost on the same domain, positivity of adjacent differences, and well-defined positioning on the phi-ladder.

background

Recognition Science builds the phi ladder from the golden-ratio fixed point phi and the J-cost function J(x) = (x + x^{-1})/2 - 1. Positions on the ladder are indexed by integer rungs with gaps determined by atomic number Z, feeding the mass formula yardstick times phi to the power (rung - 8 + gap(Z)). The module imports Constants, which fixes the base time quantum tau_0 to one tick, and Cost, which supplies the defect and J-cost primitives used in adjacent collapses and gapCost calculations.

proof idea

The module collects a sequence of lemmas. add_inv_mono_on_one proves the stated monotonicity by comparing differences for x greater than or equal to 1. Jcost_mono_on_one and phi_pow_mono lift the same comparison to the J-cost and to positive powers of phi. phiLadderPosition and its positivity companion define the rung index and show it is positive; adjacent_phi_ratio, adjacent_collapses, and adjacent_Jcost_eq then equate neighboring values via algebraic cancellation. All steps are direct order arguments drawn from Mathlib.

why it matters in Recognition Science

The module feeds the parent RamanujanBridge, whose documentation presents it as the formal bridge between Ramanujan's deepest structures and Recognition Science. It supplies the monotonicity and positivity scaffolding required for the phi-ladder stability that underpins downstream mass formulas and the eight-tick octave. Without these lemmas the ladder would lack the order properties needed for consistent rung placement and defect accounting.

scope and limits

Does not prove monotonicity outside the real interval [1, ∞).
Does not connect the ladder directly to the fine-structure constant band.
Does not discharge the full set of Ramanujan identities.
Does not treat non-phi self-similar fixed points.

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