module module high

`IndisputableMonolith.NumberTheory.PhiLadderLattice`

The NumberTheory.PhiLadderLattice module introduces the golden ratio as the self-similar fixed point and defines associated lattice points for weighting in the Recognition Science framework. Researchers deriving mass formulas on the phi-ladder or completing the cost theta function would cite these definitions. The module consists of algebraic identities and positivity lemmas obtained by direct verification from the quadratic equation.

claimLet $φ = (1 + √5)/2$. Then $φ$ is the unique positive real satisfying $φ² = φ + 1$, and the phi-ladder lattice points are the discrete points generated by integer powers of $φ$ on the cost lattice.

background

The module defines the golden ratio $φ$ as the unique positive solution to $x² = x + 1$. It imports the Cost module, which supplies the J-cost function and Recognition Composition Law used to weight these lattice points. The phi-ladder lattice points furnish the discrete self-similar structure required by the T6 step of the unified forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions feed the RecognitionTheta module, which constructs the Recognition Theta function incorporating the phi-ladder weight (T6) and eight-tick character (T7) so as to inherit a modular identity under $t ↦ 1/t$. The downstream module states: 'The Recognition Theta function Θ̃_RS(t) is the candidate completion of the cost theta function Θ_J(t) = Σ e^{-t c(n)} that incorporates the 8-tick character (T7) and the phi-ladder weight (T6)'.

scope and limits

Does not derive the full forcing chain from T0 to T8.
Does not compute numerical values for constants such as α^{-1}.
Does not establish modular identities for the theta function.
Does not address the Berry creation threshold or Z_cf.

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