phiLatticePoint_one
plain-language theorem explainer
The result shows that the phi-lattice point at rung index 1 equals the natural logarithm of the golden ratio. Researchers modeling the discrete hierarchy of complexity levels in Recognition Science cite this base case for the log-scale lattice. The proof is a direct unfolding of the definition followed by simplification.
Claim. The phi-lattice point at rung index 1 satisfies the position equality with the natural logarithm of the golden ratio, where the golden ratio is defined as (1 + sqrt(5))/2 and the phi-lattice point at rung r is the position r times the natural logarithm of the golden ratio.
background
The module formalizes the phi-ladder as the geometric sequence of powers of the golden ratio on the positive reals, which becomes the additive lattice of integer multiples of log phi under the logarithm map. The phi-lattice point at rung r is the position r log phi. This construction follows from the self-similar fixed point forced by T6 in the unified forcing chain, with the lattice admitting Poisson summation on the log scale. Upstream results include the reciprocal automorphism from CostAlgebra, which encodes the inversion symmetry x to 1/x that corresponds to rung negation on the lattice, and the ledger factorization structure that calibrates the J-cost function.
proof idea
The proof is a term-mode one-line wrapper. It unfolds the definition of the phi-lattice point function and applies the simp tactic to reduce the equality to the identity.
why it matters
This base case anchors the phi-lattice properties in the module, including closure under negation and the cost invariance under reciprocal symmetry. It fills the discrete hierarchy step from T6 and supports the eight-tick octave in T7. The module leaves sub-conjecture A.2 on phi-Poisson summation as a hypothesis structure representing analytic content outside mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.