module module high

`IndisputableMonolith.NumberTheory.PhiLadderLattice`

Module defines the golden ratio φ as the unique positive root of x² = x + 1 and constructs the associated phi-ladder lattice points. It is imported by the Recognition Theta module to supply the phi-ladder weight. Content consists of elementary definitions and positivity lemmas derived from the quadratic equation.

claimLet $\phi = \frac{1 + \sqrt{5}}{2}$ be the unique positive solution of $x^2 = x + 1$ (equivalently $x = 1 + 1/x$). The module introduces the lattice points generated on the phi-ladder from this fixed point.

background

The module sits in NumberTheory and imports the Cost module. It defines the golden ratio φ from its quadratic equation and records standard algebraic properties including positivity, φ > 1, and the inversion relation φ^{-1} = φ - 1. The phi-ladder lattice points are generated by successive multiplication by φ, providing the discrete rungs used for weight assignments.

The supplied doc-comment states that φ is the unique positive solution of x² = x + 1. These objects supply the self-similar fixed point required for the Recognition Composition Law and the T6 step of the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the Recognition Theta construction, which builds the candidate completion of the cost theta function that incorporates the 8-tick character (T7) and the phi-ladder weight (T6) to inherit a modular identity under t ↦ 1/t. It supplies the T6 phi fixed point required for the ladder structure in the Recognition framework.

scope and limits

Does not derive any steps of the forcing chain T0-T8.
Does not compute values for physical constants such as alpha or G.
Does not state or apply the Recognition Composition Law.
Does not contain mass formulas or Berry threshold results.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.RecognitionTheta module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (25)

def phi L54
theorem phi_pos L57
theorem phi_ne_zero L64
theorem phi_gt_one L67
theorem phi_ne_one L78
theorem phi_sq_eq L81
theorem phi_mul_inv L91
theorem phi_inv_eq_phi_minus_one L100
theorem log_phi_pos L113
theorem log_phi_ne_zero L116
theorem log_phi_inv L119
def phiLatticePoint L126
theorem phiLatticePoint_zero L128
theorem phiLatticePoint_one L131
theorem phiLatticePoint_neg L136
theorem phiLatticePoint_succ L143
def phiLatticeReciprocal L153
theorem phiLatticeReciprocal_involutive L155
theorem phiLatticePoint_reciprocal L160
def costAtPhiPow L168
theorem cost_at_phi_pow_eq_neg L171
theorem cost_phi_ladder_reciprocal L181
structure that L192
structure PhiLadderPoissonSummation L205
theorem phi_ladder_certificate L229